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 Source #

Constructors

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

Instances

Eq MetaInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: MetaInfo -> MetaInfo -> Bool # (/=) :: MetaInfo -> MetaInfo -> Bool #
Data MetaInfo Source #
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 Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MetaInfo -> ShowS # show :: MetaInfo -> String # showList :: [MetaInfo] -> ShowS #
KillRange MetaInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT MetaInfo Source #
HasRange MetaInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: MetaInfo -> Range Source #

emptyMetaInfo :: MetaInfo Source #

newtype ExprInfo Source #

Constructors

ExprRange Range

Instances

Eq ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: ExprInfo -> ExprInfo -> Bool # (/=) :: ExprInfo -> ExprInfo -> Bool #
Data ExprInfo Source #
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 Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ExprInfo -> ShowS # show :: ExprInfo -> String # showList :: [ExprInfo] -> ShowS #
Null ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods empty :: ExprInfo Source # null :: ExprInfo -> Bool Source #
KillRange ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ExprInfo Source #
HasRange ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ExprInfo -> Range Source #

exprNoRange :: ExprInfo Source #

data AppInfo Source #

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 Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: AppInfo -> AppInfo -> Bool # (/=) :: AppInfo -> AppInfo -> Bool #
Data AppInfo Source #
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 Source #
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 Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> AppInfo -> ShowS # show :: AppInfo -> String # showList :: [AppInfo] -> ShowS #
KillRange AppInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT AppInfo Source #
HasRange AppInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: AppInfo -> Range Source #
LensOrigin AppInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getOrigin :: AppInfo -> Origin Source # setOrigin :: Origin -> AppInfo -> AppInfo Source # mapOrigin :: (Origin -> Origin) -> AppInfo -> AppInfo Source #

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 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 Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: ModuleInfo -> ModuleInfo -> Bool # (/=) :: ModuleInfo -> ModuleInfo -> Bool #
Data ModuleInfo Source #
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 Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ModuleInfo -> ShowS # show :: ModuleInfo -> String # showList :: [ModuleInfo] -> ShowS #
KillRange ModuleInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ModuleInfo Source #
SetRange ModuleInfo Source #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> ModuleInfo -> ModuleInfo Source #
HasRange ModuleInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ModuleInfo -> Range Source #
UniverseBi Declaration ModuleInfo
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [ModuleInfo]

newtype LetInfo Source #

Constructors

LetRange Range

Instances

Eq LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: LetInfo -> LetInfo -> Bool # (/=) :: LetInfo -> LetInfo -> Bool #
Data LetInfo Source #
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 Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> LetInfo -> ShowS # show :: LetInfo -> String # showList :: [LetInfo] -> ShowS #
Null LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods empty :: LetInfo Source # null :: LetInfo -> Bool Source #
KillRange LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LetInfo Source #
HasRange LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: LetInfo -> Range Source #

data DefInfo Source #

Constructors

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

Instances

Eq DefInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: DefInfo -> DefInfo -> Bool # (/=) :: DefInfo -> DefInfo -> Bool #
Data DefInfo Source #
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 Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> DefInfo -> ShowS # show :: DefInfo -> String # showList :: [DefInfo] -> ShowS #
KillRange DefInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT DefInfo Source #
SetRange DefInfo Source #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> DefInfo -> DefInfo Source #
HasRange DefInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: DefInfo -> Range Source #

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

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

Same as mkDefInfo but where we can also give the IsInstance

data DeclInfo Source #

Constructors

DeclInfo
Fields declName :: Name declRange :: Range

Instances

Eq DeclInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: DeclInfo -> DeclInfo -> Bool # (/=) :: DeclInfo -> DeclInfo -> Bool #
Data DeclInfo Source #
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 Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> DeclInfo -> ShowS # show :: DeclInfo -> String # showList :: [DeclInfo] -> ShowS #
KillRange DeclInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT DeclInfo Source #
SetRange DeclInfo Source #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> DeclInfo -> DeclInfo Source #
HasRange DeclInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: DeclInfo -> Range Source #

data MutualInfo Source #

Constructors

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

Instances

Eq MutualInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: MutualInfo -> MutualInfo -> Bool # (/=) :: MutualInfo -> MutualInfo -> Bool #
Data MutualInfo Source #
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 Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MutualInfo -> ShowS # show :: MutualInfo -> String # showList :: [MutualInfo] -> ShowS #
Null MutualInfo Source #	Default value for `MutualInfo`.
Instance details Defined in Agda.Syntax.Info Methods empty :: MutualInfo Source # null :: MutualInfo -> Bool Source #
KillRange MutualInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT MutualInfo Source #
HasRange MutualInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: MutualInfo -> Range Source #

newtype LHSInfo Source #

Constructors

LHSRange Range

Instances

Eq LHSInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: LHSInfo -> LHSInfo -> Bool # (/=) :: LHSInfo -> LHSInfo -> Bool #
Data LHSInfo Source #
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 Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> LHSInfo -> ShowS # show :: LHSInfo -> String # showList :: [LHSInfo] -> ShowS #
Null LHSInfo Source #
Instance details Defined in Agda.Syntax.Info Methods empty :: LHSInfo Source # null :: LHSInfo -> Bool Source #
KillRange LHSInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LHSInfo Source #
HasRange LHSInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: LHSInfo -> Range Source #

newtype PatInfo Source #

For a general pattern we remember the source code position.

Constructors

PatRange Range

Instances

Eq PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: PatInfo -> PatInfo -> Bool # (/=) :: PatInfo -> PatInfo -> Bool #
Data PatInfo Source #
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 Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> PatInfo -> ShowS # show :: PatInfo -> String # showList :: [PatInfo] -> ShowS #
Null PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods empty :: PatInfo Source # null :: PatInfo -> Bool 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 #
HasRange PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: PatInfo -> Range Source #

patNoRange :: PatInfo Source #

Empty range for patterns.

data ConPatInfo Source #

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 Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: ConPatInfo -> ConPatInfo -> Bool # (/=) :: ConPatInfo -> ConPatInfo -> Bool #
Data ConPatInfo Source #
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 Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatInfo -> ShowS # show :: ConPatInfo -> String # showList :: [ConPatInfo] -> ShowS #
KillRange ConPatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ConPatInfo Source #
SetRange ConPatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> ConPatInfo -> ConPatInfo Source #
HasRange ConPatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ConPatInfo -> Range Source #
EmbPrj ConPatInfo Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatInfo -> S Int32 Source # icod_ :: ConPatInfo -> S Int32 Source # value :: Int32 -> R ConPatInfo Source #