Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Fixity
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
- data Associativity
- data Fixity = Fixity {}
- noFixity :: Fixity
- defaultFixity :: 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
- _notaFixity :: Lens' Fixity NewNotation
- _fixityAssoc :: Lens' Associativity Fixity
- _fixityLevel :: Lens' PrecedenceLevel Fixity
Notation coupled with Fixity
The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.
Constructors
Fixity' | |
Fields
|
Instances
Eq Fixity' Source # | |
Data Fixity' Source # | |
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' 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' Source # | |
NFData Fixity' Source # | |
Defined in Agda.Syntax.Fixity | |
Pretty Fixity' Source # | |
KillRange Fixity' Source # | |
Defined in Agda.Syntax.Fixity Methods | |
EmbPrj Fixity' Source # | |
ToTerm Fixity' Source # | |
PrimTerm Fixity' Source # | |
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 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 :: (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 # |
data NewNotation Source #
All the notation information related to a name.
Constructors
NewNotation | |
Fields
|
Instances
Show NewNotation Source # | |
Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> NewNotation -> ShowS show :: NewNotation -> String showList :: [NewNotation] -> ShowS |
namesToNotation :: QName -> Name -> NewNotation Source #
If an operator has no specific notation, then it is computed from its name.
useDefaultFixity :: NewNotation -> NewNotation Source #
Replace noFixity
by defaultFixity
.
notationNames :: NewNotation -> [QName] Source #
Return the IdPart
s 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 Source #
Create a Notation
(without binders) from a concrete Name
.
Does the obvious thing:
Hole
s become NormalHole
s, Id
s become IdParts
.
If Name
has no Hole
s, it returns noNotation
.
mergeNotations :: [NewNotation] -> [NewNotation] Source #
Merges NewNotation
s 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 NewNotation
s 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 Source #
Sections, as well as non-sectioned operators.
Constructors
NotationSection | |
Fields
|
Instances
Show NotationSection Source # | |
Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> NotationSection -> ShowS show :: NotationSection -> String showList :: [NotationSection] -> ShowS |
noSection :: NewNotation -> NotationSection Source #
Converts a notation to a (non-)section.
Fixity
data PrecedenceLevel Source #
Precedence levels for operators.
Instances
data Associativity Source #
Associativity.
Constructors
NonAssoc | |
LeftAssoc | |
RightAssoc |
Instances
Eq Associativity Source # | |
Defined in Agda.Syntax.Fixity | |
Data Associativity Source # | |
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 Source # | |
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 Source # | |
Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> Associativity -> ShowS show :: Associativity -> String showList :: [Associativity] -> ShowS | |
EmbPrj Associativity Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Associativity -> S Int32 Source # icod_ :: Associativity -> S Int32 Source # value :: Int32 -> R Associativity Source # | |
ToTerm Associativity Source # | |
Defined in Agda.TypeChecking.Primitive |
Fixity of operators.
Constructors
Fixity | |
Fields
|
Instances
Eq Fixity Source # | |
Data Fixity Source # | |
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 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 Source # | |
Show Fixity Source # | |
NFData Fixity Source # | Ranges are not forced. |
Defined in Agda.Syntax.Fixity | |
Pretty Fixity Source # | |
KillRange Fixity Source # | |
Defined in Agda.Syntax.Fixity Methods | |
HasRange Fixity Source # | |
EmbPrj Fixity Source # | |
ToTerm Fixity 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 :: (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 :: (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 #