Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
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

Foldable ThingWithFixity Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

fold :: Monoid m => ThingWithFixity m -> m Source #

foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> m Source #

foldMap' :: Monoid m => (a -> m) -> ThingWithFixity a -> m Source #

foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b Source #

foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b Source #

foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b Source #

foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b Source #

foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a Source #

foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a Source #

toList :: ThingWithFixity a -> [a] Source #

null :: ThingWithFixity a -> Bool Source #

length :: ThingWithFixity a -> Int Source #

elem :: Eq a => a -> ThingWithFixity a -> Bool Source #

maximum :: Ord a => ThingWithFixity a -> a Source #

minimum :: Ord a => ThingWithFixity a -> a Source #

sum :: Num a => ThingWithFixity a -> a Source #

product :: Num a => ThingWithFixity a -> a Source #

Traversable ThingWithFixity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods traverse :: Applicative f => (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b) Source # sequenceA :: Applicative f => ThingWithFixity (f a) -> f (ThingWithFixity a) Source # mapM :: Monad m => (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b) Source # sequence :: Monad m => ThingWithFixity (m a) -> m (ThingWithFixity a) Source #
Functor ThingWithFixity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b Source # (<$) :: a -> ThingWithFixity b -> ThingWithFixity a 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 #
KillRange x => KillRange (ThingWithFixity x) Source # |
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) Source #
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 #
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) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x) Source #

toConstr :: ThingWithFixity x -> Constr Source #

dataTypeOf :: ThingWithFixity x -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ThingWithFixity x)) Source #

gmapT :: (forall b. Data b => b -> b) -> ThingWithFixity x -> ThingWithFixity x Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ThingWithFixity x -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) Source #

Show x => Show (ThingWithFixity x) Source # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ThingWithFixity x -> ShowS Source # show :: ThingWithFixity x -> String Source # showList :: [ThingWithFixity x] -> ShowS Source #

data ParenPreference Source #

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

Constructors

PreferParen |
PreferParenless |

#### Instances

Instances details

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 #
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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ParenPreference Source #

toConstr :: ParenPreference -> Constr Source #

dataTypeOf :: ParenPreference -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ParenPreference) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ParenPreference) Source #

gmapT :: (forall b. Data b => b -> b) -> ParenPreference -> ParenPreference Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ParenPreference -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ParenPreference -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ParenPreference -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ParenPreference -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ParenPreference -> m ParenPreference Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ParenPreference -> m ParenPreference Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ParenPreference -> m ParenPreference Source #

Generic ParenPreference Source # |
Instance details Defined in Agda.Syntax.Fixity Associated Types type Rep ParenPreference :: Type -> Type Source # Methods from :: ParenPreference -> Rep ParenPreference x Source # to :: Rep ParenPreference x -> ParenPreference Source #
Show ParenPreference Source # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ParenPreference -> ShowS Source # show :: ParenPreference -> String Source # showList :: [ParenPreference] -> ShowS Source #
NFData ParenPreference Source # |
Instance details Defined in Agda.Syntax.Fixity Methods rnf :: ParenPreference -> () Source #
Eq ParenPreference Source # |
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: ParenPreference -> ParenPreference -> Bool Source # (/=) :: ParenPreference -> ParenPreference -> Bool Source #
Ord ParenPreference Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

compare :: ParenPreference -> ParenPreference -> Ordering Source #

(<) :: ParenPreference -> ParenPreference -> Bool Source #

(<=) :: ParenPreference -> ParenPreference -> Bool Source #

(>) :: ParenPreference -> ParenPreference -> Bool Source #

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

max :: ParenPreference -> ParenPreference -> ParenPreference Source #

min :: ParenPreference -> ParenPreference -> ParenPreference Source #

type Rep ParenPreference Source # |
Instance details Defined in Agda.Syntax.Fixity type Rep ParenPreference = D1 ('MetaData "ParenPreference" "Agda.Syntax.Fixity" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "PreferParen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PreferParenless" 'PrefixI 'False) (U1 :: Type -> Type))

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

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 #
Pretty Precedence Source # |
Instance details Defined in Agda.Syntax.Fixity Methods pretty :: Precedence -> Doc Source # prettyPrec :: Int -> Precedence -> Doc Source # prettyList :: [Precedence] -> Doc Source #
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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Precedence Source #

toConstr :: Precedence -> Constr Source #

dataTypeOf :: Precedence -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Precedence) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Precedence) Source #

gmapT :: (forall b. Data b => b -> b) -> Precedence -> Precedence Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Precedence -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Precedence -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Precedence -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Precedence -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Precedence -> m Precedence Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Precedence -> m Precedence Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Precedence -> m Precedence Source #

Generic Precedence Source # |
Instance details Defined in Agda.Syntax.Fixity Associated Types type Rep Precedence :: Type -> Type Source # Methods from :: Precedence -> Rep Precedence x Source # to :: Rep Precedence x -> Precedence Source #
Show Precedence Source # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> Precedence -> ShowS Source # show :: Precedence -> String Source # showList :: [Precedence] -> ShowS Source #
NFData Precedence Source # |
Instance details Defined in Agda.Syntax.Fixity Methods rnf :: Precedence -> () Source #
Eq Precedence Source # |
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: Precedence -> Precedence -> Bool Source # (/=) :: Precedence -> Precedence -> Bool Source #
type Rep Precedence Source # |

Instance details

Defined in Agda.Syntax.Fixity

type Rep Precedence = D1 ('MetaData "Precedence" "Agda.Syntax.Fixity" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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] 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 #