Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

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
  - metaNameSuggestion :: String
  }
- emptyMetaInfo :: MetaInfo
- 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
  }
- data MutualInfo = MutualInfo {
  - mutualTermCheck :: Bool
  - mutualRange :: Range
  }
- newtype LHSInfo = LHSRange Range
- data PatInfo
  - = PatRange Range
  - | PatSource Range (Precedence -> Pattern)

# Documentation

data Info

Constructors

Nope |

data MetaInfo

Constructors

MetaInfo |
Fields metaRange :: Range metaScope :: ScopeInfo metaNumber :: Maybe Nat metaNameSuggestion :: String

Instances

Show MetaInfo |
Typeable MetaInfo |
KillRange MetaInfo |
HasRange MetaInfo |

emptyMetaInfo :: MetaInfo

data ExprInfo

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

Show ExprInfo |
Typeable ExprInfo |
KillRange ExprInfo |
HasRange ExprInfo |

data ModuleInfo

Constructors

ModuleInfo |
Fields minfoRange :: Range minfoAsTo :: Range minfoAsName :: Maybe Name minfoOpenShort :: Maybe OpenShortHand minfoDirective :: Maybe ImportDirective

Instances

(Show OpenShortHand, Show ImportDirective) => Show ModuleInfo |
Typeable ModuleInfo |
KillRange ModuleInfo |
SetRange ModuleInfo |
HasRange ModuleInfo |
UniverseBi Declaration ModuleInfo |

newtype LetInfo

Constructors

LetRange Range |

Instances

Show LetInfo |
Typeable LetInfo |
KillRange LetInfo |
HasRange LetInfo |

data DefInfo

Constructors

DefInfo |
Fields defFixity :: Fixity' defAccess :: Access defAbstract :: IsAbstract defInfo :: DeclInfo

Instances

Show DefInfo |
Typeable DefInfo |
KillRange DefInfo |
SetRange DefInfo |
HasRange DefInfo |

mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo

data DeclInfo

Constructors

DeclInfo |
Fields declName :: Name declRange :: Range

Instances

Show DeclInfo |
Typeable DeclInfo |
KillRange DeclInfo |
SetRange DeclInfo |
HasRange DeclInfo |

data MutualInfo

Constructors

MutualInfo |
Fields mutualTermCheck :: Bool termination check (default=True) mutualRange :: Range

Instances

Show MutualInfo |
Typeable MutualInfo |
KillRange MutualInfo |
HasRange MutualInfo |

newtype LHSInfo

Constructors

LHSRange Range |

Instances

Show LHSInfo |
Typeable LHSInfo |
KillRange LHSInfo |
HasRange LHSInfo |

data PatInfo

Constructors

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

Instances

Show PatInfo |
Typeable PatInfo |
KillRange PatInfo |
HasRange PatInfo |