Agda-2.6.1: 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

Documentation

data ThingWithFixity x Source #

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity' 

Instances

Instances details
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

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

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> ThingWithFixity x -> ShowS

show :: ThingWithFixity x -> String

showList :: [ThingWithFixity x] -> ShowS

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

LensFixity' (ThingWithFixity a) Source # 
Instance details

Defined in Agda.Syntax.Fixity

LensFixity (ThingWithFixity a) Source # 
Instance details

Defined in Agda.Syntax.Fixity

data ParenPreference Source #

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

Instances

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

Defined in Agda.Syntax.Fixity

Show ParenPreference Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> ParenPreference -> ShowS

show :: ParenPreference -> String

showList :: [ParenPreference] -> ShowS

EmbPrj ParenPreference Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Precendence

data Precedence Source #

Precedence is associated with a context.

Instances

Instances details
Eq Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

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

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

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

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> Precedence -> ShowS

show :: Precedence -> String

showList :: [Precedence] -> ShowS

Pretty Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

EmbPrj Precedence Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Precedence -> S Int32 Source #

icod_ :: Precedence -> S Int32 Source #

value :: Int32 -> R Precedence Source #

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?