Safe Haskell | None |
---|---|
Language | Haskell98 |
Definitions for fixity, precedence levels, and declared syntax.
- data Fixity' = Fixity' {
- theFixity :: !Fixity
- theNotation :: Notation
- data ThingWithFixity x = ThingWithFixity x Fixity'
- data NewNotation = NewNotation {}
- namesToNotation :: QName -> Name -> NewNotation
- useDefaultFixity :: NewNotation -> NewNotation
- notationNames :: NewNotation -> [QName]
- syntaxOf :: Name -> Notation
- noFixity' :: Fixity'
- mergeNotations :: [NewNotation] -> [NewNotation]
- data NotationSection = NotationSection {}
- noSection :: NewNotation -> NotationSection
- data PrecedenceLevel
- data Associativity
- data Fixity = Fixity {}
- noFixity :: Fixity
- defaultFixity :: Fixity
- data Precedence
- hiddenArgumentCtx :: Hiding -> Precedence
- opBrackets :: Fixity -> Precedence -> Bool
- lamBrackets :: Precedence -> Bool
- appBrackets :: Precedence -> Bool
- withAppBrackets :: Precedence -> Bool
- piBrackets :: Precedence -> Bool
- roundFixBrackets :: Precedence -> Bool
- _notaFixity :: Lens' Fixity NewNotation
- _fixityAssoc :: Lens' Associativity Fixity
- _fixityLevel :: Lens' PrecedenceLevel Fixity
Notation coupled with Fixity
The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.
Fixity' | |
|
data ThingWithFixity x Source
Decorating something with Fixity'
.
data NewNotation Source
All the notation information related to a name.
NewNotation | |
|
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.
Sections
data NotationSection Source
Sections, as well as non-sectioned operators.
NotationSection | |
|
noSection :: NewNotation -> NotationSection Source
Converts a notation to a (non-)section.
Fixity
data PrecedenceLevel Source
Precedence levels for operators.
data Associativity Source
Associativity.
Fixity of operators.
Precendence
data Precedence Source
Precedence is associated with a context.
hiddenArgumentCtx :: Hiding -> Precedence Source
The precedence corresponding to a possibly hidden argument.
opBrackets :: Fixity -> Precedence -> Bool Source
Do we need to bracket an operator application of the given fixity in a context with the given precedence.
lamBrackets :: Precedence -> Bool Source
Does a lambda-like thing (lambda, let or pi) need brackets in the given context? A peculiar thing with lambdas is that they don't need brackets in certain right operand contexts. However, we insert brackets anyway, for the following reasons:
- Clarity.
- Sometimes brackets are needed. Example:
m₁ >>= (λ x → x) >>= m₂
(here_>>=_
is left associative).
appBrackets :: Precedence -> Bool Source
Does a function application need brackets?
withAppBrackets :: Precedence -> Bool Source
Does a with application need brackets?
piBrackets :: Precedence -> Bool Source
Does a function space need brackets?
roundFixBrackets :: Precedence -> Bool Source