clash-lib-1.8.4: Clash: a functional hardware description language - As a library

Copyright | (C) 2012-2016 University of Twente 2017 Google Inc. 2021 QBayLogic B.V.
License | BSD2 (see the file LICENSE)
Maintainer | QBayLogic B.V. <devops@qbaylogic.com>
Safe Haskell | None
Language | Haskell2010

Clash.Core.Subst

Contents

- Substitution into types
  - Substitution environments
  - Applying substitutions
- Substitution into terms
  - Substitution environments
  - Applying substitutions
- Variable renaming
- Alpha equivalence
- Structural equivalence
- Orphan instances

Description

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
- maybeSubstTm :: HasCallStack => Doc () -> Maybe 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 -> Bind Term -> Term -> (Bind Term, Term)
- aeqType :: Type -> Type -> Bool
- aeqTerm :: Term -> Term -> Bool
- eqTerm :: Term -> Term -> Bool
- eqType :: Type -> Type -> Bool

# 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

ClashPretty TvSubst Source # |
Instance details Defined in Clash.Core.Subst Methods clashPretty :: TvSubst -> Doc () Source #

type TvSubstEnv = VarEnv Type Source #

A substitution of `Type`s for `TyVar`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 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 `TvSubst`s 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`.

substGlobalsInExistentials Source #

Arguments

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

substInExistentials Source #

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.

substInExistentialsList Source #

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 `Id` and `TyVar` substitutions.

Some invariants apply to how you use the substitution:

1. The `InScopeSet` contains at least those `Id`s and `TyVar`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.
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 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 `Id`s 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 `Term`

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

Substitute within a `Term`. Just return original term if given substitution is Nothing.

substAlt Source #

Arguments

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

Substitute within a case-alternative

substId :: HasCallStack => Subst -> Id -> Id Source #

# 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

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.

deshadowLetExpr Source #

Arguments

:: HasCallStack |
=> InScopeSet | Current InScopeSet
-> Bind Term | Bindings of the let-expression
-> Term | The body of the let-expression
-> (Bind Term, 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

aeqType :: Type -> Type -> Bool Source #

Alpha equality for types

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

Alpha equality for terms

# Structural equivalence

eqTerm :: Term -> Term -> Bool Source #

Structural equality on `Term`

eqType :: Type -> Type -> Bool Source #

Structural equality on `Type`

# Orphan instances

Eq Term Source # |
Instance details Methods (==) :: Term -> Term -> Bool Source # (/=) :: Term -> Term -> Bool Source #
Eq Type Source # |
Instance details Methods (==) :: Type -> Type -> Bool Source # (/=) :: Type -> Type -> Bool Source #
Ord Term Source # |
Instance details Methods compare :: Term -> Term -> Ordering Source # (<) :: Term -> Term -> Bool Source # (<=) :: Term -> Term -> Bool Source # (>) :: Term -> Term -> Bool Source # (>=) :: Term -> Term -> Bool Source # max :: Term -> Term -> Term Source # min :: Term -> Term -> Term Source #
Ord Type Source # |
Instance details Methods compare :: Type -> Type -> Ordering Source # (<) :: Type -> Type -> Bool Source # (<=) :: Type -> Type -> Bool Source # (>) :: Type -> Type -> Bool Source # (>=) :: Type -> Type -> Bool Source # max :: Type -> Type -> Type Source # min :: Type -> Type -> Type Source #
(TypeError (('Text "A broken implementation of Hashable Term has been " ':<>: 'Text "removed in Clash 1.4.7. If this is an issue for you, please submit ") ':<>: 'Text "an issue report at https://github.com/clash-lang/clash-compiler/issues.") :: Constraint) => Hashable Term Source # |
Instance details Methods hashWithSalt :: Int -> Term -> Int Source # hash :: Term -> Int Source #