Safe Haskell	Safe-Inferred
Language	Haskell2010

PlutusCore.Subst

Synopsis

substTyVarA ∷ Applicative f ⇒ (tyname → f (Maybe (Type tyname uni ann))) → Type tyname uni ann → f (Type tyname uni ann)
substVarA ∷ Applicative f ⇒ (name → f (Maybe (Term tyname name uni fun ann))) → Term tyname name uni fun ann → f (Term tyname name uni fun ann)
substTyVar ∷ (tyname → Maybe (Type tyname uni ann)) → Type tyname uni ann → Type tyname uni ann
substVar ∷ (name → Maybe (Term tyname name uni fun ann)) → Term tyname name uni fun ann → Term tyname name uni fun ann
termSubstNamesM ∷ Monad m ⇒ (name → m (Maybe (Term tyname name uni fun ann))) → Term tyname name uni fun ann → m (Term tyname name uni fun ann)
termSubstTyNamesM ∷ Monad m ⇒ (tyname → m (Maybe (Type tyname uni ann))) → Term tyname name uni fun ann → m (Term tyname name uni fun ann)
typeSubstTyNamesM ∷ Monad m ⇒ (tyname → m (Maybe (Type tyname uni ann))) → Type tyname uni ann → m (Type tyname uni ann)
termSubstNames ∷ (name → Maybe (Term tyname name uni fun ann)) → Term tyname name uni fun ann → Term tyname name uni fun ann
termSubstTyNames ∷ (tyname → Maybe (Type tyname uni ann)) → Term tyname name uni fun ann → Term tyname name uni fun ann
typeSubstTyNames ∷ (tyname → Maybe (Type tyname uni ann)) → Type tyname uni ann → Type tyname uni ann
typeSubstClosedType ∷ Eq tyname ⇒ tyname → Type tyname uni a → Type tyname uni a → Type tyname uni a
termSubstClosedType ∷ Eq tyname ⇒ tyname → Type tyname uni a → Term tyname name uni fun a → Term tyname name uni fun a
termSubstClosedTerm ∷ Eq name ⇒ name → Term tyname name uni fun a → Term tyname name uni fun a → Term tyname name uni fun a
typeMapNames ∷ ∀ tyname tyname' uni ann. (tyname → tyname') → Type tyname uni ann → Type tyname' uni ann
termMapNames ∷ ∀ tyname tyname' name name' uni fun ann. (tyname → tyname') → (name → name') → Term tyname name uni fun ann → Term tyname' name' uni fun ann
programMapNames ∷ ∀ tyname tyname' name name' uni fun ann. (tyname → tyname') → (name → name') → Program tyname name uni fun ann → Program tyname' name' uni fun ann
fvTerm ∷ HasUnique name unique ⇒ Traversal' (Term tyname name uni fun ann) name
ftvTerm ∷ HasUnique tyname unique ⇒ Traversal' (Term tyname name uni fun ann) tyname
ftvTy ∷ HasUnique tyname unique ⇒ Traversal' (Type tyname uni ann) tyname
ftvTyCtx ∷ HasUnique tyname unique ⇒ UniqueSet unique → Traversal' (Type tyname uni ann) tyname
vTerm ∷ Fold (Term tyname name uni fun ann) name
tvTerm ∷ Fold (Term tyname name uni fun ann) tyname
tvTy ∷ Fold (Type tyname uni ann) tyname
purely ∷ ((a → Identity b) → c → Identity d) → (a → b) → c → d

Documentation

substTyVarA ∷ Applicative f ⇒ (tyname → f (Maybe (Type tyname uni ann))) → Type tyname uni ann → f (Type tyname uni ann) Source #

Applicatively replace a type variable using the given function.

substVarA ∷ Applicative f ⇒ (name → f (Maybe (Term tyname name uni fun ann))) → Term tyname name uni fun ann → f (Term tyname name uni fun ann) Source #

Applicatively replace a variable using the given function.

substTyVar ∷ (tyname → Maybe (Type tyname uni ann)) → Type tyname uni ann → Type tyname uni ann Source #

Replace a type variable using the given function.

substVar ∷ (name → Maybe (Term tyname name uni fun ann)) → Term tyname name uni fun ann → Term tyname name uni fun ann Source #

Replace a variable using the given function.

termSubstNamesM ∷ Monad m ⇒ (name → m (Maybe (Term tyname name uni fun ann))) → Term tyname name uni fun ann → m (Term tyname name uni fun ann) Source #

Naively monadically substitute names using the given function (i.e. do not substitute binders).

termSubstTyNamesM ∷ Monad m ⇒ (tyname → m (Maybe (Type tyname uni ann))) → Term tyname name uni fun ann → m (Term tyname name uni fun ann) Source #

Naively monadically substitute type names using the given function (i.e. do not substitute binders).

typeSubstTyNamesM ∷ Monad m ⇒ (tyname → m (Maybe (Type tyname uni ann))) → Type tyname uni ann → m (Type tyname uni ann) Source #

Naively monadically substitute type names (i.e. do not substitute binders). INLINE is important here because the function is too polymorphic (determined from profiling)

termSubstNames ∷ (name → Maybe (Term tyname name uni fun ann)) → Term tyname name uni fun ann → Term tyname name uni fun ann Source #

Naively substitute names using the given function (i.e. do not substitute binders).

termSubstTyNames ∷ (tyname → Maybe (Type tyname uni ann)) → Term tyname name uni fun ann → Term tyname name uni fun ann Source #

Naively substitute type names using the given function (i.e. do not substitute binders).

typeSubstTyNames ∷ (tyname → Maybe (Type tyname uni ann)) → Type tyname uni ann → Type tyname uni ann Source #

Naively substitute type names (i.e. do not substitute binders).

typeSubstClosedType ∷ Eq tyname ⇒ tyname → Type tyname uni a → Type tyname uni a → Type tyname uni a Source #

Substitute the given closed Kind for the given type variable in the given Kind. Does not descend under binders that bind the same variable as the one we're substituting for (since from there that variable is no longer free). The resulting Term may and likely will not satisfy global uniqueness.

termSubstClosedType ∷ Eq tyname ⇒ tyname → Type tyname uni a → Term tyname name uni fun a → Term tyname name uni fun a Source #

Substitute the given closed Kind for the given type variable in the given Term. Does not descend under binders that bind the same variable as the one we're substituting for (since from there that variable is no longer free). The resulting Term may and likely will not satisfy global uniqueness.

termSubstClosedTerm ∷ Eq name ⇒ name → Term tyname name uni fun a → Term tyname name uni fun a → Term tyname name uni fun a Source #

Substitute the given closed Term for the given term variable in the given Term. Does not descend under binders that bind the same variable as the one we're substituting for (since from there that variable is no longer free). The resulting Term may and likely will not satisfy global uniqueness.

typeMapNames ∷ ∀ tyname tyname' uni ann. (tyname → tyname') → Type tyname uni ann → Type tyname' uni ann Source #

termMapNames ∷ ∀ tyname tyname' name name' uni fun ann. (tyname → tyname') → (name → name') → Term tyname name uni fun ann → Term tyname' name' uni fun ann Source #

programMapNames ∷ ∀ tyname tyname' name name' uni fun ann. (tyname → tyname') → (name → name') → Program tyname name uni fun ann → Program tyname' name' uni fun ann Source #

fvTerm ∷ HasUnique name unique ⇒ Traversal' (Term tyname name uni fun ann) name Source #

Get all the free term variables in a term.

ftvTerm ∷ HasUnique tyname unique ⇒ Traversal' (Term tyname name uni fun ann) tyname Source #

Get all the free type variables in a term.

ftvTy ∷ HasUnique tyname unique ⇒ Traversal' (Type tyname uni ann) tyname Source #

Get all the free type variables in a type.

ftvTyCtx ∷ HasUnique tyname unique ⇒ UniqueSet unique → Traversal' (Type tyname uni ann) tyname Source #

vTerm ∷ Fold (Term tyname name uni fun ann) name Source #

Get all the term variables in a term.

tvTerm ∷ Fold (Term tyname name uni fun ann) tyname Source #

Get all the type variables in a term.

tvTy ∷ Fold (Type tyname uni ann) tyname Source #

Get all the type variables in a type.

purely ∷ ((a → Identity b) → c → Identity d) → (a → b) → c → d Source #