Agda.Syntax.Fixity

Definitions for fixity, precedence levels, and declared syntax.

Notation coupled with Fixity

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'

KillRange Fixity'

EmbPrj Fixity'

data ThingWithFixity x

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances

Functor ThingWithFixity

Foldable ThingWithFixity

Traversable ThingWithFixity

Show x => Show (ThingWithFixity x)

data NewNotation

All the notation information related to a name.

Constructors

NewNotation

Fields

notaName :: QName

notaNames :: Set Name

The names the syntax and/or fixity belong to.

Invariant: The set is non-empty. Every name in the list matches notaName.

notaFixity :: Fixity

Associativity and precedence (fixity) of the names.

notation :: Notation

Syntax associated with the names.

Instances

Show NewNotation

namesToNotation :: QName -> Name -> NewNotation

If an operator has no specific notation, then it is computed from its name.

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.

defaultFixity' :: Fixity'

mergeNotations :: [NewNotation] -> [NewNotation]

Merges all NewNotations that have the same notation.

If all NewNotations 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

Associativity.

Constructors

NonAssoc

LeftAssoc

RightAssoc

Instances

Eq Associativity

Ord Associativity

Show Associativity

EmbPrj Associativity

data Fixity

Fixity of operators.

Constructors

Fixity

Fields

fixityRange :: Range

fixityLevel :: Integer

fixityAssoc :: Associativity

Instances

Eq Fixity

Ord Fixity

Show Fixity

KillRange Fixity

HasRange Fixity

EmbPrj Fixity

defaultFixity :: Fixity

The default fixity. Currently defined to be NonAssoc 20.

noFixity :: Fixity

Hack used for syntax facility.

Precendence

data Precedence

Precedence is associated with a context.

Constructors

TopCtx

FunctionSpaceDomainCtx

LeftOperandCtx Fixity

RightOperandCtx Fixity

FunctionCtx

ArgumentCtx

InsideOperandCtx

WithFunCtx

WithArgCtx

DotPatternCtx

Instances

Show 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