ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Internal.Defs

Extract used definitions from terms.

2 types
2 classes
1 value

PackageAgda-2.7.0.1
Exports5
LanguageHaskell2010
LicenceMIT
SourceDefs.hs

valuegetDefs'

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

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

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

datadata GetDefsEnv b

Constructors

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

Instances1MonadGetDefs

Monoid b => MonadGetDefs (GetDefsM b)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs

classclass Monad m => MonadGetDefs (m :: Type -> Type) where

What it takes to get the used definitions.

Methods

doDef :: QName -> m ()
doMeta :: MetaId -> m ()

Instances1MonadGetDefs

Monoid b => MonadGetDefs (GetDefsM b)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs

classclass 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 ()

Instances16GetDefs, …

GetDefs MetaIdDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs ClauseDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs LevelDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs PlusLevelDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs SortDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs TelescopeDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs TermDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs TypeDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs StringDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs a => GetDefs (Arg a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs a => GetDefs (Abs a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs a => GetDefs (Dom a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs a => GetDefs (Elim' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs a => GetDefs (Maybe a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
GetDefs a => GetDefs [a]Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
(GetDefs a, GetDefs b) => GetDefs (a, b)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs