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)

class Monad m => MonadGetDefs m where

What it takes to get the used definitions.

Methods

doDef :: QName -> m ()

doMeta :: MetaId -> m ()

Instances

Monoid b => MonadGetDefs (GetDefsM b)

class GetDefs a where

Getting the used definitions.

Methods

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

Instances

GetDefs ClauseBody

GetDefs Clause

GetDefs MetaId

GetDefs LevelAtom

GetDefs PlusLevel

GetDefs Level

GetDefs Sort

GetDefs Type

GetDefs Term

GetDefs a => GetDefs [a]

GetDefs a => GetDefs (Maybe a)

GetDefs c => GetDefs (ArgInfo c)

GetDefs a => GetDefs (Abs a)

GetDefs a => GetDefs (Elim' a)

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

(GetDefs c, GetDefs a) => GetDefs (Dom c a)

(GetDefs c, GetDefs a) => GetDefs (Arg c a)