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'

Defined in Agda.Syntax.Fixity

Methods

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

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

Data Fixity'

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'

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> Fixity' -> ShowS

show :: Fixity' -> String

showList :: [Fixity'] -> ShowS

NFData Fixity'

Defined in Agda.Syntax.Fixity

Methods

rnf :: Fixity' -> ()

Pretty Fixity'

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Fixity' -> Doc

prettyPrec :: Int -> Fixity' -> Doc

prettyList :: [Fixity'] -> Doc

KillRange Fixity'

Defined in Agda.Syntax.Fixity

Methods

killRange :: KillRangeT Fixity'

EmbPrj Fixity'

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Fixity' -> S Int32

icod_ :: Fixity' -> S Int32

value :: Int32 -> R Fixity'

ToTerm Fixity'

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Fixity' -> Term)

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

PrimTerm Fixity'

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Fixity' -> TCM Term

data ThingWithFixity x

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances

Functor ThingWithFixity

Defined in Agda.Syntax.Fixity

Methods

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

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

Foldable ThingWithFixity

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

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)

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)

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> ThingWithFixity x -> ShowS

show :: ThingWithFixity x -> String

showList :: [ThingWithFixity x] -> ShowS

Pretty (ThingWithFixity Name)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ThingWithFixity Name -> Doc

prettyPrec :: Int -> ThingWithFixity Name -> Doc

prettyList :: [ThingWithFixity Name] -> Doc

KillRange x => KillRange (ThingWithFixity x)

Defined in Agda.Syntax.Fixity

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

Defined in Agda.Syntax.Fixity

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

Defined in Agda.Syntax.Fixity

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

Defined in Agda.Syntax.Fixity

Methods

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

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

Data PrecedenceLevel

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

Defined in Agda.Syntax.Fixity

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

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> PrecedenceLevel -> ShowS

show :: PrecedenceLevel -> String

showList :: [PrecedenceLevel] -> ShowS

EmbPrj PrecedenceLevel

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: PrecedenceLevel -> S Int32

icod_ :: PrecedenceLevel -> S Int32

value :: Int32 -> R PrecedenceLevel

ToTerm PrecedenceLevel

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (PrecedenceLevel -> Term)

toTermR :: TCM (PrecedenceLevel -> ReduceM Term)

data Associativity

Associativity.

Constructors

NonAssoc

LeftAssoc

RightAssoc

Instances

Eq Associativity

Defined in Agda.Syntax.Fixity

Methods

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

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

Data Associativity

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

Defined in Agda.Syntax.Fixity

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

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> Associativity -> ShowS

show :: Associativity -> String

showList :: [Associativity] -> ShowS

EmbPrj Associativity

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Associativity -> S Int32

icod_ :: Associativity -> S Int32

value :: Int32 -> R Associativity

ToTerm Associativity

Defined in Agda.TypeChecking.Primitive

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

Defined in Agda.Syntax.Fixity

Methods

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

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

Data Fixity

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

Defined in Agda.Syntax.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

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> Fixity -> ShowS

show :: Fixity -> String

showList :: [Fixity] -> ShowS

NFData Fixity

Ranges are not forced.

Defined in Agda.Syntax.Fixity

Methods

rnf :: Fixity -> ()

Pretty Fixity

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Fixity -> Doc

prettyPrec :: Int -> Fixity -> Doc

prettyList :: [Fixity] -> Doc

KillRange Fixity

Defined in Agda.Syntax.Fixity

Methods

killRange :: KillRangeT Fixity

HasRange Fixity

Defined in Agda.Syntax.Fixity

Methods

getRange :: Fixity -> Range

EmbPrj Fixity

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Fixity -> S Int32

icod_ :: Fixity -> S Int32

value :: Int32 -> R Fixity

ToTerm Fixity

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Fixity -> Term)

toTermR :: TCM (Fixity -> ReduceM Term)

noFixity :: Fixity

defaultFixity :: Fixity

data ParenPreference

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

Constructors

PreferParen

PreferParenless

Instances

Eq ParenPreference

Defined in Agda.Syntax.Fixity

Methods

(==) :: ParenPreference -> ParenPreference -> Bool

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

Data ParenPreference

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

Defined in Agda.Syntax.Fixity

Methods

compare :: ParenPreference -> ParenPreference -> Ordering

(<) :: ParenPreference -> ParenPreference -> Bool

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

(>) :: ParenPreference -> ParenPreference -> Bool

(>=) :: ParenPreference -> ParenPreference -> Bool

max :: ParenPreference -> ParenPreference -> ParenPreference

min :: ParenPreference -> ParenPreference -> ParenPreference

Show ParenPreference

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> ParenPreference -> ShowS

show :: ParenPreference -> String

showList :: [ParenPreference] -> ShowS

EmbPrj ParenPreference

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ParenPreference -> S Int32

icod_ :: ParenPreference -> S Int32

value :: Int32 -> R ParenPreference

preferParen :: ParenPreference -> Bool

preferParenless :: ParenPreference -> Bool

Precendence

data Precedence

Precedence is associated with a context.

Constructors

TopCtx

FunctionSpaceDomainCtx

LeftOperandCtx Fixity

RightOperandCtx Fixity ParenPreference

FunctionCtx

ArgumentCtx ParenPreference

InsideOperandCtx

WithFunCtx

WithArgCtx

DotPatternCtx

Instances

Eq Precedence

Defined in Agda.Syntax.Fixity

Methods

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

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

Data Precedence

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

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> Precedence -> ShowS

show :: Precedence -> String

showList :: [Precedence] -> ShowS

Pretty Precedence

Defined in Agda.Syntax.Fixity

Methods

pretty :: Precedence -> Doc

prettyPrec :: Int -> Precedence -> Doc

prettyList :: [Precedence] -> Doc

EmbPrj Precedence

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Precedence -> S Int32

icod_ :: Precedence -> S Int32

value :: Int32 -> R Precedence

type PrecedenceStack = [Precedence]

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`.

pushPrecedence :: Precedence -> PrecedenceStack -> PrecedenceStack

headPrecedence :: PrecedenceStack -> Precedence

argumentCtx_ :: Precedence

Argument context preferring parens.

opBrackets :: Fixity -> PrecedenceStack -> Bool

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

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

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

lamBrackets :: PrecedenceStack -> 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. 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

Does a function application need brackets?

appBrackets' :: Bool -> PrecedenceStack -> Bool

Does a function application need brackets?

withAppBrackets :: PrecedenceStack -> Bool

Does a with application need brackets?

piBrackets :: PrecedenceStack -> Bool

Does a function space need brackets?

roundFixBrackets :: PrecedenceStack -> Bool

Some lenses

_notaFixity :: Lens' Fixity NewNotation

_fixityAssoc :: Lens' Associativity Fixity

_fixityLevel :: Lens' PrecedenceLevel Fixity

Printing

NFData instances