Safe Haskell | None |
---|---|
Language | Haskell2010 |
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.
InstanceMeta | Meta variable solved by instance search. |
UnificationMeta | Meta variable solved by unification (default). |
Instances
Null MetaKind Source # | |||||
NFData MetaKind Source # | |||||
Defined in Agda.Syntax.Info | |||||
Generic MetaKind Source # | |||||
Defined in Agda.Syntax.Info
| |||||
Show MetaKind Source # | |||||
Eq MetaKind Source # | |||||
type Rep MetaKind Source # | |||||
Defined in Agda.Syntax.Info type Rep MetaKind = D1 ('MetaData "MetaKind" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "InstanceMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnificationMeta" 'PrefixI 'False) (U1 :: Type -> Type)) |
type MetaNameSuggestion = String Source #
Name suggestion for meta variable. Empty string means no suggestion.
Information associated to a meta variable in the abstract syntax.
Instances
HasRange MetaInfo Source # | |||||
KillRange MetaInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
Null MetaInfo Source # | |||||
NFData MetaInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
Generic MetaInfo Source # | |||||
Defined in Agda.Syntax.Info
| |||||
Show MetaInfo Source # | |||||
Eq MetaInfo Source # | |||||
type Rep MetaInfo Source # | |||||
Defined in Agda.Syntax.Info type Rep MetaInfo = D1 ('MetaData "MetaInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" '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))))) |
Information about application
Instances
LensOrigin AppInfo Source # | |||||
HasRange AppInfo Source # | |||||
KillRange AppInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
NFData AppInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
Generic AppInfo Source # | |||||
Defined in Agda.Syntax.Info
| |||||
Show AppInfo Source # | |||||
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.6.20240714-inplace" '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 #
ModuleInfo | |
|
Instances
HasRange ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info getRange :: ModuleInfo -> Range Source # | |||||
KillRange ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
SetRange ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info setRange :: Range -> ModuleInfo -> ModuleInfo Source # | |||||
NFData ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info rnf :: ModuleInfo -> () | |||||
Generic ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info
from :: ModuleInfo -> Rep ModuleInfo x to :: Rep ModuleInfo x -> ModuleInfo | |||||
Show ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info showsPrec :: Int -> ModuleInfo -> ShowS show :: ModuleInfo -> String showList :: [ModuleInfo] -> ShowS | |||||
Eq ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info (==) :: ModuleInfo -> ModuleInfo -> Bool (/=) :: ModuleInfo -> ModuleInfo -> Bool | |||||
type Rep ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" '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)))))) |
DefInfo | |
|
Instances
AllAreOpaque (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info jointOpacity :: DefInfo' t -> JointOpacity Source # | |||||
AnyIsAbstract (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info anyIsAbstract :: DefInfo' t -> IsAbstract Source # | |||||
LensIsAbstract (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info lensIsAbstract :: Lens' (DefInfo' t) IsAbstract Source # | |||||
LensIsOpaque (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info | |||||
HasRange (DefInfo' t) Source # | |||||
KillRange t => KillRange (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info killRange :: KillRangeT (DefInfo' t) Source # | |||||
SetRange (DefInfo' t) Source # | |||||
NFData t => NFData (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info | |||||
Generic (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info
| |||||
Show t => Show (DefInfo' t) Source # | |||||
Eq t => Eq (DefInfo' t) Source # | |||||
type Rep (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info type Rep (DefInfo' t) = D1 ('MetaData "DefInfo'" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" '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)))))) |
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 | |||||
SetRange DeclInfo Source # | |||||
NFData DeclInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
Generic DeclInfo Source # | |||||
Defined in Agda.Syntax.Info
| |||||
Show DeclInfo Source # | |||||
Eq DeclInfo Source # | |||||
type Rep DeclInfo Source # | |||||
Defined in Agda.Syntax.Info type Rep DeclInfo = D1 ('MetaData "DeclInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" '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 #
Instances
HasRange MutualInfo Source # | |||||
Defined in Agda.Syntax.Info getRange :: MutualInfo -> Range Source # | |||||
KillRange MutualInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
Null MutualInfo Source # | Default value for | ||||
Defined in Agda.Syntax.Info empty :: MutualInfo Source # null :: MutualInfo -> Bool Source # | |||||
NFData MutualInfo Source # | |||||
Defined in Agda.Syntax.Info rnf :: MutualInfo -> () | |||||
Generic MutualInfo Source # | |||||
Defined in Agda.Syntax.Info
from :: MutualInfo -> Rep MutualInfo x to :: Rep MutualInfo x -> MutualInfo | |||||
Show MutualInfo Source # | |||||
Defined in Agda.Syntax.Info showsPrec :: Int -> MutualInfo -> ShowS show :: MutualInfo -> String showList :: [MutualInfo] -> ShowS | |||||
Eq MutualInfo Source # | |||||
Defined in Agda.Syntax.Info (==) :: MutualInfo -> MutualInfo -> Bool (/=) :: MutualInfo -> MutualInfo -> Bool | |||||
type Rep MutualInfo Source # | |||||
Defined in Agda.Syntax.Info type Rep MutualInfo = D1 ('MetaData "MutualInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" '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)))) |
Instances
HasRange LHSInfo Source # | |||||
KillRange LHSInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
Null LHSInfo Source # | |||||
NFData LHSInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
Generic LHSInfo Source # | |||||
Defined in Agda.Syntax.Info
| |||||
Show LHSInfo Source # | |||||
Eq LHSInfo Source # | |||||
type Rep LHSInfo Source # | |||||
Defined in Agda.Syntax.Info type Rep LHSInfo = D1 ('MetaData "LHSInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" '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.
ConPatInfo | |
|
Instances
HasRange ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info getRange :: ConPatInfo -> Range Source # | |||||
KillRange ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
SetRange ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info setRange :: Range -> ConPatInfo -> ConPatInfo Source # | |||||
EmbPrj ConPatInfo Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Abstract icode :: ConPatInfo -> S Int32 Source # icod_ :: ConPatInfo -> S Int32 Source # value :: Int32 -> R ConPatInfo Source # | |||||
NFData ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info rnf :: ConPatInfo -> () | |||||
Generic ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info
from :: ConPatInfo -> Rep ConPatInfo x to :: Rep ConPatInfo x -> ConPatInfo | |||||
Show ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info showsPrec :: Int -> ConPatInfo -> ShowS show :: ConPatInfo -> String showList :: [ConPatInfo] -> ShowS | |||||
Eq ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info (==) :: ConPatInfo -> ConPatInfo -> Bool (/=) :: ConPatInfo -> ConPatInfo -> Bool | |||||
type Rep ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info type Rep ConPatInfo = D1 ('MetaData "ConPatInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" '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)))) |
data ConPatLazy Source #
Has the constructor pattern a dotted (forced) constructor?
ConPatLazy | Dotted constructor. |
ConPatEager | Ordinary constructor. |
Instances
EmbPrj ConPatLazy Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Abstract icode :: ConPatLazy -> S Int32 Source # icod_ :: ConPatLazy -> S Int32 Source # value :: Int32 -> R ConPatLazy Source # | |||||
NFData ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info rnf :: ConPatLazy -> () | |||||
Bounded ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info | |||||
Enum ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info succ :: ConPatLazy -> ConPatLazy pred :: ConPatLazy -> ConPatLazy toEnum :: Int -> ConPatLazy fromEnum :: ConPatLazy -> Int enumFrom :: ConPatLazy -> [ConPatLazy] enumFromThen :: ConPatLazy -> ConPatLazy -> [ConPatLazy] enumFromTo :: ConPatLazy -> ConPatLazy -> [ConPatLazy] enumFromThenTo :: ConPatLazy -> ConPatLazy -> ConPatLazy -> [ConPatLazy] | |||||
Generic ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info
from :: ConPatLazy -> Rep ConPatLazy x to :: Rep ConPatLazy x -> ConPatLazy | |||||
Show ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info showsPrec :: Int -> ConPatLazy -> ShowS show :: ConPatLazy -> String showList :: [ConPatLazy] -> ShowS | |||||
Eq ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info (==) :: ConPatLazy -> ConPatLazy -> Bool (/=) :: ConPatLazy -> ConPatLazy -> Bool | |||||
Ord ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info compare :: ConPatLazy -> ConPatLazy -> Ordering (<) :: ConPatLazy -> ConPatLazy -> Bool (<=) :: ConPatLazy -> ConPatLazy -> Bool (>) :: ConPatLazy -> ConPatLazy -> Bool (>=) :: ConPatLazy -> ConPatLazy -> Bool max :: ConPatLazy -> ConPatLazy -> ConPatLazy min :: ConPatLazy -> ConPatLazy -> ConPatLazy | |||||
type Rep ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info type Rep ConPatLazy = D1 ('MetaData "ConPatLazy" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ConPatLazy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConPatEager" 'PrefixI 'False) (U1 :: Type -> Type)) |