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'

Pretty Fixity'

KillRange Fixity'

EmbPrj Fixity'

Typeable * Fixity'

data ThingWithFixity x

Decorating something with Fixity'.

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

data NewNotation

All the notation information related to a name.

Constructors

NewNotation

Fields

notaName :: QName

The concrete name the syntax or fixity belongs to.

notaFixity :: Fixity

Associativity and precedence (fixity) of the name.

notation :: Notation

Syntax associated with the name.

Instances

Show NewNotation

Typeable * NewNotation

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

If an operator has no specific notation, recover it 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'

interestingFixities :: [Fixity'] -> [Fixity']

Removes copies of defaultFixity' from a list of fixities. Never returns an empty list, though, rather a singleton list consisting of defaultFixity'.

chooseFixity :: [Fixity'] -> Fixity'

If different interesting fixities are available for the same symbol, we take none of them.

Fixity

data Fixity

Fixity of operators.

Constructors

LeftAssoc

Fields

fixityRange :: Range

fixityLevel :: Integer

RightAssoc

Fields

fixityRange :: Range

fixityLevel :: Integer

NonAssoc

Fields

fixityRange :: Range

fixityLevel :: Integer

Instances

Eq Fixity

Show Fixity

Pretty Fixity

KillRange Fixity

HasRange Fixity

EmbPrj Fixity

Typeable * 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

Typeable * 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