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
• theNameRange :: Range

  Range of the name in the fixity declaration (used for correct highlighting, see issue #2140).

Instances

Eq Fixity'

Methods

(==) :: Fixity' -> Fixity' -> Bool

(/=) :: Fixity' -> Fixity' -> Bool

Show Fixity'

Methods

showsPrec :: Int -> Fixity' -> ShowS

show :: Fixity' -> String

showList :: [Fixity'] -> ShowS

NFData Fixity'

Methods

rnf :: Fixity' -> ()

KillRange Fixity'

Methods

killRange :: KillRangeT Fixity'

ToTerm Fixity'

Methods

toTerm :: TCM (Fixity' -> Term)

toTermR :: TCM (Fixity' -> ReduceM Term)

PrimTerm Fixity'

Methods

primTerm :: Fixity' -> TCM Term

data ThingWithFixity x

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances

Functor ThingWithFixity

Methods

fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b

(<$) :: a -> ThingWithFixity b -> ThingWithFixity a

Foldable ThingWithFixity

Methods

fold :: Monoid m => ThingWithFixity m -> m

foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> m

foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b

foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b

foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b

foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b

foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a

foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a

toList :: ThingWithFixity a -> [a]

null :: ThingWithFixity a -> Bool

length :: ThingWithFixity a -> Int

elem :: Eq a => a -> ThingWithFixity a -> Bool

maximum :: Ord a => ThingWithFixity a -> a

minimum :: Ord a => ThingWithFixity a -> a

sum :: Num a => ThingWithFixity a -> a

product :: Num a => ThingWithFixity a -> a

Traversable ThingWithFixity

Methods

traverse :: Applicative f => (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b)

sequenceA :: Applicative f => ThingWithFixity (f a) -> f (ThingWithFixity a)

mapM :: Monad m => (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b)

sequence :: Monad m => ThingWithFixity (m a) -> m (ThingWithFixity a)

Show x => Show (ThingWithFixity x)

Methods

showsPrec :: Int -> ThingWithFixity x -> ShowS

show :: ThingWithFixity x -> String

showList :: [ThingWithFixity x] -> ShowS

KillRange x => KillRange (ThingWithFixity x)

Methods

killRange :: KillRangeT (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.

• notaIsOperator :: Bool

  True if the notation comes from an operator (rather than a syntax declaration).

Instances

Show NewNotation

Methods

showsPrec :: Int -> NewNotation -> ShowS

show :: NewNotation -> String

showList :: [NewNotation] -> ShowS

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.

noFixity' :: Fixity'

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 NewNotation have 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

• sectNotation :: NewNotation
• sectKind :: NotationKind

  For non-sectioned operators this should match the notation's notationKind.

• sectLevel :: Maybe PrecedenceLevel

  Effective precedence level. Nothing for closed notations.

• sectIsSection :: Bool

  False for non-sectioned operators.

Instances

Show NotationSection

Methods

showsPrec :: Int -> NotationSection -> ShowS

show :: NotationSection -> String

showList :: [NotationSection] -> ShowS

noSection :: NewNotation -> NotationSection

Converts a notation to a (non-)section.

Fixity

data PrecedenceLevel

Precedence levels for operators.

Constructors

Unrelated

No fixity declared.

Related !Integer

Fixity level declared as the Integer.

Instances

Eq PrecedenceLevel

Methods

(==) :: PrecedenceLevel -> PrecedenceLevel -> Bool

(/=) :: PrecedenceLevel -> PrecedenceLevel -> Bool

Ord PrecedenceLevel

Methods

compare :: PrecedenceLevel -> PrecedenceLevel -> Ordering

(<) :: PrecedenceLevel -> PrecedenceLevel -> Bool

(<=) :: PrecedenceLevel -> PrecedenceLevel -> Bool

(>) :: PrecedenceLevel -> PrecedenceLevel -> Bool

(>=) :: PrecedenceLevel -> PrecedenceLevel -> Bool

max :: PrecedenceLevel -> PrecedenceLevel -> PrecedenceLevel

min :: PrecedenceLevel -> PrecedenceLevel -> PrecedenceLevel

Show PrecedenceLevel

Methods

showsPrec :: Int -> PrecedenceLevel -> ShowS

show :: PrecedenceLevel -> String

showList :: [PrecedenceLevel] -> ShowS

ToTerm PrecedenceLevel

Methods

toTerm :: TCM (PrecedenceLevel -> Term)

toTermR :: TCM (PrecedenceLevel -> ReduceM Term)

data Associativity

Associativity.

Constructors

NonAssoc

LeftAssoc

RightAssoc

Instances

Eq Associativity

Methods

(==) :: Associativity -> Associativity -> Bool

(/=) :: Associativity -> Associativity -> Bool

Ord Associativity

Methods

compare :: Associativity -> Associativity -> Ordering

(<) :: Associativity -> Associativity -> Bool

(<=) :: Associativity -> Associativity -> Bool

(>) :: Associativity -> Associativity -> Bool

(>=) :: Associativity -> Associativity -> Bool

max :: Associativity -> Associativity -> Associativity

min :: Associativity -> Associativity -> Associativity

Show Associativity

Methods

showsPrec :: Int -> Associativity -> ShowS

show :: Associativity -> String

showList :: [Associativity] -> ShowS

ToTerm Associativity

Methods

toTerm :: TCM (Associativity -> Term)

toTermR :: TCM (Associativity -> ReduceM Term)

data Fixity

Fixity of operators.

Constructors

Fixity

Fields

• fixityRange :: Range

  Range of the whole fixity declaration.

• fixityLevel :: !PrecedenceLevel
• fixityAssoc :: !Associativity

Instances

Eq Fixity

Methods

(==) :: Fixity -> Fixity -> Bool

(/=) :: Fixity -> Fixity -> Bool

Ord Fixity

Methods

compare :: Fixity -> Fixity -> Ordering

(<) :: Fixity -> Fixity -> Bool

(<=) :: Fixity -> Fixity -> Bool

(>) :: Fixity -> Fixity -> Bool

(>=) :: Fixity -> Fixity -> Bool

max :: Fixity -> Fixity -> Fixity

min :: Fixity -> Fixity -> Fixity

Show Fixity

Methods

showsPrec :: Int -> Fixity -> ShowS

show :: Fixity -> String

showList :: [Fixity] -> ShowS

NFData Fixity

Ranges are not forced.

Methods

rnf :: Fixity -> ()

KillRange Fixity

Methods

killRange :: KillRangeT Fixity

HasRange Fixity

Methods

getRange :: Fixity -> Range

ToTerm Fixity

Methods

toTerm :: TCM (Fixity -> Term)

toTermR :: TCM (Fixity -> ReduceM Term)

noFixity :: Fixity

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

Eq Precedence

Methods

(==) :: Precedence -> Precedence -> Bool

(/=) :: Precedence -> Precedence -> Bool

Show Precedence

Methods

showsPrec :: Int -> Precedence -> ShowS

show :: Precedence -> String

showList :: [Precedence] -> ShowS

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

Some lenses

_notaFixity :: Lens' Fixity NewNotation

_fixityAssoc :: Lens' Associativity Fixity

_fixityLevel :: Lens' PrecedenceLevel Fixity

Printing

NFData instances