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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Fixity

Contents

Description

Definitions for fixity, precedence levels, and declared syntax.

Synopsis

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

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) # 
KillRange x => KillRange (ThingWithFixity x) # 

data NewNotation #

All the notation information related to a name.

Constructors

NewNotation 

Fields

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.

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

noSection :: NewNotation -> NotationSection #

Converts a notation to a (non-)section.

Fixity

data Fixity #

Fixity of operators.

Constructors

Fixity 

Fields

Instances

Eq Fixity # 

Methods

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

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

Ord Fixity # 
Show Fixity # 
NFData Fixity #

Ranges are not forced.

Methods

rnf :: Fixity -> () #

KillRange Fixity # 
HasRange Fixity # 

Methods

getRange :: Fixity -> Range #

ToTerm Fixity # 

Methods

toTerm :: TCM (Fixity -> Term) #

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

Precendence

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?

Some lenses

Printing

NFData instances