clash-lib-1.0.1: CAES Language for Synchronous Hardware - As a Library

Clash.Core.Subst

Description

Capture-free substitution function for CoreHW

Synopsis

# Substitution into types

## Substitution environments

data TvSubst Source #

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

Instances details
 Source # Instance detailsDefined in Clash.Core.Subst Methods

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

Extend the substitution environment with a new TyVar substitution

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

Extend the substitution environment with a list of TyVar substitutions

## Applying substitutions

Substitute within a Type

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

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

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 Source #

Substitute within a TyVar. See substTy.

# Substitution into terms

## Substitution environments

data Subst Source #

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 FieldssubstInScope :: InScopeSet substTmEnv :: IdSubstEnv substTyEnv :: TvSubstEnv substGblEnv :: IdSubstEnv

An empty substitution, starting the variables currently in scope

Create a type substitution

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

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

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

Extend the substitution environment with a new Id substitution

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

Extend the substitution environment with a list of Id substitutions

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

Extend the substitution environment with a list of global Id substitutions

## Applying substitutions

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

Substitute within a Type

# Variable renaming

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

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

Alpha equality for types

Alpha equality for terms

# Orphan instances

 Source # Instance details Methods(==) :: Type -> Type -> Bool #(/=) :: Type -> Type -> Bool # Source # Instance details Methods(==) :: Term -> Term -> Bool #(/=) :: Term -> Term -> Bool # Source # Instance details Methodscompare :: Type -> Type -> Ordering #(<) :: Type -> Type -> Bool #(<=) :: Type -> Type -> Bool #(>) :: Type -> Type -> Bool #(>=) :: Type -> Type -> Bool #max :: Type -> Type -> Type #min :: Type -> Type -> Type # Source # Instance details Methodscompare :: Term -> Term -> Ordering #(<) :: Term -> Term -> Bool #(<=) :: Term -> Term -> Bool #(>) :: Term -> Term -> Bool #(>=) :: Term -> Term -> Bool #max :: Term -> Term -> Term #min :: Term -> Term -> Term #