| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
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 position of an expression or the concrete syntax that an internal expression originates from.
Synopsis
- data MetaKind
- hidingToMetaKind :: Hiding -> MetaKind
- type MetaNameSuggestion = String
- data MetaInfo = MetaInfo {}
- emptyMetaInfo :: MetaInfo
- newtype ExprInfo = ExprRange Range
- exprNoRange :: ExprInfo
- data AppInfo = AppInfo {}
- defaultAppInfo :: Range -> AppInfo
- defaultAppInfo_ :: AppInfo
- data ModuleInfo = ModuleInfo {}
- newtype LetInfo = LetRange Range
- data DefInfo' t = DefInfo {}
- mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
- mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo' t
- data DeclInfo = DeclInfo {}
- data MutualInfo = MutualInfo {}
- data LHSInfo = LHSInfo {}
- newtype PatInfo = PatRange Range
- patNoRange :: PatInfo
- data ConPatInfo = ConPatInfo {}
- data ConPatLazy
Documentation
Kind of a meta: the method how to solve it.
Constructors
| InstanceMeta | Meta variable solved by instance search. |
| UnificationMeta | Meta variable solved by unification (default). |
type MetaNameSuggestion = String Source #
Name suggestion for meta variable. Empty string means no suggestion.
Information associated to a meta variable in the abstract syntax.
Constructors
| MetaInfo | |
Fields | |
Instances
Information about application
Constructors
| AppInfo | |
Instances
| LensOrigin AppInfo Source # | |
| HasRange AppInfo Source # | |
| KillRange AppInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| Generic AppInfo Source # | |
| Show AppInfo Source # | |
| NFData AppInfo Source # | |
Defined in Agda.Syntax.Info | |
| Eq AppInfo Source # | |
| Ord AppInfo Source # | |
| type Rep AppInfo Source # | |
Defined in Agda.Syntax.Info type Rep AppInfo = D1 ('MetaData "AppInfo" "Agda.Syntax.Info" "Agda-2.7.0-GLfwtYnpcYgL7izVkqfuSR" 'False) (C1 ('MetaCons "AppInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "appRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Just "appOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Origin) :*: S1 ('MetaSel ('Just "appParens") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference)))) | |
defaultAppInfo :: Range -> AppInfo Source #
Default is system inserted and prefer parens.
defaultAppInfo_ :: AppInfo Source #
AppInfo with no range information.
data ModuleInfo Source #
Constructors
| ModuleInfo | |
Fields
| |
Instances
Constructors
| DefInfo | |
Fields
| |
Instances
mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo' t Source #
Same as mkDefInfo but where we can also give the IsInstance
Instances
| HasRange DeclInfo Source # | |
| KillRange DeclInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| SetRange DeclInfo Source # | |
| Generic DeclInfo Source # | |
| Show DeclInfo Source # | |
| NFData DeclInfo Source # | |
Defined in Agda.Syntax.Info | |
| Eq DeclInfo Source # | |
| type Rep DeclInfo Source # | |
Defined in Agda.Syntax.Info type Rep DeclInfo = D1 ('MetaData "DeclInfo" "Agda.Syntax.Info" "Agda-2.7.0-GLfwtYnpcYgL7izVkqfuSR" 'False) (C1 ('MetaCons "DeclInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "declName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "declRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) | |
data MutualInfo Source #
Constructors
| MutualInfo | |
Instances
Constructors
| LHSInfo | |
Fields | |
Instances
| HasRange LHSInfo Source # | |
| KillRange LHSInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| Null LHSInfo Source # | |
| Generic LHSInfo Source # | |
| Show LHSInfo Source # | |
| NFData LHSInfo Source # | |
Defined in Agda.Syntax.Info | |
| Eq LHSInfo Source # | |
| type Rep LHSInfo Source # | |
Defined in Agda.Syntax.Info type Rep LHSInfo = D1 ('MetaData "LHSInfo" "Agda.Syntax.Info" "Agda-2.7.0-GLfwtYnpcYgL7izVkqfuSR" 'False) (C1 ('MetaCons "LHSInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "lhsEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis))) | |
For a general pattern we remember the source code position.
patNoRange :: PatInfo Source #
Empty range for patterns.
data ConPatInfo Source #
Constructor pattern info.
Constructors
| ConPatInfo | |
Fields
| |
Instances
data ConPatLazy Source #
Has the constructor pattern a dotted (forced) constructor?
Constructors
| ConPatLazy | Dotted constructor. |
| ConPatEager | Ordinary constructor. |