Agda.Syntax.Notation

As a concrete name, a notation is a non-empty list of alternating IdParts 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.

Documentation

data HoleName

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

Constructors

LambdaHole

λ x₁ … xₙ → y: The first argument contains the bound names.

Fields

• _bindHoleNames :: List1 RString
• holeName :: RString

ExprHole

Simple named hole with hiding.

Fields

• holeName :: RString

isLambdaHole :: HoleName -> Bool

Is the hole a binder?

stringParts :: Notation -> [String]

Get a flat list of identifier parts of a notation.

holeTarget :: NotationPart -> Maybe Int

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

isAHole :: NotationPart -> Bool

Is the part a hole?

isBinder :: NotationPart -> Bool

Is the part a binder?

data NotationKind

Classification of notations.

Constructors

InfixNotation

Ex: _bla_blub_.

PrefixNotation

Ex: _bla_blub.

PostfixNotation

Ex: bla_blub_.

NonfixNotation

Ex: bla_blub.

NoNotation

Instances

Pretty NotationKind

Defined in Agda.Syntax.Notation

Methods

pretty :: NotationKind -> Doc

prettyPrec :: Int -> NotationKind -> Doc

prettyList :: [NotationKind] -> Doc

Generic NotationKind

Defined in Agda.Syntax.Notation

Associated Types

type Rep NotationKind :: Type -> Type

Methods

from :: NotationKind -> Rep NotationKind x

to :: Rep NotationKind x -> NotationKind

Show NotationKind

Defined in Agda.Syntax.Notation

Methods

showsPrec :: Int -> NotationKind -> ShowS

show :: NotationKind -> String

showList :: [NotationKind] -> ShowS

NFData NotationKind

Defined in Agda.Syntax.Notation

Methods

rnf :: NotationKind -> ()

Eq NotationKind

Defined in Agda.Syntax.Notation

Methods

(==) :: NotationKind -> NotationKind -> Bool

(/=) :: NotationKind -> NotationKind -> Bool

type Rep NotationKind

Defined in Agda.Syntax.Notation

type Rep NotationKind = D1 ('MetaData "NotationKind" "Agda.Syntax.Notation" "Agda-2.6.4-inplace" '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

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

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

From notation with names to notation with indices.

An example (with some parts of the code omitted): The lists ["for", "x", "∈", "xs", "return", "e"] and [LambdaHole ("x" :| []) "e", ExprHole "xs"] are mapped to the following notation: [ IdPart "for" , VarPart (BoundVariablePosition 0 0) , IdPart "∈" , HolePart 1 , IdPart "return" , HolePart 0 ]

data NewNotation

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

LensFixity NewNotation

Defined in Agda.Syntax.Notation

Methods

lensFixity :: Lens' NewNotation Fixity

Pretty NewNotation

Defined in Agda.Syntax.Notation

Methods

pretty :: NewNotation -> Doc

prettyPrec :: Int -> NewNotation -> Doc

prettyList :: [NewNotation] -> Doc

Generic NewNotation

Defined in Agda.Syntax.Notation

Associated Types

type Rep NewNotation :: Type -> Type

Methods

from :: NewNotation -> Rep NewNotation x

to :: Rep NewNotation x -> NewNotation

Show NewNotation

Defined in Agda.Syntax.Notation

Methods

showsPrec :: Int -> NewNotation -> ShowS

show :: NewNotation -> String

showList :: [NewNotation] -> ShowS

NFData NewNotation

Defined in Agda.Syntax.Notation

Methods

rnf :: NewNotation -> ()

type Rep NewNotation

Defined in Agda.Syntax.Notation

type Rep NewNotation = D1 ('MetaData "NewNotation" "Agda.Syntax.Notation" "Agda-2.6.4-inplace" '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

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

useDefaultFixity :: NewNotation -> NewNotation

Replace noFixity by defaultFixity.

notationNames :: NewNotation -> [QName]

Return the IdParts 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

Create a Notation (without binders) from a concrete Name. Does the obvious thing: Holes become HoleParts, Ids become IdParts. If Name has no Holes, it returns noNotation.

mergeNotations :: List1 NewNotation -> List1 NewNotation

Merges NewNotations 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 NewNotations 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.

isLambdaNotation :: NewNotation -> Bool

Check if a notation contains any lambdas (in which case it cannot be used in a pattern).

_notaFixity :: Lens' NewNotation Fixity

Lens for Fixity in NewNotation.

Sections

data NotationSection

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

Pretty NotationSection

Defined in Agda.Syntax.Notation

Methods

pretty :: NotationSection -> Doc

prettyPrec :: Int -> NotationSection -> Doc

prettyList :: [NotationSection] -> Doc

Generic NotationSection

Defined in Agda.Syntax.Notation

Associated Types

type Rep NotationSection :: Type -> Type

Methods

from :: NotationSection -> Rep NotationSection x

to :: Rep NotationSection x -> NotationSection

Show NotationSection

Defined in Agda.Syntax.Notation

Methods

showsPrec :: Int -> NotationSection -> ShowS

show :: NotationSection -> String

showList :: [NotationSection] -> ShowS

NFData NotationSection

Defined in Agda.Syntax.Notation

Methods

rnf :: NotationSection -> ()

type Rep NotationSection

Defined in Agda.Syntax.Notation

type Rep NotationSection = D1 ('MetaData "NotationSection" "Agda.Syntax.Notation" "Agda-2.6.4-inplace" '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

Converts a notation to a (non-)section.

Pretty printing