| Safe Haskell | None |
|---|
Agda.Syntax.Internal.Defs
Description
Extract used definitions from terms.
- getDefs' :: (GetDefs a, Monoid b) => (MetaId -> Maybe Term) -> (QName -> b) -> a -> b
- type GetDefsM b = ReaderT (GetDefsEnv b) (Writer b)
- data GetDefsEnv b = GetDefsEnv {
- lookupMeta :: MetaId -> Maybe Term
- embDef :: QName -> b
- class Monad m => MonadGetDefs m where
- class GetDefs a where
- getDefs :: MonadGetDefs m => a -> m ()
Documentation
getDefs' :: (GetDefs a, Monoid b) => (MetaId -> Maybe Term) -> (QName -> b) -> a -> bSource
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)Source
Inputs to and outputs of getDefs' are organized as a monad.
data GetDefsEnv b Source
Constructors
| GetDefsEnv | |
Fields
| |
Instances
| Monoid b => MonadGetDefs (GetDefsM b) |
class Monad m => MonadGetDefs m whereSource
What it takes to get the used definitions.
Instances
| Monoid b => MonadGetDefs (GetDefsM b) |
Getting the used definitions.
Methods
getDefs :: MonadGetDefs m => a -> m ()Source
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) |