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 {
- metaRange :: Range
- metaScope :: ScopeInfo
- metaNumber :: Maybe MetaId
- metaNameSuggestion :: String
}
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 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 {
- declName :: Name
- declRange :: Range
}
data MutualInfo = MutualInfo {
}
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 MetaInfo Source #

Constructors

MetaInfo
Fields metaRange :: Range metaScope :: ScopeInfo metaNumber :: Maybe MetaId metaNameSuggestion :: String

Instances

Instances details

HasRange MetaInfo Source #

Instance details

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 #
Show ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ExprInfo -> ShowS # show :: ExprInfo -> String # showList :: [ExprInfo] -> ShowS #
NFData ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: ExprInfo -> () #
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 #
Show LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> LetInfo -> ShowS # show :: LetInfo -> String # showList :: [LetInfo] -> ShowS #
NFData LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: LetInfo -> () #
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 :: Maybe (Ranged 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 #
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 #
NFData PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: PatInfo -> () #
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.