Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Syntax.Fixity

Description

Definitions for fixity and precedence levels.

Synopsis

- data Fixity' = Fixity' {
  - theFixity :: Fixity
  - theNotation :: Notation
  }
- data ThingWithFixity x = ThingWithFixity x Fixity'
- type NewNotation = (QName, Fixity, Notation)
- oldToNewNotation :: (QName, Fixity') -> NewNotation
- syntaxOf :: Name -> Notation
- defaultFixity' :: Fixity'
- noFixity :: Fixity
- data Fixity
  - = LeftAssoc Range Integer
  - | RightAssoc Range Integer
  - | NonAssoc Range Integer
- fixityLevel :: Fixity -> Integer
- defaultFixity :: Fixity
- data Precedence
  - = TopCtx
  - | FunctionSpaceDomainCtx
  - | LeftOperandCtx Fixity
  - | RightOperandCtx Fixity
  - | FunctionCtx
  - | ArgumentCtx
  - | InsideOperandCtx
  - | WithFunCtx
  - | WithArgCtx
  - | DotPatternCtx
- hiddenArgumentCtx :: Hiding -> Precedence
- opBrackets :: Fixity -> Precedence -> Bool
- lamBrackets :: Precedence -> Bool
- appBrackets :: Precedence -> Bool
- withAppBrackets :: Precedence -> Bool
- piBrackets :: Precedence -> Bool
- roundFixBrackets :: Precedence -> Bool

# Documentation

data Fixity'

The notation is handled as the fixity in the renamer. Hence they are grouped together in this type.

Constructors

Fixity' |
Fields theFixity :: Fixity theNotation :: Notation

Instances

Eq Fixity' |
Show Fixity' |
Typeable Fixity' |
KillRange Fixity' |
EmbPrj Fixity' |

data ThingWithFixity x

Constructors

ThingWithFixity x Fixity' |

Instances

Functor ThingWithFixity |
Typeable1 ThingWithFixity |
Foldable ThingWithFixity |
Traversable ThingWithFixity |
Show x => Show (ThingWithFixity x) |
Pretty (ThingWithFixity Name) |
KillRange x => KillRange (ThingWithFixity x) |

type NewNotation = (QName, Fixity, Notation)

All the notation information related to a name.

oldToNewNotation :: (QName, Fixity') -> NewNotation

If an operator has no specific notation, recover it from its name.

syntaxOf :: Name -> Notation

defaultFixity' :: Fixity'

noFixity :: Fixity

data Fixity

Fixity of operators.

Constructors

LeftAssoc Range Integer |
RightAssoc Range Integer |
NonAssoc Range Integer |

Instances

Eq Fixity |
Show Fixity |
Typeable Fixity |
Pretty Fixity |
KillRange Fixity |
HasRange Fixity |
EmbPrj Fixity |

fixityLevel :: Fixity -> Integer

defaultFixity :: Fixity

The default fixity. Currently defined to be ``NonAssoc` 20`.

data Precedence

Precedence is associated with a context.

Constructors

TopCtx |
FunctionSpaceDomainCtx |
LeftOperandCtx Fixity |
RightOperandCtx Fixity |
FunctionCtx |
ArgumentCtx |
InsideOperandCtx |
WithFunCtx |
WithArgCtx |
DotPatternCtx |

Instances

Show Precedence |
Typeable Precedence |
EmbPrj Precedence |

hiddenArgumentCtx :: Hiding -> Precedence

The precedence corresponding to a possibly hidden argument.

opBrackets :: Fixity -> Precedence -> Bool

Do we need to bracket an operator application of the given fixity in a context with the given precedence.

lamBrackets :: Precedence -> 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. 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

Does a function application need brackets?

withAppBrackets :: Precedence -> Bool

Does a with application need brackets?

piBrackets :: Precedence -> Bool

Does a function space need brackets?

roundFixBrackets :: Precedence -> Bool