Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Internal.Defs

Description

Extract used definitions from terms.

Synopsis

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

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