| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Fixity
Description
Definitions for fixity, precedence levels, and declared syntax.
- data Fixity' = Fixity' {
- theFixity :: !Fixity
- theNotation :: Notation
- theNameRange :: Range
- 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
- type PrecedenceStack = [Precedence]
- pushPrecedence :: Precedence -> PrecedenceStack -> PrecedenceStack
- headPrecedence :: PrecedenceStack -> Precedence
- hiddenArgumentCtx :: Hiding -> Precedence
- opBrackets :: Fixity -> PrecedenceStack -> Bool
- opBrackets' :: Bool -> Fixity -> PrecedenceStack -> Bool
- lamBrackets' :: Bool -> PrecedenceStack -> Bool
- lamBrackets :: PrecedenceStack -> Bool
- appBrackets :: PrecedenceStack -> Bool
- appBrackets' :: Bool -> PrecedenceStack -> Bool
- withAppBrackets :: PrecedenceStack -> Bool
- piBrackets :: PrecedenceStack -> Bool
- roundFixBrackets :: PrecedenceStack -> 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.
Constructors
| Fixity' | |
Fields
| |
data ThingWithFixity x #
Decorating something with Fixity'.
Constructors
| ThingWithFixity x Fixity' |
Instances
| Functor ThingWithFixity # | |
| Foldable ThingWithFixity # | |
| Traversable ThingWithFixity # | |
| Data x => Data (ThingWithFixity x) # | |
| Show x => Show (ThingWithFixity x) # | |
| KillRange x => KillRange (ThingWithFixity x) # | |
data NewNotation #
All the notation information related to a name.
Constructors
| NewNotation | |
Fields
| |
Instances
namesToNotation :: QName -> Name -> NewNotation #
If an operator has no specific notation, then it is computed from its name.
useDefaultFixity :: NewNotation -> NewNotation #
Replace noFixity by defaultFixity.
notationNames :: NewNotation -> [QName] #
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 #
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] #
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.
Sections
data NotationSection #
Sections, as well as non-sectioned operators.
Constructors
| NotationSection | |
Fields
| |
Instances
noSection :: NewNotation -> NotationSection #
Converts a notation to a (non-)section.
Fixity
data PrecedenceLevel #
Precedence levels for operators.
Fixity of operators.
Constructors
| Fixity | |
Fields
| |
defaultFixity :: Fixity #
Precendence
data Precedence #
Precedence is associated with a context.
Constructors
| TopCtx | |
| FunctionSpaceDomainCtx | |
| LeftOperandCtx Fixity | |
| RightOperandCtx Fixity | |
| FunctionCtx | |
| ArgumentCtx | |
| InsideOperandCtx | |
| WithFunCtx | |
| WithArgCtx | |
| DotPatternCtx |
Instances
type PrecedenceStack = [Precedence] #
When printing we keep track of a stack of precedences in order to be able
to decide whether it's safe to leave out parens around lambdas. An empty
stack is equivalent to TopCtx. Invariant: `notElem TopCtx`.
:: Hiding -> Precedence #
The precedence corresponding to a possibly hidden argument.
opBrackets :: Fixity -> PrecedenceStack -> Bool #
Do we need to bracket an operator application of the given fixity in a context with the given precedence.
opBrackets' :: Bool -> Fixity -> PrecedenceStack -> Bool #
Do we need to bracket an operator application of the given fixity in a context with the given precedence.
lamBrackets' :: Bool -> PrecedenceStack -> Bool #
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. To decide we need to look
at the stack of precedences and not just the current precedence.
Example: m₁ >>= (λ x → x) >>= m₂ (for _>>=_ left associative).
The first argument is the parenthesis preference. If True, we add
parentheses also in right operand contexts where they aren't strictly
needed.
lamBrackets :: PrecedenceStack -> Bool #
Preference for adding parentheses.
appBrackets :: PrecedenceStack -> Bool #
Does a function application need brackets?
appBrackets' :: Bool -> PrecedenceStack -> Bool #
Does a function application need brackets?
withAppBrackets :: PrecedenceStack -> Bool #
Does a with application need brackets?
piBrackets :: PrecedenceStack -> Bool #
Does a function space need brackets?
roundFixBrackets :: PrecedenceStack -> Bool #