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 = DefInfo {
- defFixity :: Fixity'
- defAccess :: Access
- defAbstract :: IsAbstract
- defInstance :: IsInstance
- defMacro :: IsMacro
- defInfo :: DeclInfo
}
mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo
mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo
data DeclInfo = DeclInfo {
- declName :: Name
- declRange :: Range
}
data MutualInfo = MutualInfo {
}
newtype LHSInfo = LHSRange Range
newtype PatInfo = PatRange Range
patNoRange :: PatInfo
data ConPatInfo = ConPatInfo {
- patOrigin :: ConOrigin
- patInfo :: PatInfo
- patLazy :: Bool
}

Documentation

data MetaInfo #

Constructors

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

Instances

Eq MetaInfo #
Instance details Defined in Agda.Syntax.Info Methods (==) :: MetaInfo -> MetaInfo -> Bool # (/=) :: MetaInfo -> MetaInfo -> Bool #
Data MetaInfo #
Instance details Defined in Agda.Syntax.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MetaInfo -> c MetaInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaInfo # toConstr :: MetaInfo -> Constr # dataTypeOf :: MetaInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaInfo) # gmapT :: (forall b. Data b => b -> b) -> MetaInfo -> MetaInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> MetaInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaInfo -> m MetaInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaInfo -> m MetaInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaInfo -> m MetaInfo #
Show MetaInfo #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MetaInfo -> ShowS # show :: MetaInfo -> String # showList :: [MetaInfo] -> ShowS #
KillRange MetaInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT MetaInfo #
HasRange MetaInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: MetaInfo -> Range #

emptyMetaInfo :: MetaInfo #

newtype ExprInfo #

Constructors

ExprRange Range

Instances

Eq ExprInfo #
Instance details Defined in Agda.Syntax.Info Methods (==) :: ExprInfo -> ExprInfo -> Bool # (/=) :: ExprInfo -> ExprInfo -> Bool #
Data ExprInfo #
Instance details Defined in Agda.Syntax.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExprInfo -> c ExprInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExprInfo # toConstr :: ExprInfo -> Constr # dataTypeOf :: ExprInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExprInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExprInfo) # gmapT :: (forall b. Data b => b -> b) -> ExprInfo -> ExprInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExprInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExprInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> ExprInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ExprInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExprInfo -> m ExprInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExprInfo -> m ExprInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExprInfo -> m ExprInfo #
Show ExprInfo #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ExprInfo -> ShowS # show :: ExprInfo -> String # showList :: [ExprInfo] -> ShowS #
Null ExprInfo #
Instance details Defined in Agda.Syntax.Info Methods empty :: ExprInfo # null :: ExprInfo -> Bool #
KillRange ExprInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ExprInfo #
HasRange ExprInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ExprInfo -> Range #

exprNoRange :: ExprInfo #

data AppInfo #

Information about application

Constructors

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

Instances

Eq AppInfo #
Instance details Defined in Agda.Syntax.Info Methods (==) :: AppInfo -> AppInfo -> Bool # (/=) :: AppInfo -> AppInfo -> Bool #
Data AppInfo #
Instance details Defined in Agda.Syntax.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AppInfo -> c AppInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AppInfo # toConstr :: AppInfo -> Constr # dataTypeOf :: AppInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AppInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AppInfo) # gmapT :: (forall b. Data b => b -> b) -> AppInfo -> AppInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AppInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AppInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> AppInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AppInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AppInfo -> m AppInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AppInfo -> m AppInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AppInfo -> m AppInfo #
Ord AppInfo #
Instance details Defined in Agda.Syntax.Info Methods compare :: AppInfo -> AppInfo -> Ordering # (<) :: AppInfo -> AppInfo -> Bool # (<=) :: AppInfo -> AppInfo -> Bool # (>) :: AppInfo -> AppInfo -> Bool # (>=) :: AppInfo -> AppInfo -> Bool # max :: AppInfo -> AppInfo -> AppInfo # min :: AppInfo -> AppInfo -> AppInfo #
Show AppInfo #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> AppInfo -> ShowS # show :: AppInfo -> String # showList :: [AppInfo] -> ShowS #
KillRange AppInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT AppInfo #
HasRange AppInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: AppInfo -> Range #
LensOrigin AppInfo #
Instance details Defined in Agda.Syntax.Info Methods getOrigin :: AppInfo -> Origin # setOrigin :: Origin -> AppInfo -> AppInfo # mapOrigin :: (Origin -> Origin) -> AppInfo -> AppInfo #

defaultAppInfo :: Range -> AppInfo #

Default is system inserted and prefer parens.

defaultAppInfo_ :: AppInfo #

AppInfo with no range information.

data ModuleInfo #

Constructors

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

Instances

Eq ModuleInfo #
Instance details Defined in Agda.Syntax.Info Methods (==) :: ModuleInfo -> ModuleInfo -> Bool # (/=) :: ModuleInfo -> ModuleInfo -> Bool #
Data ModuleInfo #
Instance details Defined in Agda.Syntax.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleInfo -> c ModuleInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleInfo # toConstr :: ModuleInfo -> Constr # dataTypeOf :: ModuleInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleInfo) # gmapT :: (forall b. Data b => b -> b) -> ModuleInfo -> ModuleInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> ModuleInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleInfo -> m ModuleInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleInfo -> m ModuleInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleInfo -> m ModuleInfo #
Show ModuleInfo #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ModuleInfo -> ShowS # show :: ModuleInfo -> String # showList :: [ModuleInfo] -> ShowS #
KillRange ModuleInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ModuleInfo #
SetRange ModuleInfo #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> ModuleInfo -> ModuleInfo #
HasRange ModuleInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ModuleInfo -> Range #
UniverseBi Declaration ModuleInfo #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [ModuleInfo] #

newtype LetInfo #

Constructors

LetRange Range

Instances

Eq LetInfo #
Instance details Defined in Agda.Syntax.Info Methods (==) :: LetInfo -> LetInfo -> Bool # (/=) :: LetInfo -> LetInfo -> Bool #
Data LetInfo #
Instance details Defined in Agda.Syntax.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LetInfo -> c LetInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LetInfo # toConstr :: LetInfo -> Constr # dataTypeOf :: LetInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LetInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LetInfo) # gmapT :: (forall b. Data b => b -> b) -> LetInfo -> LetInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LetInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LetInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> LetInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LetInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LetInfo -> m LetInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LetInfo -> m LetInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LetInfo -> m LetInfo #
Show LetInfo #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> LetInfo -> ShowS # show :: LetInfo -> String # showList :: [LetInfo] -> ShowS #
Null LetInfo #
Instance details Defined in Agda.Syntax.Info Methods empty :: LetInfo # null :: LetInfo -> Bool #
KillRange LetInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LetInfo #
HasRange LetInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: LetInfo -> Range #

data DefInfo #

Constructors

DefInfo
Fields defFixity :: Fixity' defAccess :: Access defAbstract :: IsAbstract defInstance :: IsInstance defMacro :: IsMacro defInfo :: DeclInfo

Instances

Eq DefInfo #
Instance details Defined in Agda.Syntax.Info Methods (==) :: DefInfo -> DefInfo -> Bool # (/=) :: DefInfo -> DefInfo -> Bool #
Data DefInfo #
Instance details Defined in Agda.Syntax.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefInfo -> c DefInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefInfo # toConstr :: DefInfo -> Constr # dataTypeOf :: DefInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefInfo) # gmapT :: (forall b. Data b => b -> b) -> DefInfo -> DefInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> DefInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DefInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefInfo -> m DefInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefInfo -> m DefInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefInfo -> m DefInfo #
Show DefInfo #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> DefInfo -> ShowS # show :: DefInfo -> String # showList :: [DefInfo] -> ShowS #
KillRange DefInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT DefInfo #
SetRange DefInfo #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> DefInfo -> DefInfo #
HasRange DefInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: DefInfo -> Range #

mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo #

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

Same as mkDefInfo but where we can also give the IsInstance

data DeclInfo #

Constructors

DeclInfo
Fields declName :: Name declRange :: Range

Instances

Eq DeclInfo #
Instance details Defined in Agda.Syntax.Info Methods (==) :: DeclInfo -> DeclInfo -> Bool # (/=) :: DeclInfo -> DeclInfo -> Bool #
Data DeclInfo #
Instance details Defined in Agda.Syntax.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DeclInfo -> c DeclInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DeclInfo # toConstr :: DeclInfo -> Constr # dataTypeOf :: DeclInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DeclInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DeclInfo) # gmapT :: (forall b. Data b => b -> b) -> DeclInfo -> DeclInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DeclInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DeclInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> DeclInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DeclInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DeclInfo -> m DeclInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclInfo -> m DeclInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclInfo -> m DeclInfo #
Show DeclInfo #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> DeclInfo -> ShowS # show :: DeclInfo -> String # showList :: [DeclInfo] -> ShowS #
KillRange DeclInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT DeclInfo #
SetRange DeclInfo #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> DeclInfo -> DeclInfo #
HasRange DeclInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: DeclInfo -> Range #

data MutualInfo #

Constructors

MutualInfo
Fields mutualTermCheck :: TerminationCheck Name mutualPositivityCheck :: PositivityCheck mutualRange :: Range

Instances

Eq MutualInfo #
Instance details Defined in Agda.Syntax.Info Methods (==) :: MutualInfo -> MutualInfo -> Bool # (/=) :: MutualInfo -> MutualInfo -> Bool #
Data MutualInfo #
Instance details Defined in Agda.Syntax.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MutualInfo -> c MutualInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MutualInfo # toConstr :: MutualInfo -> Constr # dataTypeOf :: MutualInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MutualInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MutualInfo) # gmapT :: (forall b. Data b => b -> b) -> MutualInfo -> MutualInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MutualInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MutualInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> MutualInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MutualInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MutualInfo -> m MutualInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualInfo -> m MutualInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualInfo -> m MutualInfo #
Show MutualInfo #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MutualInfo -> ShowS # show :: MutualInfo -> String # showList :: [MutualInfo] -> ShowS #
Null MutualInfo #	Default value for `MutualInfo`.
Instance details Defined in Agda.Syntax.Info Methods empty :: MutualInfo # null :: MutualInfo -> Bool #
KillRange MutualInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT MutualInfo #
HasRange MutualInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: MutualInfo -> Range #

newtype LHSInfo #

Constructors

LHSRange Range

Instances

Eq LHSInfo #
Instance details Defined in Agda.Syntax.Info Methods (==) :: LHSInfo -> LHSInfo -> Bool # (/=) :: LHSInfo -> LHSInfo -> Bool #
Data LHSInfo #
Instance details Defined in Agda.Syntax.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHSInfo -> c LHSInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHSInfo # toConstr :: LHSInfo -> Constr # dataTypeOf :: LHSInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHSInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHSInfo) # gmapT :: (forall b. Data b => b -> b) -> LHSInfo -> LHSInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHSInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHSInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> LHSInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LHSInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHSInfo -> m LHSInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSInfo -> m LHSInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSInfo -> m LHSInfo #
Show LHSInfo #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> LHSInfo -> ShowS # show :: LHSInfo -> String # showList :: [LHSInfo] -> ShowS #
Null LHSInfo #
Instance details Defined in Agda.Syntax.Info Methods empty :: LHSInfo # null :: LHSInfo -> Bool #
KillRange LHSInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LHSInfo #
HasRange LHSInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: LHSInfo -> Range #

newtype PatInfo #

For a general pattern we remember the source code position.

Constructors

PatRange Range

Instances

Eq PatInfo #
Instance details Defined in Agda.Syntax.Info Methods (==) :: PatInfo -> PatInfo -> Bool # (/=) :: PatInfo -> PatInfo -> Bool #
Data PatInfo #
Instance details Defined in Agda.Syntax.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PatInfo -> c PatInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatInfo # toConstr :: PatInfo -> Constr # dataTypeOf :: PatInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PatInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatInfo) # gmapT :: (forall b. Data b => b -> b) -> PatInfo -> PatInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> PatInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PatInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PatInfo -> m PatInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PatInfo -> m PatInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PatInfo -> m PatInfo #
Show PatInfo #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> PatInfo -> ShowS # show :: PatInfo -> String # showList :: [PatInfo] -> ShowS #
Null PatInfo #
Instance details Defined in Agda.Syntax.Info Methods empty :: PatInfo # null :: PatInfo -> Bool #
KillRange PatInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT PatInfo #
SetRange PatInfo #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> PatInfo -> PatInfo #
HasRange PatInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: PatInfo -> Range #

patNoRange :: PatInfo #

Empty range for patterns.

data ConPatInfo #

Constructor pattern info.

Constructors

ConPatInfo
Fields patOrigin :: ConOrigin Does this pattern come form the eta-expansion of an implicit pattern? patInfo :: PatInfo patLazy :: Bool

Instances

Eq ConPatInfo #
Instance details Defined in Agda.Syntax.Info Methods (==) :: ConPatInfo -> ConPatInfo -> Bool # (/=) :: ConPatInfo -> ConPatInfo -> Bool #
Data ConPatInfo #
Instance details Defined in Agda.Syntax.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConPatInfo -> c ConPatInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConPatInfo # toConstr :: ConPatInfo -> Constr # dataTypeOf :: ConPatInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConPatInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConPatInfo) # gmapT :: (forall b. Data b => b -> b) -> ConPatInfo -> ConPatInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConPatInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConPatInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> ConPatInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ConPatInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConPatInfo -> m ConPatInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatInfo -> m ConPatInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatInfo -> m ConPatInfo #
Show ConPatInfo #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatInfo -> ShowS # show :: ConPatInfo -> String # showList :: [ConPatInfo] -> ShowS #
KillRange ConPatInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ConPatInfo #
SetRange ConPatInfo #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> ConPatInfo -> ConPatInfo #
HasRange ConPatInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ConPatInfo -> Range #
EmbPrj ConPatInfo #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatInfo -> S Int32 # icod_ :: ConPatInfo -> S Int32 # value :: Int32 -> R ConPatInfo #