Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Fixity
Contents
Description
Definitions for fixity, precedence levels, and declared syntax.
Synopsis
- data ThingWithFixity x = ThingWithFixity x Fixity'
- data ParenPreference
- preferParen :: ParenPreference -> Bool
- preferParenless :: ParenPreference -> Bool
- data Precedence
- 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
Functor ThingWithFixity Source # | |
Defined in Agda.Syntax.Fixity Methods fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b (<$) :: a -> ThingWithFixity b -> ThingWithFixity a # | |
Foldable ThingWithFixity Source # | |
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 # | |
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 # | |
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 # | |
Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ThingWithFixity x -> ShowS show :: ThingWithFixity x -> String showList :: [ThingWithFixity x] -> ShowS | |
Pretty (ThingWithFixity Name) Source # | |
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 # | |
Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) Source # | |
LensFixity' (ThingWithFixity a) Source # | |
Defined in Agda.Syntax.Fixity Methods lensFixity' :: Lens' Fixity' (ThingWithFixity a) Source # | |
LensFixity (ThingWithFixity a) Source # | |
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
Eq ParenPreference Source # | |
Defined in Agda.Syntax.Fixity Methods (==) :: ParenPreference -> ParenPreference -> Bool (/=) :: ParenPreference -> ParenPreference -> Bool | |
Data ParenPreference Source # | |
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 # | |
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 # | |
Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ParenPreference -> ShowS show :: ParenPreference -> String showList :: [ParenPreference] -> ShowS | |
EmbPrj ParenPreference Source # | |
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
Eq Precedence Source # | |
Defined in Agda.Syntax.Fixity | |
Data Precedence Source # | |
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 # | |
Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> Precedence -> ShowS show :: Precedence -> String showList :: [Precedence] -> ShowS | |
Pretty Precedence Source # | |
Defined in Agda.Syntax.Fixity Methods pretty :: Precedence -> Doc Source # prettyPrec :: Int -> Precedence -> Doc Source # prettyList :: [Precedence] -> Doc Source # | |
EmbPrj Precedence Source # | |
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?
roundFixBrackets :: PrecedenceStack -> Bool Source #