| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 |

Instances

Data MetaInfo
Show MetaInfo
Typeable MetaInfo
KillRange MetaInfo
HasRange MetaInfo

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.

Instances

Data ExprInfo
Show ExprInfo
Typeable ExprInfo
KillRange ExprInfo
HasRange ExprInfo

data ModuleInfo | Source

Constructors

ModuleInfo |

minfoRange :: Range |
minfoAsTo :: Range |
minfoAsName :: Maybe Name |

Instances

Data ModuleInfo
Show ModuleInfo
Typeable ModuleInfo
KillRange ModuleInfo
HasRange ModuleInfo

newtype LetInfo | Source

Constructors

LetRange Range |

Instances

Data LetInfo
Show LetInfo
Typeable LetInfo
KillRange LetInfo
HasRange LetInfo

data DefInfo | Source

Constructors

DefInfo |

defFixity :: Fixity |
defAccess :: Access |
defAbstract :: IsAbstract |
defInfo :: DeclInfo |

Instances

Data DefInfo
Show DefInfo
Typeable DefInfo
KillRange DefInfo
HasRange DefInfo

mkDefInfo :: Name -> Fixity -> Access -> IsAbstract -> Range -> DefInfo | Source

data DeclInfo | Source

Constructors

DeclInfo |

declName :: Name |
declRange :: Range |

Instances

Eq DeclInfo
Data DeclInfo
Show DeclInfo
Typeable DeclInfo
KillRange DeclInfo
HasRange DeclInfo

newtype LHSInfo | Source

Constructors

LHSRange Range |

Instances

Data LHSInfo
Show LHSInfo
Typeable LHSInfo
KillRange LHSInfo
HasRange LHSInfo

data PatInfo | Source

Constructors

PatRange Range |
PatSource Range (Precedence -> Pattern) |

Instances

Data PatInfo
Show PatInfo
Typeable PatInfo
KillRange PatInfo
HasRange PatInfo

Produced by Haddock version 2.4.2