ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Info

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
value hidingToMetaKind
type MetaNameSuggestion
data MetaInfo
value emptyMetaInfo
newtype ExprInfo
value exprNoRange
data AppInfo
value defaultAppInfo
value defaultAppInfo_
data ModuleInfo
newtype LetInfo
data DefInfo'
value mkDefInfo
value mkDefInfoInstance
data DeclInfo
data MutualInfo
data LHSInfo
newtype PatInfo
value patNoRange
data ConPatInfo
data ConPatLazy

PackageAgda-2.8.0.2
Exports22
LanguageHaskell2010
LicenceMIT
SourceInfo.hs

datadata MetaKind

Source#

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).

Instances6Eq, Show, Generic, NFData, Null, Rep

Eq MetaKindDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Show MetaKindDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Generic MetaKindDefined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData MetaKindDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Null MetaKindDefined in Agda-2.8.0.2 · Agda.Syntax.Info
type Rep MetaKind = D1 ('MetaData "MetaKind" "Agda.Syntax.Info" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "InstanceMeta" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnificationMeta" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Info

valuehidingToMetaKind :: Hiding -> MetaKind

Source#

Default meta kind from its Hiding context.

typetype MetaNameSuggestion = String

Source#

Name suggestion for meta variable. Empty string means no suggestion.

datadata MetaInfo

Source#

Information associated to a meta variable in the abstract syntax.

Constructors

MetaInfo
- metaRange :: Range
- metaScope :: ScopeInfo
- metaNumber :: Maybe MetaId
- metaNameSuggestion :: MetaNameSuggestion
- metaKind :: MetaKind

Instances8Eq, Show, Generic, NFData, Null, HasRange, …

Eq MetaInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Show MetaInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Generic MetaInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData MetaInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Null MetaInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange MetaInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange MetaInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
type Rep MetaInfo = D1 ('MetaData "MetaInfo" "Agda.Syntax.Info" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "MetaInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "metaRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "metaScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo)) :*: (S1 ('MetaSel ('Just "metaNumber") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe MetaId)) :*: (S1 ('MetaSel ('Just "metaNameSuggestion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaNameSuggestion) :*: S1 ('MetaSel ('Just "metaKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaKind)))))Defined in Agda-2.8.0.2 · Agda.Syntax.Info

valueemptyMetaInfo :: MetaInfo

newtypenewtype ExprInfo

Constructors

ExprRange Range

Instances6Eq, Show, NFData, Null, HasRange, KillRange

Eq ExprInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Show ExprInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData ExprInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Null ExprInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange ExprInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange ExprInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info

valueexprNoRange :: ExprInfo

datadata AppInfo

Source#

Information about application

Constructors

AppInfo
- appRange :: Range
- appOrigin :: Origin
- appParens :: ParenPreference
  Do we prefer a lambda argument with or without parens?

Instances10Eq, Ord, Show, Generic, NFData, Null, …

Eq AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Ord AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Show AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Generic AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Null AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
LensOrigin AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
type Rep AppInfo = D1 ('MetaData "AppInfo" "Agda.Syntax.Info" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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))))Defined in Agda-2.8.0.2 · Agda.Syntax.Info

valuedefaultAppInfo :: Range -> AppInfo

Source#

Default is system inserted and prefer parens.

valuedefaultAppInfo_ :: AppInfo

Source#

AppInfo with no range information.

datadata ModuleInfo

Constructors

ModuleInfo
- minfoRange :: Range
- minfoAsTo :: Range
  The range of the "as" and "to" keywords, if any. Retained for highlighting purposes.
- minfoAsName :: Maybe Name
  The "as" module name, if any. Retained for highlighting purposes.
- minfoOpenShort :: Maybe OpenShortHand
- minfoDirective :: Maybe ImportDirective
  Retained for abstractToConcrete of ModuleMacro.

Instances9Eq, Show, Generic, NFData, HasRange, Hilite, …

Eq ModuleInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Show ModuleInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Generic ModuleInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData ModuleInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange ModuleInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Hilite ModuleInfoDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
KillRange ModuleInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
SetRange ModuleInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.Syntax.Info" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "ModuleInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "minfoRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "minfoAsTo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :*: (S1 ('MetaSel ('Just "minfoAsName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Name)) :*: (S1 ('MetaSel ('Just "minfoOpenShort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe OpenShortHand)) :*: S1 ('MetaSel ('Just "minfoDirective") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImportDirective))))))Defined in Agda-2.8.0.2 · Agda.Syntax.Info

newtypenewtype LetInfo

Constructors

LetRange Range

Instances6Eq, Show, NFData, Null, HasRange, KillRange

Eq LetInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Show LetInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData LetInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Null LetInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange LetInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange LetInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info

datadata DefInfo' t

Constructors

DefInfo
- defFixity :: Fixity'
- defAccess :: Access
- defAbstract :: IsAbstract
- defOpaque :: IsOpaque
- defInstance :: IsInstance
- defMacro :: IsMacro
- defInfo :: DeclInfo
- defTactic :: TacticAttribute' t

Instances12Eq, Show, Generic, NFData, HasRange, KillRange, …

Eq t => Eq (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
Show t => Show (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
Generic (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData t => NFData (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange t => KillRange (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
SetRange (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
AllAreOpaque (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
AnyIsAbstract (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
LensIsAbstract (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
LensIsOpaque (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
type Rep (DefInfo' t) = D1 ('MetaData "DefInfo'" "Agda.Syntax.Info" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "DefInfo" 'PrefixI 'True) (((S1 ('MetaSel ('Just "defFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity') :*: S1 ('MetaSel ('Just "defAccess") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Just "defAbstract") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Just "defOpaque") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsOpaque))) :*: ((S1 ('MetaSel ('Just "defInstance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :*: S1 ('MetaSel ('Just "defMacro") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsMacro)) :*: (S1 ('MetaSel ('Just "defInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclInfo) :*: S1 ('MetaSel ('Just "defTactic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TacticAttribute' t))))))Defined in Agda-2.8.0.2 · Agda.Syntax.Info

valuemkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t

valuemkDefInfoInstance

:: Name
-> Fixity'
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> Range
-> DefInfo' t

Source#

Same as mkDefInfo but where we can also give the IsInstance

datadata DeclInfo

Constructors

DeclInfo
- declName :: Name
- declRange :: Range

Instances8Eq, Show, Generic, NFData, HasRange, KillRange, …

Eq DeclInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Show DeclInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Generic DeclInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData DeclInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange DeclInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange DeclInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
SetRange DeclInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
type Rep DeclInfo = D1 ('MetaData "DeclInfo" "Agda.Syntax.Info" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "DeclInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "declName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "declRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))Defined in Agda-2.8.0.2 · Agda.Syntax.Info

datadata MutualInfo

Constructors

MutualInfo
- mutualTerminationCheck :: TerminationCheck Name
- mutualCoverageCheck :: CoverageCheck
- mutualPositivityCheck :: PositivityCheck
- mutualRange :: Range

Instances8Eq, Show, Generic, NFData, Null, HasRange, …

Eq MutualInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Show MutualInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Generic MutualInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData MutualInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Null MutualInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Default value for MutualInfo.
HasRange MutualInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange MutualInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
type Rep MutualInfo = D1 ('MetaData "MutualInfo" "Agda.Syntax.Info" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "MutualInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mutualTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TerminationCheck Name)) :*: S1 ('MetaSel ('Just "mutualCoverageCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Just "mutualPositivityCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck) :*: S1 ('MetaSel ('Just "mutualRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))Defined in Agda-2.8.0.2 · Agda.Syntax.Info

datadata LHSInfo

Constructors

LHSInfo
- lhsRange :: Range
- lhsEllipsis :: ExpandedEllipsis

Instances8Eq, Show, Generic, NFData, Null, HasRange, …

Eq LHSInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Show LHSInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Generic LHSInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData LHSInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Null LHSInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange LHSInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange LHSInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
type Rep LHSInfo = D1 ('MetaData "LHSInfo" "Agda.Syntax.Info" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "LHSInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "lhsEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis)))Defined in Agda-2.8.0.2 · Agda.Syntax.Info

newtypenewtype PatInfo

Source#

For a general pattern we remember the source code position.

Constructors

PatRange Range

Instances9Eq, Show, Semigroup, Monoid, NFData, Null, …

Eq PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Show PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Semigroup PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Monoid PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Null PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
SetRange PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info

valuepatNoRange :: PatInfo

Source#

Empty range for patterns.

datadata ConPatInfo

Source#

Constructor pattern info.

Constructors

ConPatInfo
- conPatOrigin :: ConOrigin
  Does this pattern come form the eta-expansion of an implicit pattern?
- conPatInfo :: PatInfo
- conPatLazy :: ConPatLazy

Instances9Eq, Show, Generic, NFData, HasRange, KillRange, …

Eq ConPatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Show ConPatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Generic ConPatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData ConPatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange ConPatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange ConPatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
SetRange ConPatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
EmbPrj ConPatInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Abstract · orphan
type Rep ConPatInfo = D1 ('MetaData "ConPatInfo" "Agda.Syntax.Info" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "ConPatInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "conPatOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConOrigin) :*: (S1 ('MetaSel ('Just "conPatInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Just "conPatLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatLazy))))Defined in Agda-2.8.0.2 · Agda.Syntax.Info

datadata ConPatLazy

Source#

Has the constructor pattern a dotted (forced) constructor?

Constructors

ConPatLazy
Dotted constructor.
ConPatEager
Ordinary constructor.

Instances9Bounded, Enum, Eq, Ord, Show, Generic, …

Bounded ConPatLazyDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Enum ConPatLazyDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Eq ConPatLazyDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Ord ConPatLazyDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Show ConPatLazyDefined in Agda-2.8.0.2 · Agda.Syntax.Info
Generic ConPatLazyDefined in Agda-2.8.0.2 · Agda.Syntax.Info
NFData ConPatLazyDefined in Agda-2.8.0.2 · Agda.Syntax.Info
EmbPrj ConPatLazyDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Abstract · orphan
type Rep ConPatLazy = D1 ('MetaData "ConPatLazy" "Agda.Syntax.Info" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "ConPatLazy" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ConPatEager" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Info