Agda.Syntax.Fixity

Definitions for fixity, precedence levels, and declared syntax.

Documentation

data ThingWithFixity x

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances

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)

Functor ThingWithFixity

Defined in Agda.Syntax.Fixity

Methods

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

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

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)

KillRange x => KillRange (ThingWithFixity x)

Defined in Agda.Syntax.Fixity

Methods

killRange :: KillRangeT (ThingWithFixity x)

Pretty (ThingWithFixity Name)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ThingWithFixity Name -> Doc

prettyPrec :: Int -> ThingWithFixity Name -> Doc

prettyList :: [ThingWithFixity Name] -> Doc

Show x => Show (ThingWithFixity x)

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> ThingWithFixity x -> ShowS

show :: ThingWithFixity x -> String

showList :: [ThingWithFixity x] -> ShowS

data ParenPreference

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

Constructors

PreferParen

PreferParenless

Instances

EmbPrj ParenPreference

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ParenPreference -> S Int32

icod_ :: ParenPreference -> S Int32

value :: Int32 -> R ParenPreference

Generic ParenPreference

Defined in Agda.Syntax.Fixity

Associated Types

type Rep ParenPreference :: Type -> Type

Methods

from :: ParenPreference -> Rep ParenPreference x

to :: Rep ParenPreference x -> ParenPreference

Show ParenPreference

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> ParenPreference -> ShowS

show :: ParenPreference -> String

showList :: [ParenPreference] -> ShowS

NFData ParenPreference

Defined in Agda.Syntax.Fixity

Methods

rnf :: ParenPreference -> ()

Eq ParenPreference

Defined in Agda.Syntax.Fixity

Methods

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

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

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

type Rep ParenPreference

Defined in Agda.Syntax.Fixity

type Rep ParenPreference = D1 ('MetaData "ParenPreference" "Agda.Syntax.Fixity" "Agda-2.6.2.2.20230105-inplace" 'False) (C1 ('MetaCons "PreferParen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PreferParenless" 'PrefixI 'False) (U1 :: Type -> Type))

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

EmbPrj Precedence

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Precedence -> S Int32

icod_ :: Precedence -> S Int32

value :: Int32 -> R Precedence

Pretty Precedence

Defined in Agda.Syntax.Fixity

Methods

pretty :: Precedence -> Doc

prettyPrec :: Int -> Precedence -> Doc

prettyList :: [Precedence] -> Doc

Generic Precedence

Defined in Agda.Syntax.Fixity

Associated Types

type Rep Precedence :: Type -> Type

Methods

from :: Precedence -> Rep Precedence x

to :: Rep Precedence x -> Precedence

Show Precedence

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> Precedence -> ShowS

show :: Precedence -> String

showList :: [Precedence] -> ShowS

NFData Precedence

Defined in Agda.Syntax.Fixity

Methods

rnf :: Precedence -> ()

Eq Precedence

Defined in Agda.Syntax.Fixity

Methods

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

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

type Rep Precedence

Defined in Agda.Syntax.Fixity

type Rep Precedence = D1 ('MetaData "Precedence" "Agda.Syntax.Fixity" "Agda-2.6.2.2.20230105-inplace" 'False) (((C1 ('MetaCons "TopCtx" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FunctionSpaceDomainCtx" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LeftOperandCtx" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity)) :+: (C1 ('MetaCons "RightOperandCtx" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference)) :+: C1 ('MetaCons "FunctionCtx" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "ArgumentCtx" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference)) :+: C1 ('MetaCons "InsideOperandCtx" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WithFunCtx" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithArgCtx" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DotPatternCtx" 'PrefixI 'False) (U1 :: Type -> Type)))))

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