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 MetaKind
- = InstanceMeta
- | UnificationMeta
hidingToMetaKind :: Hiding -> MetaKind
type MetaNameSuggestion = String
data MetaInfo = MetaInfo {
- metaRange :: Range
- metaScope :: ScopeInfo
- metaNumber :: Maybe MetaId
- metaNameSuggestion :: MetaNameSuggestion
- metaKind :: MetaKind
}
emptyMetaInfo :: MetaInfo
newtype ExprInfo = ExprRange Range
exprNoRange :: ExprInfo
data AppInfo = AppInfo {
- appRange :: Range
- appOrigin :: Origin
- appParens :: ParenPreference
}
defaultAppInfo :: Range -> AppInfo
defaultAppInfo_ :: AppInfo
data ModuleInfo = ModuleInfo {
- minfoRange :: Range
- minfoAsTo :: Range
- minfoAsName :: Maybe Name
- minfoOpenShort :: Maybe OpenShortHand
- minfoDirective :: Maybe ImportDirective
}
newtype LetInfo = LetRange Range
data RecInfo = RecInfo Range RecStyle
data RecStyle
- = RecStyleWhere
- | RecStyleBrace
recInfoBrace :: Range -> RecInfo
recInfoWhere :: Range -> RecInfo
data DefInfo' t = DefInfo {
- defFixity :: Fixity'
- defAccess :: Access
- defAbstract :: IsAbstract
- defOpaque :: IsOpaque
- defInstance :: IsInstance
- defMacro :: IsMacro
- defInfo :: DeclInfo
- defTactic :: TacticAttribute' t
}
mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo' t
data DeclInfo = DeclInfo {
- declName :: Name
- declRange :: Range
}
data MutualInfo = MutualInfo {
- mutualTerminationCheck :: TerminationCheck Name
- mutualCoverageCheck :: CoverageCheck
- mutualPositivityCheck :: PositivityCheck
- mutualRange :: Range
}
data LHSInfo = LHSInfo {
- lhsRange :: Range
- lhsEllipsis :: ExpandedEllipsis
}
newtype PatInfo = PatRange Range
patNoRange :: PatInfo
data ConPatInfo = ConPatInfo {
- conPatOrigin :: ConOrigin
- conPatInfo :: PatInfo
- conPatLazy :: ConPatLazy
}
data ConPatLazy
- = ConPatLazy
- | ConPatEager

Documentation

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

Instances

Instances details

Null MetaKind Source #

Instance details

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

HasRange ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ExprInfo -> Range Source #
KillRange ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ExprInfo Source #
Null ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods empty :: ExprInfo Source # null :: ExprInfo -> Bool Source #
NFData ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: ExprInfo -> () #
Show ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ExprInfo -> ShowS # show :: ExprInfo -> String # showList :: [ExprInfo] -> ShowS #
Eq ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: ExprInfo -> ExprInfo -> Bool # (/=) :: ExprInfo -> ExprInfo -> Bool #

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

ModuleInfo
Fields 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`.

HasRange LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: LetInfo -> Range Source #
KillRange LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LetInfo Source #
Null LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods empty :: LetInfo Source # null :: LetInfo -> Bool Source #
NFData LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: LetInfo -> () #
Show LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> LetInfo -> ShowS # show :: LetInfo -> String # showList :: [LetInfo] -> ShowS #
Eq LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: LetInfo -> LetInfo -> Bool # (/=) :: LetInfo -> LetInfo -> Bool #

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

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

LHSInfo
Fields lhsRange :: Range lhsEllipsis :: ExpandedEllipsis

HasRange PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: PatInfo -> Range Source #
KillRange PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT PatInfo Source #
SetRange PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> PatInfo -> PatInfo Source #
Null PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods empty :: PatInfo Source # null :: PatInfo -> Bool Source #
NFData PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: PatInfo -> () #
Monoid PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods mempty :: PatInfo # mappend :: PatInfo -> PatInfo -> PatInfo # mconcat :: [PatInfo] -> PatInfo #
Semigroup PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (<>) :: PatInfo -> PatInfo -> PatInfo # sconcat :: NonEmpty PatInfo -> PatInfo # stimes :: Integral b => b -> PatInfo -> PatInfo #
Show PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> PatInfo -> ShowS # show :: PatInfo -> String # showList :: [PatInfo] -> ShowS #
Eq PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: PatInfo -> PatInfo -> Bool # (/=) :: PatInfo -> PatInfo -> Bool #

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

ConPatLazy	Dotted constructor.
ConPatEager	Ordinary constructor.