Clash.Normalize.Transformations

Transformations of the Normalization process

Documentation

caseLet :: HasCallStack => NormRewrite

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

caseCon :: HasCallStack => NormRewrite

caseCase :: HasCallStack => NormRewrite

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

caseElemNonReachable :: HasCallStack => NormRewrite

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: https://github.com/clash-lang/clash-compiler/pull/465

elemExistentials :: HasCallStack => NormRewrite

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

Inline function with a non-representable result if it's the subject of a Case-decomposition. It's a custom topdown traversal that -for efficiency reasons- does not explore alternative of cases whose subject triggered an inlineNonRepWorker.

inlineOrLiftNonRep :: HasCallStack => NormRewrite

typeSpec :: HasCallStack => NormRewrite

Specialize functions on their type

nonRepSpec :: HasCallStack => NormRewrite

Specialize functions on their non-representable argument

etaExpansionTL :: HasCallStack => NormRewrite

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

nonRepANF :: HasCallStack => NormRewrite

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

bindConstantVar :: HasCallStack => NormRewrite

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

constantSpec :: HasCallStack => NormRewrite

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

makeANF :: HasCallStack => NormRewrite

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

deadCode :: HasCallStack => NormRewrite

Remove unused let-bindings

topLet :: HasCallStack => NormRewrite

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

recToLetRec :: HasCallStack => NormRewrite

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

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

inlineHO :: HasCallStack => NormRewrite

Inline a function with functional arguments

inlineSmall :: HasCallStack => NormRewrite

Inline small functions

simpleCSE :: HasCallStack => NormRewrite

Simplified CSE, only works on let-bindings, does an inverse topological sort of the let-bindings and then works from top to bottom

XXX: Check whether inverse top-sort followed by single traversal removes as many binders as the previous "apply-until-fixpoint" approach in the presence of recursive groups in the let-bindings. If not but just for checking whether changes to transformation affect the eventual size of the circuit, it would be really helpful if we tracked circuit size in the regression/test suite. On the two examples that were tested, Reducer and PipelinesViaFolds, this new version of CSE removed the same amount of let-binders.

reduceConst :: HasCallStack => NormRewrite

reduceNonRepPrim :: HasCallStack => NormRewrite

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 Clash.Size.Vector.map 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.map
• 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#

Note [Unroll shouldSplit types] 1. Certain higher-order functions over Vec, such as map, have specialized code-paths to turn them into generate-for loops in HDL, instead of having to having to unroll/inline their recursive definitions, e.g. Clash.Sized.Vector.map

1. Clash, in general, translates Haskell product types to VHDL records. This mostly works out fine, there is however one exception: certain synthesis tools, and some HDL simulation tools (like verilator), do not like it when the clock (and certain other global control signals) is contained in a record type; they want them to be separate inputs to the entity/module. And Clash actually does some transformations to try to ensure that values of type Clock do not end up in a VHDL record type.

The problem is that the transformations in 2. never took into account the specialized code-paths in 1. Making the code-paths in 1. aware of the transformations in 2. is really not worth the effort for such a niche case. It's easier to just unroll the recursive definitions.

See https://github.com/clash-lang/clash-compiler/issues/1606

caseFlat :: HasCallStack => NormRewrite

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

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

into:

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

removeUnusedExpr :: HasCallStack => NormRewrite

inlineCleanup :: HasCallStack => NormRewrite

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 * I/O actions

inlineBndrsCleanup

Arguments

:: HasCallStack

=> InScopeSet

Current InScopeSet

-> VarEnv ((Id, Term), VarEnv Int)

Original let-binders with their free variables (+ #occurrences), that we want to inline

-> VarEnv ((Id, Term), VarEnv Int, Mark)

Processed let-binders with their free variables and a tag to mark the progress: * Temp: Will eventually form a recursive cycle * Done: Processed, non-recursive * Rec: Processed, recursive

-> [((Id, Term), VarEnv Int)]

The let-binders with their free variables (+ #occurrences), that we want to keep

-> [(Id, Term)]

Used by inlineCleanup to inline binders that we want to inline into the binders that we want to keep.

flattenLet :: HasCallStack => NormRewrite

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

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

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

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

letCast :: HasCallStack => NormRewrite

Push a cast over a Letrec into it's body

eliminateCastCast :: HasCallStack => NormRewrite

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

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

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

appPropFast :: HasCallStack => NormRewrite

Propagate arguments of application inwards; except for Lam where the argument becomes let-bound. 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.

Note [AppProp no shadowing]

Case 1.

Imagine:

(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 deshadow w.r.t. the new variable and rewrite to:

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

Case 2.

Imagine

(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. To prevent this from happening we over-approximate and check whether x is in the current InScopeSet, and deshadow if that's the case, i.e. we then rewrite to:

let x1 = u in e [x:=x1]

Case 3.

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 unconditionally deshadow the function part of the application w.r.t. the free variables in the argument part of the application. It is okay to over-approximate in this case and deshadow w.r.t the current InScopeSet.

separateArguments :: HasCallStack => NormRewrite

Split apart (global) function arguments that contain types that we want to separate off, e.g. Clocks. Works on both the definition side (i.e. the lambda), and the call site (i.e. the application of the global variable). e.g. turns

f :: (Clock System, Reset System) -> Signal System Int

into

f :: Clock System -> Reset System -> Signal System Int

separateLambda

Arguments

:: TyConMap

-> TransformContext

-> Id

Lambda binder

-> Term

Lambda body

-> Maybe Term

If lambda is split up, this function returns a Just containing the new term

Worker function of separateArguments.

xOptimize :: HasCallStack => NormRewrite

Remove all undefined alternatives from case expressions, replacing them with the value of another defined alternative. If there is one defined alternative, the entire expression is replaced with that alternative. If there are no defined alternatives, the entire expression is replaced with a call to errorX.

e.g. It converts

case x of D1 a -> f a D2 -> undefined D3 -> undefined

to

let subj = x a = case subj of D1 a -> field0 in f a

where fieldN is an internal variable referring to the nth argument of a data constructor.

setupMultiResultPrim :: HasCallStack => NormRewrite

inlineSimIO :: HasCallStack => NormRewrite

Inline anything of type SimIO: IO actions cannot be shared