Safe Haskell | None |
---|---|
Language | Haskell98 |
Definitions for fixity, precedence levels, and declared syntax.
- data Fixity' = Fixity' {}
- data ThingWithFixity x = ThingWithFixity x Fixity'
- data NewNotation = NewNotation {}
- namesToNotation :: QName -> Name -> NewNotation
- notationNames :: NewNotation -> [QName]
- syntaxOf :: Name -> Notation
- defaultFixity' :: Fixity'
- noFixity' :: Fixity'
- mergeNotations :: [NewNotation] -> [NewNotation]
- data Associativity
- data Fixity = Fixity {}
- defaultFixity :: Fixity
- noFixity :: 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
Notation coupled with Fixity
The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.
data ThingWithFixity x Source
Decorating something with Fixity'
.
namesToNotation :: QName -> Name -> NewNotation Source
If an operator has no specific notation, then it is computed from its name.
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 all NewNotation
s that have the same notation.
If all NewNotation
s with a given notation have the same fixity,
then this fixity is preserved, and otherwise it is replaced by
defaultFixity
.
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.
Fixity
data Associativity Source
Associativity.
Fixity of operators.
defaultFixity :: Fixity Source
The default fixity. Currently defined to be
.NonAssoc
20
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