| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.Syntax.Fixity
Description
Definitions for fixity and precedence levels.
- data Fixity' = Fixity' {}
- data ThingWithFixity x = ThingWithFixity x Fixity'
- type NewNotation = (QName, Fixity, Notation)
- oldToNewNotation :: (QName, Fixity') -> NewNotation
- syntaxOf :: Name -> Notation
- defaultFixity' :: Fixity'
- noFixity :: Fixity
- data Fixity
- fixityLevel :: Fixity -> Integer
- 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
Documentation
The notation is handled as the fixity in the renamer. Hence they are grouped together in this type.
Constructors
| Fixity' | |
Fields
| |
data ThingWithFixity x Source
Constructors
| ThingWithFixity x Fixity' |
Instances
| Functor ThingWithFixity | |
| Foldable ThingWithFixity | |
| Traversable ThingWithFixity | |
| Show x => Show (ThingWithFixity x) | |
| Pretty (ThingWithFixity Name) | |
| KillRange x => KillRange (ThingWithFixity x) | |
| Typeable (* -> *) ThingWithFixity |
type NewNotation = (QName, Fixity, Notation) Source
All the notation information related to a name.
oldToNewNotation :: (QName, Fixity') -> NewNotation Source
If an operator has no specific notation, recover it from its name.
Fixity of operators.
fixityLevel :: Fixity -> Integer Source
defaultFixity :: Fixity Source
The default fixity. Currently defined to be NonAssoc 20
data Precedence Source
Precedence is associated with a context.
Constructors
| TopCtx | |
| FunctionSpaceDomainCtx | |
| LeftOperandCtx Fixity | |
| RightOperandCtx Fixity | |
| FunctionCtx | |
| ArgumentCtx | |
| InsideOperandCtx | |
| WithFunCtx | |
| WithArgCtx | |
| DotPatternCtx |
Instances
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