b058b63a2a3debae92f4fe435fe1f31799555c40
[matthijs/master-project/report.git] / Chapters / Normalization.tex
1 \chapter[chap:normalization]{Normalization}
2   % A helper to print a single example in the half the page width. The example
3   % text should be in a buffer whose name is given in an argument.
4   %
5   % The align=right option really does left-alignment, but without the program
6   % will end up on a single line. The strut=no option prevents a bunch of empty
7   % space at the start of the frame.
8   \define[1]\example{
9     \framed[offset=1mm,align=right,strut=no,background=box,frame=off]{
10       \setuptyping[option=LAM,style=sans,before=,after=,strip=auto]
11       \typebuffer[#1]
12       \setuptyping[option=none,style=\tttf,strip=auto]
13     }
14   }
15
16   \define[4]\transexample{
17     \placeexample[here][ex:trans:#1]{#2}
18     \startcombination[2*1]
19       {\example{#3}}{Original program}
20       {\example{#4}}{Transformed program}
21     \stopcombination
22   }
23
24   The first step in the core to \small{VHDL} translation process, is normalization. We
25   aim to bring the core description into a simpler form, which we can
26   subsequently translate into \small{VHDL} easily. This normal form is needed because
27   the full core language is more expressive than \small{VHDL} in some
28   areas (higher-order expressions, limited polymorphism using type
29   classes, etc.) and because core can describe expressions that do not
30   have a direct hardware interpretation.
31
32   \section{Normal form}
33     The transformations described here have a well-defined goal: To bring the
34     program in a well-defined form that is directly translatable to
35     \VHDL, while fully preserving the semantics of the program. We refer
36     to this form as the \emph{normal form} of the program. The formal
37     definition of this normal form is quite simple:
38
39     \placedefinition{}{\startboxed A program is in \emph{normal form} if none of the
40     transformations from this chapter apply.\stopboxed}
41
42     Of course, this is an \quote{easy} definition of the normal form, since our
43     program will end up in normal form automatically. The more interesting part is
44     to see if this normal form actually has the properties we would like it to
45     have.
46
47     But, before getting into more definitions and details about this normal
48     form, let us try to get a feeling for it first. The easiest way to do this
49     is by describing the things that are unwanted in the intended normal form.
50
51     \startitemize
52       \item Any \emph{polymorphism} must be removed. When laying down hardware, we
53       cannot generate any signals that can have multiple types. All types must be
54       completely known to generate hardware.
55       
56       \item All \emph{higher-order} constructions must be removed. We cannot
57       generate a hardware signal that contains a function, so all values,
58       arguments and return values used must be first order.
59
60       \item All complex \emph{nested scopes} must be removed. In the \small{VHDL}
61       description, every signal is in a single scope. Also, full expressions are
62       not supported everywhere (in particular port maps can only map signal
63       names and constants, not complete expressions). To make the \small{VHDL}
64       generation easy, a separate binder must be bound to ever application or
65       other expression.
66     \stopitemize
67
68     \todo{Intermezzo: functions vs plain values}
69
70     A very simple example of a program in normal form is given in
71     \in{example}[ex:MulSum]. As you can see, all arguments to the function (which
72     will become input ports in the generated \VHDL) are at the outer level.
73     This means that the body of the inner lambda abstraction is never a
74     function, but always a plain value.
75
76     As the body of the inner lambda abstraction, we see a single (recursive)
77     let expression, that binds two variables (\lam{mul} and \lam{sum}). These
78     variables will be signals in the generated \VHDL, bound to the output port
79     of the \lam{*} and \lam{+} components.
80
81     The final line (the \quote{return value} of the function) selects the
82     \lam{sum} signal to be the output port of the function. This \quote{return
83     value} can always only be a variable reference, never a more complex
84     expression.
85
86     \todo{Add generated VHDL}
87
88     \startbuffer[MulSum]
89     alu :: Bit -> Word -> Word -> Word
90     alu = λa.λb.λc.
91         let
92           mul = (*) a b
93           sum = (+) mul c
94         in
95           sum
96     \stopbuffer
97
98     \startuseMPgraphic{MulSum}
99       save a, b, c, mul, add, sum;
100
101       % I/O ports
102       newCircle.a(btex $a$ etex) "framed(false)";
103       newCircle.b(btex $b$ etex) "framed(false)";
104       newCircle.c(btex $c$ etex) "framed(false)";
105       newCircle.sum(btex $sum$ etex) "framed(false)";
106
107       % Components
108       newCircle.mul(btex * etex);
109       newCircle.add(btex + etex);
110
111       a.c      - b.c   = (0cm, 2cm);
112       b.c      - c.c   = (0cm, 2cm);
113       add.c            = c.c + (2cm, 0cm);
114       mul.c            = midpoint(a.c, b.c) + (2cm, 0cm);
115       sum.c            = add.c + (2cm, 0cm);
116       c.c              = origin;
117
118       % Draw objects and lines
119       drawObj(a, b, c, mul, add, sum);
120
121       ncarc(a)(mul) "arcangle(15)";
122       ncarc(b)(mul) "arcangle(-15)";
123       ncline(c)(add);
124       ncline(mul)(add);
125       ncline(add)(sum);
126     \stopuseMPgraphic
127
128     \placeexample[here][ex:MulSum]{Simple architecture consisting of a
129     multiplier and a subtractor.}
130       \startcombination[2*1]
131         {\typebufferlam{MulSum}}{Core description in normal form.}
132         {\boxedgraphic{MulSum}}{The architecture described by the normal form.}
133       \stopcombination
134
135     \in{Example}[ex:MulSum] showed a function that just applied two
136     other functions (multiplication and addition), resulting in a simple
137     architecture with two components and some connections.  There is of
138     course also some mechanism for choice in the normal form. In a
139     normal Core program, the \emph{case} expression can be used in a few
140     different ways to describe choice. In normal form, this is limited
141     to a very specific form.
142
143     \in{Example}[ex:AddSubAlu] shows an example describing a
144     simple \small{ALU}, which chooses between two operations based on an opcode
145     bit. The main structure is similar to \in{example}[ex:MulSum], but this
146     time the \lam{res} variable is bound to a case expression. This case
147     expression scrutinizes the variable \lam{opcode} (and scrutinizing more
148     complex expressions is not supported). The case expression can select a
149     different variable based on the constructor of \lam{opcode}.
150     \refdef{case expression}
151
152     \startbuffer[AddSubAlu]
153     alu :: Bit -> Word -> Word -> Word
154     alu = λopcode.λa.λb.
155         let
156           res1 = (+) a b
157           res2 = (-) a b
158           res = case opcode of
159             Low -> res1
160             High -> res2
161         in
162           res
163     \stopbuffer
164
165     \startuseMPgraphic{AddSubAlu}
166       save opcode, a, b, add, sub, mux, res;
167
168       % I/O ports
169       newCircle.opcode(btex $opcode$ etex) "framed(false)";
170       newCircle.a(btex $a$ etex) "framed(false)";
171       newCircle.b(btex $b$ etex) "framed(false)";
172       newCircle.res(btex $res$ etex) "framed(false)";
173       % Components
174       newCircle.add(btex + etex);
175       newCircle.sub(btex - etex);
176       newMux.mux;
177
178       opcode.c - a.c   = (0cm, 2cm);
179       add.c    - a.c   = (4cm, 0cm);
180       sub.c    - b.c   = (4cm, 0cm);
181       a.c      - b.c   = (0cm, 3cm);
182       mux.c            = midpoint(add.c, sub.c) + (1.5cm, 0cm);
183       res.c    - mux.c = (1.5cm, 0cm);
184       b.c              = origin;
185
186       % Draw objects and lines
187       drawObj(opcode, a, b, res, add, sub, mux);
188
189       ncline(a)(add) "posA(e)";
190       ncline(b)(sub) "posA(e)";
191       nccurve(a)(sub) "posA(e)", "angleA(0)";
192       nccurve(b)(add) "posA(e)", "angleA(0)";
193       nccurve(add)(mux) "posB(inpa)", "angleB(0)";
194       nccurve(sub)(mux) "posB(inpb)", "angleB(0)";
195       nccurve(opcode)(mux) "posB(n)", "angleA(0)", "angleB(-90)";
196       ncline(mux)(res) "posA(out)";
197     \stopuseMPgraphic
198
199     \placeexample[here][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.}
200       \startcombination[2*1]
201         {\typebufferlam{AddSubAlu}}{Core description in normal form.}
202         {\boxedgraphic{AddSubAlu}}{The architecture described by the normal form.}
203       \stopcombination
204
205     As a more complete example, consider
206     \in{example}[ex:NormalComplete]. This example shows everything that
207     is allowed in normal form, except for built-in higher-order functions
208     (like \lam{map}). The graphical version of the architecture contains
209     a slightly simplified version, since the state tuple packing and
210     unpacking have been left out. Instead, two separate registers are
211     drawn. Most synthesis tools will further optimize this architecture by
212     removing the multiplexers at the register input and instead use the write
213     enable port of the register (when it is available), but we want to show
214     the architecture as close to the description as possible.
215
216     As you can see from the previous examples, the generation of the final
217     architecture from the normal form is straightforward. In each of the
218     examples, there is a direct match between the normal form structure,
219     the generated VHDL and the architecture shown in the images.
220
221     \startbuffer[NormalComplete]
222       regbank :: Bit 
223                  -> Word 
224                  -> State (Word, Word) 
225                  -> (State (Word, Word), Word)
226
227       -- All arguments are an inital lambda (address, data, packed state)
228       regbank = λa.λd.λsp.
229       -- There are nested let expressions at top level
230       let
231         -- Unpack the state by coercion (\eg, cast from
232         -- State (Word, Word) to (Word, Word))
233         s = sp ▶ (Word, Word)
234         -- Extract both registers from the state
235         r1 = case s of (a, b) -> a
236         r2 = case s of (a, b) -> b
237         -- Calling some other user-defined function.
238         d' = foo d
239         -- Conditional connections
240         out = case a of
241           High -> r1
242           Low -> r2
243         r1' = case a of
244           High -> d'
245           Low -> r1
246         r2' = case a of
247           High -> r2
248           Low -> d'
249         -- Packing a tuple
250         s' = (,) r1' r2'
251         -- pack the state by coercion (\eg, cast from
252         -- (Word, Word) to State (Word, Word))
253         sp' = s' ▶ State (Word, Word)
254         -- Pack our return value
255         res = (,) sp' out
256       in
257         -- The actual result
258         res
259     \stopbuffer
260
261     \startuseMPgraphic{NormalComplete}
262       save a, d, r, foo, muxr, muxout, out;
263
264       % I/O ports
265       newCircle.a(btex \lam{a} etex) "framed(false)";
266       newCircle.d(btex \lam{d} etex) "framed(false)";
267       newCircle.out(btex \lam{out} etex) "framed(false)";
268       % Components
269       %newCircle.add(btex + etex);
270       newBox.foo(btex \lam{foo} etex);
271       newReg.r1(btex $\lam{r1}$ etex) "dx(4mm)", "dy(6mm)";
272       newReg.r2(btex $\lam{r2}$ etex) "dx(4mm)", "dy(6mm)", "reflect(true)";
273       newMux.muxr1;
274       % Reflect over the vertical axis
275       reflectObj(muxr1)((0,0), (0,1));
276       newMux.muxr2;
277       newMux.muxout;
278       rotateObj(muxout)(-90);
279
280       d.c               = foo.c + (0cm, 1.5cm); 
281       a.c               = (xpart r2.c + 2cm, ypart d.c - 0.5cm);
282       foo.c             = midpoint(muxr1.c, muxr2.c) + (0cm, 2cm);
283       muxr1.c           = r1.c + (0cm, 2cm);
284       muxr2.c           = r2.c + (0cm, 2cm);
285       r2.c              = r1.c + (4cm, 0cm);
286       r1.c              = origin;
287       muxout.c          = midpoint(r1.c, r2.c) - (0cm, 2cm);
288       out.c             = muxout.c - (0cm, 1.5cm);
289
290     %  % Draw objects and lines
291       drawObj(a, d, foo, r1, r2, muxr1, muxr2, muxout, out);
292       
293       ncline(d)(foo);
294       nccurve(foo)(muxr1) "angleA(-90)", "posB(inpa)", "angleB(180)";
295       nccurve(foo)(muxr2) "angleA(-90)", "posB(inpb)", "angleB(0)";
296       nccurve(muxr1)(r1) "posA(out)", "angleA(180)", "posB(d)", "angleB(0)";
297       nccurve(r1)(muxr1) "posA(out)", "angleA(0)", "posB(inpb)", "angleB(180)";
298       nccurve(muxr2)(r2) "posA(out)", "angleA(0)", "posB(d)", "angleB(180)";
299       nccurve(r2)(muxr2) "posA(out)", "angleA(180)", "posB(inpa)", "angleB(0)";
300       nccurve(r1)(muxout) "posA(out)", "angleA(0)", "posB(inpb)", "angleB(-90)";
301       nccurve(r2)(muxout) "posA(out)", "angleA(180)", "posB(inpa)", "angleB(-90)";
302       % Connect port a
303       nccurve(a)(muxout) "angleA(-90)", "angleB(180)", "posB(sel)";
304       nccurve(a)(muxr1) "angleA(180)", "angleB(-90)", "posB(sel)";
305       nccurve(a)(muxr2) "angleA(180)", "angleB(-90)", "posB(sel)";
306       ncline(muxout)(out) "posA(out)";
307     \stopuseMPgraphic
308
309     \todo{Don't split registers in this image?}
310     \placeexample[here][ex:NormalComplete]{Simple architecture consisting of an adder and a
311     subtractor.}
312       \startcombination[2*1]
313         {\typebufferlam{NormalComplete}}{Core description in normal form.}
314         {\boxedgraphic{NormalComplete}}{The architecture described by the normal form.}
315       \stopcombination
316     
317
318
319     \subsection[sec:normalization:intendednormalform]{Intended normal form definition}
320       Now we have some intuition for the normal form, we can describe how we want
321       the normal form to look like in a slightly more formal manner. The following
322       EBNF-like description captures most of the intended structure (and
323       generates a subset of \GHC's core format). 
324       
325       There are two things missing: Cast expressions are sometimes
326       allowed by the prototype, but not specified here and the below
327       definition allows uses of state that cannot be translated to \VHDL\
328       properly. These two problems are discussed in
329       \in{section}[sec:normalization:castproblems] and
330       \in{section}[sec:normalization:stateproblems] respectively.
331
332       Some clauses have an expression listed behind them in parentheses.
333       These are conditions that need to apply to the clause. The
334       predicates used there (\lam{lvar()}, \lam{representable()},
335       \lam{gvar()}) will be defined in
336       \in{section}[sec:normalization:predicates].
337
338       An expression is in normal form if it matches the first
339       definition, \emph{normal}.
340
341       \todo{Fix indentation}
342       \startbuffer[IntendedNormal]
343       \italic{normal} := \italic{lambda}
344       \italic{lambda} := λvar.\italic{lambda}                        (representable(var))
345                       | \italic{toplet} 
346       \italic{toplet} := letrec [\italic{binding}...] in var         (representable(var))
347       \italic{binding} := var = \italic{rhs}                         (representable(rhs))
348                        -- State packing and unpacking by coercion
349                        | var0 = var1 ▶ State ty                      (lvar(var1))
350                        | var0 = var1 ▶ ty                            (var1 :: State ty ∧ lvar(var1))
351       \italic{rhs} := \italic{userapp}
352                    | \italic{builtinapp}
353                    -- Extractor case
354                    | case var of C a0 ... an -> ai                   (lvar(var))
355                    -- Selector case
356                    | case var of                                     (lvar(var))
357                       [ DEFAULT -> var ]                             (lvar(var))
358                       C0 w0,0 ... w0,n -> var0
359                       \vdots
360                       Cm wm,0 ... wm,n -> varm                       (\forall{}i \forall{}j, wi,j \neq vari, lvar(vari))
361       \italic{userapp} := \italic{userfunc}
362                        | \italic{userapp} {userarg}
363       \italic{userfunc} := var                                       (gvar(var))
364       \italic{userarg} := var                                        (lvar(var))
365       \italic{builtinapp} := \italic{builtinfunc}
366                           | \italic{builtinapp} \italic{builtinarg}
367       \italic{built-infunc} := var                                    (bvar(var))
368       \italic{built-inarg} := var                                     (representable(var) ∧ lvar(var))
369                           | \italic{partapp}                         (partapp :: a -> b)
370                           | \italic{coreexpr}                        (¬representable(coreexpr) ∧ ¬(coreexpr :: a -> b))
371       \italic{partapp} := \italic{userapp} 
372                        | \italic{builtinapp}
373       \stopbuffer
374
375       \placedefinition[][def:IntendedNormal]{Definition of the intended nnormal form using an \small{EBNF}-like syntax.}
376           {\defref{intended normal form definition}
377            \typebufferlam{IntendedNormal}}
378
379       When looking at such a program from a hardware perspective, the
380       top level lambda abstractions define the input ports. Lambda
381       abstractions cannot appear anywhere else. The variable reference
382       in the body of the recursive let expression is the output port.
383       Most function applications bound by the let expression define a
384       component instantiation, where the input and output ports are
385       mapped to local signals or arguments. Some of the others use a
386       built-in construction (\eg\ the \lam{case} expression) or call a
387       built-in function (\eg\ \lam{+} or \lam{map}). For these, a
388       hardcoded \small{VHDL} translation is available.
389
390   \section[sec:normalization:transformation]{Transformation notation}
391     To be able to concisely present transformations, we use a specific format
392     for them. It is a simple format, similar to one used in logic reasoning.
393
394     Such a transformation description looks like the following.
395
396     \starttrans
397     <context conditions>
398     ~
399     <original expression>
400     --------------------------          <expression conditions>
401     <transformed expression>
402     ~
403     <context additions>
404     \stoptrans
405
406     This format describes a transformation that applies to \lam{<original
407     expression>} and transforms it into \lam{<transformed expression>}, assuming
408     that all conditions are satisfied. In this format, there are a number of placeholders
409     in pointy brackets, most of which should be rather obvious in their meaning.
410     Nevertheless, we will more precisely specify their meaning below:
411
412       \startdesc{<original expression>} The expression pattern that will be matched
413       against (subexpressions of) the expression to be transformed. We call this a
414       pattern, because it can contain \emph{placeholders} (variables), which match
415       any expression or binder. Any such placeholder is said to be \emph{bound} to
416       the expression it matches. It is convention to use an uppercase letter (\eg\
417       \lam{M} or \lam{E}) to refer to any expression (including a simple variable
418       reference) and lowercase letters (\eg\ \lam{v} or \lam{b}) to refer to
419       (references to) binders.
420
421       For example, the pattern \lam{a + B} will match the expression 
422       \lam{v + (2 * w)} (binding \lam{a} to \lam{v} and \lam{B} to 
423       \lam{(2 * w)}), but not \lam{(2 * w) + v}.
424       \stopdesc
425
426       \startdesc{<expression conditions>}
427       These are extra conditions on the expression that is matched. These
428       conditions can be used to further limit the cases in which the
429       transformation applies, commonly to prevent a transformation from
430       causing a loop with itself or another transformation.
431
432       Only if these conditions are \emph{all} satisfied, the transformation
433       applies.
434       \stopdesc
435
436       \startdesc{<context conditions>}
437       These are a number of extra conditions on the context of the function. In
438       particular, these conditions can require some (other) top level function to be
439       present, whose value matches the pattern given here. The format of each of
440       these conditions is: \lam{binder = <pattern>}.
441
442       Typically, the binder is some placeholder bound in the \lam{<original
443       expression>}, while the pattern contains some placeholders that are used in
444       the \lam{transformed expression}.
445       
446       Only if a top level binder exists that matches each binder and pattern,
447       the transformation applies.
448       \stopdesc
449
450       \startdesc{<transformed expression>}
451       This is the expression template that is the result of the transformation. If, looking
452       at the above three items, the transformation applies, the \lam{<original
453       expression>} is completely replaced by the \lam{<transformed expression>}.
454       We call this a template, because it can contain placeholders, referring to
455       any placeholder bound by the \lam{<original expression>} or the
456       \lam{<context conditions>}. The resulting expression will have those
457       placeholders replaced by the values bound to them.
458
459       Any binder (lowercase) placeholder that has no value bound to it yet will be
460       bound to (and replaced with) a fresh binder.
461       \stopdesc
462
463       \startdesc{<context additions>}
464       These are templates for new functions to be added to the context.
465       This is a way to let a transformation create new top level
466       functions.
467
468       Each addition has the form \lam{binder = template}. As above, any
469       placeholder in the addition is replaced with the value bound to it, and any
470       binder placeholder that has no value bound to it yet will be bound to (and
471       replaced with) a fresh binder.
472       \stopdesc
473
474     To understand this notation better, the step by step application of
475     the η-abstraction transformation to a simple \small{ALU} will be
476     shown. Consider η-abstraction, which is a common transformation from
477     labmda calculus, described using above notation as follows:
478
479     \starttrans
480     E                 \lam{E :: a -> b}
481     --------------    \lam{E} does not occur on a function position in an application
482     λx.E x            \lam{E} is not a lambda abstraction.
483     \stoptrans
484
485     η-abstraction is a well known transformation from lambda calculus. What
486     this transformation does, is take any expression that has a function type
487     and turn it into a lambda expression (giving an explicit name to the
488     argument). There are some extra conditions that ensure that this
489     transformation does not apply infinitely (which are not necessarily part
490     of the conventional definition of η-abstraction).
491
492     Consider the following function, in Core notation, which is a fairly obvious way to specify a
493     simple \small{ALU} (Note that it is not yet in normal form, but
494     \in{example}[ex:AddSubAlu] shows the normal form of this function).
495     The parentheses around the \lam{+} and \lam{-} operators are
496     commonly used in Haskell to show that the operators are used as
497     normal functions, instead of \emph{infix} operators (\eg, the
498     operators appear before their arguments, instead of in between).
499
500     \startlambda 
501     alu :: Bit -> Word -> Word -> Word
502     alu = λopcode. case opcode of
503       Low -> (+)
504       High -> (-)
505     \stoplambda
506
507     There are a few subexpressions in this function to which we could possibly
508     apply the transformation. Since the pattern of the transformation is only
509     the placeholder \lam{E}, any expression will match that. Whether the
510     transformation applies to an expression is thus solely decided by the
511     conditions to the right of the transformation.
512
513     We will look at each expression in the function in a top down manner. The
514     first expression is the entire expression the function is bound to.
515
516     \startlambda
517     λopcode. case opcode of
518       Low -> (+)
519       High -> (-)
520     \stoplambda
521
522     As said, the expression pattern matches this. The type of this expression is
523     \lam{Bit -> Word -> Word -> Word}, which matches \lam{a -> b} (Note that in
524     this case \lam{a = Bit} and \lam{b = Word -> Word -> Word}).
525
526     Since this expression is at top level, it does not occur at a function
527     position of an application. However, The expression is a lambda abstraction,
528     so this transformation does not apply.
529
530     The next expression we could apply this transformation to, is the body of
531     the lambda abstraction:
532
533     \startlambda
534     case opcode of
535       Low -> (+)
536       High -> (-)
537     \stoplambda
538
539     The type of this expression is \lam{Word -> Word -> Word}, which again
540     matches \lam{a -> b}. The expression is the body of a lambda expression, so
541     it does not occur at a function position of an application. Finally, the
542     expression is not a lambda abstraction but a case expression, so all the
543     conditions match. There are no context conditions to match, so the
544     transformation applies.
545
546     By now, the placeholder \lam{E} is bound to the entire expression. The
547     placeholder \lam{x}, which occurs in the replacement template, is not bound
548     yet, so we need to generate a fresh binder for that. Let us use the binder
549     \lam{a}. This results in the following replacement expression:
550
551     \startlambda
552     λa.(case opcode of
553       Low -> (+)
554       High -> (-)) a
555     \stoplambda
556
557     Continuing with this expression, we see that the transformation does not
558     apply again (it is a lambda expression). Next we look at the body of this
559     lambda abstraction:
560
561     \startlambda
562     (case opcode of
563       Low -> (+)
564       High -> (-)) a
565     \stoplambda
566     
567     Here, the transformation does apply, binding \lam{E} to the entire
568     expression (which has type \lam{Word -> Word}) and binding \lam{x}
569     to the fresh binder \lam{b}, resulting in the replacement:
570
571     \startlambda
572     λb.(case opcode of
573       Low -> (+)
574       High -> (-)) a b
575     \stoplambda
576
577     The transformation does not apply to this lambda abstraction, so we
578     look at its body. For brevity, we will put the case expression on one line from
579     now on.
580
581     \startlambda
582     (case opcode of Low -> (+); High -> (-)) a b
583     \stoplambda
584
585     The type of this expression is \lam{Word}, so it does not match \lam{a -> b}
586     and the transformation does not apply. Next, we have two options for the
587     next expression to look at: The function position and argument position of
588     the application. The expression in the argument position is \lam{b}, which
589     has type \lam{Word}, so the transformation does not apply. The expression in
590     the function position is:
591
592     \startlambda
593     (case opcode of Low -> (+); High -> (-)) a
594     \stoplambda
595
596     Obviously, the transformation does not apply here, since it occurs in
597     function position (which makes the second condition false). In the same
598     way the transformation does not apply to both components of this
599     expression (\lam{case opcode of Low -> (+); High -> (-)} and \lam{a}), so
600     we will skip to the components of the case expression: The scrutinee and
601     both alternatives. Since the opcode is not a function, it does not apply
602     here.
603
604     The first alternative is \lam{(+)}. This expression has a function type
605     (the operator still needs two arguments). It does not occur in function
606     position of an application and it is not a lambda expression, so the
607     transformation applies.
608
609     We look at the \lam{<original expression>} pattern, which is \lam{E}.
610     This means we bind \lam{E} to \lam{(+)}. We then replace the expression
611     with the \lam{<transformed expression>}, replacing all occurences of
612     \lam{E} with \lam{(+)}. In the \lam{<transformed expression>}, the This gives us the replacement expression:
613     \lam{λx.(+) x} (A lambda expression binding \lam{x}, with a body that
614     applies the addition operator to \lam{x}).
615
616     The complete function then becomes:
617     \startlambda
618     (case opcode of Low -> λa1.(+) a1; High -> (-)) a
619     \stoplambda
620
621     Now the transformation no longer applies to the complete first alternative
622     (since it is a lambda expression). It does not apply to the addition
623     operator again, since it is now in function position in an application. It
624     does, however, apply to the application of the addition operator, since
625     that is neither a lambda expression nor does it occur in function
626     position. This means after one more application of the transformation, the
627     function becomes:
628
629     \startlambda
630     (case opcode of Low -> λa1.λb1.(+) a1 b1; High -> (-)) a
631     \stoplambda
632
633     The other alternative is left as an exercise to the reader. The final
634     function, after applying η-abstraction until it does no longer apply is:
635
636     \startlambda 
637     alu :: Bit -> Word -> Word -> Word
638     alu = λopcode.λa.b. (case opcode of
639       Low -> λa1.λb1 (+) a1 b1
640       High -> λa2.λb2 (-) a2 b2) a b
641     \stoplambda
642
643     \subsection{Transformation application}
644       In this chapter we define a number of transformations, but how will we apply
645       these? As stated before, our normal form is reached as soon as no
646       transformation applies anymore. This means our application strategy is to
647       simply apply any transformation that applies, and continuing to do that with
648       the result of each transformation.
649
650       In particular, we define no particular order of transformations. Since
651       transformation order should not influence the resulting normal form,
652       this leaves the implementation free to choose any application order that
653       results in an efficient implementation. Unfortunately this is not
654       entirely true for the current set of transformations. See
655       \in{section}[sec:normalization:non-determinism] for a discussion of this
656       problem.
657
658       When applying a single transformation, we try to apply it to every (sub)expression
659       in a function, not just the top level function body. This allows us to
660       keep the transformation descriptions concise and powerful.
661
662     \subsection{Definitions}
663       A \emph{global variable} is any variable (binder) that is bound at the
664       top level of a program, or an external module. A \emph{local variable} is any
665       other variable (\eg, variables local to a function, which can be bound by
666       lambda abstractions, let expressions and pattern matches of case
667       alternatives). This is a slightly different notion of global versus
668       local than what \small{GHC} uses internally, but for our purposes
669       the distinction \GHC\ makes is not useful.
670       \defref{global variable} \defref{local variable}
671
672       A \emph{hardware representable} (or just \emph{representable}) type or value
673       is (a value of) a type that we can generate a signal for in hardware. For
674       example, a bit, a vector of bits, a 32 bit unsigned word, etc. Values that are
675       not runtime representable notably include (but are not limited to): Types,
676       dictionaries, functions.
677       \defref{representable}
678
679       A \emph{built-in function} is a function supplied by the Cλash framework, whose
680       implementation is not valid Cλash. The implementation is of course valid
681       Haskell, for simulation, but it is not expressable in Cλash.
682       \defref{built-in function} \defref{user-defined function}
683
684       For these functions, Cλash has a \emph{built-in hardware translation}, so calls
685       to these functions can still be translated. These are functions like
686       \lam{map}, \lam{hwor} and \lam{length}.
687
688       A \emph{user-defined} function is a function for which we do have a Cλash
689       implementation available.
690
691       \subsubsection[sec:normalization:predicates]{Predicates}
692         Here, we define a number of predicates that can be used below to concisely
693         specify conditions.
694
695         \emph{gvar(expr)} is true when \emph{expr} is a variable that references a
696         global variable. It is false when it references a local variable.
697
698         \emph{lvar(expr)} is the complement of \emph{gvar}; it is true when \emph{expr}
699         references a local variable, false when it references a global variable.
700
701         \emph{representable(expr)} is true when \emph{expr} is \emph{representable}.
702
703     \subsection[sec:normalization:uniq]{Binder uniqueness}
704       A common problem in transformation systems, is binder uniqueness. When not
705       considering this problem, it is easy to create transformations that mix up
706       bindings and cause name collisions. Take for example, the following core
707       expression:
708
709       \startlambda
710       (λa.λb.λc. a * b * c) x c
711       \stoplambda
712
713       By applying β-reduction (see \in{section}[sec:normalization:beta]) once,
714       we can simplify this expression to:
715
716       \startlambda
717       (λb.λc. x * b * c) c
718       \stoplambda
719
720       Now, we have replaced the \lam{a} binder with a reference to the \lam{x}
721       binder. No harm done here. But note that we see multiple occurences of the
722       \lam{c} binder. The first is a binding occurence, to which the second refers.
723       The last, however refers to \emph{another} instance of \lam{c}, which is
724       bound somewhere outside of this expression. Now, if we would apply beta
725       reduction without taking heed of binder uniqueness, we would get:
726
727       \startlambda
728       λc. x * c * c
729       \stoplambda
730
731       This is obviously not what was supposed to happen! The root of this problem is
732       the reuse of binders: Identical binders can be bound in different,
733       but overlapping scopes. Any variable reference in those
734       overlapping scopes then refers to the variable bound in the inner
735       (smallest) scope. There is not way to refer to the variable in the
736       outer scope. This effect is usually referred to as
737       \emph{shadowing}: When a binder is bound in a scope where the
738       binder already had a value, the inner binding is said to
739       \emph{shadow} the outer binding. In the example above, the \lam{c}
740       binder was bound outside of the expression and in the inner lambda
741       expression. Inside that lambda expression, only the inner \lam{c}
742       can be accessed.
743
744       There are a number of ways to solve this. \small{GHC} has isolated this
745       problem to their binder substitution code, which performs \emph{deshadowing}
746       during its expression traversal. This means that any binding that shadows
747       another binding on a higher level is replaced by a new binder that does not
748       shadow any other binding. This non-shadowing invariant is enough to prevent
749       binder uniqueness problems in \small{GHC}.
750
751       In our transformation system, maintaining this non-shadowing invariant is
752       a bit harder to do (mostly due to implementation issues, the prototype
753       does not use \small{GHC}'s subsitution code). Also, the following points
754       can be observed.
755
756       \startitemize
757       \item Deshadowing does not guarantee overall uniqueness. For example, the
758       following (slightly contrived) expression shows the identifier \lam{x} bound in
759       two seperate places (and to different values), even though no shadowing
760       occurs.
761
762       \startlambda
763       (let x = 1 in x) + (let x = 2 in x)
764       \stoplambda
765
766       \item In our normal form (and the resulting \small{VHDL}), all binders
767       (signals) within the same function (entity) will end up in the same
768       scope. To allow this, all binders within the same function should be
769       unique.
770
771       \item When we know that all binders in an expression are unique, moving around
772       or removing a subexpression will never cause any binder conflicts. If we have
773       some way to generate fresh binders, introducing new subexpressions will not
774       cause any problems either. The only way to cause conflicts is thus to
775       duplicate an existing subexpression.
776       \stopitemize
777
778       Given the above, our prototype maintains a unique binder invariant. This
779       means that in any given moment during normalization, all binders \emph{within
780       a single function} must be unique. To achieve this, we apply the following
781       technique.
782
783       \todo{Define fresh binders and unique supplies}
784
785       \startitemize
786       \item Before starting normalization, all binders in the function are made
787       unique. This is done by generating a fresh binder for every binder used. This
788       also replaces binders that did not cause any conflict, but it does ensure that
789       all binders within the function are generated by the same unique supply.
790       \refdef{fresh binder}
791       \item Whenever a new binder must be generated, we generate a fresh binder that
792       is guaranteed to be different from \emph{all binders generated so far}. This
793       can thus never introduce duplication and will maintain the invariant.
794       \item Whenever (a part of) an expression is duplicated (for example when
795       inlining), all binders in the expression are replaced with fresh binders
796       (using the same method as at the start of normalization). These fresh binders
797       can never introduce duplication, so this will maintain the invariant.
798       \item Whenever we move part of an expression around within the function, there
799       is no need to do anything special. There is obviously no way to introduce
800       duplication by moving expressions around. Since we know that each of the
801       binders is already unique, there is no way to introduce (incorrect) shadowing
802       either.
803       \stopitemize
804
805   \section{Transform passes}
806     In this section we describe the actual transforms.
807
808     Each transformation will be described informally first, explaining
809     the need for and goal of the transformation. Then, we will formally define
810     the transformation using the syntax introduced in
811     \in{section}[sec:normalization:transformation].
812
813     \subsection{General cleanup}
814       These transformations are general cleanup transformations, that aim to
815       make expressions simpler. These transformations usually clean up the
816        mess left behind by other transformations or clean up expressions to
817        expose new transformation opportunities for other transformations.
818
819        Most of these transformations are standard optimizations in other
820        compilers as well. However, in our compiler, most of these are not just
821        optimizations, but they are required to get our program into intended
822        normal form.
823
824         \placeintermezzo{}{
825           \defref{substitution notation}
826           \startframedtext[width=8cm,background=box,frame=no]
827           \startalignment[center]
828             {\tfa Substitution notation}
829           \stopalignment
830           \blank[medium]
831
832           In some of the transformations in this chapter, we need to perform
833           substitution on an expression. Substitution means replacing every
834           occurence of some expression (usually a variable reference) with
835           another expression.
836
837           There have been a lot of different notations used in literature for
838           specifying substitution. The notation that will be used in this report
839           is the following:
840
841           \startlambda
842             E[A=>B]
843           \stoplambda
844
845           This means expression \lam{E} with all occurences of \lam{A} replaced
846           with \lam{B}.
847           \stopframedtext
848         }
849
850       \subsubsection[sec:normalization:beta]{β-reduction}
851         β-reduction is a well known transformation from lambda calculus, where it is
852         the main reduction step. It reduces applications of lambda abstractions,
853         removing both the lambda abstraction and the application.
854
855         In our transformation system, this step helps to remove unwanted lambda
856         abstractions (basically all but the ones at the top level). Other
857         transformations (application propagation, non-representable inlining) make
858         sure that most lambda abstractions will eventually be reducable by
859         β-reduction.
860
861         Note that β-reduction also works on type lambda abstractions and type
862         applications as well. This means the substitution below also works on
863         type variables, in the case that the binder is a type variable and teh
864         expression applied to is a type.
865
866         \starttrans
867         (λx.E) M
868         -----------------
869         E[x=>M]
870         \stoptrans
871
872         % And an example
873         \startbuffer[from]
874         (λa. 2 * a) (2 * b)
875         \stopbuffer
876
877         \startbuffer[to]
878         2 * (2 * b)
879         \stopbuffer
880
881         \transexample{beta}{β-reduction}{from}{to}
882
883         \startbuffer[from]
884         (λt.λa::t. a) @Int
885         \stopbuffer
886
887         \startbuffer[to]
888         (λa::Int. a)
889         \stopbuffer
890
891         \transexample{beta-type}{β-reduction for type abstractions}{from}{to}
892        
893       \subsubsection{Unused let binding removal}
894         This transformation removes let bindings that are never used.
895         Occasionally, \GHC's desugarer introduces some unused let bindings.
896
897         This normalization pass should really be not be necessary to get
898         into intended normal form (since the intended normal form
899         definition \refdef{intended normal form definition} does not
900         require that every binding is used), but in practice the
901         desugarer or simplifier emits some bindings that cannot be
902         normalized (e.g., calls to a
903         \hs{Control.Exception.Base.patError}) but are not used anywhere
904         either. To prevent the \VHDL\ generation from breaking on these
905         artifacts, this transformation removes them.
906
907         \todo{Do not use old-style numerals in transformations}
908         \starttrans
909         letrec
910           a0 = E0
911           \vdots
912           ai = Ei
913           \vdots
914           an = En
915         in
916           M                             \lam{ai} does not occur free in \lam{M}
917         ----------------------------    \lam{\forall j, 0 ≤ j ≤ n, j ≠ i} (\lam{ai} does not occur free in \lam{Ej})
918         letrec
919           a0 = E0
920           \vdots
921           ai-1 = Ei-1
922           ai+1 = Ei+1
923           \vdots
924           an = En
925         in
926           M
927         \stoptrans
928
929         % And an example
930         \startbuffer[from]
931         let
932           x = 1
933         in
934           2
935         \stopbuffer
936
937         \startbuffer[to]
938         let
939         in
940           2
941         \stopbuffer
942
943         \transexample{unusedlet}{Unused let binding removal}{from}{to}
944
945       \subsubsection{Empty let removal}
946         This transformation is simple: It removes recursive lets that have no bindings
947         (which usually occurs when unused let binding removal removes the last
948         binding from it).
949
950         Note that there is no need to define this transformation for
951         non-recursive lets, since they always contain exactly one binding.
952
953         \starttrans
954         letrec in M
955         --------------
956         M
957         \stoptrans
958
959         % And an example
960         \startbuffer[from]
961         let
962         in
963           2
964         \stopbuffer
965
966         \startbuffer[to]
967           2
968         \stopbuffer
969
970         \transexample{emptylet}{Empty let removal}{from}{to}
971
972       \subsubsection[sec:normalization:simplelet]{Simple let binding removal}
973         This transformation inlines simple let bindings, that bind some
974         binder to some other binder instead of a more complex expression (\ie\
975         a = b).
976
977         This transformation is not needed to get an expression into intended
978         normal form (since these bindings are part of the intended normal
979         form), but makes the resulting \small{VHDL} a lot shorter.
980        
981         \refdef{substitution notation}
982         \starttrans
983         letrec
984           a0 = E0
985           \vdots
986           ai = b
987           \vdots
988           an = En
989         in
990           M
991         -----------------------------  \lam{b} is a variable reference
992         letrec                         \lam{ai} ≠ \lam{b}
993           a0 = E0 [ai=>b]
994           \vdots
995           ai-1 = Ei-1 [ai=>b]
996           ai+1 = Ei+1 [ai=>b]
997           \vdots
998           an = En [ai=>b]
999         in
1000           M[ai=>b]
1001         \stoptrans
1002
1003         \todo{example}
1004
1005       \subsubsection{Cast propagation / simplification}
1006         This transform pushes casts down into the expression as far as
1007         possible. This transformation has been added to make a few
1008         specific corner cases work, but it is not clear yet if this
1009         transformation handles cast expressions completely or in the
1010         right way. See \in{section}[sec:normalization:castproblems].
1011
1012         \starttrans
1013         (let binds in E) ▶ T
1014         -------------------------
1015         let binds in (E ▶ T)
1016         \stoptrans
1017
1018         \starttrans
1019         (case S of
1020           p0 -> E0
1021           \vdots
1022           pn -> En
1023         ) ▶ T
1024         -------------------------
1025         case S of
1026           p0 -> E0 ▶ T
1027           \vdots
1028           pn -> En ▶ T
1029         \stoptrans
1030
1031       \subsubsection{Top level binding inlining}
1032         \refdef{top level binding}
1033         This transform takes simple top level bindings generated by the
1034         \small{GHC} compiler. \small{GHC} sometimes generates very simple
1035         \quote{wrapper} bindings, which are bound to just a variable
1036         reference, or contain just a (partial) function appliation with
1037         the type and dictionary arguments filled in (such as the
1038         \lam{(+)} in the example below).
1039
1040         Note that this transformation is completely optional. It is not
1041         required to get any function into intended normal form, but it does help making
1042         the resulting VHDL output easier to read (since it removes components
1043         that do not add any real structure, but do hide away operations and
1044         cause extra clutter).
1045
1046         This transform takes any top level binding generated by \GHC,
1047         whose normalized form contains only a single let binding.
1048
1049         \starttrans
1050         x = λa0 ... λan.let y = E in y
1051         ~
1052         x
1053         --------------------------------------         \lam{x} is generated by the compiler
1054         λa0 ... λan.let y = E in y
1055         \stoptrans
1056
1057         \startbuffer[from]
1058         (+) :: Word -> Word -> Word
1059         (+) = GHC.Num.(+) @Word \$dNum
1060         ~
1061         (+) a b
1062         \stopbuffer
1063         \startbuffer[to]
1064         GHC.Num.(+) @ Alu.Word \$dNum a b
1065         \stopbuffer
1066
1067         \transexample{toplevelinline}{Top level binding inlining}{from}{to}
1068        
1069         \in{Example}[ex:trans:toplevelinline] shows a typical application of
1070         the addition operator generated by \GHC. The type and dictionary
1071         arguments used here are described in
1072         \in{Section}[section:prototype:polymorphism].
1073
1074         Without this transformation, there would be a \lam{(+)} entity
1075         in the \VHDL\ which would just add its inputs. This generates a
1076         lot of overhead in the \VHDL, which is particularly annoying
1077         when browsing the generated RTL schematic (especially since most
1078         non-alphanumerics, like all characters in \lam{(+)}, are not
1079         allowed in \VHDL\ architecture names\footnote{Technically, it is
1080         allowed to use non-alphanumerics when using extended
1081         identifiers, but it seems that none of the tooling likes
1082         extended identifiers in filenames, so it effectively does not
1083         work.}, so the entity would be called \quote{w7aA7f} or
1084         something similarly meaningless and autogenerated).
1085
1086     \subsection{Program structure}
1087       These transformations are aimed at normalizing the overall structure
1088       into the intended form. This means ensuring there is a lambda abstraction
1089       at the top for every argument (input port or current state), putting all
1090       of the other value definitions in let bindings and making the final
1091       return value a simple variable reference.
1092
1093       \subsubsection[sec:normalization:eta]{η-abstraction}
1094         This transformation makes sure that all arguments of a function-typed
1095         expression are named, by introducing lambda expressions. When combined with
1096         β-reduction and non-representable binding inlining, all function-typed
1097         expressions should be lambda abstractions or global identifiers.
1098
1099         \starttrans
1100         E                 \lam{E :: a -> b}
1101         --------------    \lam{E} does not occur on a function position in an application
1102         λx.E x            \lam{E} is not a lambda abstraction.
1103         \stoptrans
1104
1105         \startbuffer[from]
1106         foo = λa.case a of 
1107           True -> λb.mul b b
1108           False -> id
1109         \stopbuffer
1110
1111         \startbuffer[to]
1112         foo = λa.λx.(case a of 
1113             True -> λb.mul b b
1114             False -> λy.id y) x
1115         \stopbuffer
1116
1117         \transexample{eta}{η-abstraction}{from}{to}
1118
1119       \subsubsection[sec:normalization:appprop]{Application propagation}
1120         This transformation is meant to propagate application expressions downwards
1121         into expressions as far as possible. This allows partial applications inside
1122         expressions to become fully applied and exposes new transformation
1123         opportunities for other transformations (like β-reduction and
1124         specialization).
1125
1126         Since all binders in our expression are unique (see
1127         \in{section}[sec:normalization:uniq]), there is no risk that we will
1128         introduce unintended shadowing by moving an expression into a lower
1129         scope. Also, since only move expression into smaller scopes (down into
1130         our expression), there is no risk of moving a variable reference out
1131         of the scope in which it is defined.
1132
1133         \starttrans
1134         (letrec binds in E) M
1135         ------------------------
1136         letrec binds in E M
1137         \stoptrans
1138
1139         % And an example
1140         \startbuffer[from]
1141         ( letrec
1142             val = 1
1143           in 
1144             add val
1145         ) 3
1146         \stopbuffer
1147
1148         \startbuffer[to]
1149         letrec
1150           val = 1
1151         in 
1152           add val 3
1153         \stopbuffer
1154
1155         \transexample{appproplet}{Application propagation for a let expression}{from}{to}
1156
1157         \starttrans
1158         (case x of
1159           p0 -> E0
1160           \vdots
1161           pn -> En) M
1162         -----------------
1163         case x of
1164           p0 -> E0 M
1165           \vdots
1166           pn -> En M
1167         \stoptrans
1168
1169         % And an example
1170         \startbuffer[from]
1171         ( case x of 
1172             True -> id
1173             False -> neg
1174         ) 1
1175         \stopbuffer
1176
1177         \startbuffer[to]
1178         case x of 
1179           True -> id 1
1180           False -> neg 1
1181         \stopbuffer
1182
1183         \transexample{apppropcase}{Application propagation for a case expression}{from}{to}
1184
1185       \subsubsection[sec:normalization:letrecurse]{Let recursification}
1186         This transformation makes all non-recursive lets recursive. In the
1187         end, we want a single recursive let in our normalized program, so all
1188         non-recursive lets can be converted. This also makes other
1189         transformations simpler: They only need to be specified for recursive
1190         let expressions (and simply will not apply to non-recursive let
1191         expressions until this transformation has been applied).
1192
1193         \starttrans
1194         let
1195           a = E
1196         in
1197           M
1198         ------------------------------------------
1199         letrec
1200           a = E
1201         in
1202           M
1203         \stoptrans
1204
1205       \subsubsection{Let flattening}
1206         This transformation puts nested lets in the same scope, by lifting the
1207         binding(s) of the inner let into the outer let. Eventually, this will
1208         cause all let bindings to appear in the same scope.
1209
1210         This transformation only applies to recursive lets, since all
1211         non-recursive lets will be made recursive (see
1212         \in{section}[sec:normalization:letrecurse]).
1213
1214         Since we are joining two scopes together, there is no risk of moving a
1215         variable reference out of the scope where it is defined.
1216
1217         \starttrans
1218         letrec 
1219           a0 = E0
1220           \vdots
1221           ai = (letrec bindings in M)
1222           \vdots
1223           an = En
1224         in
1225           N
1226         ------------------------------------------
1227         letrec
1228           a0 = E0
1229           \vdots
1230           ai = M
1231           \vdots
1232           an = En
1233           bindings
1234         in
1235           N
1236         \stoptrans
1237
1238         \startbuffer[from]
1239         letrec
1240           a = 1
1241           b = letrec
1242             x = a
1243             y = c
1244           in
1245             x + y
1246           c = 2
1247         in
1248           b
1249         \stopbuffer
1250         \startbuffer[to]
1251         letrec
1252           a = 1
1253           b = x + y
1254           c = 2
1255           x = a
1256           y = c
1257         in
1258           b
1259         \stopbuffer
1260
1261         \transexample{letflat}{Let flattening}{from}{to}
1262
1263       \subsubsection{Return value simplification}
1264         This transformation ensures that the return value of a function is always a
1265         simple local variable reference.
1266
1267         This transformation only applies to the entire body of a
1268         function instead of any subexpression in a function. This is
1269         achieved by the contexts, like \lam{x = E}, though this is
1270         strictly not correct (you could read this as "if there is any
1271         function \lam{x} that binds \lam{E}, any \lam{E} can be
1272         transformed, while we only mean the \lam{E} that is bound by
1273         \lam{x}).
1274
1275         Note that the return value is not simplified if its not
1276         representable.  Otherwise, this would cause a direct loop with
1277         the inlining of unrepresentable bindings. If the return value is
1278         not representable because it has a function type, η-abstraction
1279         should make sure that this transformation will eventually apply.
1280         If the value is not representable for other reasons, the
1281         function result itself is not representable, meaning this
1282         function is not translatable anyway.
1283
1284         \starttrans
1285         x = E                            \lam{E} is representable
1286         ~                                \lam{E} is not a lambda abstraction
1287         E                                \lam{E} is not a let expression
1288         ---------------------------      \lam{E} is not a local variable reference
1289         letrec x = E in x
1290         \stoptrans
1291
1292         \starttrans
1293         x = λv0 ... λvn.E
1294         ~                                \lam{E} is representable
1295         E                                \lam{E} is not a let expression
1296         ---------------------------      \lam{E} is not a local variable reference
1297         letrec x = E in x
1298         \stoptrans
1299
1300         \starttrans
1301         x = λv0 ... λvn.let ... in E
1302         ~                                \lam{E} is representable
1303         E                                \lam{E} is not a local variable reference
1304         -----------------------------
1305         letrec x = E in x
1306         \stoptrans
1307
1308         \startbuffer[from]
1309         x = add 1 2
1310         \stopbuffer
1311
1312         \startbuffer[to]
1313         x = letrec x = add 1 2 in x
1314         \stopbuffer
1315
1316         \transexample{retvalsimpl}{Return value simplification}{from}{to}
1317         
1318         \todo{More examples}
1319
1320     \subsection[sec:normalization:argsimpl]{Representable arguments simplification}
1321       This section contains just a single transformation that deals with
1322       representable arguments in applications. Non-representable arguments are
1323       handled by the transformations in
1324       \in{section}[sec:normalization:nonrep]. 
1325       
1326       This transformation ensures that all representable arguments will become
1327       references to local variables. This ensures they will become references
1328       to local signals in the resulting \small{VHDL}, which is required due to
1329       limitations in the component instantiation code in \VHDL\ (one can only
1330       assign a signal or constant to an input port). By ensuring that all
1331       arguments are always simple variable references, we always have a signal
1332       available to map to the input ports.
1333
1334       To reduce a complex expression to a simple variable reference, we create
1335       a new let expression around the application, which binds the complex
1336       expression to a new variable. The original function is then applied to
1337       this variable.
1338
1339       \refdef{global variable}
1340       Note that references to \emph{global variables} (like a top level
1341       function without arguments, but also an argumentless dataconstructors
1342       like \lam{True}) are also simplified. Only local variables generate
1343       signals in the resulting architecture. Even though argumentless
1344       dataconstructors generate constants in generated \VHDL\ code and could be
1345       mapped to an input port directly, they are still simplified to make the
1346       normal form more regular.
1347
1348       \refdef{representable}
1349       \starttrans
1350       M N
1351       --------------------    \lam{N} is representable
1352       letrec x = N in M x     \lam{N} is not a local variable reference
1353       \stoptrans
1354       \refdef{local variable}
1355
1356       \startbuffer[from]
1357       add (add a 1) 1
1358       \stopbuffer
1359
1360       \startbuffer[to]
1361       letrec x = add a 1 in add x 1
1362       \stopbuffer
1363
1364       \transexample{argsimpl}{Argument simplification}{from}{to}
1365
1366     \subsection[sec:normalization:built-ins]{Built-in functions}
1367       This section deals with (arguments to) built-in functions.  In the
1368       intended normal form definition\refdef{intended normal form definition}
1369       we can see that there are three sorts of arguments a built-in function
1370       can receive.
1371       
1372       \startitemize[KR]
1373         \item A representable local variable reference. This is the most
1374         common argument to any function. The argument simplification
1375         transformation described in \in{section}[sec:normalization:argsimpl]
1376         makes sure that \emph{any} representable argument to \emph{any}
1377         function (including built-in functions) is turned into a local variable
1378         reference.
1379         \item (A partial application of) a top level function (either built-in on
1380         user-defined). The function extraction transformation described in
1381         this section takes care of turning every functiontyped argument into
1382         (a partial application of) a top level function.
1383         \item Any expression that is not representable and does not have a
1384         function type. Since these can be any expression, there is no
1385         transformation needed. Note that this category is exactly all
1386         expressions that are not transformed by the transformations for the
1387         previous two categories. This means that \emph{any} core expression
1388         that is used as an argument to a built-in function will be either
1389         transformed into one of the above categories, or end up in this
1390         categorie. In any case, the result is in normal form.
1391       \stopitemize
1392
1393       As noted, the argument simplification will handle any representable
1394       arguments to a built-in function. The following transformation is needed
1395       to handle non-representable arguments with a function type, all other
1396       non-representable arguments do not need any special handling.
1397
1398       \subsubsection[sec:normalization:funextract]{Function extraction}
1399         This transform deals with function-typed arguments to built-in
1400         functions. 
1401         Since built-in functions cannot be specialized (see
1402         \in{section}[sec:normalization:specialize]) to remove the arguments,
1403         these arguments are extracted into a new global function instead. In
1404         other words, we create a new top level function that has exactly the
1405         extracted argument as its body. This greatly simplifies the
1406         translation rules needed for built-in functions, since they only need
1407         to handle (partial applications of) top level functions.
1408
1409         Any free variables occuring in the extracted arguments will become
1410         parameters to the new global function. The original argument is replaced
1411         with a reference to the new function, applied to any free variables from
1412         the original argument.
1413
1414         This transformation is useful when applying higher-order built-in functions
1415         like \hs{map} to a lambda abstraction, for example. In this case, the code
1416         that generates \small{VHDL} for \hs{map} only needs to handle top level functions and
1417         partial applications, not any other expression (such as lambda abstractions or
1418         even more complicated expressions).
1419
1420         \starttrans
1421         M N                     \lam{M} is (a partial aplication of) a built-in function.
1422         ---------------------   \lam{f0 ... fn} are all free local variables of \lam{N}
1423         M (x f0 ... fn)         \lam{N :: a -> b}
1424         ~                       \lam{N} is not a (partial application of) a top level function
1425         x = λf0 ... λfn.N
1426         \stoptrans
1427
1428         \startbuffer[from]
1429         addList = λb.λxs.map (λa . add a b) xs
1430         \stopbuffer
1431
1432         \startbuffer[to]
1433         addList = λb.λxs.map (f b) xs
1434         ~
1435         f = λb.λa.add a b
1436         \stopbuffer
1437
1438         \transexample{funextract}{Function extraction}{from}{to}
1439
1440         Note that the function \lam{f} will still need normalization after
1441         this.
1442
1443     \subsection{Case normalisation}
1444       The transformations in this section ensure that case statements end up
1445       in normal form.
1446
1447       \subsubsection{Scrutinee simplification}
1448         This transform ensures that the scrutinee of a case expression is always
1449         a simple variable reference.
1450
1451         \starttrans
1452         case E of
1453           alts
1454         -----------------        \lam{E} is not a local variable reference
1455         letrec x = E in 
1456           case x of
1457             alts
1458         \stoptrans
1459
1460         \startbuffer[from]
1461         case (foo a) of
1462           True -> a
1463           False -> b
1464         \stopbuffer
1465
1466         \startbuffer[to]
1467         letrec x = foo a in
1468           case x of
1469             True -> a
1470             False -> b
1471         \stopbuffer
1472
1473         \transexample{letflat}{Case normalisation}{from}{to}
1474
1475
1476         \placeintermezzo{}{
1477           \defref{wild binders}
1478           \startframedtext[width=7cm,background=box,frame=no]
1479           \startalignment[center]
1480             {\tfa Wild binders}
1481           \stopalignment
1482           \blank[medium]
1483             In a functional expression, a \emph{wild binder} refers to any
1484             binder that is never referenced. This means that even though it
1485             will be bound to a particular value, that value is never used.
1486
1487             The Haskell syntax offers the underscore as a wild binder that
1488             cannot even be referenced (It can be seen as introducing a new,
1489             anonymous, binder everytime it is used).
1490             
1491             In these transformations, the term wild binder will sometimes be
1492             used to indicate that a binder must not be referenced.
1493           \stopframedtext
1494         }
1495
1496       \subsubsection{Case normalization}
1497         This transformation ensures that all case expressions get a form
1498         that is allowed by the intended normal form. This means they
1499         will become one of:
1500
1501         \startitemize
1502         \item An extractor case with a single alternative that picks a field
1503         from a datatype, \eg\ \lam{case x of (a, b) -> a}.
1504         \item A selector case with multiple alternatives and only wild binders, that
1505         makes a choice between expressions based on the constructor of another
1506         expression, \eg\ \lam{case x of Low -> a; High -> b}.
1507         \stopitemize
1508
1509         For an arbitrary case, that has \lam{n} alternatives, with
1510         \lam{m} binders in each alternatives, this will result in \lam{m
1511         * n} extractor case expression to get at each variable, \lam{n}
1512         let bindings for each of the alternatives' value and a single
1513         selector case to select the right value out of these.
1514
1515         Technically, the defintion of this transformation would require
1516         that the constructor for every alternative has exactly the same
1517         amount (\lam{m}) of arguments, but of course this transformation
1518         also applies when this is not the case.
1519         
1520         \starttrans
1521         case E of
1522           C0 v0,0 ... v0,m -> E0
1523           \vdots
1524           Cn vn,0 ... vn,m -> En
1525         --------------------------------------------------- \lam{\forall i \forall j, 0 ≤ i ≤ n, 0 ≤ i < m} (\lam{wi,j} is a wild (unused) binder)
1526         letrec                                              The case expression is not an extractor case
1527           v0,0 = case E of C0 x0,0 .. x0,m -> x0,0          The case expression is not a selector case
1528           \vdots
1529           v0,m = case E of C0 x0,0 .. x0,m -> x0,m
1530           \vdots
1531           vn,m = case E of Cn xn,0 .. xn,m -> xn,m
1532           y0 = E0
1533           \vdots
1534           yn = En
1535         in
1536           case E of
1537             C0 w0,0 ... w0,m -> y0
1538             \vdots
1539             Cn wn,0 ... wn,m -> yn
1540         \stoptrans
1541
1542         Note that this transformation applies to case expressions with any
1543         scrutinee. If the scrutinee is a complex expression, this might
1544         result in duplication of work (hardware). An extra condition to
1545         only apply this transformation when the scrutinee is already
1546         simple (effectively causing this transformation to be only
1547         applied after the scrutinee simplification transformation) might
1548         be in order. 
1549
1550         \startbuffer[from]
1551         case a of
1552           True -> add b 1
1553           False -> add b 2
1554         \stopbuffer
1555
1556         \startbuffer[to]
1557         letrec
1558           x0 = add b 1
1559           x1 = add b 2
1560         in
1561           case a of
1562             True -> x0
1563             False -> x1
1564         \stopbuffer
1565
1566         \transexample{selcasesimpl}{Selector case simplification}{from}{to}
1567
1568         \startbuffer[from]
1569         case a of
1570           (,) b c -> add b c
1571         \stopbuffer
1572         \startbuffer[to]
1573         letrec
1574           b = case a of (,) b c -> b
1575           c = case a of (,) b c -> c
1576           x0 = add b c
1577         in
1578           case a of
1579             (,) w0 w1 -> x0
1580         \stopbuffer
1581
1582         \transexample{excasesimpl}{Extractor case simplification}{from}{to}
1583
1584         \refdef{selector case}
1585         In \in{example}[ex:trans:excasesimpl] the case expression is expanded
1586         into multiple case expressions, including a pretty useless expression
1587         (that is neither a selector or extractor case). This case can be
1588         removed by the Case removal transformation in
1589         \in{section}[sec:transformation:caseremoval].
1590
1591       \subsubsection[sec:transformation:caseremoval]{Case removal}
1592         This transform removes any case expression with a single alternative and
1593         only wild binders.\refdef{wild binder}
1594
1595         These "useless" case expressions are usually leftovers from case simplification
1596         on extractor case (see the previous example).
1597
1598         \starttrans
1599         case x of
1600           C v0 ... vm -> E
1601         ----------------------     \lam{\forall i, 0 ≤ i ≤ m} (\lam{vi} does not occur free in E)
1602         E
1603         \stoptrans
1604
1605         \startbuffer[from]
1606         case a of
1607           (,) w0 w1 -> x0
1608         \stopbuffer
1609
1610         \startbuffer[to]
1611         x0
1612         \stopbuffer
1613
1614         \transexample{caserem}{Case removal}{from}{to}
1615
1616     \subsection[sec:normalization:nonrep]{Removing unrepresentable values}
1617       The transformations in this section are aimed at making all the
1618       values used in our expression representable. There are two main
1619       transformations that are applied to \emph{all} unrepresentable let
1620       bindings and function arguments. These are meant to address three
1621       different kinds of unrepresentable values: Polymorphic values,
1622       higher-order values and literals. The transformation are described
1623       generically: They apply to all non-representable values. However,
1624       non-representable values that do not fall into one of these three
1625       categories will be moved around by these transformations but are
1626       unlikely to completely disappear. They usually mean the program was not
1627       valid in the first place, because unsupported types were used (for
1628       example, a program using strings).
1629      
1630       Each of these three categories will be detailed below, followed by the
1631       actual transformations.
1632
1633       \subsubsection{Removing Polymorphism}
1634         As noted in \in{section}[sec:prototype:polymporphism],
1635         polymorphism is made explicit in Core through type and
1636         dictionary arguments. To remove the polymorphism from a
1637         function, we can simply specialize the polymorphic function for
1638         the particular type applied to it. The same goes for dictionary
1639         arguments. To remove polymorphism from let bound values, we
1640         simply inline the let bindings that have a polymorphic type,
1641         which should (eventually) make sure that the polymorphic
1642         expression is applied to a type and/or dictionary, which can
1643         then be removed by β-reduction (\in{section}[sec:normalization:beta]).
1644
1645         Since both type and dictionary arguments are not representable,
1646         \refdef{representable}
1647         the non-representable argument specialization and
1648         non-representable let binding inlining transformations below
1649         take care of exactly this.
1650
1651         There is one case where polymorphism cannot be completely
1652         removed: Built-in functions are still allowed to be polymorphic
1653         (Since we have no function body that we could properly
1654         specialize). However, the code that generates \VHDL\ for built-in
1655         functions knows how to handle this, so this is not a problem.
1656
1657       \subsubsection[sec:normalization:defunctionalization]{Defunctionalization}
1658         These transformations remove higher-order expressions from our
1659         program, making all values first-order. The approach used for
1660         defunctionalization uses a combination of specialization, inlining and
1661         some cleanup transformations, was also proposed in parallel research
1662         by Neil Mitchell \cite[mitchell09].
1663       
1664         Higher order values are always introduced by lambda abstractions, none
1665         of the other Core expression elements can introduce a function type.
1666         However, other expressions can \emph{have} a function type, when they
1667         have a lambda expression in their body. 
1668         
1669         For example, the following expression is a higher-order expression
1670         that is not a lambda expression itself:
1671         
1672         \refdef{id function}
1673         \startlambda
1674           case x of
1675             High -> id
1676             Low -> λx.x
1677         \stoplambda
1678
1679         The reference to the \lam{id} function shows that we can introduce a
1680         higher-order expression in our program without using a lambda
1681         expression directly. However, inside the definition of the \lam{id}
1682         function, we can be sure that a lambda expression is present.
1683         
1684         Looking closely at the definition of our normal form in
1685         \in{section}[sec:normalization:intendednormalform], we can see that
1686         there are three possibilities for higher-order values to appear in our
1687         intended normal form:
1688
1689         \startitemize[KR]
1690           \item[item:toplambda] Lambda abstractions can appear at the highest level of a
1691           top level function. These lambda abstractions introduce the
1692           arguments (input ports / current state) of the function.
1693           \item[item:built-inarg] (Partial applications of) top level functions can appear as an
1694           argument to a built-in function.
1695           \item[item:completeapp] (Partial applications of) top level functions can appear in
1696           function position of an application. Since a partial application
1697           cannot appear anywhere else (except as built-in function arguments),
1698           all partial applications are applied, meaning that all applications
1699           will become complete applications. However, since application of
1700           arguments happens one by one, in the expression:
1701           \startlambda
1702             f 1 2
1703           \stoplambda
1704           the subexpression \lam{f 1} has a function type. But this is
1705           allowed, since it is inside a complete application.
1706         \stopitemize
1707
1708         We will take a typical function with some higher-order values as an
1709         example. The following function takes two arguments: a \lam{Bit} and a
1710         list of numbers. Depending on the first argument, each number in the
1711         list is doubled, or the list is returned unmodified. For the sake of
1712         the example, no polymorphism is shown. In reality, at least map would
1713         be polymorphic.
1714
1715         \startlambda
1716         λy.let double = λx. x + x in
1717              case y of
1718                 Low -> map double
1719                 High -> λz. z
1720         \stoplambda
1721
1722         This example shows a number of higher-order values that we cannot
1723         translate to \VHDL\ directly. The \lam{double} binder bound in the let
1724         expression has a function type, as well as both of the alternatives of
1725         the case expression. The first alternative is a partial application of
1726         the \lam{map} built-in function, whereas the second alternative is a
1727         lambda abstraction.
1728
1729         To reduce all higher-order values to one of the above items, a number
1730         of transformations we have already seen are used. The η-abstraction
1731         transformation from \in{section}[sec:normalization:eta] ensures all
1732         function arguments are introduced by lambda abstraction on the highest
1733         level of a function. These lambda arguments are allowed because of
1734         \in{item}[item:toplambda] above. After η-abstraction, our example
1735         becomes a bit bigger:
1736
1737         \startlambda
1738         λy.λq.(let double = λx. x + x in
1739                  case y of
1740                    Low -> map double
1741                    High -> λz. z
1742               ) q
1743         \stoplambda
1744
1745         η-abstraction also introduces extra applications (the application of
1746         the let expression to \lam{q} in the above example). These
1747         applications can then propagated down by the application propagation
1748         transformation (\in{section}[sec:normalization:appprop]). In our
1749         example, the \lam{q} and \lam{r} variable will be propagated into the
1750         let expression and then into the case expression:
1751
1752         \startlambda
1753         λy.λq.let double = λx. x + x in
1754                 case y of
1755                   Low -> map double q
1756                   High -> (λz. z) q
1757         \stoplambda
1758         
1759         This propagation makes higher-order values become applied (in
1760         particular both of the alternatives of the case now have a
1761         representable type). Completely applied top level functions (like the
1762         first alternative) are now no longer invalid (they fall under
1763         \in{item}[item:completeapp] above). (Completely) applied lambda
1764         abstractions can be removed by β-abstraction. For our example,
1765         applying β-abstraction results in the following:
1766
1767         \startlambda
1768         λy.λq.let double = λx. x + x in
1769                 case y of
1770                   Low -> map double q
1771                   High -> q
1772         \stoplambda
1773
1774         As you can see in our example, all of this moves applications towards
1775         the higher-order values, but misses higher-order functions bound by
1776         let expressions. The applications cannot be moved towards these values
1777         (since they can be used in multiple places), so the values will have
1778         to be moved towards the applications. This is achieved by inlining all
1779         higher-order values bound by let applications, by the
1780         non-representable binding inlining transformation below. When applying
1781         it to our example, we get the following:
1782         
1783         \startlambda
1784         λy.λq.case y of
1785                 Low -> map (λx. x + x) q
1786                 High -> q
1787         \stoplambda
1788
1789         We have nearly eliminated all unsupported higher-order values from this
1790         expressions. The one that is remaining is the first argument to the
1791         \lam{map} function. Having higher-order arguments to a built-in
1792         function like \lam{map} is allowed in the intended normal form, but
1793         only if the argument is a (partial application) of a top level
1794         function. This is easily done by introducing a new top level function
1795         and put the lambda abstraction inside. This is done by the function
1796         extraction transformation from
1797         \in{section}[sec:normalization:funextract].
1798
1799         \startlambda
1800         λy.λq.case y of
1801                 Low -> map func q
1802                 High -> q
1803         \stoplambda
1804
1805         This also introduces a new function, that we have called \lam{func}:
1806
1807         \startlambda
1808         func = λx. x + x
1809         \stoplambda
1810
1811         Note that this does not actually remove the lambda, but now it is a
1812         lambda at the highest level of a function, which is allowed in the
1813         intended normal form.
1814
1815         There is one case that has not been discussed yet. What if the
1816         \lam{map} function in the example above was not a built-in function
1817         but a user-defined function? Then extracting the lambda expression
1818         into a new function would not be enough, since user-defined functions
1819         can never have higher-order arguments. For example, the following
1820         expression shows an example:
1821
1822         \startlambda
1823         twice :: (Word -> Word) -> Word -> Word
1824         twice = λf.λa.f (f a)
1825
1826         main = λa.app (λx. x + x) a
1827         \stoplambda
1828
1829         This example shows a function \lam{twice} that takes a function as a
1830         first argument and applies that function twice to the second argument.
1831         Again, we have made the function monomorphic for clarity, even though
1832         this function would be a lot more useful if it was polymorphic. The
1833         function \lam{main} uses \lam{twice} to apply a lambda epression twice.
1834
1835         When faced with a user defined function, a body is available for that
1836         function. This means we could create a specialized version of the
1837         function that only works for this particular higher-order argument
1838         (\ie, we can just remove the argument and call the specialized
1839         function without the argument). This transformation is detailed below.
1840         Applying this transformation to the example gives:
1841
1842         \startlambda
1843         twice' :: Word -> Word
1844         twice' = λb.(λf.λa.f (f a)) (λx. x + x) b
1845
1846         main = λa.app' a
1847         \stoplambda
1848
1849         The \lam{main} function is now in normal form, since the only
1850         higher-order value there is the top level lambda expression. The new
1851         \lam{twice'} function is a bit complex, but the entire original body
1852         of the original \lam{twice} function is wrapped in a lambda
1853         abstraction and applied to the argument we have specialized for
1854         (\lam{λx. x + x}) and the other arguments. This complex expression can
1855         fortunately be effectively reduced by repeatedly applying β-reduction: 
1856
1857         \startlambda
1858         twice' :: Word -> Word
1859         twice' = λb.(b + b) + (b + b)
1860         \stoplambda
1861
1862         This example also shows that the resulting normal form might not be as
1863         efficient as we might hope it to be (it is calculating \lam{(b + b)}
1864         twice). This is discussed in more detail in
1865         \in{section}[sec:normalization:duplicatework].
1866
1867       \subsubsection{Literals}
1868         There are a limited number of literals available in Haskell and Core.
1869         \refdef{enumerated types} When using (enumerating) algebraic
1870         datatypes, a literal is just a reference to the corresponding data
1871         constructor, which has a representable type (the algebraic datatype)
1872         and can be translated directly. This also holds for literals of the
1873         \hs{Bool} Haskell type, which is just an enumerated type.
1874
1875         There is, however, a second type of literal that does not have a
1876         representable type: Integer literals. Cλash supports using integer
1877         literals for all three integer types supported (\hs{SizedWord},
1878         \hs{SizedInt} and \hs{RangedWord}). This is implemented using
1879         Haskell's \hs{Num} type class, which offers a \hs{fromInteger} method
1880         that converts any \hs{Integer} to the Cλash datatypes.
1881
1882         When \GHC\ sees integer literals, it will automatically insert calls to
1883         the \hs{fromInteger} method in the resulting Core expression. For
1884         example, the following expression in Haskell creates a 32 bit unsigned
1885         word with the value 1. The explicit type signature is needed, since
1886         there is no context for \GHC\ to determine the type from otherwise.
1887
1888         \starthaskell
1889         1 :: SizedWord D32
1890         \stophaskell
1891
1892         This Haskell code results in the following Core expression:
1893
1894         \startlambda
1895         fromInteger @(SizedWord D32) \$dNum (smallInteger 10)
1896         \stoplambda
1897
1898         The literal 10 will have the type \lam{GHC.Prim.Int\#}, which is
1899         converted into an \lam{Integer} by \lam{smallInteger}. Finally, the
1900         \lam{fromInteger} function will finally convert this into a
1901         \lam{SizedWord D32}.
1902
1903         Both the \lam{GHC.Prim.Int\#} and \lam{Integer} types are not
1904         representable, and cannot be translated directly. Fortunately, there
1905         is no need to translate them, since \lam{fromInteger} is a built-in
1906         function that knows how to handle these values. However, this does
1907         require that the \lam{fromInteger} function is directly applied to
1908         these non-representable literal values, otherwise errors will occur.
1909         For example, the following expression is not in the intended normal
1910         form, since one of the let bindings has an unrepresentable type
1911         (\lam{Integer}):
1912
1913         \startlambda
1914         let l = smallInteger 10 in fromInteger @(SizedWord D32) \$dNum l
1915         \stoplambda
1916
1917         By inlining these let-bindings, we can ensure that unrepresentable
1918         literals bound by a let binding end up in an application of the
1919         appropriate built-in function, where they are allowed. Since it is
1920         possible that the application of that function is in a different
1921         function than the definition of the literal value, we will always need
1922         to specialize away any unrepresentable literals that are used as
1923         function arguments. The following two transformations do exactly this.
1924
1925       \subsubsection{Non-representable binding inlining}
1926         This transform inlines let bindings that are bound to a
1927         non-representable value. Since we can never generate a signal
1928         assignment for these bindings (we cannot declare a signal assignment
1929         with a non-representable type, for obvious reasons), we have no choice
1930         but to inline the binding to remove it.
1931
1932         As we have seen in the previous sections, inlining these bindings
1933         solves (part of) the polymorphism, higher-order values and
1934         unrepresentable literals in an expression.
1935
1936         \refdef{substitution notation}
1937         \starttrans
1938         letrec 
1939           a0 = E0
1940           \vdots
1941           ai = Ei
1942           \vdots
1943           an = En
1944         in
1945           M
1946         --------------------------    \lam{Ei} has a non-representable type.
1947         letrec
1948           a0 = E0 [ai=>Ei] \vdots
1949           ai-1 = Ei-1 [ai=>Ei]
1950           ai+1 = Ei+1 [ai=>Ei]
1951           \vdots
1952           an = En [ai=>Ei]
1953         in
1954           M[ai=>Ei]
1955         \stoptrans
1956
1957         \startbuffer[from]
1958         letrec
1959           a = smallInteger 10
1960           inc = λb -> add b 1
1961           inc' = add 1
1962           x = fromInteger a 
1963         in
1964           inc (inc' x)
1965         \stopbuffer
1966
1967         \startbuffer[to]
1968         letrec
1969           x = fromInteger (smallInteger 10)
1970         in
1971           (λb -> add b 1) (add 1 x)
1972         \stopbuffer
1973
1974         \transexample{nonrepinline}{Nonrepresentable binding inlining}{from}{to}
1975
1976       \subsubsection[sec:normalization:specialize]{Function specialization}
1977         This transform removes arguments to user-defined functions that are
1978         not representable at runtime. This is done by creating a
1979         \emph{specialized} version of the function that only works for one
1980         particular value of that argument (in other words, the argument can be
1981         removed).
1982
1983         Specialization means to create a specialized version of the called
1984         function, with one argument already filled in. As a simple example, in
1985         the following program (this is not actual Core, since it directly uses
1986         a literal with the unrepresentable type \lam{GHC.Prim.Int\#}).
1987
1988         \startlambda
1989         f = λa.λb.a + b
1990         inc = λa.f a 1
1991         \stoplambda
1992
1993         We could specialize the function \lam{f} against the literal argument
1994         1, with the following result:
1995
1996         \startlambda
1997         f' = λa.a + 1
1998         inc = λa.f' a
1999         \stoplambda
2000
2001         In some way, this transformation is similar to β-reduction, but it
2002         operates across function boundaries. It is also similar to
2003         non-representable let binding inlining above, since it sort of
2004         \quote{inlines} an expression into a called function.
2005
2006         Special care must be taken when the argument has any free variables.
2007         If this is the case, the original argument should not be removed
2008         completely, but replaced by all the free variables of the expression.
2009         In this way, the original expression can still be evaluated inside the
2010         new function.
2011
2012         To prevent us from propagating the same argument over and over, a
2013         simple local variable reference is not propagated (since is has
2014         exactly one free variable, itself, we would only replace that argument
2015         with itself).
2016
2017         This shows that any free local variables that are not runtime
2018         representable cannot be brought into normal form by this transform. We
2019         rely on an inlining or β-reduction transformation to replace such a
2020         variable with an expression we can propagate again.
2021
2022         \starttrans
2023         x = E
2024         ~
2025         x Y0 ... Yi ... Yn                               \lam{Yi} is not representable
2026         ---------------------------------------------    \lam{Yi} is not a local variable reference
2027         x' Y0 ... Yi-1 f0 ...  fm Yi+1 ... Yn            \lam{f0 ... fm} are all free local vars of \lam{Yi}
2028         ~                                                \lam{T0 ... Tn} are the types of \lam{Y0 ... Yn}
2029         x' = λ(y0 :: T0) ... λ(yi-1 :: Ty-1). 
2030              λf0 ... λfm.
2031              λ(yi+1 :: Ty+1) ...  λ(yn :: Tn).       
2032                E y0 ... yi-1 Yi yi+1 ... yn   
2033         \stoptrans
2034
2035         This is a bit of a complex transformation. It transforms an
2036         application of the function \lam{x}, where one of the arguments
2037         (\lam{Y_i}) is not representable. A new
2038         function \lam{x'} is created that wraps the body of the old function.
2039         The body of the new function becomes a number of nested lambda
2040         abstractions, one for each of the original arguments that are left
2041         unchanged.
2042         
2043         The ith argument is replaced with the free variables of
2044         \lam{Y_i}. Note that we reuse the same binders as those used in
2045         \lam{Y_i}, since we can then just use \lam{Y_i} inside the new
2046         function body and have all of the variables it uses be in scope.
2047
2048         The argument that we are specializing for, \lam{Y_i}, is put inside
2049         the new function body. The old function body is applied to it. Since
2050         we use this new function only in place of an application with that
2051         particular argument \lam{Y_i}, behaviour should not change.
2052         
2053         Note that the types of the arguments of our new function are taken
2054         from the types of the \emph{actual} arguments (\lam{T0 ... Tn}). This
2055         means that any polymorphism in the arguments is removed, even when the
2056         corresponding explicit type lambda is not removed
2057         yet.
2058
2059         \todo{Examples. Perhaps reference the previous sections}
2060
2061   \section{Unsolved problems}
2062     The above system of transformations has been implemented in the prototype
2063     and seems to work well to compile simple and more complex examples of
2064     hardware descriptions. \todo{Ref christiaan?} However, this normalization
2065     system has not seen enough review and work to be complete and work for
2066     every Core expression that is supplied to it. A number of problems
2067     have already been identified and are discussed in this section.
2068
2069     \subsection[sec:normalization:duplicatework]{Work duplication}
2070         A possible problem of β-reduction is that it could duplicate work.
2071         When the expression applied is not a simple variable reference, but
2072         requires calculation and the binder the lambda abstraction binds to
2073         is used more than once, more hardware might be generated than strictly
2074         needed. 
2075
2076         As an example, consider the expression:
2077
2078         \startlambda
2079         (λx. x + x) (a * b)
2080         \stoplambda
2081
2082         When applying β-reduction to this expression, we get:
2083
2084         \startlambda
2085         (a * b) + (a * b)
2086         \stoplambda
2087
2088         which of course calculates \lam{(a * b)} twice.
2089         
2090         A possible solution to this would be to use the following alternative
2091         transformation, which is of course no longer normal β-reduction. The
2092         followin transformation has not been tested in the prototype, but is
2093         given here for future reference:
2094
2095         \starttrans
2096         (λx.E) M
2097         -----------------
2098         letrec x = M in E
2099         \stoptrans
2100         
2101         This does not seem like much of an improvement, but it does get rid of
2102         the lambda expression (and the associated higher-order value), while
2103         at the same time introducing a new let binding. Since the result of
2104         every application or case expression must be bound by a let expression
2105         in the intended normal form anyway, this is probably not a problem. If
2106         the argument happens to be a variable reference, then simple let
2107         binding removal (\in{section}[sec:normalization:simplelet]) will
2108         remove it, making the result identical to that of the original
2109         β-reduction transformation.
2110
2111         When also applying argument simplification to the above example, we
2112         get the following expression:
2113
2114         \startlambda
2115         let y = (a * b)
2116             z = (a * b)
2117         in y + z
2118         \stoplambda
2119
2120         Looking at this, we could imagine an alternative approach: Create a
2121         transformation that removes let bindings that bind identical values.
2122         In the above expression, the \lam{y} and \lam{z} variables could be
2123         merged together, resulting in the more efficient expression:
2124
2125         \startlambda
2126         let y = (a * b) in y + y
2127         \stoplambda
2128
2129       \subsection[sec:normalization:non-determinism]{Non-determinism}
2130         As an example, again consider the following expression:
2131
2132         \startlambda
2133         (λx. x + x) (a * b)
2134         \stoplambda
2135
2136         We can apply both β-reduction (\in{section}[sec:normalization:beta])
2137         as well as argument simplification
2138         (\in{section}[sec:normalization:argsimpl]) to this expression.
2139
2140         When applying argument simplification first and then β-reduction, we
2141         get the following expression:
2142
2143         \startlambda
2144         let y = (a * b) in y + y
2145         \stoplambda
2146
2147         When applying β-reduction first and then argument simplification, we
2148         get the following expression:
2149
2150         \startlambda
2151         let y = (a * b)
2152             z = (a * b)
2153         in y + z
2154         \stoplambda
2155
2156         As you can see, this is a different expression. This means that the
2157         order of expressions, does in fact change the resulting normal form,
2158         which is something that we would like to avoid. In this particular
2159         case one of the alternatives is even clearly more efficient, so we
2160         would of course like the more efficient form to be the normal form.
2161
2162         For this particular problem, the solutions for duplication of work
2163         seem from the previous section seem to fix the determinism of our
2164         transformation system as well. However, it is likely that there are
2165         other occurences of this problem.
2166
2167       \subsection[sec:normalization:castproblems]{Casts}
2168         We do not fully understand the use of cast expressions in Core, so
2169         there are probably expressions involving cast expressions that cannot
2170         be brought into intended normal form by this transformation system.
2171
2172         The uses of casts in the core system should be investigated more and
2173         transformations will probably need updating to handle them in all
2174         cases.
2175
2176       \subsection[sec:normalization:stateproblems]{Normalization of stateful descriptions}
2177         Currently, the intended normal form definition\refdef{intended
2178         normal form definition} offers enough freedom to describe all
2179         valid stateful descriptions, but is not limiting enough. It is
2180         possible to write descriptions which are in intended normal
2181         form, but cannot be translated into \VHDL\ in a meaningful way
2182         (\eg, a function that swaps two substates in its result, or a
2183         function that changes a substate itself instead of passing it to
2184         a subfunction).
2185
2186         It is now up to the programmer to not do anything funny with
2187         these state values, whereas the normalization just tries not to
2188         mess up the flow of state values. In practice, there are
2189         situations where a Core program that \emph{could} be a valid
2190         stateful description is not translateable by the prototype. This
2191         most often happens when statefulness is mixed with pattern
2192         matching, causing a state input to be unpacked multiple times or
2193         be unpacked and repacked only in some of the code paths.
2194
2195         Without going into detail about the exact problems (of which
2196         there are probably more than have shown up so far), it seems
2197         unlikely that these problems can be solved entirely by just
2198         improving the \VHDL\ state generation in the final stage. The
2199         normalization stage seems the best place to apply the rewriting
2200         needed to support more complex stateful descriptions. This does
2201         of course mean that the intended normal form definition must be
2202         extended as well to be more specific about how state handling
2203         should look like in normal form.
2204         \in{Section}[sec:prototype:statelimits] already contains a
2205         tight description of the limitations on the use of state
2206         variables, which could be adapted into the intended normal form.
2207
2208   \section[sec:normalization:properties]{Provable properties}
2209     When looking at the system of transformations outlined above, there are a
2210     number of questions that we can ask ourselves. The main question is of course:
2211     \quote{Does our system work as intended?}. We can split this question into a
2212     number of subquestions:
2213
2214     \startitemize[KR]
2215     \item[q:termination] Does our system \emph{terminate}? Since our system will
2216     keep running as long as transformations apply, there is an obvious risk that
2217     it will keep running indefinitely. This typically happens when one
2218     transformation produces a result that is transformed back to the original
2219     by another transformation, or when one or more transformations keep
2220     expanding some expression.
2221     \item[q:soundness] Is our system \emph{sound}? Since our transformations
2222     continuously modify the expression, there is an obvious risk that the final
2223     normal form will not be equivalent to the original program: Its meaning could
2224     have changed.
2225     \item[q:completeness] Is our system \emph{complete}? Since we have a complex
2226     system of transformations, there is an obvious risk that some expressions will
2227     not end up in our intended normal form, because we forgot some transformation.
2228     In other words: Does our transformation system result in our intended normal
2229     form for all possible inputs?
2230     \item[q:determinism] Is our system \emph{deterministic}? Since we have defined
2231     no particular order in which the transformation should be applied, there is an
2232     obvious risk that different transformation orderings will result in
2233     \emph{different} normal forms. They might still both be intended normal forms
2234     (if our system is \emph{complete}) and describe correct hardware (if our
2235     system is \emph{sound}), so this property is less important than the previous
2236     three: The translator would still function properly without it.
2237     \stopitemize
2238
2239     Unfortunately, the final transformation system has only been
2240     developed in the final part of the research, leaving no more time
2241     for verifying these properties. In fact, it is likely that the
2242     current transformation system still violates some of these
2243     properties in some cases and should be improved (or extra conditions
2244     on the input hardware descriptions should be formulated).
2245
2246     This is most likely the case with the completeness and determinism
2247     properties, perhaps als the termination property. The soundness
2248     property probably holds, since it is easier to manually verify (each
2249     transformation can be reviewed separately).
2250
2251     Even though no complete proofs have been made, some ideas for
2252     possible proof strategies are shown below.
2253
2254     \subsection{Graph representation}
2255       Before looking into how to prove these properties, we will look at
2256       transformation systems from a graph perspective. We will first define
2257       the graph view and then illustrate it using a simple example from lambda
2258       calculus (which is a different system than the Cλash normalization
2259       system). The nodes of the graph are all possible Core expressions. The
2260       (directed) edges of the graph are transformations. When a transformation
2261       α applies to an expression \lam{A} to produce an expression \lam{B}, we
2262       add an edge from the node for \lam{A} to the node for \lam{B}, labeled
2263       α.
2264
2265       \startuseMPgraphic{TransformGraph}
2266         save a, b, c, d;
2267
2268         % Nodes
2269         newCircle.a(btex \lam{(λx.λy. (+) x y) 1} etex);
2270         newCircle.b(btex \lam{λy. (+) 1 y} etex);
2271         newCircle.c(btex \lam{(λx.(+) x) 1} etex);
2272         newCircle.d(btex \lam{(+) 1} etex);
2273
2274         b.c = origin;
2275         c.c = b.c + (4cm, 0cm);
2276         a.c = midpoint(b.c, c.c) + (0cm, 4cm);
2277         d.c = midpoint(b.c, c.c) - (0cm, 3cm);
2278
2279         % β-conversion between a and b
2280         ncarc.a(a)(b) "name(bred)";
2281         ObjLabel.a(btex $\xrightarrow[normal]{}{β}$ etex) "labpathname(bred)", "labdir(rt)";
2282         ncarc.b(b)(a) "name(bexp)", "linestyle(dashed withdots)";
2283         ObjLabel.b(btex $\xleftarrow[normal]{}{β}$ etex) "labpathname(bexp)", "labdir(lft)";
2284
2285         % η-conversion between a and c
2286         ncarc.a(a)(c) "name(ered)";
2287         ObjLabel.a(btex $\xrightarrow[normal]{}{η}$ etex) "labpathname(ered)", "labdir(rt)";
2288         ncarc.c(c)(a) "name(eexp)", "linestyle(dashed withdots)";
2289         ObjLabel.c(btex $\xleftarrow[normal]{}{η}$ etex) "labpathname(eexp)", "labdir(lft)";
2290
2291         % η-conversion between b and d
2292         ncarc.b(b)(d) "name(ered)";
2293         ObjLabel.b(btex $\xrightarrow[normal]{}{η}$ etex) "labpathname(ered)", "labdir(rt)";
2294         ncarc.d(d)(b) "name(eexp)", "linestyle(dashed withdots)";
2295         ObjLabel.d(btex $\xleftarrow[normal]{}{η}$ etex) "labpathname(eexp)", "labdir(lft)";
2296
2297         % β-conversion between c and d
2298         ncarc.c(c)(d) "name(bred)";
2299         ObjLabel.c(btex $\xrightarrow[normal]{}{β}$ etex) "labpathname(bred)", "labdir(rt)";
2300         ncarc.d(d)(c) "name(bexp)", "linestyle(dashed withdots)";
2301         ObjLabel.d(btex $\xleftarrow[normal]{}{β}$ etex) "labpathname(bexp)", "labdir(lft)";
2302
2303         % Draw objects and lines
2304         drawObj(a, b, c, d);
2305       \stopuseMPgraphic
2306
2307       \placeexample[right][ex:TransformGraph]{Partial graph of a lambda calculus
2308       system with β and η reduction (solid lines) and expansion (dotted lines).}
2309           \boxedgraphic{TransformGraph}
2310
2311       Of course the graph for Cλash is unbounded, since we can construct an
2312       infinite amount of Core expressions. Also, there might potentially be
2313       multiple edges between two given nodes (with different labels), though
2314       this seems unlikely to actually happen in our system.
2315
2316       See \in{example}[ex:TransformGraph] for the graph representation of a very
2317       simple lambda calculus that contains just the expressions \lam{(λx.λy. (+) x
2318       y) 1}, \lam{λy. (+) 1 y}, \lam{(λx.(+) x) 1} and \lam{(+) 1}. The
2319       transformation system consists of β-reduction and η-reduction (solid edges) or
2320       β-expansion and η-expansion (dotted edges).
2321
2322       \todo{Define β-reduction and η-reduction?}
2323
2324       Note that the normal form of such a system consists of the set of nodes
2325       (expressions) without outgoing edges, since those are the expressions to which
2326       no transformation applies anymore. We call this set of nodes the \emph{normal
2327       set}. The set of nodes containing expressions in intended normal
2328       form \refdef{intended normal form} is called the \emph{intended
2329       normal set}.
2330
2331       From such a graph, we can derive some properties easily:
2332       \startitemize[KR]
2333         \item A system will \emph{terminate} if there is no walk (sequence of
2334         edges, or transformations) of infinite length in the graph (this
2335         includes cycles, but can also happen without cycles).
2336         \item Soundness is not easily represented in the graph.
2337         \item A system is \emph{complete} if all of the nodes in the normal set have
2338         the intended normal form. The inverse (that all of the nodes outside of
2339         the normal set are \emph{not} in the intended normal form) is not
2340         strictly required. In other words, our normal set must be a
2341         subset of the intended normal form, but they do not need to be
2342         the same set.
2343         form.
2344         \item A system is deterministic if all paths starting at a particular
2345         node, which end in a node in the normal set, end at the same node.
2346       \stopitemize
2347
2348       When looking at the \in{example}[ex:TransformGraph], we see that the system
2349       terminates for both the reduction and expansion systems (but note that, for
2350       expansion, this is only true because we have limited the possible
2351       expressions.  In complete lambda calculus, there would be a path from
2352       \lam{(λx.λy. (+) x y) 1} to \lam{(λx.λy.(λz.(+) z) x y) 1} to
2353       \lam{(λx.λy.(λz.(λq.(+) q) z) x y) 1} etc.)
2354
2355       If we would consider the system with both expansion and reduction, there
2356       would no longer be termination either, since there would be cycles all
2357       over the place.
2358
2359       The reduction and expansion systems have a normal set of containing just
2360       \lam{(+) 1} or \lam{(λx.λy. (+) x y) 1} respectively. Since all paths in
2361       either system end up in these normal forms, both systems are \emph{complete}.
2362       Also, since there is only one node in the normal set, it must obviously be
2363       \emph{deterministic} as well.
2364
2365     \subsection{Termination}
2366       In general, proving termination of an arbitrary program is a very
2367       hard problem. \todo{Ref about arbitrary termination} Fortunately,
2368       we only have to prove termination for our specific transformation
2369       system.
2370
2371       A common approach for these kinds of proofs is to associate a
2372       measure with each possible expression in our system. If we can
2373       show that each transformation strictly decreases this measure
2374       (\ie, the expression transformed to has a lower measure than the
2375       expression transformed from).  \todo{ref about measure-based
2376       termination proofs / analysis}
2377       
2378       A good measure for a system consisting of just β-reduction would
2379       be the number of lambda expressions in the expression. Since every
2380       application of β-reduction removes a lambda abstraction (and there
2381       is always a bounded number of lambda abstractions in every
2382       expression) we can easily see that a transformation system with
2383       just β-reduction will always terminate.
2384
2385       For our complete system, this measure would be fairly complex
2386       (probably the sum of a lot of things). Since the (conditions on)
2387       our transformations are pretty complex, we would need to include
2388       both simple things like the number of let expressions as well as
2389       more complex things like the number of case expressions that are
2390       not yet in normal form.
2391
2392       No real attempt has been made at finding a suitable measure for
2393       our system yet.
2394
2395     \subsection{Soundness}
2396       Soundness is a property that can be proven for each transformation
2397       separately. Since our system only runs separate transformations
2398       sequentially, if each of our transformations leaves the
2399       \emph{meaning} of the expression unchanged, then the entire system
2400       will of course leave the meaning unchanged and is thus
2401       \emph{sound}.
2402
2403       The current prototype has only been verified in an ad-hoc fashion
2404       by inspecting (the code for) each transformation. A more formal
2405       verification would be more appropriate.
2406
2407       To be able to formally show that each transformation properly
2408       preserves the meaning of every expression, we require an exact
2409       definition of the \emph{meaning} of every expression, so we can
2410       compare them. A definition of the operational semantics of \GHC's Core
2411       language is available \cite[sulzmann07], but this does not seem
2412       sufficient for our goals (but it is a good start).
2413
2414       It should be possible to have a single formal definition of
2415       meaning for Core for both normal Core compilation by \GHC\ and for
2416       our compilation to \VHDL. The main difference seems to be that in
2417       hardware every expression is always evaluated, while in software
2418       it is only evaluated if needed, but it should be possible to
2419       assign a meaning to core expressions that assumes neither.
2420       
2421       Since each of the transformations can be applied to any
2422       subexpression as well, there is a constraint on our meaning
2423       definition: The meaning of an expression should depend only on the
2424       meaning of subexpressions, not on the expressions themselves. For
2425       example, the meaning of the application in \lam{f (let x = 4 in
2426       x)} should be the same as the meaning of the application in \lam{f
2427       4}, since the argument subexpression has the same meaning (though
2428       the actual expression is different).
2429       
2430     \subsection{Completeness}
2431       Proving completeness is probably not hard, but it could be a lot
2432       of work. We have seen above that to prove completeness, we must
2433       show that the normal set of our graph representation is a subset
2434       of the intended normal set.
2435
2436       However, it is hard to systematically generate or reason about the
2437       normal set, since it is defined as any nodes to which no
2438       transformation applies. To determine this set, each transformation
2439       must be considered and when a transformation is added, the entire
2440       set should be re-evaluated. This means it is hard to show that
2441       each node in the normal set is also in the intended normal set.
2442       Reasoning about our intended normal set is easier, since we know
2443       how to generate it from its definition. \refdef{intended normal
2444       form definition}.
2445
2446       Fortunately, we can also prove the complement (which is
2447       equivalent, since $A \subseteq B \Leftrightarrow \overline{B}
2448       \subseteq \overline{A}$): Show that the set of nodes not in
2449       intended normal form is a subset of the set of nodes not in normal
2450       form. In other words, show that for every expression that is not
2451       in intended normal form, that there is at least one transformation
2452       that applies to it (since that means it is not in normal form
2453       either and since $A \subseteq C \Leftrightarrow \forall x (x \in A
2454       \rightarrow x \in C)$).
2455
2456       By systematically reviewing the entire Core language definition
2457       along with the intended normal form definition (both of which have
2458       a similar structure), it should be possible to identify all
2459       possible (sets of) core expressions that are not in intended
2460       normal form and identify a transformation that applies to it.
2461       
2462       This approach is especially useful for proving completeness of our
2463       system, since if expressions exist to which none of the
2464       transformations apply (\ie\ if the system is not yet complete), it
2465       is immediately clear which expressions these are and adding
2466       (or modifying) transformations to fix this should be relatively
2467       easy.
2468
2469       As observed above, applying this approach is a lot of work, since
2470       we need to check every (set of) transformation(s) separately.
2471
2472       \todo{Perhaps do a few steps of the proofs as proof-of-concept}
2473
2474 % vim: set sw=2 sts=2 expandtab: