Agda.Syntax.Fixity

Definitions for fixity, precedence levels, and declared syntax.

Documentation

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

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 :: forall r r'. (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)

LensFixity' (ThingWithFixity a)

Defined in Agda.Syntax.Fixity

Methods

lensFixity' :: Lens' Fixity' (ThingWithFixity a)

LensFixity (ThingWithFixity a)

Defined in Agda.Syntax.Fixity

Methods

lensFixity :: Lens' Fixity (ThingWithFixity a)

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 :: forall r r'. (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 :: forall r r'. (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