Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 {
  - lookupMeta :: MetaId -> Maybe Term
  - embDef :: QName -> b
  }
- class Monad m => MonadGetDefs (m :: Type -> Type) where
  - doDef :: QName -> m ()
  - doMeta :: MetaId -> m ()
- 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 |

Fields

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

#### Instances

Instances details

Monoid b => MonadGetDefs (GetDefsM b) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods doDef :: QName -> GetDefsM b () Source # doMeta :: MetaId -> GetDefsM b () Source #

class Monad m => MonadGetDefs (m :: Type -> Type) where Source #

What it takes to get the used definitions.

Methods

doDef :: QName -> m () Source #

doMeta :: MetaId -> m () Source #

#### Instances

Instances details

Monoid b => MonadGetDefs (GetDefsM b) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods doDef :: QName -> GetDefsM b () Source # doMeta :: MetaId -> GetDefsM b () Source #

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 #

#### Instances

Instances details

GetDefs MetaId Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => MetaId -> m () Source #
GetDefs Clause Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Clause -> m () Source #
GetDefs Level Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Level -> m () Source #
GetDefs PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => PlusLevel -> m () Source #
GetDefs Sort Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Sort -> m () Source #
GetDefs Telescope Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Telescope -> m () Source #
GetDefs Term Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Term -> m () Source #
GetDefs Type Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Type -> m () Source #
GetDefs String Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => String -> m () Source #
GetDefs a => GetDefs (Arg a) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Arg a -> m () Source #
GetDefs a => GetDefs (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Abs a -> m () Source #
GetDefs a => GetDefs (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Dom a -> m () Source #
GetDefs a => GetDefs (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Elim' a -> m () Source #
GetDefs a => GetDefs (Maybe a) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Maybe a -> m () Source #
GetDefs a => GetDefs [a] Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => [a] -> m () Source #
(GetDefs a, GetDefs b) => GetDefs (a, b) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => (a, b) -> m () Source #