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.ExprHoleSimple named hole with hiding.
ModuleAgda-2.7.0.1Haskell2010
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.
- 4 types
- 15 values
- PackageAgda-2.7.0.1
- Exports19
- LanguageHaskell2010
- LicenceMIT
- SourceNotation.hs
Is the hole a binder?
Get a flat list of identifier parts of a notation.
Target argument position of a part (Nothing if it is not a hole).
Is the part a hole?
Is the part a binder?
Classification of notations.
Constructors
InfixNotationEx:
_bla_blub_.PrefixNotationEx:
_bla_blub.PostfixNotationEx:
bla_blub_.NonfixNotationEx:
bla_blub.NoNotation
Instances6Eq, Show, Generic, NFData, Pretty, Rep
Eq NotationKindDefined in Agda-2.7.0.1 · Agda.Syntax.NotationShow NotationKindDefined in Agda-2.7.0.1 · Agda.Syntax.NotationGeneric NotationKindDefined in Agda-2.7.0.1 · Agda.Syntax.NotationNFData NotationKindDefined in Agda-2.7.0.1 · Agda.Syntax.NotationPretty NotationKindDefined in Agda-2.7.0.1 · Agda.Syntax.Notationtype Rep NotationKind = D1 ('MetaDataDefined in Agda-2.7.0.1 · Agda.Syntax.Notation"NotationKind"
"Agda.Syntax.Notation"
"Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8"
'False) ((C1 ('MetaCons"InfixNotation"
'PrefixI 'False) U1 :+: C1 ('MetaCons"PrefixNotation"
'PrefixI 'False) U1) :+: (C1 ('MetaCons"PostfixNotation"
'PrefixI 'False) U1 :+: (C1 ('MetaCons"NonfixNotation"
'PrefixI 'False) U1 :+: C1 ('MetaCons"NoNotation"
'PrefixI 'False) U1)))
Classify a notation by presence of leading and/or trailing normal holes.
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
]
All the notation information related to a name.
Constructors
NewNotationnotaName :: QNamenotaNames :: Set NameThe names the syntax and/or fixity belong to.
Invariant: The set is non-empty. Every name in the list matches notaName.
notaFixity :: FixityAssociativity and precedence (fixity) of the names.
notation :: NotationSyntax associated with the names.
notaIsOperator :: BoolTrue if the notation comes from an operator (rather than a syntax declaration).
Instances6Show, Generic, NFData, Pretty, LensFixity, Rep
Show NewNotationDefined in Agda-2.7.0.1 · Agda.Syntax.NotationGeneric NewNotationDefined in Agda-2.7.0.1 · Agda.Syntax.NotationNFData NewNotationDefined in Agda-2.7.0.1 · Agda.Syntax.NotationPretty NewNotationDefined in Agda-2.7.0.1 · Agda.Syntax.NotationLensFixity NewNotationDefined in Agda-2.7.0.1 · Agda.Syntax.Notationtype Rep NewNotation = D1 ('MetaDataDefined in Agda-2.7.0.1 · Agda.Syntax.Notation"NewNotation"
"Agda.Syntax.Notation"
"Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8"
'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)))))
If an operator has no specific notation, then it is computed from its name.
Replace noFixity by defaultFixity.
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.
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.
Check if a notation contains any lambdas (in which case it cannot be used in a pattern).
Lens for Fixity in NewNotation.
Sections
2 declarationsSections, as well as non-sectioned operators.
Constructors
NotationSectionsectNotation :: NewNotationsectKind :: NotationKindFor non-sectioned operators this should match the notation's notationKind.
sectLevel :: Maybe FixityLevelEffective precedence level. Nothing for closed notations.
sectIsSection :: BoolFalse for non-sectioned operators.
Instances5Show, Generic, NFData, Pretty, Rep
Show NotationSectionDefined in Agda-2.7.0.1 · Agda.Syntax.NotationGeneric NotationSectionDefined in Agda-2.7.0.1 · Agda.Syntax.NotationNFData NotationSectionDefined in Agda-2.7.0.1 · Agda.Syntax.NotationPretty NotationSectionDefined in Agda-2.7.0.1 · Agda.Syntax.Notationtype Rep NotationSection = D1 ('MetaDataDefined in Agda-2.7.0.1 · Agda.Syntax.Notation"NotationSection"
"Agda.Syntax.Notation"
"Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8"
'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))))
Converts a notation to a (non-)section.