Clash.Core.Subst

Capture-free substitution function for CoreHW

Substitution into types

Substitution environments

data TvSubst

Type substitution

The following invariants must hold:

1. The InScopeSet is needed only to guide the generation of fresh uniques
2. In particular, the kind of the type variables in the InScopeSet is not relevant.
3. The substitution is only applied once

Note [Apply Once]

We might instantiate forall a b. ty with the types [a, b] or [b, a]. So the substitution might go like [a -> b, b -> a]. A similar situation arises in terms when we find a redex like (a -> b -> e) b a. Then we also end up with a substitution that permutes variables. Other variations happen to; for example [a -> (a,b)].

SO A TvSubst MUST BE APPLIED PRECISELY ONCE, OR THINGS MIGHT LOOP

Note [The substitution invariant]

When calling (substTy subst ty) it should be the case that the InScopeSet is a superset of both:

• The free variables of the range of the substitution
• The free variables of ty minus the domain of the substitution

Constructors

TvSubst InScopeSet TvSubstEnv

Instances

ClashPretty TvSubst

Defined in Clash.Core.Subst

Methods

clashPretty :: TvSubst -> Doc ()

type TvSubstEnv = VarEnv Type

A substitution of Types for TyVars

Note [Extending the TvSubstEnv] See TvSubst for the invariants that must hold

This invariant allows a short-cut when the subst env is empty: if the TvSubstEnv is empty, i.e. nullVarEnv TvSubstEnv holds, then (substTy subst ty) does nothing.

For example, consider:

(a -> b(a ~ Int) -> ... b ...) Int

We substitute Int for a. The Unique of b does not change, but nevertheless we add b to the TvSubstEnv because b's kind does change

This invariant has several consequences:

• In substTyVarBndr, we extend TvSubstEnv if the unique has changed, or if the kind has changed
• In substTyVar, we do not need to consult the InScopeSet; the TvSubstEnv is enough
• In substTy, we can short-circuit when TvSubstEnv is empty

extendTvSubst :: Subst -> TyVar -> Type -> Subst

Extend the substitution environment with a new TyVar substitution

extendTvSubstList :: Subst -> [(TyVar, Type)] -> Subst

Extend the substitution environment with a list of TyVar substitutions

Applying substitutions

substTy :: HasCallStack => Subst -> Type -> Type

Substitute within a Type

The substitution has to satisfy the invariant described in TvSubsts Note [The substitution environment]

substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type

Type substitution, see zipTvSubst

Works only if the domain of the substitution is superset of the type being substituted into

substTyInVar :: HasCallStack => Subst -> Var a -> Var a

Substitute within a TyVar. See substTy.

Substitution into terms

Substitution environments

data Subst

A substitution environment containing containing both Id and TyVar substitutions.

Some invariants apply to how you use the substitution:

1. The InScopeSet contains at least those Ids and TyVars that will be in scope after applying the substitution to a term. Precisely, the in-scope set must be a superset of the free variables of the substitution range that might possibly clash with locally-bound variables in the thing being substituted in.
2. You may only apply the substitution once. See TvSubst

There are various ways of setting up the in-scope set such that the first of of these invariants holds:

• Arrange that the in-scope set really is all the things in scope
• Arrange that it's the free vars of the range of the substitution
• Make it empty, if you know that all the free variables of the substitution are fresh, and hence can´t possibly clash

Constructors

Subst

Fields

• substInScope :: InScopeSet
• substTmEnv :: IdSubstEnv
• substTyEnv :: TvSubstEnv
• substGblEnv :: IdSubstEnv

mkSubst :: InScopeSet -> Subst

An empty substitution, starting the variables currently in scope

mkTvSubst :: InScopeSet -> VarEnv Type -> Subst

Create a type substitution

extendInScopeId :: Subst -> Id -> Subst

Add an Id to the in-scope set: as a side effect, remove any existing substitutions for it.

extendInScopeIdList :: Subst -> [Id] -> Subst

Add Ids to the in-scope set. See also extendInScopeId

extendIdSubst :: Subst -> Id -> Term -> Subst

Extend the substitution environment with a new Id substitution

extendIdSubstList :: Subst -> [(Id, Term)] -> Subst

Extend the substitution environment with a list of Id substitutions

extendGblSubstList :: Subst -> [(Id, Term)] -> Subst

Extend the substitution environment with a list of global Id substitutions

Applying substitutions

substTm :: HasCallStack => Doc () -> Subst -> Term -> Term

Substitute within a Type

Variable renaming

deShadowTerm :: HasCallStack => InScopeSet -> Term -> Term

Ensure that non of the binders in an expression shadow each-other, nor conflict with he in-scope set

freshenTm

Arguments

:: InScopeSet

Current set of variables in scope

-> Term

-> (InScopeSet, Term)

A much stronger variant of deShadowTerm that ensures that all bound variables are unique.

Also returns an extended InScopeSet additionally containing the (renamed) unique bound variables of the term.

Alpha equivalence

aeqType :: Type -> Type -> Bool

Alpha equality for types

aeqTerm :: Term -> Term -> Bool

Alpha equality for terms

Orphan instances

Eq Type

Methods

(==) :: Type -> Type -> Bool

(/=) :: Type -> Type -> Bool

Eq Term

Methods

(==) :: Term -> Term -> Bool

(/=) :: Term -> Term -> Bool

Ord Type

Methods

compare :: Type -> Type -> Ordering

(<) :: Type -> Type -> Bool

(<=) :: Type -> Type -> Bool

(>) :: Type -> Type -> Bool

(>=) :: Type -> Type -> Bool

max :: Type -> Type -> Type

min :: Type -> Type -> Type

Ord Term

Methods

compare :: Term -> Term -> Ordering

(<) :: Term -> Term -> Bool

(<=) :: Term -> Term -> Bool

(>) :: Term -> Term -> Bool

(>=) :: Term -> Term -> Bool

max :: Term -> Term -> Term

min :: Term -> Term -> Term