Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Info
Description
An info object contains additional information about a piece of abstract syntax that isn't part of the actual syntax. For instance, it might contain the source code posisiton of an expression or the concrete syntax that an internal expression originates from.
Synopsis
data Info = Nope
data MetaInfo = MetaInfo {
metaRange :: Range
metaScope :: ScopeInfo
metaNumber :: Maybe Nat
}
data ExprInfo
= ExprRange Range
| ExprSource Range (Precedence -> Expr)
data ModuleInfo = ModuleInfo {
minfoRange :: Range
minfoAsTo :: Range
minfoAsName :: Maybe Name
}
newtype LetInfo = LetRange Range
data DefInfo = DefInfo {
defFixity :: Fixity
defAccess :: Access
defAbstract :: IsAbstract
defInfo :: DeclInfo
}
mkDefInfo :: Name -> Fixity -> Access -> IsAbstract -> Range -> DefInfo
data DeclInfo = DeclInfo {
declName :: Name
declRange :: Range
}
newtype LHSInfo = LHSRange Range
data PatInfo
= PatRange Range
| PatSource Range (Precedence -> Pattern)
Documentation
data Info Source
Constructors
Nope
data MetaInfo Source
Constructors
MetaInfo
metaRange :: Range
metaScope :: ScopeInfo
metaNumber :: Maybe Nat
show/hide Instances
data ExprInfo Source
For a general expression we can either remember just the source code position or the entire concrete expression it came from.
Constructors
ExprRange Range
ExprSource Range (Precedence -> Expr)Even if we store the original expression we have to know whether to put parenthesis around it.
show/hide Instances
data ModuleInfo Source
Constructors
ModuleInfo
minfoRange :: Range
minfoAsTo :: Range
minfoAsName :: Maybe Name
show/hide Instances
newtype LetInfo Source
Constructors
LetRange Range
show/hide Instances
data DefInfo Source
Constructors
DefInfo
defFixity :: Fixity
defAccess :: Access
defAbstract :: IsAbstract
defInfo :: DeclInfo
show/hide Instances
mkDefInfo :: Name -> Fixity -> Access -> IsAbstract -> Range -> DefInfoSource
data DeclInfo Source
Constructors
DeclInfo
declName :: Name
declRange :: Range
show/hide Instances
newtype LHSInfo Source
Constructors
LHSRange Range
show/hide Instances
data PatInfo Source
Constructors
PatRange Range
PatSource Range (Precedence -> Pattern)
show/hide Instances
Produced by Haddock version 2.4.2