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

Agda.Syntax.Fixity

Description

Definitions for fixity and precedence levels.

Synopsis

- data Fixity' = Fixity' {
  - theFixity :: Fixity
  - theNotation :: Notation
  }
- type NewNotation = (Name, Fixity, Notation)
- oldToNewNotation :: (Name, Fixity') -> NewNotation
- syntaxOf :: Name -> Notation
- data Fixity
  - = LeftAssoc Range Nat
  - | RightAssoc Range Nat
  - | NonAssoc Range Nat
- fixityLevel :: Fixity -> Nat
- 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' |
Data Fixity' |
Show Fixity' |
Typeable Fixity' |
EmbPrj Fixity' |

type NewNotation = (Name, Fixity, Notation)

All the notation information related to a name.

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

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

syntaxOf :: Name -> Notation

data Fixity

Fixity of operators.

Constructors

LeftAssoc Range Nat |
RightAssoc Range Nat |
NonAssoc Range Nat |

Instances

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

fixityLevel :: Fixity -> Nat

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

Data Precedence |
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 a right operand context. For instance: `m >>= x -> m'` is a valid infix application.

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