clash-lib-1.2.0: 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
 Source # Instance detailsDefined in Clash.Core.Subst Methods

A substitution of Types for Vars

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 Var substitution

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

Extend the substitution environment with a list of Var 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 Var. See substTy.

Arguments

 :: HasCallStack => InScopeSet Variables in scope -> [TyVar] List of existentials to apply the substitution for -> [(TyVar, Type)] Substitutions -> [TyVar]

Arguments

 :: HasCallStack => InScopeSet Variables in scope -> [TyVar] List of existentials to apply the substitution for -> (TyVar, Type) Substitution -> [TyVar]

Safely substitute a type variable in a list of existentials. This function will account for cases where existentials shadow each other.

Arguments

 :: HasCallStack => InScopeSet Variables in scope -> [TyVar] List of existentials to apply the substitution for -> [(TyVar, Type)] Substitutions -> [TyVar]

Safely substitute type variables in a list of existentials. This function will account for cases where existentials shadow each other.

# Substitution into terms

## Substitution environments

data Subst Source #

A substitution environment containing containing both Var and Var substitutions.

Some invariants apply to how you use the substitution:

1. The InScopeSet contains at least those Vars and Vars 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 Var to the in-scope set: as a side effect, remove any existing substitutions for it.

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

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

Extend the substitution environment with a new Var substitution

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

Extend the substitution environment with a list of Var substitutions

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

Extend the substitution environment with a list of global Var substitutions

## Applying substitutions

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

Substitute within a Type

Arguments

 :: HasCallStack => Doc () -> Subst The substitution -> (Pat, Term) The alternative in which to apply the substitution -> (Pat, Term)

Substitute within a case-alternative

# Variable renaming

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

deShadowAlt :: HasCallStack => InScopeSet -> (Pat, Term) -> (Pat, Term) Source #

Ensure that non of the binders in an alternative shadow each-other, nor conflict with the 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.

Arguments

 :: HasCallStack => InScopeSet Current InScopeSet -> [LetBinding] Bindings of the let-expression -> Term The body of the let-expression -> ([LetBinding], Term) Deshadowed let-bindings, where let-bound expressions and the let-body properly reference the renamed variables

Ensure that non of the let-bindings of a let-expression shadow w.r.t the in-scope set

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