clash-lib-1.0.1: CAES Language for Synchronous Hardware - As a Library
Copyright(C) 2012-2016 University of Twente
2016-2017 Myrtle Software Ltd
2017-2018 Google Inc.
LicenseBSD2 (see the file LICENSE)
MaintainerChristiaan Baaij <>
Safe HaskellNone



Transformations of the Normalization process



appProp :: HasCallStack => NormRewrite Source #

Propagate arguments of application inwards; except for Lam where the argument becomes let-bound.

Note [AppProp deshadow]


(case x of
   D a b -> h a) (f x y)

rewriting this to:

let b = f x y
in  case x of
      D a b -> h a b

is very bad because b in 'h a b' is now bound by the pattern instead of the newly introduced let-binding

instead me must rewrite to:

let b1 = f x y
in  case x of
      D a b -> h a b1

Note [AppProp no-shadow invariant]


(x -> e) u

where u has a free variable named x, rewriting this to:

let x = u
in  e

would be very bad, because the let-binding suddenly captures the free variable in u. The same for:

(let x = w in e) u

where u again has a free variable x, rewriting this to:

let x = w in (e u)

would be bad because the let-binding now captures the free variable in u.

To prevent this from happening, we can either:

  1. Rename the bindings, so that they cannot capture
  2. Ensure that AppProp is only called in a context where there is no shadowing, i.e. the bindings can never never collide with the current inScopeSet.

We have gone for option 2 so that AppProp requires less computation and because AppProp is such a commonly applied transformation. This means that when normalisation starts we deshadow the expression, and when we inline global binders, we ensure that inlined expression is deshadowed taking the InScopeSet of the context into account.

caseLet :: HasCallStack => NormRewrite Source #

Lift the let-bindings out of the subject of a Case-decomposition

caseCon :: HasCallStack => NormRewrite Source #

Specialize a Case-decomposition (replace by the RHS of an alternative) if the subject is (an application of) a DataCon; or if there is only a single alternative that doesn't reference variables bound by the pattern.

Note [CaseCon deshadow]


case D (f a b) (g x y) of
  D a b -> h a

rewriting this to:

let a = f a b
in  h a

is very bad because the newly introduced let-binding now captures the free variable a in 'f a b'.

instead me must rewrite to:

let a1 = f a b
in  h a1

caseCase :: HasCallStack => NormRewrite Source #

Move a Case-decomposition from the subject of a Case-decomposition to the alternatives

caseElemNonReachable :: HasCallStack => NormRewrite Source #

Remove non-reachable alternatives. For example, consider:

data STy ty where SInt :: Int -> STy Int SBool :: Bool -> STy Bool

f :: STy ty -> ty f (SInt b) = b + 1 f (SBool True) = False f (SBool False) = True {--}

g :: STy Int -> Int g = f

f is always specialized on STy Int. The SBool alternatives are therefore unreachable. Additional information can be found at:

elemExistentials :: HasCallStack => NormRewrite Source #

Tries to eliminate existentials by using heuristics to determine what the existential should be. For example, consider Vec:

data Vec :: Nat -> Type -> Type where Nil :: Vec 0 a Cons x xs :: a -> Vec n a -> Vec (n + 1) a

Thus, null (annotated with existentials) could look like:

null :: forall n . Vec n Bool -> Bool null v = case v of Nil {n ~ 0} -> True Cons {n1:Nat} {n~n1+1} (x :: a) (xs :: Vec n1 a) -> False

When it's applied to a vector of length 5, this becomes:

null :: Vec 5 Bool -> Bool null v = case v of Nil {5 ~ 0} -> True Cons {n1:Nat} {5~n1+1} (x :: a) (xs :: Vec n1 a) -> False

This function solves n1 and replaces every occurrence with its solution. A very limited number of solutions are currently recognized: only adds (such as in the example) will be solved.

inlineNonRep :: HasCallStack => NormRewrite Source #

Inline function with a non-representable result if it's the subject of a Case-decomposition

typeSpec :: HasCallStack => NormRewrite Source #

Specialize functions on their type

nonRepSpec :: HasCallStack => NormRewrite Source #

Specialize functions on their non-representable argument

etaExpansionTL :: HasCallStack => NormRewrite Source #

Eta-expand top-level lambda's (DON'T use in a traversal!)

nonRepANF :: HasCallStack => NormRewrite Source #

Bring an application of a DataCon or Primitive in ANF, when the argument is is considered non-representable

bindConstantVar :: HasCallStack => NormRewrite Source #

Inline let-bindings when the RHS is either a local variable reference or is constant (except clock or reset generators)

constantSpec :: HasCallStack => NormRewrite Source #

Specialise functions on arguments which are constant, except when they are clock, reset generators.

makeANF :: HasCallStack => NormRewrite Source #

Turn an expression into a modified ANF-form. As opposed to standard ANF, constants do not become let-bound.

deadCode :: HasCallStack => NormRewrite Source #

Remove unused let-bindings

topLet :: HasCallStack => NormRewrite Source #

Ensure that top-level lambda's eventually bind a let-expression of which the body is a variable-reference.

recToLetRec :: HasCallStack => NormRewrite Source #

Turn a normalized recursive function, where the recursive calls only pass along the unchanged original arguments, into let-recursive function. This means that all recursive calls are replaced by the same variable reference as found in the body of the top-level let-expression.

inlineWorkFree :: HasCallStack => NormRewrite Source #

Inline work-free functions, i.e. fully applied functions that evaluate to a constant

inlineHO :: HasCallStack => NormRewrite Source #

Inline a function with functional arguments

inlineSmall :: HasCallStack => NormRewrite Source #

Inline small functions

simpleCSE :: HasCallStack => NormRewrite Source #

Simplified CSE, only works on let-bindings, works from top to bottom

reduceNonRepPrim :: HasCallStack => NormRewrite Source #

Replace primitives by their "definition" if they would lead to let-bindings with a non-representable type when a function is in ANF. This happens for example when consumes or produces a vector of non-representable elements.

Basically what this transformation does is replace a primitive the completely unrolled recursive definition that it represents. e.g.

zipWith ($) (xs :: Vec 2 (Int -> Int)) (ys :: Vec 2 Int)

is replaced by:

let (x0  :: (Int -> Int))       = case xs  of (:>) _ x xr -> x
    (xr0 :: Vec 1 (Int -> Int)) = case xs  of (:>) _ x xr -> xr
    (x1  :: (Int -> Int)(       = case xr0 of (:>) _ x xr -> x
    (y0  :: Int)                = case ys  of (:>) _ y yr -> y
    (yr0 :: Vec 1 Int)          = case ys  of (:>) _ y yr -> xr
    (y1  :: Int                 = case yr0 of (:>) _ y yr -> y
in  (($) x0 y0 :> ($) x1 y1 :> Nil)

Currently, it only handles the following functions:

  • Clash.Sized.Vector.zipWith
  • Clash.Sized.Vector.traverse#
  • Clash.Sized.Vector.fold
  • Clash.Sized.Vector.foldr
  • Clash.Sized.Vector.dfold
  • Clash.Sized.Vector.(++)
  • Clash.Sized.Vector.head
  • Clash.Sized.Vector.tail
  • Clash.Sized.Vector.last
  • Clash.Sized.Vector.init
  • Clash.Sized.Vector.unconcat
  • Clash.Sized.Vector.transpose
  • Clash.Sized.Vector.replicate
  • Clash.Sized.Vector.replace_int
  • Clash.Sized.Vector.imap
  • Clash.Sized.Vector.dtfold
  • Clash.Sized.RTree.tdfold
  • Clash.Sized.RTree.treplicate
  • Clash.Sized.Internal.BitVector.split#
  • Clash.Sized.Internal.BitVector.eq#

caseFlat :: HasCallStack => NormRewrite Source #

Flatten ridiculous case-statements generated by GHC

For case-statements in haskell of the form:

f :: Unsigned 4 -> Unsigned 4
f x = case x of
  0 -> 3
  1 -> 2
  2 -> 1
  3 -> 0

GHC generates Core that looks like:

f = (x :: Unsigned 4) -> case x == fromInteger 3 of
                            False -> case x == fromInteger 2 of
                              False -> case x == fromInteger 1 of
                                False -> case x == fromInteger 0 of
                                  False -> error "incomplete case"
                                  True  -> fromInteger 3
                                True -> fromInteger 2
                              True -> fromInteger 1
                            True -> fromInteger 0

Which would result in a priority decoder circuit where a normal decoder circuit was desired.

This transformation transforms the above Core to the saner:

f = (x :: Unsigned 4) -> case x of
       _ -> error "incomplete case"
       0 -> fromInteger 3
       1 -> fromInteger 2
       2 -> fromInteger 1
       3 -> fromInteger 0

disjointExpressionConsolidation :: HasCallStack => NormRewrite Source #

This transformation lifts applications of global binders out of alternatives of case-statements.

e.g. It converts:

case x of
  A -> f 3 y
  B -> f x x
  C -> h x


let f_arg0 = case x of {A -> 3; B -> x}
    f_arg1 = case x of {A -> y; B -> x}
    f_out  = f f_arg0 f_arg1
in  case x of
      A -> f_out
      B -> f_out
      C -> h x

inlineCleanup :: HasCallStack => NormRewrite Source #

Given a function in the desired normal form, inline all the following let-bindings:

Let-bindings with an internal name that is only used once, where it binds: * a primitive that will be translated to an HDL expression (as opposed to a HDL declaration) * a projection case-expression (1 alternative) * a data constructor

flattenLet :: HasCallStack => NormRewrite Source #

Flatten's letrecs after inlineCleanup

inlineCleanup sometimes exposes additional possibilities for caseCon, which then introduces let-bindings in what should be ANF. This transformation flattens those nested let-bindings again.

NB: must only be called in the cleaning up phase.

splitCastWork :: HasCallStack => NormRewrite Source #

Make a cast work-free by splitting the work of to a separate binding

let x = cast (f a b)
let x  = cast x'
    x' = f a b

inlineCast :: HasCallStack => NormRewrite Source #

Only inline casts that just contain a Var, because these are guaranteed work-free. These are the result of the splitCastWork transformation.

caseCast :: HasCallStack => NormRewrite Source #

Push a cast over a case into it's alternatives.

letCast :: HasCallStack => NormRewrite Source #

Push a cast over a Letrec into it's body

eliminateCastCast :: HasCallStack => NormRewrite Source #

Eliminate two back to back casts where the type going in and coming out are the same

  (cast :: b -> a) $ (cast :: a -> b) x   ==> x

argCastSpec :: HasCallStack => NormRewrite Source #

Push cast over an argument to a function into that function

This is done by specializing on the casted argument. Example: y = f (cast a) where f x = g x transforms to: y = f' a where f' x' = (x -> g x) (cast x')

The reason d'etre for this transformation is that we hope to end up with and expression where two casts are "back-to-back" after which we can eliminate them in eliminateCastCast.

etaExpandSyn :: HasCallStack => NormRewrite Source #

Eta-expand functions with a Synthesize annotation, needed to allow such functions to appear as arguments to higher-order primitives.

appPropFast :: HasCallStack => NormRewrite Source #

Unlike appProp, which propagates a single argument in an application one level down (and should be called in an innermost traversal), appPropFast tries to propagate as many arguments as possible, down as many levels as possible; and should be called in a top-down traversal.

The idea is that this reduces the number of traversals, which hopefully leads to shorter compile times.

Implementation only works if terms are fully deshadowed, see Note [AppProp deshadow]