Agda.Syntax.Info

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.

Documentation

data MetaInfo

Constructors

MetaInfo

Fields

• metaRange :: Range
• metaScope :: ScopeInfo
• metaNumber :: Maybe MetaId
• metaNameSuggestion :: String

Instances

HasRange MetaInfo

Defined in Agda.Syntax.Info

Methods

getRange :: MetaInfo -> Range

KillRange MetaInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT MetaInfo

Data MetaInfo

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

Defined in Agda.Syntax.Info

Associated Types

type Rep MetaInfo :: Type -> Type

Methods

from :: MetaInfo -> Rep MetaInfo x

to :: Rep MetaInfo x -> MetaInfo

Show MetaInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> MetaInfo -> ShowS

show :: MetaInfo -> String

showList :: [MetaInfo] -> ShowS

NFData MetaInfo

Defined in Agda.Syntax.Info

Methods

rnf :: MetaInfo -> ()

Eq MetaInfo

Defined in Agda.Syntax.Info

Methods

(==) :: MetaInfo -> MetaInfo -> Bool

(/=) :: MetaInfo -> MetaInfo -> Bool

type Rep MetaInfo

Defined in Agda.Syntax.Info

type Rep MetaInfo = D1 ('MetaData "MetaInfo" "Agda.Syntax.Info" "Agda-2.6.2.1.20220320-inplace" '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))))

emptyMetaInfo :: MetaInfo

newtype ExprInfo

Constructors

ExprRange Range

Instances

HasRange ExprInfo

Defined in Agda.Syntax.Info

Methods

getRange :: ExprInfo -> Range

KillRange ExprInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT ExprInfo

Null ExprInfo

Defined in Agda.Syntax.Info

Methods

empty :: ExprInfo

null :: ExprInfo -> Bool

Data ExprInfo

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

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ExprInfo -> ShowS

show :: ExprInfo -> String

showList :: [ExprInfo] -> ShowS

NFData ExprInfo

Defined in Agda.Syntax.Info

Methods

rnf :: ExprInfo -> ()

Eq ExprInfo

Defined in Agda.Syntax.Info

Methods

(==) :: ExprInfo -> ExprInfo -> Bool

(/=) :: ExprInfo -> ExprInfo -> Bool

exprNoRange :: ExprInfo

data AppInfo

Information about application

Constructors

AppInfo

Fields

• appRange :: Range
• appOrigin :: Origin
• appParens :: ParenPreference

  Do we prefer a lambda argument with or without parens?

Instances

LensOrigin AppInfo

Defined in Agda.Syntax.Info

Methods

getOrigin :: AppInfo -> Origin

setOrigin :: Origin -> AppInfo -> AppInfo

mapOrigin :: (Origin -> Origin) -> AppInfo -> AppInfo

HasRange AppInfo

Defined in Agda.Syntax.Info

Methods

getRange :: AppInfo -> Range

KillRange AppInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT AppInfo

Data AppInfo

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 :: 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

Defined in Agda.Syntax.Info

Associated Types

type Rep AppInfo :: Type -> Type

Methods

from :: AppInfo -> Rep AppInfo x

to :: Rep AppInfo x -> AppInfo

Show AppInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> AppInfo -> ShowS

show :: AppInfo -> String

showList :: [AppInfo] -> ShowS

NFData AppInfo

Defined in Agda.Syntax.Info

Methods

rnf :: AppInfo -> ()

Eq AppInfo

Defined in Agda.Syntax.Info

Methods

(==) :: AppInfo -> AppInfo -> Bool

(/=) :: AppInfo -> AppInfo -> Bool

Ord AppInfo

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

type Rep AppInfo

Defined in Agda.Syntax.Info

type Rep AppInfo = D1 ('MetaData "AppInfo" "Agda.Syntax.Info" "Agda-2.6.2.1.20220320-inplace" '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

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

HasRange ModuleInfo

Defined in Agda.Syntax.Info

Methods

getRange :: ModuleInfo -> Range

KillRange ModuleInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT ModuleInfo

SetRange ModuleInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> ModuleInfo -> ModuleInfo

Data ModuleInfo

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

Defined in Agda.Syntax.Info

Associated Types

type Rep ModuleInfo :: Type -> Type

Methods

from :: ModuleInfo -> Rep ModuleInfo x

to :: Rep ModuleInfo x -> ModuleInfo

Show ModuleInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ModuleInfo -> ShowS

show :: ModuleInfo -> String

showList :: [ModuleInfo] -> ShowS

NFData ModuleInfo

Defined in Agda.Syntax.Info

Methods

rnf :: ModuleInfo -> ()

Eq ModuleInfo

Defined in Agda.Syntax.Info

Methods

(==) :: ModuleInfo -> ModuleInfo -> Bool

(/=) :: ModuleInfo -> ModuleInfo -> Bool

type Rep ModuleInfo

Defined in Agda.Syntax.Info

type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.Syntax.Info" "Agda-2.6.2.1.20220320-inplace" '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))))))

newtype LetInfo

Constructors

LetRange Range

Instances

HasRange LetInfo

Defined in Agda.Syntax.Info

Methods

getRange :: LetInfo -> Range

KillRange LetInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT LetInfo

Null LetInfo

Defined in Agda.Syntax.Info

Methods

empty :: LetInfo

null :: LetInfo -> Bool

Data LetInfo

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 :: 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

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> LetInfo -> ShowS

show :: LetInfo -> String

showList :: [LetInfo] -> ShowS

NFData LetInfo

Defined in Agda.Syntax.Info

Methods

rnf :: LetInfo -> ()

Eq LetInfo

Defined in Agda.Syntax.Info

Methods

(==) :: LetInfo -> LetInfo -> Bool

(/=) :: LetInfo -> LetInfo -> Bool

data DefInfo' t

Constructors

DefInfo

Fields

• defFixity :: Fixity'
• defAccess :: Access
• defAbstract :: IsAbstract
• defInstance :: IsInstance
• defMacro :: IsMacro
• defInfo :: DeclInfo
• defTactic :: Maybe t

Instances

AnyIsAbstract (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

anyIsAbstract :: DefInfo' t -> IsAbstract

LensIsAbstract (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

lensIsAbstract :: Lens' IsAbstract (DefInfo' t)

HasRange (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

getRange :: DefInfo' t -> Range

KillRange t => KillRange (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT (DefInfo' t)

SetRange (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> DefInfo' t -> DefInfo' t

Data t => Data (DefInfo' t)

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)

Defined in Agda.Syntax.Info

Associated Types

type Rep (DefInfo' t) :: Type -> Type

Methods

from :: DefInfo' t -> Rep (DefInfo' t) x

to :: Rep (DefInfo' t) x -> DefInfo' t

Show t => Show (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> DefInfo' t -> ShowS

show :: DefInfo' t -> String

showList :: [DefInfo' t] -> ShowS

NFData t => NFData (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

rnf :: DefInfo' t -> ()

Eq t => Eq (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

(==) :: DefInfo' t -> DefInfo' t -> Bool

(/=) :: DefInfo' t -> DefInfo' t -> Bool

type Rep (DefInfo' t)

Defined in Agda.Syntax.Info

type Rep (DefInfo' t) = D1 ('MetaData "DefInfo'" "Agda.Syntax.Info" "Agda-2.6.2.1.20220320-inplace" '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))))))

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

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

Same as mkDefInfo but where we can also give the IsInstance

data DeclInfo

Constructors

DeclInfo

Fields

• declName :: Name
• declRange :: Range

Instances

HasRange DeclInfo

Defined in Agda.Syntax.Info

Methods

getRange :: DeclInfo -> Range

KillRange DeclInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT DeclInfo

SetRange DeclInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> DeclInfo -> DeclInfo

Data DeclInfo

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

Defined in Agda.Syntax.Info

Associated Types

type Rep DeclInfo :: Type -> Type

Methods

from :: DeclInfo -> Rep DeclInfo x

to :: Rep DeclInfo x -> DeclInfo

Show DeclInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> DeclInfo -> ShowS

show :: DeclInfo -> String

showList :: [DeclInfo] -> ShowS

NFData DeclInfo

Defined in Agda.Syntax.Info

Methods

rnf :: DeclInfo -> ()

Eq DeclInfo

Defined in Agda.Syntax.Info

Methods

(==) :: DeclInfo -> DeclInfo -> Bool

(/=) :: DeclInfo -> DeclInfo -> Bool

type Rep DeclInfo

Defined in Agda.Syntax.Info

type Rep DeclInfo = D1 ('MetaData "DeclInfo" "Agda.Syntax.Info" "Agda-2.6.2.1.20220320-inplace" '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

Constructors

MutualInfo

Fields

• mutualTerminationCheck :: TerminationCheck Name
• mutualCoverageCheck :: CoverageCheck
• mutualPositivityCheck :: PositivityCheck
• mutualRange :: Range

Instances

HasRange MutualInfo

Defined in Agda.Syntax.Info

Methods

getRange :: MutualInfo -> Range

KillRange MutualInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT MutualInfo

Null MutualInfo

Default value for MutualInfo.

Defined in Agda.Syntax.Info

Methods

empty :: MutualInfo

null :: MutualInfo -> Bool

Data MutualInfo

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

Defined in Agda.Syntax.Info

Associated Types

type Rep MutualInfo :: Type -> Type

Methods

from :: MutualInfo -> Rep MutualInfo x

to :: Rep MutualInfo x -> MutualInfo

Show MutualInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> MutualInfo -> ShowS

show :: MutualInfo -> String

showList :: [MutualInfo] -> ShowS

NFData MutualInfo

Defined in Agda.Syntax.Info

Methods

rnf :: MutualInfo -> ()

Eq MutualInfo

Defined in Agda.Syntax.Info

Methods

(==) :: MutualInfo -> MutualInfo -> Bool

(/=) :: MutualInfo -> MutualInfo -> Bool

type Rep MutualInfo

Defined in Agda.Syntax.Info

type Rep MutualInfo = D1 ('MetaData "MutualInfo" "Agda.Syntax.Info" "Agda-2.6.2.1.20220320-inplace" '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))))

data LHSInfo

Constructors

LHSInfo

Fields

• lhsRange :: Range
• lhsEllipsis :: ExpandedEllipsis

Instances

HasRange LHSInfo

Defined in Agda.Syntax.Info

Methods

getRange :: LHSInfo -> Range

KillRange LHSInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT LHSInfo

Null LHSInfo

Defined in Agda.Syntax.Info

Methods

empty :: LHSInfo

null :: LHSInfo -> Bool

Data LHSInfo

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 :: 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

Defined in Agda.Syntax.Info

Associated Types

type Rep LHSInfo :: Type -> Type

Methods

from :: LHSInfo -> Rep LHSInfo x

to :: Rep LHSInfo x -> LHSInfo

Show LHSInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> LHSInfo -> ShowS

show :: LHSInfo -> String

showList :: [LHSInfo] -> ShowS

NFData LHSInfo

Defined in Agda.Syntax.Info

Methods

rnf :: LHSInfo -> ()

Eq LHSInfo

Defined in Agda.Syntax.Info

Methods

(==) :: LHSInfo -> LHSInfo -> Bool

(/=) :: LHSInfo -> LHSInfo -> Bool

type Rep LHSInfo

Defined in Agda.Syntax.Info

type Rep LHSInfo = D1 ('MetaData "LHSInfo" "Agda.Syntax.Info" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "LHSInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "lhsEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis)))

newtype PatInfo

For a general pattern we remember the source code position.

Constructors

PatRange Range

Instances

HasRange PatInfo

Defined in Agda.Syntax.Info

Methods

getRange :: PatInfo -> Range

KillRange PatInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT PatInfo

SetRange PatInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> PatInfo -> PatInfo

Null PatInfo

Defined in Agda.Syntax.Info

Methods

empty :: PatInfo

null :: PatInfo -> Bool

Data PatInfo

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 :: 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

Defined in Agda.Syntax.Info

Methods

mempty :: PatInfo

mappend :: PatInfo -> PatInfo -> PatInfo

mconcat :: [PatInfo] -> PatInfo

Semigroup PatInfo

Defined in Agda.Syntax.Info

Methods

(<>) :: PatInfo -> PatInfo -> PatInfo

sconcat :: NonEmpty PatInfo -> PatInfo

stimes :: Integral b => b -> PatInfo -> PatInfo

Show PatInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> PatInfo -> ShowS

show :: PatInfo -> String

showList :: [PatInfo] -> ShowS

NFData PatInfo

Defined in Agda.Syntax.Info

Methods

rnf :: PatInfo -> ()

Eq PatInfo

Defined in Agda.Syntax.Info

Methods

(==) :: PatInfo -> PatInfo -> Bool

(/=) :: PatInfo -> PatInfo -> Bool

patNoRange :: PatInfo

Empty range for patterns.

data ConPatInfo

Constructor pattern info.

Constructors

ConPatInfo

Fields

• conPatOrigin :: ConOrigin

  Does this pattern come form the eta-expansion of an implicit pattern?

• conPatInfo :: PatInfo
• conPatLazy :: ConPatLazy

Instances

HasRange ConPatInfo

Defined in Agda.Syntax.Info

Methods

getRange :: ConPatInfo -> Range

KillRange ConPatInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT ConPatInfo

SetRange ConPatInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> ConPatInfo -> ConPatInfo

EmbPrj ConPatInfo

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatInfo -> S Int32

icod_ :: ConPatInfo -> S Int32

value :: Int32 -> R ConPatInfo

Data ConPatInfo

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

Defined in Agda.Syntax.Info

Associated Types

type Rep ConPatInfo :: Type -> Type

Methods

from :: ConPatInfo -> Rep ConPatInfo x

to :: Rep ConPatInfo x -> ConPatInfo

Show ConPatInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ConPatInfo -> ShowS

show :: ConPatInfo -> String

showList :: [ConPatInfo] -> ShowS

NFData ConPatInfo

Defined in Agda.Syntax.Info

Methods

rnf :: ConPatInfo -> ()

Eq ConPatInfo

Defined in Agda.Syntax.Info

Methods

(==) :: ConPatInfo -> ConPatInfo -> Bool

(/=) :: ConPatInfo -> ConPatInfo -> Bool

type Rep ConPatInfo

Defined in Agda.Syntax.Info

type Rep ConPatInfo = D1 ('MetaData "ConPatInfo" "Agda.Syntax.Info" "Agda-2.6.2.1.20220320-inplace" '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

Has the constructor pattern a dotted (forced) constructor?

Constructors

ConPatLazy

Dotted constructor.

ConPatEager

Ordinary constructor.

Instances

EmbPrj ConPatLazy

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatLazy -> S Int32

icod_ :: ConPatLazy -> S Int32

value :: Int32 -> R ConPatLazy

Data ConPatLazy

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

Defined in Agda.Syntax.Info

Methods

minBound :: ConPatLazy

maxBound :: ConPatLazy

Enum ConPatLazy

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

Defined in Agda.Syntax.Info

Associated Types

type Rep ConPatLazy :: Type -> Type

Methods

from :: ConPatLazy -> Rep ConPatLazy x

to :: Rep ConPatLazy x -> ConPatLazy

Show ConPatLazy

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ConPatLazy -> ShowS

show :: ConPatLazy -> String

showList :: [ConPatLazy] -> ShowS

NFData ConPatLazy

Defined in Agda.Syntax.Info

Methods

rnf :: ConPatLazy -> ()

Eq ConPatLazy

Defined in Agda.Syntax.Info

Methods

(==) :: ConPatLazy -> ConPatLazy -> Bool

(/=) :: ConPatLazy -> ConPatLazy -> Bool

Ord ConPatLazy

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

Defined in Agda.Syntax.Info

type Rep ConPatLazy = D1 ('MetaData "ConPatLazy" "Agda.Syntax.Info" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "ConPatLazy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConPatEager" 'PrefixI 'False) (U1 :: Type -> Type))