Safe Haskell | None |
---|---|
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 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 {
- defFixity :: Fixity'
- defAccess :: Access
- defAbstract :: IsAbstract
- defOpaque :: IsOpaque
- defInstance :: IsInstance
- defMacro :: IsMacro
- defInfo :: DeclInfo
- defTactic :: Maybe (Ranged t)
- 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
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 # | |||||
Defined in Agda.Syntax.Info Associated Types
| |||||
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.6.4.1-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 #
Constructors
ModuleInfo | |
Fields
|
Instances
HasRange ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info Methods getRange :: ModuleInfo -> Range Source # | |||||
KillRange ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info Methods | |||||
SetRange ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info Methods setRange :: Range -> ModuleInfo -> ModuleInfo Source # | |||||
Generic ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info Associated Types
| |||||
Show ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ModuleInfo -> ShowS # show :: ModuleInfo -> String # showList :: [ModuleInfo] -> ShowS # | |||||
NFData ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info Methods rnf :: ModuleInfo -> () # | |||||
Eq ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
type Rep ModuleInfo Source # | |||||
Defined in Agda.Syntax.Info type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.Syntax.Info" "Agda-2.6.4.1-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)))))) |
Constructors
DefInfo | |
Fields
|
Instances
AllAreOpaque (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info Methods jointOpacity :: DefInfo' t -> JointOpacity Source # | |||||
AnyIsAbstract (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info Methods anyIsAbstract :: DefInfo' t -> IsAbstract Source # | |||||
LensIsAbstract (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info Methods 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 Methods killRange :: KillRangeT (DefInfo' t) Source # | |||||
SetRange (DefInfo' t) Source # | |||||
Generic (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info Associated Types
| |||||
Show t => Show (DefInfo' t) Source # | |||||
NFData t => NFData (DefInfo' t) Source # | |||||
Defined in Agda.Syntax.Info | |||||
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.4.1-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 (Maybe (Ranged 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 Methods | |||||
SetRange DeclInfo Source # | |||||
Generic DeclInfo Source # | |||||
Defined in Agda.Syntax.Info Associated Types
| |||||
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.6.4.1-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 #
Constructors
MutualInfo | |
Instances
HasRange MutualInfo Source # | |||||
Defined in Agda.Syntax.Info Methods getRange :: MutualInfo -> Range Source # | |||||
KillRange MutualInfo Source # | |||||
Defined in Agda.Syntax.Info Methods | |||||
Null MutualInfo Source # | Default value for | ||||
Defined in Agda.Syntax.Info | |||||
Generic MutualInfo Source # | |||||
Defined in Agda.Syntax.Info Associated Types
| |||||
Show MutualInfo Source # | |||||
Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MutualInfo -> ShowS # show :: MutualInfo -> String # showList :: [MutualInfo] -> ShowS # | |||||
NFData MutualInfo Source # | |||||
Defined in Agda.Syntax.Info Methods rnf :: MutualInfo -> () # | |||||
Eq MutualInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
type Rep MutualInfo Source # | |||||
Defined in Agda.Syntax.Info type Rep MutualInfo = D1 ('MetaData "MutualInfo" "Agda.Syntax.Info" "Agda-2.6.4.1-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)))) |
Constructors
LHSInfo | |
Fields |
Instances
HasRange LHSInfo Source # | |||||
KillRange LHSInfo Source # | |||||
Defined in Agda.Syntax.Info Methods | |||||
Null LHSInfo Source # | |||||
Generic LHSInfo Source # | |||||
Defined in Agda.Syntax.Info Associated Types
| |||||
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.6.4.1-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.
Constructors
ConPatInfo | |
Fields
|
Instances
HasRange ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info Methods getRange :: ConPatInfo -> Range Source # | |||||
KillRange ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info Methods | |||||
SetRange ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info Methods setRange :: Range -> ConPatInfo -> ConPatInfo Source # | |||||
EmbPrj ConPatInfo Source # | |||||
Generic ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info Associated Types
| |||||
Show ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatInfo -> ShowS # show :: ConPatInfo -> String # showList :: [ConPatInfo] -> ShowS # | |||||
NFData ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info Methods rnf :: ConPatInfo -> () # | |||||
Eq ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info | |||||
type Rep ConPatInfo Source # | |||||
Defined in Agda.Syntax.Info type Rep ConPatInfo = D1 ('MetaData "ConPatInfo" "Agda.Syntax.Info" "Agda-2.6.4.1-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?
Constructors
ConPatLazy | Dotted constructor. |
ConPatEager | Ordinary constructor. |
Instances
EmbPrj ConPatLazy Source # | |||||
Bounded ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info | |||||
Enum ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info Methods 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 Associated Types
| |||||
Show ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatLazy -> ShowS # show :: ConPatLazy -> String # showList :: [ConPatLazy] -> ShowS # | |||||
NFData ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info Methods rnf :: ConPatLazy -> () # | |||||
Eq ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info | |||||
Ord ConPatLazy Source # | |||||
Defined in Agda.Syntax.Info Methods 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 # | |||||