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 = DefInfo {}
- mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo
- mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo
- data DeclInfo = DeclInfo {}
- data MutualInfo = MutualInfo {}
- newtype LHSInfo = LHSRange Range
- newtype PatInfo = PatRange Range
- patNoRange :: PatInfo
- data ConPatInfo = ConPatInfo {}
- data ConPatLazy
Documentation
Constructors
MetaInfo | |
Fields
|
Instances
Eq MetaInfo Source # | |
Data MetaInfo Source # | |
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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaInfo Source # toConstr :: MetaInfo -> Constr Source # dataTypeOf :: MetaInfo -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaInfo) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaInfo) Source # gmapT :: (forall b. Data b => b -> b) -> MetaInfo -> MetaInfo Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaInfo -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaInfo -> r Source # gmapQ :: (forall d. Data d => d -> u) -> MetaInfo -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaInfo -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaInfo -> m MetaInfo Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaInfo -> m MetaInfo Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaInfo -> m MetaInfo Source # | |
Show MetaInfo Source # | |
KillRange MetaInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
HasRange MetaInfo Source # | |
Instances
Eq ExprInfo Source # | |
Data ExprInfo Source # | |
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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExprInfo Source # toConstr :: ExprInfo -> Constr Source # dataTypeOf :: ExprInfo -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExprInfo) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExprInfo) Source # gmapT :: (forall b. Data b => b -> b) -> ExprInfo -> ExprInfo Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExprInfo -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExprInfo -> r Source # gmapQ :: (forall d. Data d => d -> u) -> ExprInfo -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> ExprInfo -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExprInfo -> m ExprInfo Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExprInfo -> m ExprInfo Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExprInfo -> m ExprInfo Source # | |
Show ExprInfo Source # | |
Null ExprInfo Source # | |
KillRange ExprInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
HasRange ExprInfo Source # | |
Information about application
Constructors
AppInfo | |
Instances
Eq AppInfo Source # | |
Data AppInfo Source # | |
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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AppInfo Source # toConstr :: AppInfo -> Constr Source # dataTypeOf :: AppInfo -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AppInfo) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AppInfo) Source # gmapT :: (forall b. Data b => b -> b) -> AppInfo -> AppInfo Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AppInfo -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AppInfo -> r Source # gmapQ :: (forall d. Data d => d -> u) -> AppInfo -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> AppInfo -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AppInfo -> m AppInfo Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AppInfo -> m AppInfo Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AppInfo -> m AppInfo Source # | |
Ord AppInfo Source # | |
Defined in Agda.Syntax.Info | |
Show AppInfo Source # | |
KillRange AppInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
HasRange AppInfo Source # | |
LensOrigin 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
|
Instances
Instances
Eq LetInfo Source # | |
Data LetInfo Source # | |
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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LetInfo Source # toConstr :: LetInfo -> Constr Source # dataTypeOf :: LetInfo -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LetInfo) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LetInfo) Source # gmapT :: (forall b. Data b => b -> b) -> LetInfo -> LetInfo Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LetInfo -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LetInfo -> r Source # gmapQ :: (forall d. Data d => d -> u) -> LetInfo -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> LetInfo -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LetInfo -> m LetInfo Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LetInfo -> m LetInfo Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LetInfo -> m LetInfo Source # | |
Show LetInfo Source # | |
Null LetInfo Source # | |
KillRange LetInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
HasRange LetInfo Source # | |
Constructors
DefInfo | |
Fields
|
Instances
Eq DefInfo Source # | |
Data DefInfo Source # | |
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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefInfo Source # toConstr :: DefInfo -> Constr Source # dataTypeOf :: DefInfo -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefInfo) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefInfo) Source # gmapT :: (forall b. Data b => b -> b) -> DefInfo -> DefInfo Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefInfo -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefInfo -> r Source # gmapQ :: (forall d. Data d => d -> u) -> DefInfo -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> DefInfo -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefInfo -> m DefInfo Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefInfo -> m DefInfo Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefInfo -> m DefInfo Source # | |
Show DefInfo Source # | |
KillRange DefInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
SetRange DefInfo Source # | |
HasRange DefInfo Source # | |
mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo Source #
Same as mkDefInfo
but where we can also give the IsInstance
Instances
Eq DeclInfo Source # | |
Data DeclInfo Source # | |
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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DeclInfo Source # toConstr :: DeclInfo -> Constr Source # dataTypeOf :: DeclInfo -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DeclInfo) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DeclInfo) Source # gmapT :: (forall b. Data b => b -> b) -> DeclInfo -> DeclInfo Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DeclInfo -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DeclInfo -> r Source # gmapQ :: (forall d. Data d => d -> u) -> DeclInfo -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> DeclInfo -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DeclInfo -> m DeclInfo Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclInfo -> m DeclInfo Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclInfo -> m DeclInfo Source # | |
Show DeclInfo Source # | |
KillRange DeclInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
SetRange DeclInfo Source # | |
HasRange DeclInfo Source # | |
data MutualInfo Source #
Constructors
MutualInfo | |
Instances
Eq MutualInfo Source # | |
Defined in Agda.Syntax.Info Methods (==) :: MutualInfo -> MutualInfo -> Bool Source # (/=) :: MutualInfo -> MutualInfo -> Bool Source # | |
Data MutualInfo Source # | |
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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MutualInfo Source # toConstr :: MutualInfo -> Constr Source # dataTypeOf :: MutualInfo -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MutualInfo) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MutualInfo) Source # gmapT :: (forall b. Data b => b -> b) -> MutualInfo -> MutualInfo Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MutualInfo -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MutualInfo -> r Source # gmapQ :: (forall d. Data d => d -> u) -> MutualInfo -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> MutualInfo -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MutualInfo -> m MutualInfo Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualInfo -> m MutualInfo Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualInfo -> m MutualInfo Source # | |
Show MutualInfo Source # | |
Defined in Agda.Syntax.Info | |
Null MutualInfo Source # | Default value for |
Defined in Agda.Syntax.Info | |
KillRange MutualInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
HasRange MutualInfo Source # | |
Defined in Agda.Syntax.Info Methods getRange :: MutualInfo -> Range Source # |
Instances
Eq LHSInfo Source # | |
Data LHSInfo Source # | |
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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHSInfo Source # toConstr :: LHSInfo -> Constr Source # dataTypeOf :: LHSInfo -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHSInfo) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHSInfo) Source # gmapT :: (forall b. Data b => b -> b) -> LHSInfo -> LHSInfo Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHSInfo -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHSInfo -> r Source # gmapQ :: (forall d. Data d => d -> u) -> LHSInfo -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> LHSInfo -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHSInfo -> m LHSInfo Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSInfo -> m LHSInfo Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSInfo -> m LHSInfo Source # | |
Show LHSInfo Source # | |
Null LHSInfo Source # | |
KillRange LHSInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
HasRange LHSInfo Source # | |
For a general pattern we remember the source code position.
Instances
Eq PatInfo Source # | |
Data PatInfo Source # | |
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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatInfo Source # toConstr :: PatInfo -> Constr Source # dataTypeOf :: PatInfo -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PatInfo) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatInfo) Source # gmapT :: (forall b. Data b => b -> b) -> PatInfo -> PatInfo Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatInfo -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatInfo -> r Source # gmapQ :: (forall d. Data d => d -> u) -> PatInfo -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> PatInfo -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PatInfo -> m PatInfo Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PatInfo -> m PatInfo Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PatInfo -> m PatInfo Source # | |
Show PatInfo Source # | |
Null PatInfo Source # | |
KillRange PatInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
SetRange PatInfo Source # | |
HasRange PatInfo Source # | |
patNoRange :: PatInfo Source #
Empty range for patterns.
data ConPatInfo Source #
Constructor pattern info.
Constructors
ConPatInfo | |
Instances
data ConPatLazy Source #
Has the constructor pattern a dotted (forced) constructor?
Constructors
ConPatLazy | Dotted constructor. |
ConPatEager | Ordinary constructor. |