Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Syntax.Notation

Contents

- Sections
- Pretty printing

Description

As a concrete name, a notation is a non-empty list of alternating `IdPart`s and holes. In contrast to concrete names, holes can be binders.

Example: `syntax fmap (λ x → e) xs = for x ∈ xs return e`

The declared notation for `fmap` is `for_∈_return_` where the first hole is a binder.

Synopsis

- data HoleName
  - = LambdaHole {
    - _bindHoleName :: RString
    - holeName :: RString
    }
  - | ExprHole {
    - holeName :: RString
    }
- isLambdaHole :: HoleName -> Bool
- stringParts :: Notation -> [String]
- holeTarget :: GenPart -> Maybe Int
- isAHole :: GenPart -> Bool
- isNormalHole :: GenPart -> Bool
- isBindingHole :: GenPart -> Bool
- data NotationKind
  - = InfixNotation
  - | PrefixNotation
  - | PostfixNotation
  - | NonfixNotation
  - | NoNotation
- notationKind :: Notation -> NotationKind
- mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation
- data NewNotation = NewNotation {
  - notaName :: QName
  - notaNames :: Set Name
  - notaFixity :: Fixity
  - notation :: Notation
  - notaIsOperator :: Bool
  }
- namesToNotation :: QName -> Name -> NewNotation
- useDefaultFixity :: NewNotation -> NewNotation
- notationNames :: NewNotation -> [QName]
- syntaxOf :: Name -> Notation
- mergeNotations :: [NewNotation] -> [NewNotation]
- _notaFixity :: Lens' Fixity NewNotation
- data NotationSection = NotationSection {
  - sectNotation :: NewNotation
  - sectKind :: NotationKind
  - sectLevel :: Maybe FixityLevel
  - sectIsSection :: Bool
  }
- noSection :: NewNotation -> NotationSection

# Documentation

data HoleName Source #

Data type constructed in the Happy parser; converted to `GenPart` before it leaves the Happy code.

Constructors

LambdaHole | `x -> y`; 1st argument is the bound name (unused for now).

Fields

- _bindHoleName :: RString
- holeName :: RString

ExprHole | Simple named hole with hiding.

Fields

- holeName :: RString

isLambdaHole :: HoleName -> Bool Source #

Is the hole a binder?

stringParts :: Notation -> [String] Source #

Get a flat list of identifier parts of a notation.

holeTarget :: GenPart -> Maybe Int Source #

Target argument position of a part (Nothing if it is not a hole).

isAHole :: GenPart -> Bool Source #

Is the part a hole? WildHoles don't count since they don't correspond to anything the user writes.

isNormalHole :: GenPart -> Bool Source #

Is the part a normal hole?

isBindingHole :: GenPart -> Bool Source #

Is the part a binder?

data NotationKind Source #

Classification of notations.

Constructors

InfixNotation | Ex: `_bla_blub_`.
PrefixNotation | Ex: `_bla_blub`.
PostfixNotation | Ex: `bla_blub_`.
NonfixNotation | Ex: `bla_blub`.
NoNotation |

#### Instances

Instances details

Pretty NotationKind Source # |
Instance details Defined in Agda.Syntax.Notation Methods pretty :: NotationKind -> Doc Source # prettyPrec :: Int -> NotationKind -> Doc Source # prettyList :: [NotationKind] -> Doc Source #
Generic NotationKind Source # |
Instance details Defined in Agda.Syntax.Notation Associated Types type Rep NotationKind :: Type -> Type Source # Methods from :: NotationKind -> Rep NotationKind x Source # to :: Rep NotationKind x -> NotationKind Source #
Show NotationKind Source # |
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NotationKind -> ShowS Source # show :: NotationKind -> String Source # showList :: [NotationKind] -> ShowS Source #
NFData NotationKind Source # |
Instance details Defined in Agda.Syntax.Notation Methods rnf :: NotationKind -> () Source #
Eq NotationKind Source # |
Instance details Defined in Agda.Syntax.Notation Methods (==) :: NotationKind -> NotationKind -> Bool Source # (/=) :: NotationKind -> NotationKind -> Bool Source #
type Rep NotationKind Source # |

Instance details

Defined in Agda.Syntax.Notation

type Rep NotationKind = D1 ('MetaData "NotationKind" "Agda.Syntax.Notation" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) ((C1 ('MetaCons "InfixNotation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrefixNotation" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PostfixNotation" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NonfixNotation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoNotation" 'PrefixI 'False) (U1 :: Type -> Type))))

notationKind :: Notation -> NotationKind Source #

Classify a notation by presence of leading and/or trailing normal holes.

mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation Source #

From notation with names to notation with indices.

Example: `ids = ["for", "x", "∈", "xs", "return", "e"] holes = [ LambdaHole "x" "e", ExprHole "xs" ]` creates the notation `[ IdPart "for" , BindHole 0 , IdPart "∈" , NormalHole 1 , IdPart "return" , NormalHole 0 ]`

data NewNotation Source #

All the notation information related to a name.

Constructors

NewNotation |

Fields

- notaName :: QName
- notaNames :: Set Name

  The names the syntax and/or fixity belong to.

  Invariant: The set is non-empty. Every name in the list matches `notaName`.

- notaFixity :: Fixity

  Associativity and precedence (fixity) of the names.

- notation :: Notation

  Syntax associated with the names.

- notaIsOperator :: Bool

  True if the notation comes from an operator (rather than a syntax declaration).

#### Instances

Instances details

LensFixity NewNotation Source # |
Instance details Defined in Agda.Syntax.Notation Methods lensFixity :: Lens' Fixity NewNotation Source #
Pretty NewNotation Source # |
Instance details Defined in Agda.Syntax.Notation Methods pretty :: NewNotation -> Doc Source # prettyPrec :: Int -> NewNotation -> Doc Source # prettyList :: [NewNotation] -> Doc Source #
Generic NewNotation Source # |
Instance details Defined in Agda.Syntax.Notation Associated Types type Rep NewNotation :: Type -> Type Source # Methods from :: NewNotation -> Rep NewNotation x Source # to :: Rep NewNotation x -> NewNotation Source #
Show NewNotation Source # |
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NewNotation -> ShowS Source # show :: NewNotation -> String Source # showList :: [NewNotation] -> ShowS Source #
NFData NewNotation Source # |
Instance details Defined in Agda.Syntax.Notation Methods rnf :: NewNotation -> () Source #
type Rep NewNotation Source # |

Instance details

Defined in Agda.Syntax.Notation

type Rep NewNotation = D1 ('MetaData "NewNotation" "Agda.Syntax.Notation" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "NewNotation" 'PrefixI 'True) ((S1 ('MetaSel ('Just "notaName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "notaNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Name))) :*: (S1 ('MetaSel ('Just "notaFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity) :*: (S1 ('MetaSel ('Just "notation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Notation) :*: S1 ('MetaSel ('Just "notaIsOperator") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

namesToNotation :: QName -> Name -> NewNotation Source #

If an operator has no specific notation, then it is computed from its name.

useDefaultFixity :: NewNotation -> NewNotation Source #

Replace `noFixity` by `defaultFixity`.

notationNames :: NewNotation -> [QName] Source #

Return the `IdPart`s of a notation, the first part qualified, the other parts unqualified. This allows for qualified use of operators, e.g., `M.for x ∈ xs return e`, or `x ℕ.+ y`.

syntaxOf :: Name -> Notation Source #

Create a `Notation` (without binders) from a concrete `Name`. Does the obvious thing: `Hole`s become `NormalHole`s, `Id`s become `IdParts`. If `Name` has no `Hole`s, it returns `noNotation`.

mergeNotations :: [NewNotation] -> [NewNotation] Source #

Merges `NewNotation`s that have the same precedence level and notation, with two exceptions:

- Operators and notations coming from syntax declarations are kept separate.
- If all instances of a given `NewNotation` have the same precedence level or are "unrelated", then they are merged. They get the given precedence level, if any, and otherwise they become unrelated (but related to each other).

If `NewNotation`s that are merged have distinct associativities, then they get `NonAssoc` as their associativity.

Precondition: No `Name` may occur in more than one list element. Every `NewNotation` must have the same `notaName`.

Postcondition: No `Name` occurs in more than one list element.

_notaFixity :: Lens' Fixity NewNotation Source #

Lens for `Fixity` in `NewNotation`.

# Sections

data NotationSection Source #

Sections, as well as non-sectioned operators.

Constructors

NotationSection |

Fields

- sectNotation :: NewNotation
- sectKind :: NotationKind

  For non-sectioned operators this should match the notation's `notationKind`.

- sectLevel :: Maybe FixityLevel

  Effective precedence level. `Nothing` for closed notations.

- sectIsSection :: Bool

  `False` for non-sectioned operators.

#### Instances

Instances details

Pretty NotationSection Source # |
Instance details Defined in Agda.Syntax.Notation Methods pretty :: NotationSection -> Doc Source # prettyPrec :: Int -> NotationSection -> Doc Source # prettyList :: [NotationSection] -> Doc Source #
Generic NotationSection Source # |
Instance details Defined in Agda.Syntax.Notation Associated Types type Rep NotationSection :: Type -> Type Source # Methods from :: NotationSection -> Rep NotationSection x Source # to :: Rep NotationSection x -> NotationSection Source #
Show NotationSection Source # |
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NotationSection -> ShowS Source # show :: NotationSection -> String Source # showList :: [NotationSection] -> ShowS Source #
NFData NotationSection Source # |
Instance details Defined in Agda.Syntax.Notation Methods rnf :: NotationSection -> () Source #
type Rep NotationSection Source # |

Instance details

Defined in Agda.Syntax.Notation

type Rep NotationSection = D1 ('MetaData "NotationSection" "Agda.Syntax.Notation" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "NotationSection" 'PrefixI 'True) ((S1 ('MetaSel ('Just "sectNotation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NewNotation) :*: S1 ('MetaSel ('Just "sectKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NotationKind)) :*: (S1 ('MetaSel ('Just "sectLevel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FixityLevel)) :*: S1 ('MetaSel ('Just "sectIsSection") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))

noSection :: NewNotation -> NotationSection Source #

Converts a notation to a (non-)section.

# Pretty printing