Copyright | (C) 2012-2016 University of Twente 2017 Google Inc. |
---|---|
License | BSD2 (see the file LICENSE) |
Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com> |
Safe Haskell | None |
Language | Haskell2010 |
Capture-free substitution function for CoreHW
Synopsis
- data TvSubst = TvSubst InScopeSet TvSubstEnv
- type TvSubstEnv = VarEnv Type
- extendTvSubst :: Subst -> TyVar -> Type -> Subst
- extendTvSubstList :: Subst -> [(TyVar, Type)] -> Subst
- substTy :: HasCallStack => Subst -> Type -> Type
- substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type
- substTyInVar :: HasCallStack => Subst -> Var a -> Var a
- substGlobalsInExistentials :: HasCallStack => InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
- substInExistentials :: HasCallStack => InScopeSet -> [TyVar] -> (TyVar, Type) -> [TyVar]
- substInExistentialsList :: HasCallStack => InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
- data Subst = Subst {
- substInScope :: InScopeSet
- substTmEnv :: IdSubstEnv
- substTyEnv :: TvSubstEnv
- substGblEnv :: IdSubstEnv
- mkSubst :: InScopeSet -> Subst
- mkTvSubst :: InScopeSet -> VarEnv Type -> Subst
- extendInScopeId :: Subst -> Id -> Subst
- extendInScopeIdList :: Subst -> [Id] -> Subst
- extendIdSubst :: Subst -> Id -> Term -> Subst
- extendIdSubstList :: Subst -> [(Id, Term)] -> Subst
- extendGblSubstList :: Subst -> [(Id, Term)] -> Subst
- substTm :: HasCallStack => Doc () -> Subst -> Term -> Term
- substAlt :: HasCallStack => Doc () -> Subst -> (Pat, Term) -> (Pat, Term)
- substId :: HasCallStack => Subst -> Id -> Id
- deShadowTerm :: HasCallStack => InScopeSet -> Term -> Term
- deShadowAlt :: HasCallStack => InScopeSet -> (Pat, Term) -> (Pat, Term)
- freshenTm :: InScopeSet -> Term -> (InScopeSet, Term)
- deshadowLetExpr :: HasCallStack => InScopeSet -> [LetBinding] -> Term -> ([LetBinding], Term)
- aeqType :: Type -> Type -> Bool
- aeqTerm :: Term -> Term -> Bool
Substitution into types
Substitution environments
Type substitution
The following invariants must hold:
- The
InScopeSet
is needed only to guide the generation of fresh uniques - In particular, the kind of the type variables in the
InScopeSet
is not relevant. - 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
ClashPretty TvSubst Source # | |
Defined in Clash.Core.Subst clashPretty :: TvSubst -> Doc () Source # |
type TvSubstEnv = VarEnv Type Source #
A substitution of Type
s for Var
s
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 theInScopeSet
; 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 Var
substitution
extendTvSubstList :: Subst -> [(TyVar, Type)] -> Subst Source #
Extend the substitution environment with a list of Var
substitutions
Applying substitutions
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 #
substGlobalsInExistentials Source #
:: HasCallStack | |
=> InScopeSet | Variables in scope |
-> [TyVar] | List of existentials to apply the substitution for |
-> [(TyVar, Type)] | Substitutions |
-> [TyVar] |
:: 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.
substInExistentialsList Source #
:: 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
A substitution environment containing containing both Var
and Var
substitutions.
Some invariants apply to how you use the substitution:
- The
InScopeSet
contains at least thoseVar
s andVar
s 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. - 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
Subst | |
|
mkSubst :: InScopeSet -> Subst Source #
An empty substitution, starting the variables currently in scope
extendInScopeId :: Subst -> Id -> Subst Source #
Add an Var
to the in-scope set: as a side effect, remove any existing
substitutions for it.
extendInScopeIdList :: Subst -> [Id] -> Subst Source #
Add Var
s to the in-scope set. See also extendInScopeId
extendIdSubst :: Subst -> Id -> Term -> Subst Source #
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
:: HasCallStack | |
=> Doc () | |
-> Subst | The substitution |
-> (Pat, Term) | The alternative in which to apply the substitution |
-> (Pat, Term) |
Substitute within a case-alternative
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
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
:: 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.
:: 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