Agda-2.6.0: 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' Source #

The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.

Constructors

Fixity' 

Fields

Instances
Eq Fixity' Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

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

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

Data Fixity' Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fixity' -> c Fixity' #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity' #

toConstr :: Fixity' -> Constr #

dataTypeOf :: Fixity' -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity') #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity') #

gmapT :: (forall b. Data b => b -> b) -> Fixity' -> Fixity' #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r #

gmapQ :: (forall d. Data d => d -> u) -> Fixity' -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity' -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' #

Show Fixity' Source # 
Instance details

Defined in Agda.Syntax.Fixity

NFData Fixity' Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

rnf :: Fixity' -> () #

Pretty Fixity' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Fixity' Source # 
Instance details

Defined in Agda.Syntax.Fixity

EmbPrj Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

ToTerm Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

data ThingWithFixity x Source #

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity' 
Instances
Functor ThingWithFixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

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

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

Foldable ThingWithFixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

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 Source # 
Instance details

Defined in Agda.Syntax.Fixity

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) #

Data x => Data (ThingWithFixity x) Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ThingWithFixity x -> c (ThingWithFixity x) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x) #

toConstr :: ThingWithFixity x -> Constr #

dataTypeOf :: ThingWithFixity x -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ThingWithFixity x)) #

gmapT :: (forall b. Data b => b -> b) -> ThingWithFixity x -> ThingWithFixity x #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r #

gmapQ :: (forall d. Data d => d -> u) -> ThingWithFixity x -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) #

Show x => Show (ThingWithFixity x) Source # 
Instance details

Defined in Agda.Syntax.Fixity

Pretty (ThingWithFixity Name) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange x => KillRange (ThingWithFixity x) Source # 
Instance details

Defined in Agda.Syntax.Fixity

data NewNotation Source #

All the notation information related to a name.

Constructors

NewNotation 

Fields

Instances
Show NewNotation Source # 
Instance details

Defined in Agda.Syntax.Fixity

namesToNotation :: QName -> Name -> NewNotation Source #

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

notationNames :: NewNotation -> [QName] Source #

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 Source #

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] Source #

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 Source #

Sections, as well as non-sectioned operators.

Constructors

NotationSection 

Fields

noSection :: NewNotation -> NotationSection Source #

Converts a notation to a (non-)section.

Fixity

data PrecedenceLevel Source #

Precedence levels for operators.

Constructors

Unrelated

No fixity declared.

Related !Integer

Fixity level declared as the Integer.

Instances
Eq PrecedenceLevel Source # 
Instance details

Defined in Agda.Syntax.Fixity

Data PrecedenceLevel Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PrecedenceLevel -> c PrecedenceLevel #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PrecedenceLevel #

toConstr :: PrecedenceLevel -> Constr #

dataTypeOf :: PrecedenceLevel -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PrecedenceLevel) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PrecedenceLevel) #

gmapT :: (forall b. Data b => b -> b) -> PrecedenceLevel -> PrecedenceLevel #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PrecedenceLevel -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PrecedenceLevel -> r #

gmapQ :: (forall d. Data d => d -> u) -> PrecedenceLevel -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PrecedenceLevel -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PrecedenceLevel -> m PrecedenceLevel #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PrecedenceLevel -> m PrecedenceLevel #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PrecedenceLevel -> m PrecedenceLevel #

Ord PrecedenceLevel Source # 
Instance details

Defined in Agda.Syntax.Fixity

Show PrecedenceLevel Source # 
Instance details

Defined in Agda.Syntax.Fixity

EmbPrj PrecedenceLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

ToTerm PrecedenceLevel Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

data Associativity Source #

Associativity.

Constructors

NonAssoc 
LeftAssoc 
RightAssoc 
Instances
Eq Associativity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Data Associativity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Associativity -> c Associativity #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Associativity #

toConstr :: Associativity -> Constr #

dataTypeOf :: Associativity -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Associativity) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Associativity) #

gmapT :: (forall b. Data b => b -> b) -> Associativity -> Associativity #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r #

gmapQ :: (forall d. Data d => d -> u) -> Associativity -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Associativity -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity #

Ord Associativity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Show Associativity Source # 
Instance details

Defined in Agda.Syntax.Fixity

EmbPrj Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

ToTerm Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

data Fixity Source #

Fixity of operators.

Constructors

Fixity 

Fields

Instances
Eq Fixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

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

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

Data Fixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fixity -> c Fixity #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity #

toConstr :: Fixity -> Constr #

dataTypeOf :: Fixity -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity) #

gmapT :: (forall b. Data b => b -> b) -> Fixity -> Fixity #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r #

gmapQ :: (forall d. Data d => d -> u) -> Fixity -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity #

Ord Fixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Show Fixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

NFData Fixity Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Fixity

Methods

rnf :: Fixity -> () #

Pretty Fixity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

HasRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

EmbPrj Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

ToTerm Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

data ParenPreference Source #

Do we prefer parens around arguments like λ x → x or not? See lamBrackets.

Instances
Eq ParenPreference Source # 
Instance details

Defined in Agda.Syntax.Fixity

Data ParenPreference Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ParenPreference -> c ParenPreference #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ParenPreference #

toConstr :: ParenPreference -> Constr #

dataTypeOf :: ParenPreference -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ParenPreference) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ParenPreference) #

gmapT :: (forall b. Data b => b -> b) -> ParenPreference -> ParenPreference #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ParenPreference -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ParenPreference -> r #

gmapQ :: (forall d. Data d => d -> u) -> ParenPreference -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ParenPreference -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ParenPreference -> m ParenPreference #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ParenPreference -> m ParenPreference #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ParenPreference -> m ParenPreference #

Ord ParenPreference Source # 
Instance details

Defined in Agda.Syntax.Fixity

Show ParenPreference Source # 
Instance details

Defined in Agda.Syntax.Fixity

EmbPrj ParenPreference Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Precendence

data Precedence Source #

Precedence is associated with a context.

Instances
Eq Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

Data Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Precedence -> c Precedence #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Precedence #

toConstr :: Precedence -> Constr #

dataTypeOf :: Precedence -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Precedence) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Precedence) #

gmapT :: (forall b. Data b => b -> b) -> Precedence -> Precedence #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Precedence -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Precedence -> r #

gmapQ :: (forall d. Data d => d -> u) -> Precedence -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Precedence -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Precedence -> m Precedence #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Precedence -> m Precedence #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Precedence -> m Precedence #

Show Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

Pretty Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

EmbPrj Precedence Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

type PrecedenceStack = [Precedence] Source #

When printing we keep track of a stack of precedences in order to be able to decide whether it's safe to leave out parens around lambdas. An empty stack is equivalent to TopCtx. Invariant: `notElem TopCtx`.

argumentCtx_ :: Precedence Source #

Argument context preferring parens.

opBrackets :: Fixity -> PrecedenceStack -> Bool Source #

Do we need to bracket an operator application of the given fixity in a context with the given precedence.

opBrackets' :: Bool -> Fixity -> PrecedenceStack -> Bool Source #

Do we need to bracket an operator application of the given fixity in a context with the given precedence.

lamBrackets :: PrecedenceStack -> Bool Source #

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. To decide we need to look at the stack of precedences and not just the current precedence. Example: m₁ >>= (λ x → x) >>= m₂ (for _>>=_ left associative).

appBrackets :: PrecedenceStack -> Bool Source #

Does a function application need brackets?

appBrackets' :: Bool -> PrecedenceStack -> Bool Source #

Does a function application need brackets?

withAppBrackets :: PrecedenceStack -> Bool Source #

Does a with application need brackets?

piBrackets :: PrecedenceStack -> Bool Source #

Does a function space need brackets?

Some lenses

Printing

NFData instances