| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Internal.Defs
Description
Extract used definitions from terms.
Synopsis
- getDefs' :: (GetDefs a, Monoid b) => (MetaId -> Maybe Term) -> (QName -> b) -> a -> b
- type GetDefsM b = ReaderT (GetDefsEnv b) (Writer b)
- data GetDefsEnv b = GetDefsEnv {}
- class Monad m => MonadGetDefs (m :: Type -> Type) where
- class GetDefs a where
- getDefs :: MonadGetDefs m => a -> m ()
Documentation
getDefs' :: (GetDefs a, Monoid b) => (MetaId -> Maybe Term) -> (QName -> b) -> a -> b Source #
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 | |
class Monad m => MonadGetDefs (m :: Type -> Type) where Source #
What it takes to get the used definitions.
class GetDefs a where Source #
Getting the used definitions.
Note: in contrast to foldTerm
getDefs also collects from sorts in terms.
Thus, this is not an instance of foldTerm.
Minimal complete definition
Nothing
Methods
getDefs :: MonadGetDefs m => a -> m () Source #
default getDefs :: forall m (f :: Type -> Type) b. (MonadGetDefs m, Foldable f, GetDefs b, f b ~ a) => a -> m () Source #