Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Fixity

Contents

Notation coupled with Fixity
Sections
Fixity
Precendence
Some lenses
Printing
NFData instances

Description

Definitions for fixity, precedence levels, and declared syntax.

Synopsis

data Fixity' = Fixity' {
- theFixity :: !Fixity
- theNotation :: Notation
- theNameRange :: Range
}
data ThingWithFixity x = ThingWithFixity x Fixity'
data NewNotation = NewNotation {
- notaName :: QName
- notaNames :: Set Name
- notaFixity :: Fixity
- notation :: Notation
- notaIsOperator :: Bool
}
namesToNotation :: QName -> Name -> NewNotation
useDefaultFixity :: NewNotation -> NewNotation
notationNames :: NewNotation -> [QName]
syntaxOf :: Name -> Notation
noFixity' :: Fixity'
mergeNotations :: [NewNotation] -> [NewNotation]
data NotationSection = NotationSection {
- sectNotation :: NewNotation
- sectKind :: NotationKind
- sectLevel :: Maybe PrecedenceLevel
- sectIsSection :: Bool
}
noSection :: NewNotation -> NotationSection
data PrecedenceLevel
- = Unrelated
- | Related !Integer
data Associativity
- = NonAssoc
- | LeftAssoc
- | RightAssoc
data Fixity = Fixity {
- fixityRange :: Range
- fixityLevel :: !PrecedenceLevel
- fixityAssoc :: !Associativity
}
noFixity :: Fixity
defaultFixity :: 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
_notaFixity :: Lens' Fixity NewNotation
_fixityAssoc :: Lens' Associativity Fixity
_fixityLevel :: Lens' PrecedenceLevel Fixity

Notation coupled with `Fixity`

data Fixity' #

The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.

Constructors

Fixity'
Fields theFixity :: !Fixity theNotation :: Notation theNameRange :: Range Range of the name in the fixity declaration (used for correct highlighting, see issue #2140).

Instances

Eq Fixity' #
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: Fixity' -> Fixity' -> Bool # (/=) :: Fixity' -> Fixity' -> Bool #
Data Fixity' #
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) -> Fixity' -> c Fixity' # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity' # toConstr :: Fixity' -> Constr # dataTypeOf :: Fixity' -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity') # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity') # gmapT :: (forall b. Data b => b -> b) -> Fixity' -> Fixity' # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r # gmapQ :: (forall d. Data d => d -> u) -> Fixity' -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity' -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' #
Show Fixity' #
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> Fixity' -> ShowS # show :: Fixity' -> String # showList :: [Fixity'] -> ShowS #
NFData Fixity' #
Instance details Defined in Agda.Syntax.Fixity Methods rnf :: Fixity' -> () #
Pretty Fixity' #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Fixity' -> Doc # prettyPrec :: Int -> Fixity' -> Doc # prettyList :: [Fixity'] -> Doc #
KillRange Fixity' #
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT Fixity' #
EmbPrj Fixity' #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity' -> S Int32 # icod_ :: Fixity' -> S Int32 # value :: Int32 -> R Fixity' #
ToTerm Fixity' #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Fixity' -> Term) # toTermR :: TCM (Fixity' -> ReduceM Term) #
PrimTerm Fixity' #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Fixity' -> TCM Term #

data ThingWithFixity x #

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances

Functor ThingWithFixity #
Instance details Defined in Agda.Syntax.Fixity Methods fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b # (<$) :: a -> ThingWithFixity b -> ThingWithFixity a #
Foldable ThingWithFixity #
Instance details Defined in Agda.Syntax.Fixity Methods fold :: Monoid m => ThingWithFixity m -> 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 #
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) #
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 :: (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) #
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ThingWithFixity x -> ShowS # show :: ThingWithFixity x -> String # showList :: [ThingWithFixity x] -> ShowS #
Pretty (ThingWithFixity Name) #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ThingWithFixity Name -> Doc # prettyPrec :: Int -> ThingWithFixity Name -> Doc # prettyList :: [ThingWithFixity Name] -> Doc #
KillRange x => KillRange (ThingWithFixity x) #
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) #

data NewNotation #

All the notation information related to a name.

Constructors

NewNotation

Fields

notaName :: QName
notaNames :: Set Name
The names the syntax and/or fixity belong to.
Invariant: The set is non-empty. Every name in the list matches notaName.
notaFixity :: Fixity
Associativity and precedence (fixity) of the names.
notation :: Notation
Syntax associated with the names.
notaIsOperator :: Bool
True if the notation comes from an operator (rather than a syntax declaration).

Instances

Show NewNotation #
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> NewNotation -> ShowS # show :: NewNotation -> String # showList :: [NewNotation] -> ShowS #

namesToNotation :: QName -> Name -> NewNotation #

If an operator has no specific notation, then it is computed from its name.

useDefaultFixity :: NewNotation -> NewNotation #

Replace noFixity by defaultFixity.

notationNames :: NewNotation -> [QName] #

Return the IdParts of a notation, the first part qualified, the other parts unqualified. This allows for qualified use of operators, e.g., M.for x ∈ xs return e, or x ℕ.+ y.

syntaxOf :: Name -> Notation #

Create a Notation (without binders) from a concrete Name. Does the obvious thing: Holes become NormalHoles, Ids become IdParts. If Name has no Holes, it returns noNotation.

noFixity' :: Fixity' #

mergeNotations :: [NewNotation] -> [NewNotation] #

Merges NewNotations that have the same precedence level and notation, with two exceptions:

Operators and notations coming from syntax declarations are kept separate.
If all instances of a given NewNotation have the same precedence level or are "unrelated", then they are merged. They get the given precedence level, if any, and otherwise they become unrelated (but related to each other).

If NewNotations that are merged have distinct associativities, then they get NonAssoc as their associativity.

Precondition: No Name may occur in more than one list element. Every NewNotation must have the same notaName.

Postcondition: No Name occurs in more than one list element.

Sections

data NotationSection #

Sections, as well as non-sectioned operators.

Constructors

NotationSection
Fields sectNotation :: NewNotation sectKind :: NotationKind For non-sectioned operators this should match the notation's `notationKind`. sectLevel :: Maybe PrecedenceLevel Effective precedence level. `Nothing` for closed notations. sectIsSection :: Bool `False` for non-sectioned operators.

Instances

Show NotationSection #
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> NotationSection -> ShowS # show :: NotationSection -> String # showList :: [NotationSection] -> ShowS #

noSection :: NewNotation -> NotationSection #

Converts a notation to a (non-)section.

Fixity

data PrecedenceLevel #

Precedence levels for operators.

Constructors

Unrelated	No fixity declared.
Related !Integer	Fixity level declared as the `Integer`.

Instances

Eq PrecedenceLevel #
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: PrecedenceLevel -> PrecedenceLevel -> Bool # (/=) :: PrecedenceLevel -> PrecedenceLevel -> Bool #
Data PrecedenceLevel #
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) -> PrecedenceLevel -> c PrecedenceLevel # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PrecedenceLevel # toConstr :: PrecedenceLevel -> Constr # dataTypeOf :: PrecedenceLevel -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PrecedenceLevel) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PrecedenceLevel) # gmapT :: (forall b. Data b => b -> b) -> PrecedenceLevel -> PrecedenceLevel # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PrecedenceLevel -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PrecedenceLevel -> r # gmapQ :: (forall d. Data d => d -> u) -> PrecedenceLevel -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PrecedenceLevel -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PrecedenceLevel -> m PrecedenceLevel # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PrecedenceLevel -> m PrecedenceLevel # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PrecedenceLevel -> m PrecedenceLevel #
Ord PrecedenceLevel #
Instance details Defined in Agda.Syntax.Fixity Methods compare :: PrecedenceLevel -> PrecedenceLevel -> Ordering # (<) :: PrecedenceLevel -> PrecedenceLevel -> Bool # (<=) :: PrecedenceLevel -> PrecedenceLevel -> Bool # (>) :: PrecedenceLevel -> PrecedenceLevel -> Bool # (>=) :: PrecedenceLevel -> PrecedenceLevel -> Bool # max :: PrecedenceLevel -> PrecedenceLevel -> PrecedenceLevel # min :: PrecedenceLevel -> PrecedenceLevel -> PrecedenceLevel #
Show PrecedenceLevel #
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> PrecedenceLevel -> ShowS # show :: PrecedenceLevel -> String # showList :: [PrecedenceLevel] -> ShowS #
EmbPrj PrecedenceLevel #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: PrecedenceLevel -> S Int32 # icod_ :: PrecedenceLevel -> S Int32 # value :: Int32 -> R PrecedenceLevel #
ToTerm PrecedenceLevel #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (PrecedenceLevel -> Term) # toTermR :: TCM (PrecedenceLevel -> ReduceM Term) #

data Associativity #

Associativity.

Constructors

NonAssoc
LeftAssoc
RightAssoc

Instances

Eq Associativity #
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: Associativity -> Associativity -> Bool # (/=) :: Associativity -> Associativity -> Bool #
Data Associativity #
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) -> Associativity -> c Associativity # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Associativity # toConstr :: Associativity -> Constr # dataTypeOf :: Associativity -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Associativity) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Associativity) # gmapT :: (forall b. Data b => b -> b) -> Associativity -> Associativity # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r # gmapQ :: (forall d. Data d => d -> u) -> Associativity -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Associativity -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity #
Ord Associativity #
Instance details Defined in Agda.Syntax.Fixity Methods compare :: Associativity -> Associativity -> Ordering # (<) :: Associativity -> Associativity -> Bool # (<=) :: Associativity -> Associativity -> Bool # (>) :: Associativity -> Associativity -> Bool # (>=) :: Associativity -> Associativity -> Bool # max :: Associativity -> Associativity -> Associativity # min :: Associativity -> Associativity -> Associativity #
Show Associativity #
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> Associativity -> ShowS # show :: Associativity -> String # showList :: [Associativity] -> ShowS #
EmbPrj Associativity #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Associativity -> S Int32 # icod_ :: Associativity -> S Int32 # value :: Int32 -> R Associativity #
ToTerm Associativity #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Associativity -> Term) # toTermR :: TCM (Associativity -> ReduceM Term) #

data Fixity #

Fixity of operators.

Constructors

Fixity
Fields fixityRange :: Range Range of the whole fixity declaration. fixityLevel :: !PrecedenceLevel fixityAssoc :: !Associativity

Instances

Eq Fixity #
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: Fixity -> Fixity -> Bool # (/=) :: Fixity -> Fixity -> Bool #
Data Fixity #
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) -> Fixity -> c Fixity # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity # toConstr :: Fixity -> Constr # dataTypeOf :: Fixity -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity) # gmapT :: (forall b. Data b => b -> b) -> Fixity -> Fixity # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r # gmapQ :: (forall d. Data d => d -> u) -> Fixity -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity #
Ord Fixity #
Instance details Defined in Agda.Syntax.Fixity Methods compare :: Fixity -> Fixity -> Ordering # (<) :: Fixity -> Fixity -> Bool # (<=) :: Fixity -> Fixity -> Bool # (>) :: Fixity -> Fixity -> Bool # (>=) :: Fixity -> Fixity -> Bool # max :: Fixity -> Fixity -> Fixity # min :: Fixity -> Fixity -> Fixity #
Show Fixity #
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> Fixity -> ShowS # show :: Fixity -> String # showList :: [Fixity] -> ShowS #
NFData Fixity #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Fixity Methods rnf :: Fixity -> () #
Pretty Fixity #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Fixity -> Doc # prettyPrec :: Int -> Fixity -> Doc # prettyList :: [Fixity] -> Doc #
KillRange Fixity #
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT Fixity #
HasRange Fixity #
Instance details Defined in Agda.Syntax.Fixity Methods getRange :: Fixity -> Range #
EmbPrj Fixity #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity -> S Int32 # icod_ :: Fixity -> S Int32 # value :: Int32 -> R Fixity #
ToTerm Fixity #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Fixity -> Term) # toTermR :: TCM (Fixity -> ReduceM Term) #

noFixity :: Fixity #

defaultFixity :: Fixity #

data ParenPreference #

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

Constructors

PreferParen
PreferParenless

Instances

Eq ParenPreference #
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: ParenPreference -> ParenPreference -> Bool # (/=) :: ParenPreference -> ParenPreference -> Bool #
Data ParenPreference #
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 :: (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 #
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 #
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ParenPreference -> ShowS # show :: ParenPreference -> String # showList :: [ParenPreference] -> ShowS #
EmbPrj ParenPreference #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ParenPreference -> S Int32 # icod_ :: ParenPreference -> S Int32 # value :: Int32 -> R ParenPreference #

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

Eq Precedence #
Instance details Defined in Agda.Syntax.Fixity Methods (==) :: Precedence -> Precedence -> Bool # (/=) :: Precedence -> Precedence -> Bool #
Data Precedence #
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 :: (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 #
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> Precedence -> ShowS # show :: Precedence -> String # showList :: [Precedence] -> ShowS #
Pretty Precedence #
Instance details Defined in Agda.Syntax.Fixity Methods pretty :: Precedence -> Doc # prettyPrec :: Int -> Precedence -> Doc # prettyList :: [Precedence] -> Doc #
EmbPrj Precedence #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Precedence -> S Int32 # icod_ :: Precedence -> S Int32 # value :: Int32 -> R Precedence #

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 #