Agda.Syntax.Internal.Defs

Extract used definitions from terms.

Documentation

getDefs' :: (GetDefs a, Monoid b) => (MetaId -> Maybe Term) -> (QName -> b) -> a -> b

getDefs' lookup emb a extracts all used definitions (functions, data/record types) from a, embedded into a monoid via emb. Instantiations of meta variables are obtained via lookup.

Typical monoid instances would be [QName] or Set QName. Note that emb can also choose to discard a used definition by mapping to the unit of the monoid.

type GetDefsM b = ReaderT (GetDefsEnv b) (Writer b)

Inputs to and outputs of getDefs' are organized as a monad.

data GetDefsEnv b

Constructors

GetDefsEnv

Fields

• lookupMeta :: MetaId -> Maybe Term
• embDef :: QName -> b

Instances

Monoid b => MonadGetDefs (GetDefsM b)

Methods

doDef :: QName -> GetDefsM b ()

doMeta :: MetaId -> GetDefsM b ()

class Monad m => MonadGetDefs m where

What it takes to get the used definitions.

Minimal complete definition

doDef, doMeta

Methods

doDef :: QName -> m ()

doMeta :: MetaId -> m ()

Instances

Monoid b => MonadGetDefs (GetDefsM b)

Methods

doDef :: QName -> GetDefsM b ()

doMeta :: MetaId -> GetDefsM b ()

class GetDefs a where

Getting the used definitions.

Note: in contrast to foldTerm getDefs also collects from sorts in terms. Thus, this is not an instance of foldTerm.

Methods

getDefs :: MonadGetDefs m => a -> m ()

getDefs :: (MonadGetDefs m, Foldable f, GetDefs b, f b ~ a) => a -> m ()

Instances

GetDefs MetaId

Methods

getDefs :: MonadGetDefs m => MetaId -> m ()

GetDefs Clause

Methods

getDefs :: MonadGetDefs m => Clause -> m ()

GetDefs LevelAtom

Methods

getDefs :: MonadGetDefs m => LevelAtom -> m ()

GetDefs PlusLevel

Methods

getDefs :: MonadGetDefs m => PlusLevel -> m ()

GetDefs Level

Methods

getDefs :: MonadGetDefs m => Level -> m ()

GetDefs Sort

Methods

getDefs :: MonadGetDefs m => Sort -> m ()

GetDefs Type

Methods

getDefs :: MonadGetDefs m => Type -> m ()

GetDefs Term

Methods

getDefs :: MonadGetDefs m => Term -> m ()

GetDefs a => GetDefs [a]

Methods

getDefs :: MonadGetDefs m => [a] -> m ()

GetDefs a => GetDefs (Maybe a)

Methods

getDefs :: MonadGetDefs m => Maybe a -> m ()

GetDefs a => GetDefs (Dom a)

Methods

getDefs :: MonadGetDefs m => Dom a -> m ()

GetDefs a => GetDefs (Arg a)

Methods

getDefs :: MonadGetDefs m => Arg a -> m ()

GetDefs a => GetDefs (Abs a)

Methods

getDefs :: MonadGetDefs m => Abs a -> m ()

GetDefs a => GetDefs (Elim' a)

Methods

getDefs :: MonadGetDefs m => Elim' a -> m ()

(GetDefs a, GetDefs b) => GetDefs (a, b)

Methods

getDefs :: MonadGetDefs m => (a, b) -> m ()