Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Fixity

Contents

Precendence

Description

Definitions for fixity, precedence levels, and declared syntax.

Synopsis

data ThingWithFixity x = ThingWithFixity x Fixity'
data ParenPreference
- = PreferParen
- | PreferParenless
preferParen :: ParenPreference -> Bool
preferParenless :: ParenPreference -> Bool
data Precedence
- = TopCtx
- | FunctionSpaceDomainCtx
- | LeftOperandCtx Fixity
- | RightOperandCtx Fixity ParenPreference
- | FunctionCtx
- | ArgumentCtx ParenPreference
- | InsideOperandCtx
- | WithFunCtx
- | WithArgCtx
- | DotPatternCtx
type PrecedenceStack = [Precedence]
pushPrecedence :: Precedence -> PrecedenceStack -> PrecedenceStack
headPrecedence :: PrecedenceStack -> Precedence
argumentCtx_ :: Precedence
opBrackets :: Fixity -> PrecedenceStack -> Bool
opBrackets' :: Bool -> Fixity -> PrecedenceStack -> Bool
lamBrackets :: PrecedenceStack -> Bool
appBrackets :: PrecedenceStack -> Bool
appBrackets' :: Bool -> PrecedenceStack -> Bool
withAppBrackets :: PrecedenceStack -> Bool
piBrackets :: PrecedenceStack -> Bool
roundFixBrackets :: PrecedenceStack -> Bool

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 Methods pretty :: ThingWithFixity Name -> Doc Source # prettyPrec :: Int -> ThingWithFixity Name -> Doc Source # prettyList :: [ThingWithFixity Name] -> Doc Source #
KillRange x => KillRange (ThingWithFixity x) Source #
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) Source #
LensFixity' (ThingWithFixity a) Source #
Instance details Defined in Agda.Syntax.Fixity Methods lensFixity' :: Lens' Fixity' (ThingWithFixity a) Source #
LensFixity (ThingWithFixity a) Source #
Instance details Defined in Agda.Syntax.Fixity Methods lensFixity :: Lens' Fixity (ThingWithFixity a) Source #

data ParenPreference Source #

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

Constructors

PreferParen
PreferParenless

Instances

Instances details

Eq ParenPreference Source #
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: ParenPreference -> ParenPreference -> Bool # (/=) :: ParenPreference -> ParenPreference -> Bool #
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 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 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 Methods icode :: ParenPreference -> S Int32 Source # icod_ :: ParenPreference -> S Int32 Source # value :: Int32 -> R ParenPreference Source #

preferParen :: ParenPreference -> Bool Source #

preferParenless :: ParenPreference -> Bool Source #

Precendence

data Precedence Source #

Precedence is associated with a context.

Constructors

TopCtx
FunctionSpaceDomainCtx
LeftOperandCtx Fixity
RightOperandCtx Fixity ParenPreference
FunctionCtx
ArgumentCtx ParenPreference
InsideOperandCtx
WithFunCtx
WithArgCtx
DotPatternCtx

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 Methods pretty :: Precedence -> Doc Source # prettyPrec :: Int -> Precedence -> Doc Source # prettyList :: [Precedence] -> Doc Source #
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`.

pushPrecedence :: Precedence -> PrecedenceStack -> PrecedenceStack Source #

headPrecedence :: PrecedenceStack -> Precedence Source #

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?

roundFixBrackets :: PrecedenceStack -> Bool Source #