Safe Haskell | Safe-Inferred |
---|---|
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 {}
- 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
- defInstance :: IsInstance
- defMacro :: IsMacro
- defInfo :: DeclInfo
- defTactic :: Maybe t
- mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
- mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo' t
- data DeclInfo = DeclInfo {}
- data MutualInfo = MutualInfo {}
- data LHSInfo = LHSInfo {}
- newtype PatInfo = PatRange Range
- patNoRange :: PatInfo
- data ConPatInfo = ConPatInfo {}
- data ConPatLazy
Documentation
Constructors
MetaInfo | |
Fields
|
Instances
HasRange MetaInfo Source # | |
KillRange MetaInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
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 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 :: forall r r'. (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 | |
Generic MetaInfo Source # | |
Show MetaInfo Source # | |
NFData MetaInfo Source # | |
Defined in Agda.Syntax.Info | |
Eq MetaInfo Source # | |
type Rep MetaInfo Source # | |
Defined in Agda.Syntax.Info type Rep MetaInfo = D1 ('MetaData "MetaInfo" "Agda.Syntax.Info" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "MetaInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "metaRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "metaScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo)) :*: (S1 ('MetaSel ('Just "metaNumber") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe MetaId)) :*: S1 ('MetaSel ('Just "metaNameSuggestion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))) |
Instances
HasRange ExprInfo Source # | |
KillRange ExprInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
Null 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 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 :: forall r r'. (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 # | |
NFData ExprInfo Source # | |
Defined in Agda.Syntax.Info | |
Eq ExprInfo Source # | |
Information about application
Constructors
AppInfo | |
Instances
LensOrigin AppInfo Source # | |
HasRange AppInfo Source # | |
KillRange AppInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AppInfo 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 :: forall r r'. (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 | |
Generic AppInfo Source # | |
Show AppInfo Source # | |
NFData AppInfo Source # | |
Defined in Agda.Syntax.Info | |
Eq AppInfo Source # | |
Ord AppInfo Source # | |
type Rep AppInfo Source # | |
Defined in Agda.Syntax.Info type Rep AppInfo = D1 ('MetaData "AppInfo" "Agda.Syntax.Info" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "AppInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "appRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Just "appOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Origin) :*: S1 ('MetaSel ('Just "appParens") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference)))) |
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
HasRange ModuleInfo Source # | |
Defined in Agda.Syntax.Info Methods getRange :: ModuleInfo -> Range Source # | |
KillRange ModuleInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
SetRange ModuleInfo Source # | |
Defined in Agda.Syntax.Info Methods setRange :: Range -> ModuleInfo -> ModuleInfo Source # | |
Data ModuleInfo Source # | |
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 :: forall r r'. (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 | |
Generic ModuleInfo Source # | |
Defined in Agda.Syntax.Info Associated Types type Rep ModuleInfo :: Type -> Type | |
Show ModuleInfo Source # | |
Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ModuleInfo -> ShowS show :: ModuleInfo -> String showList :: [ModuleInfo] -> ShowS | |
NFData ModuleInfo Source # | |
Defined in Agda.Syntax.Info Methods rnf :: ModuleInfo -> () | |
Eq ModuleInfo Source # | |
Defined in Agda.Syntax.Info | |
type Rep ModuleInfo Source # | |
Defined in Agda.Syntax.Info type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.Syntax.Info" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "ModuleInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "minfoRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "minfoAsTo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :*: (S1 ('MetaSel ('Just "minfoAsName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Name)) :*: (S1 ('MetaSel ('Just "minfoOpenShort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe OpenShortHand)) :*: S1 ('MetaSel ('Just "minfoDirective") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImportDirective)))))) |
Instances
HasRange LetInfo Source # | |
KillRange LetInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
Null 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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LetInfo 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 :: forall r r'. (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 # | |
NFData LetInfo Source # | |
Defined in Agda.Syntax.Info | |
Eq LetInfo Source # | |
Constructors
DefInfo | |
Fields
|
Instances
AnyIsAbstract (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info Methods anyIsAbstract :: DefInfo' t -> IsAbstract Source # | |
LensIsAbstract (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info Methods lensIsAbstract :: Lens' IsAbstract (DefInfo' t) Source # | |
HasRange (DefInfo' t) Source # | |
KillRange t => KillRange (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info Methods killRange :: KillRangeT (DefInfo' t) Source # | |
SetRange (DefInfo' t) Source # | |
Data t => Data (DefInfo' t) 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' t -> c (DefInfo' t) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (DefInfo' t) toConstr :: DefInfo' t -> Constr dataTypeOf :: DefInfo' t -> DataType dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (DefInfo' t)) dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (DefInfo' t)) gmapT :: (forall b. Data b => b -> b) -> DefInfo' t -> DefInfo' t gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefInfo' t -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefInfo' t -> r gmapQ :: (forall d. Data d => d -> u) -> DefInfo' t -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DefInfo' t -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefInfo' t -> m (DefInfo' t) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefInfo' t -> m (DefInfo' t) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefInfo' t -> m (DefInfo' t) | |
Generic (DefInfo' t) Source # | |
Show t => Show (DefInfo' t) Source # | |
NFData t => NFData (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info | |
Eq t => Eq (DefInfo' t) Source # | |
type Rep (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info type Rep (DefInfo' t) = D1 ('MetaData "DefInfo'" "Agda.Syntax.Info" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "DefInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity') :*: (S1 ('MetaSel ('Just "defAccess") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Just "defAbstract") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :*: ((S1 ('MetaSel ('Just "defInstance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :*: S1 ('MetaSel ('Just "defMacro") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsMacro)) :*: (S1 ('MetaSel ('Just "defInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclInfo) :*: S1 ('MetaSel ('Just "defTactic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe t)))))) |
mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo' t Source #
Same as mkDefInfo
but where we can also give the IsInstance
Instances
HasRange DeclInfo Source # | |
KillRange DeclInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
SetRange 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 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 :: forall r r'. (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 | |
Generic DeclInfo Source # | |
Show DeclInfo Source # | |
NFData DeclInfo Source # | |
Defined in Agda.Syntax.Info | |
Eq DeclInfo Source # | |
type Rep DeclInfo Source # | |
Defined in Agda.Syntax.Info type Rep DeclInfo = D1 ('MetaData "DeclInfo" "Agda.Syntax.Info" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "DeclInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "declName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "declRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) |
data MutualInfo Source #
Constructors
MutualInfo | |
Instances
HasRange MutualInfo Source # | |
Defined in Agda.Syntax.Info Methods getRange :: MutualInfo -> Range Source # | |
KillRange MutualInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
Null MutualInfo Source # | Default value for |
Defined in Agda.Syntax.Info | |
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 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 :: forall r r'. (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 | |
Generic MutualInfo Source # | |
Defined in Agda.Syntax.Info Associated Types type Rep MutualInfo :: Type -> Type | |
Show MutualInfo Source # | |
Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MutualInfo -> ShowS show :: MutualInfo -> String showList :: [MutualInfo] -> ShowS | |
NFData MutualInfo Source # | |
Defined in Agda.Syntax.Info Methods rnf :: MutualInfo -> () | |
Eq MutualInfo Source # | |
Defined in Agda.Syntax.Info | |
type Rep MutualInfo Source # | |
Defined in Agda.Syntax.Info type Rep MutualInfo = D1 ('MetaData "MutualInfo" "Agda.Syntax.Info" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "MutualInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mutualTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TerminationCheck Name)) :*: S1 ('MetaSel ('Just "mutualCoverageCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Just "mutualPositivityCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck) :*: S1 ('MetaSel ('Just "mutualRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) |
Constructors
LHSInfo | |
Fields |
Instances
HasRange LHSInfo Source # | |
KillRange LHSInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
Null 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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHSInfo 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 :: forall r r'. (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 | |
Generic LHSInfo Source # | |
Show LHSInfo Source # | |
NFData LHSInfo Source # | |
Defined in Agda.Syntax.Info | |
Eq LHSInfo Source # | |
type Rep LHSInfo Source # | |
Defined in Agda.Syntax.Info type Rep LHSInfo = D1 ('MetaData "LHSInfo" "Agda.Syntax.Info" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "LHSInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "lhsEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis))) |
For a general pattern we remember the source code position.
Instances
HasRange PatInfo Source # | |
KillRange PatInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
SetRange PatInfo Source # | |
Null 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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatInfo 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 :: forall r r'. (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 | |
Monoid PatInfo Source # | |
Semigroup PatInfo Source # | |
Show PatInfo Source # | |
NFData PatInfo Source # | |
Defined in Agda.Syntax.Info | |
Eq PatInfo Source # | |
patNoRange :: PatInfo Source #
Empty range for patterns.
data ConPatInfo Source #
Constructor pattern info.
Constructors
ConPatInfo | |
Fields
|
Instances
HasRange ConPatInfo Source # | |
Defined in Agda.Syntax.Info Methods getRange :: ConPatInfo -> Range Source # | |
KillRange ConPatInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
SetRange ConPatInfo Source # | |
Defined in Agda.Syntax.Info Methods setRange :: Range -> ConPatInfo -> ConPatInfo Source # | |
EmbPrj ConPatInfo Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatInfo -> S Int32 Source # icod_ :: ConPatInfo -> S Int32 Source # value :: Int32 -> R ConPatInfo Source # | |
Data ConPatInfo Source # | |
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 :: forall r r'. (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 | |
Generic ConPatInfo Source # | |
Defined in Agda.Syntax.Info Associated Types type Rep ConPatInfo :: Type -> Type | |
Show ConPatInfo Source # | |
Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatInfo -> ShowS show :: ConPatInfo -> String showList :: [ConPatInfo] -> ShowS | |
NFData ConPatInfo Source # | |
Defined in Agda.Syntax.Info Methods rnf :: ConPatInfo -> () | |
Eq ConPatInfo Source # | |
Defined in Agda.Syntax.Info | |
type Rep ConPatInfo Source # | |
Defined in Agda.Syntax.Info type Rep ConPatInfo = D1 ('MetaData "ConPatInfo" "Agda.Syntax.Info" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "ConPatInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "conPatOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConOrigin) :*: (S1 ('MetaSel ('Just "conPatInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Just "conPatLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatLazy)))) |
data ConPatLazy Source #
Has the constructor pattern a dotted (forced) constructor?
Constructors
ConPatLazy | Dotted constructor. |
ConPatEager | Ordinary constructor. |
Instances
EmbPrj ConPatLazy Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatLazy -> S Int32 Source # icod_ :: ConPatLazy -> S Int32 Source # value :: Int32 -> R ConPatLazy Source # | |
Data ConPatLazy Source # | |
Defined in Agda.Syntax.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConPatLazy -> c ConPatLazy gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConPatLazy toConstr :: ConPatLazy -> Constr dataTypeOf :: ConPatLazy -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConPatLazy) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConPatLazy) gmapT :: (forall b. Data b => b -> b) -> ConPatLazy -> ConPatLazy gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConPatLazy -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConPatLazy -> r gmapQ :: (forall d. Data d => d -> u) -> ConPatLazy -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ConPatLazy -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConPatLazy -> m ConPatLazy gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatLazy -> m ConPatLazy gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatLazy -> m ConPatLazy | |
Bounded ConPatLazy Source # | |
Defined in Agda.Syntax.Info | |
Enum ConPatLazy Source # | |
Defined in Agda.Syntax.Info Methods succ :: ConPatLazy -> ConPatLazy pred :: ConPatLazy -> ConPatLazy toEnum :: Int -> ConPatLazy fromEnum :: ConPatLazy -> Int enumFrom :: ConPatLazy -> [ConPatLazy] enumFromThen :: ConPatLazy -> ConPatLazy -> [ConPatLazy] enumFromTo :: ConPatLazy -> ConPatLazy -> [ConPatLazy] enumFromThenTo :: ConPatLazy -> ConPatLazy -> ConPatLazy -> [ConPatLazy] | |
Generic ConPatLazy Source # | |
Defined in Agda.Syntax.Info Associated Types type Rep ConPatLazy :: Type -> Type | |
Show ConPatLazy Source # | |
Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatLazy -> ShowS show :: ConPatLazy -> String showList :: [ConPatLazy] -> ShowS | |
NFData ConPatLazy Source # | |
Defined in Agda.Syntax.Info Methods rnf :: ConPatLazy -> () | |
Eq ConPatLazy Source # | |
Defined in Agda.Syntax.Info | |
Ord ConPatLazy Source # | |
Defined in Agda.Syntax.Info Methods compare :: ConPatLazy -> ConPatLazy -> Ordering (<) :: ConPatLazy -> ConPatLazy -> Bool (<=) :: ConPatLazy -> ConPatLazy -> Bool (>) :: ConPatLazy -> ConPatLazy -> Bool (>=) :: ConPatLazy -> ConPatLazy -> Bool max :: ConPatLazy -> ConPatLazy -> ConPatLazy min :: ConPatLazy -> ConPatLazy -> ConPatLazy | |
type Rep ConPatLazy Source # | |
Defined in Agda.Syntax.Info type Rep ConPatLazy = D1 ('MetaData "ConPatLazy" "Agda.Syntax.Info" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "ConPatLazy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConPatEager" 'PrefixI 'False) (U1 :: Type -> Type)) |