clash-lib-1.0.0: CAES Language for Synchronous Hardware - As a Library
Copyright(C) 2012-2016 University of Twente
2017 Google Inc.
LicenseBSD2 (see the file LICENSE)
MaintainerChristiaan Baaij <christiaan.baaij@gmail.com>
Safe HaskellNone
LanguageHaskell2010

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

Instances

Instances details
ClashPretty TvSubst Source # 
Instance details

Defined in Clash.Core.Subst

Methods

clashPretty :: TvSubst -> Doc () Source #

type TvSubstEnv = VarEnv Type Source #

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

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

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

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 

Fields

mkSubst :: InScopeSet -> Subst Source #

An empty substitution, starting the variables currently in scope

mkTvSubst :: InScopeSet -> VarEnv Type -> Subst Source #

Create a type substitution

extendInScopeId :: Subst -> Id -> Subst Source #

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

extendIdSubst :: Subst -> Id -> Term -> Subst Source #

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

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

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

freshenTm Source #

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

Alpha equality for types

aeqTerm :: Term -> Term -> Bool Source #

Alpha equality for terms

Orphan instances

Eq Type Source # 
Instance details

Methods

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

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

Eq Term Source # 
Instance details

Methods

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

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

Ord Type Source # 
Instance details

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

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 #