| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Notation
Contents
Description
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.
Synopsis
- data HoleName
- = LambdaHole { }
- | ExprHole { }
- isLambdaHole :: HoleName -> Bool
- stringParts :: Notation -> [String]
- holeTarget :: GenPart -> Maybe Int
- isAHole :: GenPart -> Bool
- isNormalHole :: GenPart -> Bool
- isBindingHole :: GenPart -> Bool
- data NotationKind
- notationKind :: Notation -> NotationKind
- mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation
- data NewNotation = NewNotation {}
- namesToNotation :: QName -> Name -> NewNotation
- useDefaultFixity :: NewNotation -> NewNotation
- notationNames :: NewNotation -> [QName]
- syntaxOf :: Name -> Notation
- mergeNotations :: [NewNotation] -> [NewNotation]
- _notaFixity :: Lens' Fixity NewNotation
- data NotationSection = NotationSection {}
- noSection :: NewNotation -> NotationSection
Documentation
Data type constructed in the Happy parser; converted to GenPart
before it leaves the Happy code.
Constructors
| LambdaHole |
|
Fields
| |
| ExprHole | Simple named hole with hiding. |
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: |
| PrefixNotation | Ex: |
| PostfixNotation | Ex: |
| NonfixNotation | Ex: |
| NoNotation |
Instances
| Eq NotationKind Source # | |
Defined in Agda.Syntax.Notation | |
| Show NotationKind Source # | |
Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NotationKind -> ShowS # show :: NotationKind -> String # showList :: [NotationKind] -> ShowS # | |
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
| |
Instances
| Show NewNotation Source # | |
Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NewNotation -> ShowS # show :: NewNotation -> String # showList :: [NewNotation] -> ShowS # | |
| LensFixity NewNotation Source # | |
Defined in Agda.Syntax.Notation Methods | |
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 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 Source #
Create a Notation (without binders) from a concrete Name.
Does the obvious thing:
Holes become NormalHoles, Ids become IdParts.
If Name has no Holes, it returns noNotation.
mergeNotations :: [NewNotation] -> [NewNotation] Source #
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
NewNotationhave 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.
_notaFixity :: Lens' Fixity NewNotation Source #
Lens for Fixity in NewNotation.
Sections
data NotationSection Source #
Sections, as well as non-sectioned operators.
Constructors
| NotationSection | |
Fields
| |
Instances
| Show NotationSection Source # | |
Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NotationSection -> ShowS # show :: NotationSection -> String # showList :: [NotationSection] -> ShowS # | |
noSection :: NewNotation -> NotationSection Source #
Converts a notation to a (non-)section.