Agda-2.2.10: 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
minfoOpenShort :: Maybe OpenShortHand
minfoDirective :: Maybe ImportDirective
}
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
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.
data ModuleInfo Source
Constructors
ModuleInfo
minfoRange :: Range
minfoAsTo :: Range
minfoAsName :: Maybe Name
minfoOpenShort :: Maybe OpenShortHand
minfoDirective :: Maybe ImportDirective
newtype LetInfo Source
Constructors
LetRange Range
data DefInfo Source
Constructors
DefInfo
defFixity :: Fixity'
defAccess :: Access
defAbstract :: IsAbstract
defInfo :: DeclInfo
mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfoSource
data DeclInfo Source
Constructors
DeclInfo
declName :: Name
declRange :: Range
newtype LHSInfo Source
Constructors
LHSRange Range
data PatInfo Source
Constructors
PatRange Range
PatSource Range (Precedence -> Pattern)
Produced by Haddock version 2.6.1