+ \todo{Don't split registers in this image?}
+ \placeexample[here][ex:NormalComplete]{Simple architecture consisting of an adder and a
+ subtractor.}
+ \startcombination[2*1]
+ {\typebufferlam{NormalComplete}}{Core description in normal form.}
+ {\boxedgraphic{NormalComplete}}{The architecture described by the normal form.}
+ \stopcombination
+
+
+
+ \subsection[sec:normalization:intendednormalform]{Intended normal form definition}
+ Now we have some intuition for the normal form, we can describe how we want
+ the normal form to look like in a slightly more formal manner. The following
+ EBNF-like description captures most of the intended structure (and
+ generates a subset of \GHC's core format).
+
+ There are two things missing: Cast expressions are sometimes
+ allowed by the prototype, but not specified here and the below
+ definition allows uses of state that cannot be translated to \VHDL
+ properly. These two problems are discussed in
+ \in{section}[sec:normalization:castproblems] and
+ \in{section}[sec:normalization:stateproblems] respectively.
+
+ Some clauses have an expression listed behind them in parentheses.
+ These are conditions that need to apply to the clause. The
+ predicates used there (\lam{lvar()}, \lam{representable()},
+ \lam{gvar()}) will be defined in
+ \in{section}[sec:normalization:predicates].
+
+ An expression is in normal form if it matches the first
+ definition, \emph{normal}.
+
+ \todo{Fix indentation}
+ \startbuffer[IntendedNormal]
+ \italic{normal} := \italic{lambda}
+ \italic{lambda} := λvar.\italic{lambda} (representable(var))
+ | \italic{toplet}
+ \italic{toplet} := letrec [\italic{binding}...] in var (representable(var))
+ \italic{binding} := var = \italic{rhs} (representable(rhs))
+ -- State packing and unpacking by coercion
+ | var0 = var1 ▶ State ty (lvar(var1))
+ | var0 = var1 ▶ ty (var1 :: State ty ∧ lvar(var1))
+ \italic{rhs} := \italic{userapp}
+ | \italic{builtinapp}
+ -- Extractor case
+ | case var of C a0 ... an -> ai (lvar(var))
+ -- Selector case
+ | case var of (lvar(var))
+ [ DEFAULT -> var ] (lvar(var))
+ C0 w0,0 ... w0,n -> var0
+ \vdots
+ Cm wm,0 ... wm,n -> varm (\forall{}i \forall{}j, wi,j \neq vari, lvar(vari))
+ \italic{userapp} := \italic{userfunc}
+ | \italic{userapp} {userarg}
+ \italic{userfunc} := var (gvar(var))
+ \italic{userarg} := var (lvar(var))
+ \italic{builtinapp} := \italic{builtinfunc}
+ | \italic{builtinapp} \italic{builtinarg}
+ \italic{built-infunc} := var (bvar(var))
+ \italic{built-inarg} := var (representable(var) ∧ lvar(var))
+ | \italic{partapp} (partapp :: a -> b)
+ | \italic{coreexpr} (¬representable(coreexpr) ∧ ¬(coreexpr :: a -> b))
+ \italic{partapp} := \italic{userapp}
+ | \italic{builtinapp}
+ \stopbuffer
+
+ \placedefinition[][def:IntendedNormal]{Definition of the intended nnormal form using an \small{EBNF}-like syntax.}
+ {\defref{intended normal form definition}
+ \typebufferlam{IntendedNormal}}
+
+ When looking at such a program from a hardware perspective, the
+ top level lambda abstractions define the input ports. Lambda
+ abstractions cannot appear anywhere else. The variable reference
+ in the body of the recursive let expression is the output port.
+ Most function applications bound by the let expression define a
+ component instantiation, where the input and output ports are
+ mapped to local signals or arguments. Some of the others use a
+ built-in construction (\eg the \lam{case} expression) or call a
+ built-in function (\eg \lam{+} or \lam{map}). For these, a
+ hardcoded \small{VHDL} translation is available.
+
+ \section[sec:normalization:transformation]{Transformation notation}
+ To be able to concisely present transformations, we use a specific format
+ for them. It is a simple format, similar to one used in logic reasoning.
+
+ Such a transformation description looks like the following.
+
+ \starttrans
+ <context conditions>
+ ~
+ <original expression>
+ -------------------------- <expression conditions>
+ <transformed expression>
+ ~
+ <context additions>
+ \stoptrans
+
+ This format describes a transformation that applies to \lam{<original
+ expression>} and transforms it into \lam{<transformed expression>}, assuming
+ that all conditions are satisfied. In this format, there are a number of placeholders
+ in pointy brackets, most of which should be rather obvious in their meaning.
+ Nevertheless, we will more precisely specify their meaning below:
+
+ \startdesc{<original expression>} The expression pattern that will be matched
+ against (subexpressions of) the expression to be transformed. We call this a
+ pattern, because it can contain \emph{placeholders} (variables), which match
+ any expression or binder. Any such placeholder is said to be \emph{bound} to
+ the expression it matches. It is convention to use an uppercase letter (\eg
+ \lam{M} or \lam{E}) to refer to any expression (including a simple variable
+ reference) and lowercase letters (\eg \lam{v} or \lam{b}) to refer to
+ (references to) binders.
+
+ For example, the pattern \lam{a + B} will match the expression
+ \lam{v + (2 * w)} (binding \lam{a} to \lam{v} and \lam{B} to
+ \lam{(2 * w)}), but not \lam{(2 * w) + v}.
+ \stopdesc
+
+ \startdesc{<expression conditions>}
+ These are extra conditions on the expression that is matched. These
+ conditions can be used to further limit the cases in which the
+ transformation applies, commonly to prevent a transformation from
+ causing a loop with itself or another transformation.
+
+ Only if these conditions are \emph{all} satisfied, the transformation
+ applies.
+ \stopdesc
+
+ \startdesc{<context conditions>}
+ These are a number of extra conditions on the context of the function. In
+ particular, these conditions can require some (other) top level function to be
+ present, whose value matches the pattern given here. The format of each of
+ these conditions is: \lam{binder = <pattern>}.
+
+ Typically, the binder is some placeholder bound in the \lam{<original
+ expression>}, while the pattern contains some placeholders that are used in
+ the \lam{transformed expression}.
+
+ Only if a top level binder exists that matches each binder and pattern,
+ the transformation applies.
+ \stopdesc
+
+ \startdesc{<transformed expression>}
+ This is the expression template that is the result of the transformation. If, looking
+ at the above three items, the transformation applies, the \lam{<original
+ expression>} is completely replaced by the \lam{<transformed expression>}.
+ We call this a template, because it can contain placeholders, referring to
+ any placeholder bound by the \lam{<original expression>} or the
+ \lam{<context conditions>}. The resulting expression will have those
+ placeholders replaced by the values bound to them.
+
+ Any binder (lowercase) placeholder that has no value bound to it yet will be
+ bound to (and replaced with) a fresh binder.
+ \stopdesc
+
+ \startdesc{<context additions>}
+ These are templates for new functions to be added to the context.
+ This is a way to let a transformation create new top level
+ functions.
+
+ Each addition has the form \lam{binder = template}. As above, any
+ placeholder in the addition is replaced with the value bound to it, and any
+ binder placeholder that has no value bound to it yet will be bound to (and
+ replaced with) a fresh binder.
+ \stopdesc
+
+ To understand this notation better, the step by step application of
+ the η-abstraction transformation to a simple \small{ALU} will be
+ shown. Consider η-abstraction, which is a common transformation from
+ labmda calculus, described using above notation as follows:
+
+ \starttrans
+ E \lam{E :: a -> b}
+ -------------- \lam{E} does not occur on a function position in an application
+ λx.E x \lam{E} is not a lambda abstraction.
+ \stoptrans
+
+ η-abstraction is a well known transformation from lambda calculus. What
+ this transformation does, is take any expression that has a function type
+ and turn it into a lambda expression (giving an explicit name to the
+ argument). There are some extra conditions that ensure that this
+ transformation does not apply infinitely (which are not necessarily part
+ of the conventional definition of η-abstraction).
+
+ Consider the following function, in Core notation, which is a fairly obvious way to specify a
+ simple \small{ALU} (Note that it is not yet in normal form, but
+ \in{example}[ex:AddSubAlu] shows the normal form of this function).
+ The parentheses around the \lam{+} and \lam{-} operators are
+ commonly used in Haskell to show that the operators are used as
+ normal functions, instead of \emph{infix} operators (\eg, the
+ operators appear before their arguments, instead of in between).
+
+ \startlambda
+ alu :: Bit -> Word -> Word -> Word
+ alu = λopcode. case opcode of
+ Low -> (+)
+ High -> (-)
+ \stoplambda
+
+ There are a few subexpressions in this function to which we could possibly
+ apply the transformation. Since the pattern of the transformation is only
+ the placeholder \lam{E}, any expression will match that. Whether the
+ transformation applies to an expression is thus solely decided by the
+ conditions to the right of the transformation.
+
+ We will look at each expression in the function in a top down manner. The
+ first expression is the entire expression the function is bound to.
+
+ \startlambda
+ λopcode. case opcode of
+ Low -> (+)
+ High -> (-)
+ \stoplambda
+
+ As said, the expression pattern matches this. The type of this expression is
+ \lam{Bit -> Word -> Word -> Word}, which matches \lam{a -> b} (Note that in
+ this case \lam{a = Bit} and \lam{b = Word -> Word -> Word}).
+
+ Since this expression is at top level, it does not occur at a function
+ position of an application. However, The expression is a lambda abstraction,
+ so this transformation does not apply.
+
+ The next expression we could apply this transformation to, is the body of
+ the lambda abstraction:
+
+ \startlambda
+ case opcode of
+ Low -> (+)
+ High -> (-)
+ \stoplambda
+
+ The type of this expression is \lam{Word -> Word -> Word}, which again
+ matches \lam{a -> b}. The expression is the body of a lambda expression, so
+ it does not occur at a function position of an application. Finally, the
+ expression is not a lambda abstraction but a case expression, so all the
+ conditions match. There are no context conditions to match, so the
+ transformation applies.
+
+ By now, the placeholder \lam{E} is bound to the entire expression. The
+ placeholder \lam{x}, which occurs in the replacement template, is not bound
+ yet, so we need to generate a fresh binder for that. Let us use the binder
+ \lam{a}. This results in the following replacement expression:
+
+ \startlambda
+ λa.(case opcode of
+ Low -> (+)
+ High -> (-)) a
+ \stoplambda
+
+ Continuing with this expression, we see that the transformation does not
+ apply again (it is a lambda expression). Next we look at the body of this
+ lambda abstraction:
+
+ \startlambda
+ (case opcode of
+ Low -> (+)
+ High -> (-)) a
+ \stoplambda
+
+ Here, the transformation does apply, binding \lam{E} to the entire
+ expression (which has type \lam{Word -> Word}) and binding \lam{x}
+ to the fresh binder \lam{b}, resulting in the replacement:
+
+ \startlambda
+ λb.(case opcode of
+ Low -> (+)
+ High -> (-)) a b
+ \stoplambda
+
+ The transformation does not apply to this lambda abstraction, so we
+ look at its body. For brevity, we will put the case expression on one line from
+ now on.
+
+ \startlambda
+ (case opcode of Low -> (+); High -> (-)) a b
+ \stoplambda
+
+ The type of this expression is \lam{Word}, so it does not match \lam{a -> b}
+ and the transformation does not apply. Next, we have two options for the
+ next expression to look at: The function position and argument position of
+ the application. The expression in the argument position is \lam{b}, which
+ has type \lam{Word}, so the transformation does not apply. The expression in
+ the function position is:
+
+ \startlambda
+ (case opcode of Low -> (+); High -> (-)) a
+ \stoplambda
+
+ Obviously, the transformation does not apply here, since it occurs in
+ function position (which makes the second condition false). In the same
+ way the transformation does not apply to both components of this
+ expression (\lam{case opcode of Low -> (+); High -> (-)} and \lam{a}), so
+ we will skip to the components of the case expression: The scrutinee and
+ both alternatives. Since the opcode is not a function, it does not apply
+ here.
+
+ The first alternative is \lam{(+)}. This expression has a function type
+ (the operator still needs two arguments). It does not occur in function
+ position of an application and it is not a lambda expression, so the
+ transformation applies.
+
+ We look at the \lam{<original expression>} pattern, which is \lam{E}.
+ This means we bind \lam{E} to \lam{(+)}. We then replace the expression
+ with the \lam{<transformed expression>}, replacing all occurences of
+ \lam{E} with \lam{(+)}. In the \lam{<transformed expression>}, the This gives us the replacement expression:
+ \lam{λx.(+) x} (A lambda expression binding \lam{x}, with a body that
+ applies the addition operator to \lam{x}).
+
+ The complete function then becomes:
+ \startlambda
+ (case opcode of Low -> λa1.(+) a1; High -> (-)) a
+ \stoplambda
+
+ Now the transformation no longer applies to the complete first alternative
+ (since it is a lambda expression). It does not apply to the addition
+ operator again, since it is now in function position in an application. It
+ does, however, apply to the application of the addition operator, since
+ that is neither a lambda expression nor does it occur in function
+ position. This means after one more application of the transformation, the
+ function becomes:
+
+ \startlambda
+ (case opcode of Low -> λa1.λb1.(+) a1 b1; High -> (-)) a
+ \stoplambda
+
+ The other alternative is left as an exercise to the reader. The final
+ function, after applying η-abstraction until it does no longer apply is:
+
+ \startlambda
+ alu :: Bit -> Word -> Word -> Word
+ alu = λopcode.λa.b. (case opcode of
+ Low -> λa1.λb1 (+) a1 b1
+ High -> λa2.λb2 (-) a2 b2) a b
+ \stoplambda
+
+ \subsection{Transformation application}
+ In this chapter we define a number of transformations, but how will we apply
+ these? As stated before, our normal form is reached as soon as no
+ transformation applies anymore. This means our application strategy is to
+ simply apply any transformation that applies, and continuing to do that with
+ the result of each transformation.
+
+ In particular, we define no particular order of transformations. Since
+ transformation order should not influence the resulting normal form,
+ this leaves the implementation free to choose any application order that
+ results in an efficient implementation. Unfortunately this is not
+ entirely true for the current set of transformations. See
+ \in{section}[sec:normalization:non-determinism] for a discussion of this
+ problem.
+
+ When applying a single transformation, we try to apply it to every (sub)expression
+ in a function, not just the top level function body. This allows us to
+ keep the transformation descriptions concise and powerful.
+
+ \subsection{Definitions}
+ A \emph{global variable} is any variable (binder) that is bound at the
+ top level of a program, or an external module. A \emph{local variable} is any
+ other variable (\eg, variables local to a function, which can be bound by
+ lambda abstractions, let expressions and pattern matches of case
+ alternatives). This is a slightly different notion of global versus
+ local than what \small{GHC} uses internally, but for our purposes
+ the distinction \GHC makes is not useful.
+ \defref{global variable} \defref{local variable}
+
+ A \emph{hardware representable} (or just \emph{representable}) type or value
+ is (a value of) a type that we can generate a signal for in hardware. For
+ example, a bit, a vector of bits, a 32 bit unsigned word, etc. Values that are
+ not runtime representable notably include (but are not limited to): Types,
+ dictionaries, functions.
+ \defref{representable}
+
+ A \emph{built-in function} is a function supplied by the Cλash framework, whose
+ implementation is not valid Cλash. The implementation is of course valid
+ Haskell, for simulation, but it is not expressable in Cλash.
+ \defref{built-in function} \defref{user-defined function}
+
+ For these functions, Cλash has a \emph{built-in hardware translation}, so calls
+ to these functions can still be translated. These are functions like
+ \lam{map}, \lam{hwor} and \lam{length}.
+
+ A \emph{user-defined} function is a function for which we do have a Cλash
+ implementation available.
+
+ \subsubsection[sec:normalization:predicates]{Predicates}
+ Here, we define a number of predicates that can be used below to concisely
+ specify conditions.
+
+ \emph{gvar(expr)} is true when \emph{expr} is a variable that references a
+ global variable. It is false when it references a local variable.
+
+ \emph{lvar(expr)} is the complement of \emph{gvar}; it is true when \emph{expr}
+ references a local variable, false when it references a global variable.
+
+ \emph{representable(expr)} is true when \emph{expr} is \emph{representable}.
+
+ \subsection[sec:normalization:uniq]{Binder uniqueness}
+ A common problem in transformation systems, is binder uniqueness. When not
+ considering this problem, it is easy to create transformations that mix up
+ bindings and cause name collisions. Take for example, the following core
+ expression:
+
+ \startlambda
+ (λa.λb.λc. a * b * c) x c
+ \stoplambda
+
+ By applying β-reduction (see \in{section}[sec:normalization:beta]) once,
+ we can simplify this expression to:
+
+ \startlambda
+ (λb.λc. x * b * c) c
+ \stoplambda
+
+ Now, we have replaced the \lam{a} binder with a reference to the \lam{x}
+ binder. No harm done here. But note that we see multiple occurences of the
+ \lam{c} binder. The first is a binding occurence, to which the second refers.
+ The last, however refers to \emph{another} instance of \lam{c}, which is
+ bound somewhere outside of this expression. Now, if we would apply beta
+ reduction without taking heed of binder uniqueness, we would get:
+
+ \startlambda
+ λc. x * c * c
+ \stoplambda
+
+ This is obviously not what was supposed to happen! The root of this problem is
+ the reuse of binders: Identical binders can be bound in different,
+ but overlapping scopes. Any variable reference in those
+ overlapping scopes then refers to the variable bound in the inner
+ (smallest) scope. There is not way to refer to the variable in the
+ outer scope. This effect is usually referred to as
+ \emph{shadowing}: When a binder is bound in a scope where the
+ binder already had a value, the inner binding is said to
+ \emph{shadow} the outer binding. In the example above, the \lam{c}
+ binder was bound outside of the expression and in the inner lambda
+ expression. Inside that lambda expression, only the inner \lam{c}
+ can be accessed.
+
+ There are a number of ways to solve this. \small{GHC} has isolated this
+ problem to their binder substitution code, which performs \emph{deshadowing}
+ during its expression traversal. This means that any binding that shadows
+ another binding on a higher level is replaced by a new binder that does not
+ shadow any other binding. This non-shadowing invariant is enough to prevent
+ binder uniqueness problems in \small{GHC}.
+
+ In our transformation system, maintaining this non-shadowing invariant is
+ a bit harder to do (mostly due to implementation issues, the prototype
+ does not use \small{GHC}'s subsitution code). Also, the following points
+ can be observed.
+
+ \startitemize
+ \item Deshadowing does not guarantee overall uniqueness. For example, the
+ following (slightly contrived) expression shows the identifier \lam{x} bound in
+ two seperate places (and to different values), even though no shadowing
+ occurs.
+
+ \startlambda
+ (let x = 1 in x) + (let x = 2 in x)
+ \stoplambda
+
+ \item In our normal form (and the resulting \small{VHDL}), all binders
+ (signals) within the same function (entity) will end up in the same
+ scope. To allow this, all binders within the same function should be
+ unique.
+
+ \item When we know that all binders in an expression are unique, moving around
+ or removing a subexpression will never cause any binder conflicts. If we have
+ some way to generate fresh binders, introducing new subexpressions will not
+ cause any problems either. The only way to cause conflicts is thus to
+ duplicate an existing subexpression.
+ \stopitemize
+
+ Given the above, our prototype maintains a unique binder invariant. This
+ means that in any given moment during normalization, all binders \emph{within
+ a single function} must be unique. To achieve this, we apply the following
+ technique.
+
+ \todo{Define fresh binders and unique supplies}
+
+ \startitemize
+ \item Before starting normalization, all binders in the function are made
+ unique. This is done by generating a fresh binder for every binder used. This
+ also replaces binders that did not cause any conflict, but it does ensure that
+ all binders within the function are generated by the same unique supply.
+ \refdef{fresh binder}
+ \item Whenever a new binder must be generated, we generate a fresh binder that
+ is guaranteed to be different from \emph{all binders generated so far}. This
+ can thus never introduce duplication and will maintain the invariant.
+ \item Whenever (a part of) an expression is duplicated (for example when
+ inlining), all binders in the expression are replaced with fresh binders
+ (using the same method as at the start of normalization). These fresh binders
+ can never introduce duplication, so this will maintain the invariant.
+ \item Whenever we move part of an expression around within the function, there
+ is no need to do anything special. There is obviously no way to introduce
+ duplication by moving expressions around. Since we know that each of the
+ binders is already unique, there is no way to introduce (incorrect) shadowing
+ either.
+ \stopitemize
+
+ \section{Transform passes}
+ In this section we describe the actual transforms.
+
+ Each transformation will be described informally first, explaining
+ the need for and goal of the transformation. Then, we will formally define
+ the transformation using the syntax introduced in
+ \in{section}[sec:normalization:transformation].
+
+ \subsection{General cleanup}
+ These transformations are general cleanup transformations, that aim to
+ make expressions simpler. These transformations usually clean up the
+ mess left behind by other transformations or clean up expressions to
+ expose new transformation opportunities for other transformations.
+
+ Most of these transformations are standard optimizations in other
+ compilers as well. However, in our compiler, most of these are not just
+ optimizations, but they are required to get our program into intended
+ normal form.
+
+ \placeintermezzo{}{
+ \defref{substitution notation}
+ \startframedtext[width=8cm,background=box,frame=no]
+ \startalignment[center]
+ {\tfa Substitution notation}
+ \stopalignment
+ \blank[medium]
+
+ In some of the transformations in this chapter, we need to perform
+ substitution on an expression. Substitution means replacing every
+ occurence of some expression (usually a variable reference) with
+ another expression.
+
+ There have been a lot of different notations used in literature for
+ specifying substitution. The notation that will be used in this report
+ is the following:
+
+ \startlambda
+ E[A=>B]
+ \stoplambda
+
+ This means expression \lam{E} with all occurences of \lam{A} replaced
+ with \lam{B}.
+ \stopframedtext
+ }
+
+ \subsubsection[sec:normalization:beta]{β-reduction}
+ β-reduction is a well known transformation from lambda calculus, where it is
+ the main reduction step. It reduces applications of lambda abstractions,
+ removing both the lambda abstraction and the application.
+
+ In our transformation system, this step helps to remove unwanted lambda
+ abstractions (basically all but the ones at the top level). Other
+ transformations (application propagation, non-representable inlining) make
+ sure that most lambda abstractions will eventually be reducable by
+ β-reduction.
+
+ Note that β-reduction also works on type lambda abstractions and type
+ applications as well. This means the substitution below also works on
+ type variables, in the case that the binder is a type variable and teh
+ expression applied to is a type.
+
+ \starttrans
+ (λx.E) M
+ -----------------
+ E[x=>M]
+ \stoptrans
+
+ % And an example
+ \startbuffer[from]
+ (λa. 2 * a) (2 * b)
+ \stopbuffer
+
+ \startbuffer[to]
+ 2 * (2 * b)
+ \stopbuffer
+
+ \transexample{beta}{β-reduction}{from}{to}
+
+ \startbuffer[from]
+ (λt.λa::t. a) @Int
+ \stopbuffer
+
+ \startbuffer[to]
+ (λa::Int. a)
+ \stopbuffer
+
+ \transexample{beta-type}{β-reduction for type abstractions}{from}{to}
+
+ \subsubsection{Unused let binding removal}
+ This transformation removes let bindings that are never used.
+ Occasionally, \GHC's desugarer introduces some unused let bindings.
+
+ This normalization pass should really be not be necessary to get
+ into intended normal form (since the intended normal form
+ definition \refdef{intended normal form definition} does not
+ require that every binding is used), but in practice the
+ desugarer or simplifier emits some bindings that cannot be
+ normalized (e.g., calls to a
+ \hs{Control.Exception.Base.patError}) but are not used anywhere
+ either. To prevent the \VHDL generation from breaking on these
+ artifacts, this transformation removes them.
+
+ \todo{Do not use old-style numerals in transformations}
+ \starttrans
+ letrec
+ a0 = E0
+ \vdots
+ ai = Ei
+ \vdots
+ an = En
+ in
+ M \lam{ai} does not occur free in \lam{M}
+ ---------------------------- \lam{\forall j, 0 ≤ j ≤ n, j ≠ i} (\lam{ai} does not occur free in \lam{Ej})
+ letrec
+ a0 = E0
+ \vdots
+ ai-1 = Ei-1
+ ai+1 = Ei+1
+ \vdots
+ an = En
+ in
+ M
+ \stoptrans
+
+ % And an example
+ \startbuffer[from]
+ let
+ x = 1
+ in
+ 2
+ \stopbuffer
+
+ \startbuffer[to]
+ let
+ in
+ 2
+ \stopbuffer
+
+ \transexample{unusedlet}{Unused let binding removal}{from}{to}
+
+ \subsubsection{Empty let removal}
+ This transformation is simple: It removes recursive lets that have no bindings
+ (which usually occurs when unused let binding removal removes the last
+ binding from it).
+
+ Note that there is no need to define this transformation for
+ non-recursive lets, since they always contain exactly one binding.
+
+ \starttrans
+ letrec in M
+ --------------
+ M
+ \stoptrans
+
+ % And an example
+ \startbuffer[from]
+ let
+ in
+ 2
+ \stopbuffer
+
+ \startbuffer[to]
+ 2
+ \stopbuffer
+
+ \transexample{emptylet}{Empty let removal}{from}{to}
+
+ \subsubsection[sec:normalization:simplelet]{Simple let binding removal}
+ This transformation inlines simple let bindings, that bind some
+ binder to some other binder instead of a more complex expression (\ie
+ a = b).
+
+ This transformation is not needed to get an expression into intended
+ normal form (since these bindings are part of the intended normal
+ form), but makes the resulting \small{VHDL} a lot shorter.
+
+ \refdef{substitution notation}
+ \starttrans
+ letrec
+ a0 = E0
+ \vdots
+ ai = b
+ \vdots
+ an = En
+ in
+ M
+ ----------------------------- \lam{b} is a variable reference
+ letrec \lam{ai} ≠ \lam{b}
+ a0 = E0 [ai=>b]
+ \vdots
+ ai-1 = Ei-1 [ai=>b]
+ ai+1 = Ei+1 [ai=>b]
+ \vdots
+ an = En [ai=>b]
+ in
+ M[ai=>b]
+ \stoptrans
+
+ \todo{example}
+
+ \subsubsection{Cast propagation / simplification}
+ This transform pushes casts down into the expression as far as
+ possible. This transformation has been added to make a few
+ specific corner cases work, but it is not clear yet if this
+ transformation handles cast expressions completely or in the
+ right way. See \in{section}[sec:normalization:castproblems].
+
+ \starttrans
+ (let binds in E) ▶ T
+ -------------------------
+ let binds in (E ▶ T)
+ \stoptrans
+
+ \starttrans
+ (case S of
+ p0 -> E0
+ \vdots
+ pn -> En
+ ) ▶ T
+ -------------------------
+ case S of
+ p0 -> E0 ▶ T
+ \vdots
+ pn -> En ▶ T
+ \stoptrans
+
+ \subsubsection{Top level binding inlining}
+ \refdef{top level binding}
+ This transform takes simple top level bindings generated by the
+ \small{GHC} compiler. \small{GHC} sometimes generates very simple
+ \quote{wrapper} bindings, which are bound to just a variable
+ reference, or contain just a (partial) function appliation with
+ the type and dictionary arguments filled in (such as the
+ \lam{(+)} in the example below).
+
+ Note that this transformation is completely optional. It is not
+ required to get any function into intended normal form, but it does help making
+ the resulting VHDL output easier to read (since it removes components
+ that do not add any real structure, but do hide away operations and
+ cause extra clutter).
+
+ This transform takes any top level binding generated by \GHC,
+ whose normalized form contains only a single let binding.
+
+ \starttrans
+ x = λa0 ... λan.let y = E in y
+ ~
+ x
+ -------------------------------------- \lam{x} is generated by the compiler
+ λa0 ... λan.let y = E in y
+ \stoptrans
+
+ \startbuffer[from]
+ (+) :: Word -> Word -> Word
+ (+) = GHC.Num.(+) @Word \$dNum
+ ~
+ (+) a b
+ \stopbuffer
+ \startbuffer[to]
+ GHC.Num.(+) @ Alu.Word \$dNum a b
+ \stopbuffer
+
+ \transexample{toplevelinline}{Top level binding inlining}{from}{to}
+
+ \in{Example}[ex:trans:toplevelinline] shows a typical application of
+ the addition operator generated by \GHC. The type and dictionary
+ arguments used here are described in
+ \in{Section}[section:prototype:polymorphism].
+
+ Without this transformation, there would be a \lam{(+)} entity
+ in the \VHDL which would just add its inputs. This generates a
+ lot of overhead in the \VHDL, which is particularly annoying
+ when browsing the generated RTL schematic (especially since most
+ non-alphanumerics, like all characters in \lam{(+)}, are not
+ allowed in \VHDL architecture names\footnote{Technically, it is
+ allowed to use non-alphanumerics when using extended
+ identifiers, but it seems that none of the tooling likes
+ extended identifiers in filenames, so it effectively does not
+ work.}, so the entity would be called \quote{w7aA7f} or
+ something similarly meaningless and autogenerated).
+
+ \subsection{Program structure}
+ These transformations are aimed at normalizing the overall structure
+ into the intended form. This means ensuring there is a lambda abstraction
+ at the top for every argument (input port or current state), putting all
+ of the other value definitions in let bindings and making the final
+ return value a simple variable reference.
+
+ \subsubsection[sec:normalization:eta]{η-abstraction}
+ This transformation makes sure that all arguments of a function-typed
+ expression are named, by introducing lambda expressions. When combined with
+ β-reduction and non-representable binding inlining, all function-typed
+ expressions should be lambda abstractions or global identifiers.
+
+ \starttrans
+ E \lam{E :: a -> b}
+ -------------- \lam{E} does not occur on a function position in an application
+ λx.E x \lam{E} is not a lambda abstraction.
+ \stoptrans
+
+ \startbuffer[from]
+ foo = λa.case a of
+ True -> λb.mul b b
+ False -> id
+ \stopbuffer
+
+ \startbuffer[to]
+ foo = λa.λx.(case a of
+ True -> λb.mul b b
+ False -> λy.id y) x
+ \stopbuffer
+
+ \transexample{eta}{η-abstraction}{from}{to}
+
+ \subsubsection[sec:normalization:appprop]{Application propagation}
+ This transformation is meant to propagate application expressions downwards
+ into expressions as far as possible. This allows partial applications inside
+ expressions to become fully applied and exposes new transformation
+ opportunities for other transformations (like β-reduction and
+ specialization).
+
+ Since all binders in our expression are unique (see
+ \in{section}[sec:normalization:uniq]), there is no risk that we will
+ introduce unintended shadowing by moving an expression into a lower
+ scope. Also, since only move expression into smaller scopes (down into
+ our expression), there is no risk of moving a variable reference out
+ of the scope in which it is defined.
+
+ \starttrans
+ (letrec binds in E) M
+ ------------------------
+ letrec binds in E M
+ \stoptrans
+
+ % And an example
+ \startbuffer[from]
+ ( letrec
+ val = 1
+ in
+ add val
+ ) 3
+ \stopbuffer
+
+ \startbuffer[to]
+ letrec
+ val = 1
+ in
+ add val 3
+ \stopbuffer
+
+ \transexample{appproplet}{Application propagation for a let expression}{from}{to}
+
+ \starttrans
+ (case x of
+ p0 -> E0
+ \vdots
+ pn -> En) M
+ -----------------
+ case x of
+ p0 -> E0 M
+ \vdots
+ pn -> En M
+ \stoptrans
+
+ % And an example
+ \startbuffer[from]
+ ( case x of
+ True -> id
+ False -> neg
+ ) 1
+ \stopbuffer
+
+ \startbuffer[to]
+ case x of
+ True -> id 1
+ False -> neg 1
+ \stopbuffer
+
+ \transexample{apppropcase}{Application propagation for a case expression}{from}{to}
+
+ \subsubsection[sec:normalization:letrecurse]{Let recursification}
+ This transformation makes all non-recursive lets recursive. In the
+ end, we want a single recursive let in our normalized program, so all
+ non-recursive lets can be converted. This also makes other
+ transformations simpler: They only need to be specified for recursive
+ let expressions (and simply will not apply to non-recursive let
+ expressions until this transformation has been applied).
+
+ \starttrans
+ let
+ a = E
+ in
+ M
+ ------------------------------------------
+ letrec
+ a = E
+ in
+ M
+ \stoptrans
+
+ \subsubsection{Let flattening}
+ This transformation puts nested lets in the same scope, by lifting the
+ binding(s) of the inner let into the outer let. Eventually, this will
+ cause all let bindings to appear in the same scope.
+
+ This transformation only applies to recursive lets, since all
+ non-recursive lets will be made recursive (see
+ \in{section}[sec:normalization:letrecurse]).
+
+ Since we are joining two scopes together, there is no risk of moving a
+ variable reference out of the scope where it is defined.
+
+ \starttrans
+ letrec
+ a0 = E0
+ \vdots
+ ai = (letrec bindings in M)
+ \vdots
+ an = En
+ in
+ N
+ ------------------------------------------
+ letrec
+ a0 = E0
+ \vdots
+ ai = M
+ \vdots
+ an = En
+ bindings
+ in
+ N
+ \stoptrans
+
+ \startbuffer[from]
+ letrec
+ a = 1
+ b = letrec
+ x = a
+ y = c
+ in
+ x + y
+ c = 2
+ in
+ b
+ \stopbuffer
+ \startbuffer[to]
+ letrec
+ a = 1
+ b = x + y
+ c = 2
+ x = a
+ y = c
+ in
+ b
+ \stopbuffer
+
+ \transexample{letflat}{Let flattening}{from}{to}
+
+ \subsubsection{Return value simplification}
+ This transformation ensures that the return value of a function is always a
+ simple local variable reference.
+
+ This transformation only applies to the entire body of a
+ function instead of any subexpression in a function. This is
+ achieved by the contexts, like \lam{x = E}, though this is
+ strictly not correct (you could read this as "if there is any
+ function \lam{x} that binds \lam{E}, any \lam{E} can be
+ transformed, while we only mean the \lam{E} that is bound by
+ \lam{x}).
+
+ Note that the return value is not simplified if its not
+ representable. Otherwise, this would cause a direct loop with
+ the inlining of unrepresentable bindings. If the return value is
+ not representable because it has a function type, η-abstraction
+ should make sure that this transformation will eventually apply.
+ If the value is not representable for other reasons, the
+ function result itself is not representable, meaning this
+ function is not translatable anyway.
+
+ \starttrans
+ x = E \lam{E} is representable
+ ~ \lam{E} is not a lambda abstraction
+ E \lam{E} is not a let expression
+ --------------------------- \lam{E} is not a local variable reference
+ letrec x = E in x
+ \stoptrans
+
+ \starttrans
+ x = λv0 ... λvn.E
+ ~ \lam{E} is representable
+ E \lam{E} is not a let expression
+ --------------------------- \lam{E} is not a local variable reference
+ letrec x = E in x
+ \stoptrans
+
+ \starttrans
+ x = λv0 ... λvn.let ... in E
+ ~ \lam{E} is representable
+ E \lam{E} is not a local variable reference
+ -----------------------------
+ letrec x = E in x
+ \stoptrans
+
+ \startbuffer[from]
+ x = add 1 2
+ \stopbuffer
+
+ \startbuffer[to]
+ x = letrec x = add 1 2 in x
+ \stopbuffer
+
+ \transexample{retvalsimpl}{Return value simplification}{from}{to}
+
+ \todo{More examples}
+
+ \subsection[sec:normalization:argsimpl]{Representable arguments simplification}
+ This section contains just a single transformation that deals with
+ representable arguments in applications. Non-representable arguments are
+ handled by the transformations in
+ \in{section}[sec:normalization:nonrep].
+
+ This transformation ensures that all representable arguments will become
+ references to local variables. This ensures they will become references
+ to local signals in the resulting \small{VHDL}, which is required due to
+ limitations in the component instantiation code in \VHDL (one can only
+ assign a signal or constant to an input port). By ensuring that all
+ arguments are always simple variable references, we always have a signal
+ available to map to the input ports.
+
+ To reduce a complex expression to a simple variable reference, we create
+ a new let expression around the application, which binds the complex
+ expression to a new variable. The original function is then applied to
+ this variable.
+
+ \refdef{global variable}
+ Note that references to \emph{global variables} (like a top level
+ function without arguments, but also an argumentless dataconstructors
+ like \lam{True}) are also simplified. Only local variables generate
+ signals in the resulting architecture. Even though argumentless
+ dataconstructors generate constants in generated \VHDL code and could be
+ mapped to an input port directly, they are still simplified to make the
+ normal form more regular.
+
+ \refdef{representable}
+ \starttrans
+ M N
+ -------------------- \lam{N} is representable
+ letrec x = N in M x \lam{N} is not a local variable reference
+ \stoptrans
+ \refdef{local variable}
+
+ \startbuffer[from]
+ add (add a 1) 1
+ \stopbuffer
+
+ \startbuffer[to]
+ letrec x = add a 1 in add x 1
+ \stopbuffer
+
+ \transexample{argsimpl}{Argument simplification}{from}{to}
+
+ \subsection[sec:normalization:built-ins]{Built-in functions}
+ This section deals with (arguments to) built-in functions. In the
+ intended normal form definition\refdef{intended normal form definition}
+ we can see that there are three sorts of arguments a built-in function
+ can receive.
+
+ \startitemize[KR]
+ \item A representable local variable reference. This is the most
+ common argument to any function. The argument simplification
+ transformation described in \in{section}[sec:normalization:argsimpl]
+ makes sure that \emph{any} representable argument to \emph{any}
+ function (including built-in functions) is turned into a local variable
+ reference.
+ \item (A partial application of) a top level function (either built-in on
+ user-defined). The function extraction transformation described in
+ this section takes care of turning every functiontyped argument into
+ (a partial application of) a top level function.
+ \item Any expression that is not representable and does not have a
+ function type. Since these can be any expression, there is no
+ transformation needed. Note that this category is exactly all
+ expressions that are not transformed by the transformations for the
+ previous two categories. This means that \emph{any} core expression
+ that is used as an argument to a built-in function will be either
+ transformed into one of the above categories, or end up in this
+ categorie. In any case, the result is in normal form.
+ \stopitemize
+
+ As noted, the argument simplification will handle any representable
+ arguments to a built-in function. The following transformation is needed
+ to handle non-representable arguments with a function type, all other
+ non-representable arguments do not need any special handling.
+
+ \subsubsection[sec:normalization:funextract]{Function extraction}
+ This transform deals with function-typed arguments to built-in
+ functions.
+ Since built-in functions cannot be specialized (see
+ \in{section}[sec:normalization:specialize]) to remove the arguments,
+ these arguments are extracted into a new global function instead. In
+ other words, we create a new top level function that has exactly the
+ extracted argument as its body. This greatly simplifies the
+ translation rules needed for built-in functions, since they only need
+ to handle (partial applications of) top level functions.
+
+ Any free variables occuring in the extracted arguments will become
+ parameters to the new global function. The original argument is replaced
+ with a reference to the new function, applied to any free variables from
+ the original argument.
+
+ This transformation is useful when applying higher-order built-in functions
+ like \hs{map} to a lambda abstraction, for example. In this case, the code
+ that generates \small{VHDL} for \hs{map} only needs to handle top level functions and
+ partial applications, not any other expression (such as lambda abstractions or
+ even more complicated expressions).
+
+ \starttrans
+ M N \lam{M} is (a partial aplication of) a built-in function.
+ --------------------- \lam{f0 ... fn} are all free local variables of \lam{N}
+ M (x f0 ... fn) \lam{N :: a -> b}
+ ~ \lam{N} is not a (partial application of) a top level function
+ x = λf0 ... λfn.N
+ \stoptrans
+
+ \startbuffer[from]
+ addList = λb.λxs.map (λa . add a b) xs
+ \stopbuffer
+
+ \startbuffer[to]
+ addList = λb.λxs.map (f b) xs
+ ~
+ f = λb.λa.add a b
+ \stopbuffer
+
+ \transexample{funextract}{Function extraction}{from}{to}
+
+ Note that the function \lam{f} will still need normalization after
+ this.
+
+ \subsection{Case normalisation}
+ \subsubsection{Scrutinee simplification}
+ This transform ensures that the scrutinee of a case expression is always
+ a simple variable reference.
+
+ \starttrans
+ case E of
+ alts
+ ----------------- \lam{E} is not a local variable reference
+ letrec x = E in
+ case x of
+ alts
+ \stoptrans
+
+ \startbuffer[from]
+ case (foo a) of
+ True -> a
+ False -> b
+ \stopbuffer
+
+ \startbuffer[to]
+ letrec x = foo a in
+ case x of
+ True -> a
+ False -> b
+ \stopbuffer
+
+ \transexample{letflat}{Case normalisation}{from}{to}
+
+
+ \subsubsection{Case normalization}
+ This transformation ensures that all case expressions get a form
+ that is allowed by the intended normal form. This means they
+ will become one of: \refdef{intended normal form definition}
+ \startitemize
+ \item An extractor case with a single alternative that picks a field
+ from a datatype, \eg \lam{case x of (a, b) -> a}.
+ \item A selector case with multiple alternatives and only wild binders, that
+ makes a choice between expressions based on the constructor of another
+ expression, \eg \lam{case x of Low -> a; High -> b}.
+ \stopitemize
+
+ For an arbitrary case, that has \lam{n} alternatives, with
+ \lam{m} binders in each alternatives, this will result in \lam{m
+ * n} extractor case expression to get at each variable, \lam{n}
+ let bindings for each of the alternatives' value and a single
+ selector case to select the right value out of these.
+
+ Technically, the defintion of this transformation would require
+ that the constructor for every alternative has exactly the same
+ amount (\lam{m}) of arguments, but of course this transformation
+ also applies when this is not the case.
+
+ \starttrans
+ case E of
+ C0 v0,0 ... v0,m -> E0
+ \vdots
+ Cn vn,0 ... vn,m -> En
+ --------------------------------------------------- \lam{\forall i \forall j, 0 ≤ i ≤ n, 0 ≤ i < m} (\lam{wi,j} is a wild (unused) binder)
+ letrec The case expression is not an extractor case
+ v0,0 = case E of C0 x0,0 .. x0,m -> x0,0 The case expression is not a selector case
+ \vdots
+ v0,m = case E of C0 x0,0 .. x0,m -> x0,m
+ \vdots
+ vn,m = case E of Cn xn,0 .. xn,m -> xn,m
+ y0 = E0
+ \vdots
+ yn = En
+ in
+ case E of
+ C0 w0,0 ... w0,m -> y0
+ \vdots
+ Cn wn,0 ... wn,m -> yn
+ \stoptrans
+
+ \refdef{wild binder}
+ Note that this transformation applies to case expressions with any
+ scrutinee. If the scrutinee is a complex expression, this might
+ result in duplication of work (hardware). An extra condition to
+ only apply this transformation when the scrutinee is already
+ simple (effectively causing this transformation to be only
+ applied after the scrutinee simplification transformation) might
+ be in order.
+
+ \startbuffer[from]
+ case a of
+ True -> add b 1
+ False -> add b 2
+ \stopbuffer
+
+ \startbuffer[to]
+ letrec
+ x0 = add b 1
+ x1 = add b 2
+ in
+ case a of
+ True -> x0
+ False -> x1
+ \stopbuffer
+
+ \transexample{selcasesimpl}{Selector case simplification}{from}{to}
+
+ \startbuffer[from]
+ case a of
+ (,) b c -> add b c
+ \stopbuffer
+ \startbuffer[to]
+ letrec
+ b = case a of (,) b c -> b
+ c = case a of (,) b c -> c
+ x0 = add b c
+ in
+ case a of
+ (,) w0 w1 -> x0
+ \stopbuffer
+
+ \transexample{excasesimpl}{Extractor case simplification}{from}{to}
+
+ \refdef{selector case}
+ In \in{example}[ex:trans:excasesimpl] the case expression is expanded
+ into multiple case expressions, including a pretty useless expression
+ (that is neither a selector or extractor case). This case can be
+ removed by the Case removal transformation in
+ \in{section}[sec:transformation:caseremoval].
+
+ \subsubsection[sec:transformation:caseremoval]{Case removal}
+ This transform removes any case expression with a single alternative and
+ only wild binders.\refdef{wild binder}
+
+ These "useless" case expressions are usually leftovers from case simplification
+ on extractor case (see the previous example).
+
+ \starttrans
+ case x of
+ C v0 ... vm -> E
+ ---------------------- \lam{\forall i, 0 ≤ i ≤ m} (\lam{vi} does not occur free in E)
+ E
+ \stoptrans
+
+ \startbuffer[from]
+ case a of
+ (,) w0 w1 -> x0
+ \stopbuffer
+
+ \startbuffer[to]
+ x0
+ \stopbuffer
+
+ \transexample{caserem}{Case removal}{from}{to}
+
+ \subsection[sec:normalization:nonrep]{Removing unrepresentable values}
+ The transformations in this section are aimed at making all the
+ values used in our expression representable. There are two main
+ transformations that are applied to \emph{all} unrepresentable let
+ bindings and function arguments. These are meant to address three
+ different kinds of unrepresentable values: Polymorphic values,
+ higher-order values and literals. The transformation are described
+ generically: They apply to all non-representable values. However,
+ non-representable values that do not fall into one of these three
+ categories will be moved around by these transformations but are
+ unlikely to completely disappear. They usually mean the program was not
+ valid in the first place, because unsupported types were used (for
+ example, a program using strings).
+
+ Each of these three categories will be detailed below, followed by the
+ actual transformations.
+
+ \subsubsection{Removing Polymorphism}
+ As noted in \in{section}[sec:prototype:polymporphism],
+ polymorphism is made explicit in Core through type and
+ dictionary arguments. To remove the polymorphism from a
+ function, we can simply specialize the polymorphic function for
+ the particular type applied to it. The same goes for dictionary
+ arguments. To remove polymorphism from let bound values, we
+ simply inline the let bindings that have a polymorphic type,
+ which should (eventually) make sure that the polymorphic
+ expression is applied to a type and/or dictionary, which can
+ then be removed by β-reduction (\in{section}[sec:normalization:beta]).
+
+ Since both type and dictionary arguments are not representable,
+ \refdef{representable}
+ the non-representable argument specialization and
+ non-representable let binding inlining transformations below
+ take care of exactly this.
+
+ There is one case where polymorphism cannot be completely
+ removed: Built-in functions are still allowed to be polymorphic
+ (Since we have no function body that we could properly
+ specialize). However, the code that generates \VHDL for built-in
+ functions knows how to handle this, so this is not a problem.
+
+ \subsubsection[sec:normalization:defunctionalization]{Defunctionalization}
+ These transformations remove higher-order expressions from our
+ program, making all values first-order.
+
+ Higher order values are always introduced by lambda abstractions, none
+ of the other Core expression elements can introduce a function type.
+ However, other expressions can \emph{have} a function type, when they
+ have a lambda expression in their body.
+
+ For example, the following expression is a higher-order expression
+ that is not a lambda expression itself:
+
+ \refdef{id function}
+ \startlambda
+ case x of
+ High -> id
+ Low -> λx.x
+ \stoplambda
+
+ The reference to the \lam{id} function shows that we can introduce a
+ higher-order expression in our program without using a lambda
+ expression directly. However, inside the definition of the \lam{id}
+ function, we can be sure that a lambda expression is present.
+
+ Looking closely at the definition of our normal form in
+ \in{section}[sec:normalization:intendednormalform], we can see that
+ there are three possibilities for higher-order values to appear in our
+ intended normal form:
+
+ \startitemize[KR]
+ \item[item:toplambda] Lambda abstractions can appear at the highest level of a
+ top level function. These lambda abstractions introduce the
+ arguments (input ports / current state) of the function.
+ \item[item:built-inarg] (Partial applications of) top level functions can appear as an
+ argument to a built-in function.
+ \item[item:completeapp] (Partial applications of) top level functions can appear in
+ function position of an application. Since a partial application
+ cannot appear anywhere else (except as built-in function arguments),
+ all partial applications are applied, meaning that all applications
+ will become complete applications. However, since application of
+ arguments happens one by one, in the expression:
+ \startlambda
+ f 1 2
+ \stoplambda
+ the subexpression \lam{f 1} has a function type. But this is
+ allowed, since it is inside a complete application.
+ \stopitemize
+
+ We will take a typical function with some higher-order values as an
+ example. The following function takes two arguments: a \lam{Bit} and a
+ list of numbers. Depending on the first argument, each number in the
+ list is doubled, or the list is returned unmodified. For the sake of
+ the example, no polymorphism is shown. In reality, at least map would
+ be polymorphic.
+
+ \startlambda
+ λy.let double = λx. x + x in
+ case y of
+ Low -> map double
+ High -> λz. z
+ \stoplambda
+
+ This example shows a number of higher-order values that we cannot
+ translate to \VHDL directly. The \lam{double} binder bound in the let
+ expression has a function type, as well as both of the alternatives of
+ the case expression. The first alternative is a partial application of
+ the \lam{map} built-in function, whereas the second alternative is a
+ lambda abstraction.
+
+ To reduce all higher-order values to one of the above items, a number
+ of transformations we have already seen are used. The η-abstraction
+ transformation from \in{section}[sec:normalization:eta] ensures all
+ function arguments are introduced by lambda abstraction on the highest
+ level of a function. These lambda arguments are allowed because of
+ \in{item}[item:toplambda] above. After η-abstraction, our example
+ becomes a bit bigger:
+
+ \startlambda
+ λy.λq.(let double = λx. x + x in
+ case y of
+ Low -> map double
+ High -> λz. z
+ ) q
+ \stoplambda
+
+ η-abstraction also introduces extra applications (the application of
+ the let expression to \lam{q} in the above example). These
+ applications can then propagated down by the application propagation
+ transformation (\in{section}[sec:normalization:appprop]). In our
+ example, the \lam{q} and \lam{r} variable will be propagated into the
+ let expression and then into the case expression:
+
+ \startlambda
+ λy.λq.let double = λx. x + x in
+ case y of
+ Low -> map double q
+ High -> (λz. z) q
+ \stoplambda
+
+ This propagation makes higher-order values become applied (in
+ particular both of the alternatives of the case now have a
+ representable type). Completely applied top level functions (like the
+ first alternative) are now no longer invalid (they fall under
+ \in{item}[item:completeapp] above). (Completely) applied lambda
+ abstractions can be removed by β-abstraction. For our example,
+ applying β-abstraction results in the following:
+
+ \startlambda
+ λy.λq.let double = λx. x + x in
+ case y of
+ Low -> map double q
+ High -> q
+ \stoplambda
+
+ As you can see in our example, all of this moves applications towards
+ the higher-order values, but misses higher-order functions bound by
+ let expressions. The applications cannot be moved towards these values
+ (since they can be used in multiple places), so the values will have
+ to be moved towards the applications. This is achieved by inlining all
+ higher-order values bound by let applications, by the
+ non-representable binding inlining transformation below. When applying
+ it to our example, we get the following:
+
+ \startlambda
+ λy.λq.case y of
+ Low -> map (λx. x + x) q
+ High -> q
+ \stoplambda
+
+ We have nearly eliminated all unsupported higher-order values from this
+ expressions. The one that is remaining is the first argument to the
+ \lam{map} function. Having higher-order arguments to a built-in
+ function like \lam{map} is allowed in the intended normal form, but
+ only if the argument is a (partial application) of a top level
+ function. This is easily done by introducing a new top level function
+ and put the lambda abstraction inside. This is done by the function
+ extraction transformation from
+ \in{section}[sec:normalization:funextract].
+
+ \startlambda
+ λy.λq.case y of
+ Low -> map func q
+ High -> q
+ \stoplambda
+
+ This also introduces a new function, that we have called \lam{func}:
+
+ \startlambda
+ func = λx. x + x
+ \stoplambda
+
+ Note that this does not actually remove the lambda, but now it is a
+ lambda at the highest level of a function, which is allowed in the
+ intended normal form.
+
+ There is one case that has not been discussed yet. What if the
+ \lam{map} function in the example above was not a built-in function
+ but a user-defined function? Then extracting the lambda expression
+ into a new function would not be enough, since user-defined functions
+ can never have higher-order arguments. For example, the following
+ expression shows an example:
+
+ \startlambda
+ twice :: (Word -> Word) -> Word -> Word
+ twice = λf.λa.f (f a)
+
+ main = λa.app (λx. x + x) a
+ \stoplambda
+
+ This example shows a function \lam{twice} that takes a function as a
+ first argument and applies that function twice to the second argument.
+ Again, we have made the function monomorphic for clarity, even though
+ this function would be a lot more useful if it was polymorphic. The
+ function \lam{main} uses \lam{twice} to apply a lambda epression twice.
+
+ When faced with a user defined function, a body is available for that
+ function. This means we could create a specialized version of the
+ function that only works for this particular higher-order argument
+ (\ie, we can just remove the argument and call the specialized
+ function without the argument). This transformation is detailed below.
+ Applying this transformation to the example gives:
+
+ \startlambda
+ twice' :: Word -> Word
+ twice' = λb.(λf.λa.f (f a)) (λx. x + x) b
+
+ main = λa.app' a
+ \stoplambda
+
+ The \lam{main} function is now in normal form, since the only
+ higher-order value there is the top level lambda expression. The new
+ \lam{twice'} function is a bit complex, but the entire original body
+ of the original \lam{twice} function is wrapped in a lambda
+ abstraction and applied to the argument we have specialized for
+ (\lam{λx. x + x}) and the other arguments. This complex expression can
+ fortunately be effectively reduced by repeatedly applying β-reduction:
+
+ \startlambda
+ twice' :: Word -> Word
+ twice' = λb.(b + b) + (b + b)
+ \stoplambda
+
+ This example also shows that the resulting normal form might not be as
+ efficient as we might hope it to be (it is calculating \lam{(b + b)}
+ twice). This is discussed in more detail in
+ \in{section}[sec:normalization:duplicatework].
+
+ \subsubsection{Literals}
+ There are a limited number of literals available in Haskell and Core.
+ \refdef{enumerated types} When using (enumerating) algebraic
+ datatypes, a literal is just a reference to the corresponding data
+ constructor, which has a representable type (the algebraic datatype)
+ and can be translated directly. This also holds for literals of the
+ \hs{Bool} Haskell type, which is just an enumerated type.
+
+ There is, however, a second type of literal that does not have a
+ representable type: Integer literals. Cλash supports using integer
+ literals for all three integer types supported (\hs{SizedWord},
+ \hs{SizedInt} and \hs{RangedWord}). This is implemented using
+ Haskell's \hs{Num} type class, which offers a \hs{fromInteger} method
+ that converts any \hs{Integer} to the Cλash datatypes.
+
+ When \GHC sees integer literals, it will automatically insert calls to
+ the \hs{fromInteger} method in the resulting Core expression. For
+ example, the following expression in Haskell creates a 32 bit unsigned
+ word with the value 1. The explicit type signature is needed, since
+ there is no context for \GHC to determine the type from otherwise.
+
+ \starthaskell
+ 1 :: SizedWord D32
+ \stophaskell
+
+ This Haskell code results in the following Core expression:
+
+ \startlambda
+ fromInteger @(SizedWord D32) \$dNum (smallInteger 10)
+ \stoplambda
+
+ The literal 10 will have the type \lam{GHC.Prim.Int\#}, which is
+ converted into an \lam{Integer} by \lam{smallInteger}. Finally, the
+ \lam{fromInteger} function will finally convert this into a
+ \lam{SizedWord D32}.
+
+ Both the \lam{GHC.Prim.Int\#} and \lam{Integer} types are not
+ representable, and cannot be translated directly. Fortunately, there
+ is no need to translate them, since \lam{fromInteger} is a built-in
+ function that knows how to handle these values. However, this does
+ require that the \lam{fromInteger} function is directly applied to
+ these non-representable literal values, otherwise errors will occur.
+ For example, the following expression is not in the intended normal
+ form, since one of the let bindings has an unrepresentable type
+ (\lam{Integer}):
+
+ \startlambda
+ let l = smallInteger 10 in fromInteger @(SizedWord D32) \$dNum l
+ \stoplambda
+
+ By inlining these let-bindings, we can ensure that unrepresentable
+ literals bound by a let binding end up in an application of the
+ appropriate built-in function, where they are allowed. Since it is
+ possible that the application of that function is in a different
+ function than the definition of the literal value, we will always need
+ to specialize away any unrepresentable literals that are used as
+ function arguments. The following two transformations do exactly this.
+
+ \subsubsection{Non-representable binding inlining}
+ This transform inlines let bindings that are bound to a
+ non-representable value. Since we can never generate a signal
+ assignment for these bindings (we cannot declare a signal assignment
+ with a non-representable type, for obvious reasons), we have no choice
+ but to inline the binding to remove it.
+
+ As we have seen in the previous sections, inlining these bindings
+ solves (part of) the polymorphism, higher-order values and
+ unrepresentable literals in an expression.
+
+ \refdef{substitution notation}
+ \starttrans
+ letrec
+ a0 = E0
+ \vdots
+ ai = Ei
+ \vdots
+ an = En
+ in
+ M
+ -------------------------- \lam{Ei} has a non-representable type.
+ letrec
+ a0 = E0 [ai=>Ei] \vdots
+ ai-1 = Ei-1 [ai=>Ei]
+ ai+1 = Ei+1 [ai=>Ei]
+ \vdots
+ an = En [ai=>Ei]
+ in
+ M[ai=>Ei]
+ \stoptrans
+
+ \startbuffer[from]
+ letrec
+ a = smallInteger 10
+ inc = λb -> add b 1
+ inc' = add 1
+ x = fromInteger a
+ in
+ inc (inc' x)
+ \stopbuffer
+
+ \startbuffer[to]
+ letrec
+ x = fromInteger (smallInteger 10)
+ in
+ (λb -> add b 1) (add 1 x)
+ \stopbuffer
+
+ \transexample{nonrepinline}{Nonrepresentable binding inlining}{from}{to}
+
+ \subsubsection[sec:normalization:specialize]{Function specialization}
+ This transform removes arguments to user-defined functions that are
+ not representable at runtime. This is done by creating a
+ \emph{specialized} version of the function that only works for one
+ particular value of that argument (in other words, the argument can be
+ removed).
+
+ Specialization means to create a specialized version of the called
+ function, with one argument already filled in. As a simple example, in
+ the following program (this is not actual Core, since it directly uses
+ a literal with the unrepresentable type \lam{GHC.Prim.Int\#}).
+
+ \startlambda
+ f = λa.λb.a + b
+ inc = λa.f a 1
+ \stoplambda
+
+ We could specialize the function \lam{f} against the literal argument
+ 1, with the following result:
+
+ \startlambda
+ f' = λa.a + 1
+ inc = λa.f' a
+ \stoplambda
+
+ In some way, this transformation is similar to β-reduction, but it
+ operates across function boundaries. It is also similar to
+ non-representable let binding inlining above, since it sort of
+ \quote{inlines} an expression into a called function.
+
+ Special care must be taken when the argument has any free variables.
+ If this is the case, the original argument should not be removed
+ completely, but replaced by all the free variables of the expression.
+ In this way, the original expression can still be evaluated inside the
+ new function.
+
+ To prevent us from propagating the same argument over and over, a
+ simple local variable reference is not propagated (since is has
+ exactly one free variable, itself, we would only replace that argument
+ with itself).
+
+ This shows that any free local variables that are not runtime
+ representable cannot be brought into normal form by this transform. We
+ rely on an inlining or β-reduction transformation to replace such a
+ variable with an expression we can propagate again.
+
+ \starttrans
+ x = E
+ ~
+ x Y0 ... Yi ... Yn \lam{Yi} is not representable
+ --------------------------------------------- \lam{Yi} is not a local variable reference
+ x' Y0 ... Yi-1 f0 ... fm Yi+1 ... Yn \lam{f0 ... fm} are all free local vars of \lam{Yi}
+ ~ \lam{T0 ... Tn} are the types of \lam{Y0 ... Yn}
+ x' = λ(y0 :: T0) ... λ(yi-1 :: Ty-1).
+ λf0 ... λfm.
+ λ(yi+1 :: Ty+1) ... λ(yn :: Tn).
+ E y0 ... yi-1 Yi yi+1 ... yn
+ \stoptrans
+
+ This is a bit of a complex transformation. It transforms an
+ application of the function \lam{x}, where one of the arguments
+ (\lam{Y_i}) is not representable. A new
+ function \lam{x'} is created that wraps the body of the old function.
+ The body of the new function becomes a number of nested lambda
+ abstractions, one for each of the original arguments that are left
+ unchanged.
+
+ The ith argument is replaced with the free variables of
+ \lam{Y_i}. Note that we reuse the same binders as those used in
+ \lam{Y_i}, since we can then just use \lam{Y_i} inside the new
+ function body and have all of the variables it uses be in scope.
+
+ The argument that we are specializing for, \lam{Y_i}, is put inside
+ the new function body. The old function body is applied to it. Since
+ we use this new function only in place of an application with that
+ particular argument \lam{Y_i}, behaviour should not change.
+
+ Note that the types of the arguments of our new function are taken
+ from the types of the \emph{actual} arguments (\lam{T0 ... Tn}). This
+ means that any polymorphism in the arguments is removed, even when the
+ corresponding explicit type lambda is not removed
+ yet.
+
+ \todo{Examples. Perhaps reference the previous sections}
+
+ \section{Unsolved problems}
+ The above system of transformations has been implemented in the prototype
+ and seems to work well to compile simple and more complex examples of
+ hardware descriptions. \todo{Ref christiaan?} However, this normalization
+ system has not seen enough review and work to be complete and work for
+ every Core expression that is supplied to it. A number of problems
+ have already been identified and are discussed in this section.
+
+ \subsection[sec:normalization:duplicatework]{Work duplication}
+ A possible problem of β-reduction is that it could duplicate work.
+ When the expression applied is not a simple variable reference, but
+ requires calculation and the binder the lambda abstraction binds to
+ is used more than once, more hardware might be generated than strictly
+ needed.
+
+ As an example, consider the expression:
+
+ \startlambda
+ (λx. x + x) (a * b)
+ \stoplambda
+
+ When applying β-reduction to this expression, we get:
+
+ \startlambda
+ (a * b) + (a * b)
+ \stoplambda
+
+ which of course calculates \lam{(a * b)} twice.
+
+ A possible solution to this would be to use the following alternative
+ transformation, which is of course no longer normal β-reduction. The
+ followin transformation has not been tested in the prototype, but is
+ given here for future reference:
+
+ \starttrans
+ (λx.E) M
+ -----------------
+ letrec x = M in E
+ \stoptrans
+
+ This does not seem like much of an improvement, but it does get rid of
+ the lambda expression (and the associated higher-order value), while
+ at the same time introducing a new let binding. Since the result of
+ every application or case expression must be bound by a let expression
+ in the intended normal form anyway, this is probably not a problem. If
+ the argument happens to be a variable reference, then simple let
+ binding removal (\in{section}[sec:normalization:simplelet]) will
+ remove it, making the result identical to that of the original
+ β-reduction transformation.
+
+ When also applying argument simplification to the above example, we
+ get the following expression:
+
+ \startlambda
+ let y = (a * b)
+ z = (a * b)
+ in y + z
+ \stoplambda
+
+ Looking at this, we could imagine an alternative approach: Create a
+ transformation that removes let bindings that bind identical values.
+ In the above expression, the \lam{y} and \lam{z} variables could be
+ merged together, resulting in the more efficient expression:
+
+ \startlambda
+ let y = (a * b) in y + y
+ \stoplambda
+
+ \subsection[sec:normalization:non-determinism]{Non-determinism}
+ As an example, again consider the following expression:
+
+ \startlambda
+ (λx. x + x) (a * b)
+ \stoplambda
+
+ We can apply both β-reduction (\in{section}[sec:normalization:beta])
+ as well as argument simplification
+ (\in{section}[sec:normalization:argsimpl]) to this expression.
+
+ When applying argument simplification first and then β-reduction, we
+ get the following expression:
+
+ \startlambda
+ let y = (a * b) in y + y
+ \stoplambda
+
+ When applying β-reduction first and then argument simplification, we
+ get the following expression:
+
+ \startlambda
+ let y = (a * b)
+ z = (a * b)
+ in y + z
+ \stoplambda
+
+ As you can see, this is a different expression. This means that the
+ order of expressions, does in fact change the resulting normal form,
+ which is something that we would like to avoid. In this particular
+ case one of the alternatives is even clearly more efficient, so we
+ would of course like the more efficient form to be the normal form.
+
+ For this particular problem, the solutions for duplication of work
+ seem from the previous section seem to fix the determinism of our
+ transformation system as well. However, it is likely that there are
+ other occurences of this problem.
+
+ \subsection[sec:normalization:castproblems]{Casts}
+ We do not fully understand the use of cast expressions in Core, so
+ there are probably expressions involving cast expressions that cannot
+ be brought into intended normal form by this transformation system.
+
+ The uses of casts in the core system should be investigated more and
+ transformations will probably need updating to handle them in all
+ cases.
+
+ \subsection[sec:normalization:stateproblems]{Normalization of stateful descriptions}
+ Currently, the intended normal form definition\refdef{intended
+ normal form definition} offers enough freedom to describe all
+ valid stateful descriptions, but is not limiting enough. It is
+ possible to write descriptions which are in intended normal
+ form, but cannot be translated into \VHDL in a meaningful way
+ (\eg, a function that swaps two substates in its result, or a
+ function that changes a substate itself instead of passing it to
+ a subfunction).
+
+ It is now up to the programmer to not do anything funny with
+ these state values, whereas the normalization just tries not to
+ mess up the flow of state values. In practice, there are
+ situations where a Core program that \emph{could} be a valid
+ stateful description is not translateable by the prototype. This
+ most often happens when statefulness is mixed with pattern
+ matching, causing a state input to be unpacked multiple times or
+ be unpacked and repacked only in some of the code paths.
+
+ Without going into detail about the exact problems (of which
+ there are probably more than have shown up so far), it seems
+ unlikely that these problems can be solved entirely by just
+ improving the \VHDL state generation in the final stage. The
+ normalization stage seems the best place to apply the rewriting
+ needed to support more complex stateful descriptions. This does
+ of course mean that the intended normal form definition must be
+ extended as well to be more specific about how state handling
+ should look like in normal form.
+ \in{Section}[sec:prototype:statelimits] already contains a
+ tight description of the limitations on the use of state
+ variables, which could be adapted into the intended normal form.
+
+ \section[sec:normalization:properties]{Provable properties}
+ When looking at the system of transformations outlined above, there are a
+ number of questions that we can ask ourselves. The main question is of course:
+ \quote{Does our system work as intended?}. We can split this question into a
+ number of subquestions: