Add an intermezzo about the id function.
[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       \subsubsection{Case normalization}
1477         This transformation ensures that all case expressions get a form
1478         that is allowed by the intended normal form. This means they
1479         will become one of: \refdef{intended normal form definition}
1480
1481         \startitemize
1482         \item An extractor case with a single alternative that picks a field
1483         from a datatype, \eg\ \lam{case x of (a, b) -> a}.
1484         \item A selector case with multiple alternatives and only wild binders, that
1485         makes a choice between expressions based on the constructor of another
1486         expression, \eg\ \lam{case x of Low -> a; High -> b}.
1487         \stopitemize
1488
1489         For an arbitrary case, that has \lam{n} alternatives, with
1490         \lam{m} binders in each alternatives, this will result in \lam{m
1491         * n} extractor case expression to get at each variable, \lam{n}
1492         let bindings for each of the alternatives' value and a single
1493         selector case to select the right value out of these.
1494
1495         Technically, the defintion of this transformation would require
1496         that the constructor for every alternative has exactly the same
1497         amount (\lam{m}) of arguments, but of course this transformation
1498         also applies when this is not the case.
1499         
1500         \starttrans
1501         case E of
1502           C0 v0,0 ... v0,m -> E0
1503           \vdots
1504           Cn vn,0 ... vn,m -> En
1505         --------------------------------------------------- \lam{\forall i \forall j, 0 ≤ i ≤ n, 0 ≤ i < m} (\lam{wi,j} is a wild (unused) binder)
1506         letrec                                              The case expression is not an extractor case
1507           v0,0 = case E of C0 x0,0 .. x0,m -> x0,0          The case expression is not a selector case
1508           \vdots
1509           v0,m = case E of C0 x0,0 .. x0,m -> x0,m
1510           \vdots
1511           vn,m = case E of Cn xn,0 .. xn,m -> xn,m
1512           y0 = E0
1513           \vdots
1514           yn = En
1515         in
1516           case E of
1517             C0 w0,0 ... w0,m -> y0
1518             \vdots
1519             Cn wn,0 ... wn,m -> yn
1520         \stoptrans
1521
1522         \refdef{wild binder}
1523         Note that this transformation applies to case expressions with any
1524         scrutinee. If the scrutinee is a complex expression, this might
1525         result in duplication of work (hardware). An extra condition to
1526         only apply this transformation when the scrutinee is already
1527         simple (effectively causing this transformation to be only
1528         applied after the scrutinee simplification transformation) might
1529         be in order. 
1530
1531         \startbuffer[from]
1532         case a of
1533           True -> add b 1
1534           False -> add b 2
1535         \stopbuffer
1536
1537         \startbuffer[to]
1538         letrec
1539           x0 = add b 1
1540           x1 = add b 2
1541         in
1542           case a of
1543             True -> x0
1544             False -> x1
1545         \stopbuffer
1546
1547         \transexample{selcasesimpl}{Selector case simplification}{from}{to}
1548
1549         \startbuffer[from]
1550         case a of
1551           (,) b c -> add b c
1552         \stopbuffer
1553         \startbuffer[to]
1554         letrec
1555           b = case a of (,) b c -> b
1556           c = case a of (,) b c -> c
1557           x0 = add b c
1558         in
1559           case a of
1560             (,) w0 w1 -> x0
1561         \stopbuffer
1562
1563         \transexample{excasesimpl}{Extractor case simplification}{from}{to}
1564
1565         \refdef{selector case}
1566         In \in{example}[ex:trans:excasesimpl] the case expression is expanded
1567         into multiple case expressions, including a pretty useless expression
1568         (that is neither a selector or extractor case). This case can be
1569         removed by the Case removal transformation in
1570         \in{section}[sec:transformation:caseremoval].
1571
1572       \subsubsection[sec:transformation:caseremoval]{Case removal}
1573         This transform removes any case expression with a single alternative and
1574         only wild binders.\refdef{wild binder}
1575
1576         These "useless" case expressions are usually leftovers from case simplification
1577         on extractor case (see the previous example).
1578
1579         \starttrans
1580         case x of
1581           C v0 ... vm -> E
1582         ----------------------     \lam{\forall i, 0 ≤ i ≤ m} (\lam{vi} does not occur free in E)
1583         E
1584         \stoptrans
1585
1586         \startbuffer[from]
1587         case a of
1588           (,) w0 w1 -> x0
1589         \stopbuffer
1590
1591         \startbuffer[to]
1592         x0
1593         \stopbuffer
1594
1595         \transexample{caserem}{Case removal}{from}{to}
1596
1597     \subsection[sec:normalization:nonrep]{Removing unrepresentable values}
1598       The transformations in this section are aimed at making all the
1599       values used in our expression representable. There are two main
1600       transformations that are applied to \emph{all} unrepresentable let
1601       bindings and function arguments. These are meant to address three
1602       different kinds of unrepresentable values: Polymorphic values,
1603       higher-order values and literals. The transformation are described
1604       generically: They apply to all non-representable values. However,
1605       non-representable values that do not fall into one of these three
1606       categories will be moved around by these transformations but are
1607       unlikely to completely disappear. They usually mean the program was not
1608       valid in the first place, because unsupported types were used (for
1609       example, a program using strings).
1610      
1611       Each of these three categories will be detailed below, followed by the
1612       actual transformations.
1613
1614       \subsubsection{Removing Polymorphism}
1615         As noted in \in{section}[sec:prototype:polymporphism],
1616         polymorphism is made explicit in Core through type and
1617         dictionary arguments. To remove the polymorphism from a
1618         function, we can simply specialize the polymorphic function for
1619         the particular type applied to it. The same goes for dictionary
1620         arguments. To remove polymorphism from let bound values, we
1621         simply inline the let bindings that have a polymorphic type,
1622         which should (eventually) make sure that the polymorphic
1623         expression is applied to a type and/or dictionary, which can
1624         then be removed by β-reduction (\in{section}[sec:normalization:beta]).
1625
1626         Since both type and dictionary arguments are not representable,
1627         \refdef{representable}
1628         the non-representable argument specialization and
1629         non-representable let binding inlining transformations below
1630         take care of exactly this.
1631
1632         There is one case where polymorphism cannot be completely
1633         removed: Built-in functions are still allowed to be polymorphic
1634         (Since we have no function body that we could properly
1635         specialize). However, the code that generates \VHDL\ for built-in
1636         functions knows how to handle this, so this is not a problem.
1637
1638       \subsubsection[sec:normalization:defunctionalization]{Defunctionalization}
1639         These transformations remove higher-order expressions from our
1640         program, making all values first-order. The approach used for
1641         defunctionalization uses a combination of specialization, inlining and
1642         some cleanup transformations, was also proposed in parallel research
1643         by Neil Mitchell \cite[mitchell09].
1644       
1645         Higher order values are always introduced by lambda abstractions, none
1646         of the other Core expression elements can introduce a function type.
1647         However, other expressions can \emph{have} a function type, when they
1648         have a lambda expression in their body. 
1649         
1650         For example, the following expression is a higher-order expression
1651         that is not a lambda expression itself:
1652         
1653         \refdef{id function}
1654         \startlambda
1655           case x of
1656             High -> id
1657             Low -> λx.x
1658         \stoplambda
1659
1660         The reference to the \lam{id} function shows that we can introduce a
1661         higher-order expression in our program without using a lambda
1662         expression directly. However, inside the definition of the \lam{id}
1663         function, we can be sure that a lambda expression is present.
1664         
1665         Looking closely at the definition of our normal form in
1666         \in{section}[sec:normalization:intendednormalform], we can see that
1667         there are three possibilities for higher-order values to appear in our
1668         intended normal form:
1669
1670         \startitemize[KR]
1671           \item[item:toplambda] Lambda abstractions can appear at the highest level of a
1672           top level function. These lambda abstractions introduce the
1673           arguments (input ports / current state) of the function.
1674           \item[item:built-inarg] (Partial applications of) top level functions can appear as an
1675           argument to a built-in function.
1676           \item[item:completeapp] (Partial applications of) top level functions can appear in
1677           function position of an application. Since a partial application
1678           cannot appear anywhere else (except as built-in function arguments),
1679           all partial applications are applied, meaning that all applications
1680           will become complete applications. However, since application of
1681           arguments happens one by one, in the expression:
1682           \startlambda
1683             f 1 2
1684           \stoplambda
1685           the subexpression \lam{f 1} has a function type. But this is
1686           allowed, since it is inside a complete application.
1687         \stopitemize
1688
1689         We will take a typical function with some higher-order values as an
1690         example. The following function takes two arguments: a \lam{Bit} and a
1691         list of numbers. Depending on the first argument, each number in the
1692         list is doubled, or the list is returned unmodified. For the sake of
1693         the example, no polymorphism is shown. In reality, at least map would
1694         be polymorphic.
1695
1696         \startlambda
1697         λy.let double = λx. x + x in
1698              case y of
1699                 Low -> map double
1700                 High -> λz. z
1701         \stoplambda
1702
1703         This example shows a number of higher-order values that we cannot
1704         translate to \VHDL\ directly. The \lam{double} binder bound in the let
1705         expression has a function type, as well as both of the alternatives of
1706         the case expression. The first alternative is a partial application of
1707         the \lam{map} built-in function, whereas the second alternative is a
1708         lambda abstraction.
1709
1710         To reduce all higher-order values to one of the above items, a number
1711         of transformations we have already seen are used. The η-abstraction
1712         transformation from \in{section}[sec:normalization:eta] ensures all
1713         function arguments are introduced by lambda abstraction on the highest
1714         level of a function. These lambda arguments are allowed because of
1715         \in{item}[item:toplambda] above. After η-abstraction, our example
1716         becomes a bit bigger:
1717
1718         \startlambda
1719         λy.λq.(let double = λx. x + x in
1720                  case y of
1721                    Low -> map double
1722                    High -> λz. z
1723               ) q
1724         \stoplambda
1725
1726         η-abstraction also introduces extra applications (the application of
1727         the let expression to \lam{q} in the above example). These
1728         applications can then propagated down by the application propagation
1729         transformation (\in{section}[sec:normalization:appprop]). In our
1730         example, the \lam{q} and \lam{r} variable will be propagated into the
1731         let expression and then into the case expression:
1732
1733         \startlambda
1734         λy.λq.let double = λx. x + x in
1735                 case y of
1736                   Low -> map double q
1737                   High -> (λz. z) q
1738         \stoplambda
1739         
1740         This propagation makes higher-order values become applied (in
1741         particular both of the alternatives of the case now have a
1742         representable type). Completely applied top level functions (like the
1743         first alternative) are now no longer invalid (they fall under
1744         \in{item}[item:completeapp] above). (Completely) applied lambda
1745         abstractions can be removed by β-abstraction. For our example,
1746         applying β-abstraction results in the following:
1747
1748         \startlambda
1749         λy.λq.let double = λx. x + x in
1750                 case y of
1751                   Low -> map double q
1752                   High -> q
1753         \stoplambda
1754
1755         As you can see in our example, all of this moves applications towards
1756         the higher-order values, but misses higher-order functions bound by
1757         let expressions. The applications cannot be moved towards these values
1758         (since they can be used in multiple places), so the values will have
1759         to be moved towards the applications. This is achieved by inlining all
1760         higher-order values bound by let applications, by the
1761         non-representable binding inlining transformation below. When applying
1762         it to our example, we get the following:
1763         
1764         \startlambda
1765         λy.λq.case y of
1766                 Low -> map (λx. x + x) q
1767                 High -> q
1768         \stoplambda
1769
1770         We have nearly eliminated all unsupported higher-order values from this
1771         expressions. The one that is remaining is the first argument to the
1772         \lam{map} function. Having higher-order arguments to a built-in
1773         function like \lam{map} is allowed in the intended normal form, but
1774         only if the argument is a (partial application) of a top level
1775         function. This is easily done by introducing a new top level function
1776         and put the lambda abstraction inside. This is done by the function
1777         extraction transformation from
1778         \in{section}[sec:normalization:funextract].
1779
1780         \startlambda
1781         λy.λq.case y of
1782                 Low -> map func q
1783                 High -> q
1784         \stoplambda
1785
1786         This also introduces a new function, that we have called \lam{func}:
1787
1788         \startlambda
1789         func = λx. x + x
1790         \stoplambda
1791
1792         Note that this does not actually remove the lambda, but now it is a
1793         lambda at the highest level of a function, which is allowed in the
1794         intended normal form.
1795
1796         There is one case that has not been discussed yet. What if the
1797         \lam{map} function in the example above was not a built-in function
1798         but a user-defined function? Then extracting the lambda expression
1799         into a new function would not be enough, since user-defined functions
1800         can never have higher-order arguments. For example, the following
1801         expression shows an example:
1802
1803         \startlambda
1804         twice :: (Word -> Word) -> Word -> Word
1805         twice = λf.λa.f (f a)
1806
1807         main = λa.app (λx. x + x) a
1808         \stoplambda
1809
1810         This example shows a function \lam{twice} that takes a function as a
1811         first argument and applies that function twice to the second argument.
1812         Again, we have made the function monomorphic for clarity, even though
1813         this function would be a lot more useful if it was polymorphic. The
1814         function \lam{main} uses \lam{twice} to apply a lambda epression twice.
1815
1816         When faced with a user defined function, a body is available for that
1817         function. This means we could create a specialized version of the
1818         function that only works for this particular higher-order argument
1819         (\ie, we can just remove the argument and call the specialized
1820         function without the argument). This transformation is detailed below.
1821         Applying this transformation to the example gives:
1822
1823         \startlambda
1824         twice' :: Word -> Word
1825         twice' = λb.(λf.λa.f (f a)) (λx. x + x) b
1826
1827         main = λa.app' a
1828         \stoplambda
1829
1830         The \lam{main} function is now in normal form, since the only
1831         higher-order value there is the top level lambda expression. The new
1832         \lam{twice'} function is a bit complex, but the entire original body
1833         of the original \lam{twice} function is wrapped in a lambda
1834         abstraction and applied to the argument we have specialized for
1835         (\lam{λx. x + x}) and the other arguments. This complex expression can
1836         fortunately be effectively reduced by repeatedly applying β-reduction: 
1837
1838         \startlambda
1839         twice' :: Word -> Word
1840         twice' = λb.(b + b) + (b + b)
1841         \stoplambda
1842
1843         This example also shows that the resulting normal form might not be as
1844         efficient as we might hope it to be (it is calculating \lam{(b + b)}
1845         twice). This is discussed in more detail in
1846         \in{section}[sec:normalization:duplicatework].
1847
1848       \subsubsection{Literals}
1849         There are a limited number of literals available in Haskell and Core.
1850         \refdef{enumerated types} When using (enumerating) algebraic
1851         datatypes, a literal is just a reference to the corresponding data
1852         constructor, which has a representable type (the algebraic datatype)
1853         and can be translated directly. This also holds for literals of the
1854         \hs{Bool} Haskell type, which is just an enumerated type.
1855
1856         There is, however, a second type of literal that does not have a
1857         representable type: Integer literals. Cλash supports using integer
1858         literals for all three integer types supported (\hs{SizedWord},
1859         \hs{SizedInt} and \hs{RangedWord}). This is implemented using
1860         Haskell's \hs{Num} type class, which offers a \hs{fromInteger} method
1861         that converts any \hs{Integer} to the Cλash datatypes.
1862
1863         When \GHC\ sees integer literals, it will automatically insert calls to
1864         the \hs{fromInteger} method in the resulting Core expression. For
1865         example, the following expression in Haskell creates a 32 bit unsigned
1866         word with the value 1. The explicit type signature is needed, since
1867         there is no context for \GHC\ to determine the type from otherwise.
1868
1869         \starthaskell
1870         1 :: SizedWord D32
1871         \stophaskell
1872
1873         This Haskell code results in the following Core expression:
1874
1875         \startlambda
1876         fromInteger @(SizedWord D32) \$dNum (smallInteger 10)
1877         \stoplambda
1878
1879         The literal 10 will have the type \lam{GHC.Prim.Int\#}, which is
1880         converted into an \lam{Integer} by \lam{smallInteger}. Finally, the
1881         \lam{fromInteger} function will finally convert this into a
1882         \lam{SizedWord D32}.
1883
1884         Both the \lam{GHC.Prim.Int\#} and \lam{Integer} types are not
1885         representable, and cannot be translated directly. Fortunately, there
1886         is no need to translate them, since \lam{fromInteger} is a built-in
1887         function that knows how to handle these values. However, this does
1888         require that the \lam{fromInteger} function is directly applied to
1889         these non-representable literal values, otherwise errors will occur.
1890         For example, the following expression is not in the intended normal
1891         form, since one of the let bindings has an unrepresentable type
1892         (\lam{Integer}):
1893
1894         \startlambda
1895         let l = smallInteger 10 in fromInteger @(SizedWord D32) \$dNum l
1896         \stoplambda
1897
1898         By inlining these let-bindings, we can ensure that unrepresentable
1899         literals bound by a let binding end up in an application of the
1900         appropriate built-in function, where they are allowed. Since it is
1901         possible that the application of that function is in a different
1902         function than the definition of the literal value, we will always need
1903         to specialize away any unrepresentable literals that are used as
1904         function arguments. The following two transformations do exactly this.
1905
1906       \subsubsection{Non-representable binding inlining}
1907         This transform inlines let bindings that are bound to a
1908         non-representable value. Since we can never generate a signal
1909         assignment for these bindings (we cannot declare a signal assignment
1910         with a non-representable type, for obvious reasons), we have no choice
1911         but to inline the binding to remove it.
1912
1913         As we have seen in the previous sections, inlining these bindings
1914         solves (part of) the polymorphism, higher-order values and
1915         unrepresentable literals in an expression.
1916
1917         \refdef{substitution notation}
1918         \starttrans
1919         letrec 
1920           a0 = E0
1921           \vdots
1922           ai = Ei
1923           \vdots
1924           an = En
1925         in
1926           M
1927         --------------------------    \lam{Ei} has a non-representable type.
1928         letrec
1929           a0 = E0 [ai=>Ei] \vdots
1930           ai-1 = Ei-1 [ai=>Ei]
1931           ai+1 = Ei+1 [ai=>Ei]
1932           \vdots
1933           an = En [ai=>Ei]
1934         in
1935           M[ai=>Ei]
1936         \stoptrans
1937
1938         \startbuffer[from]
1939         letrec
1940           a = smallInteger 10
1941           inc = λb -> add b 1
1942           inc' = add 1
1943           x = fromInteger a 
1944         in
1945           inc (inc' x)
1946         \stopbuffer
1947
1948         \startbuffer[to]
1949         letrec
1950           x = fromInteger (smallInteger 10)
1951         in
1952           (λb -> add b 1) (add 1 x)
1953         \stopbuffer
1954
1955         \transexample{nonrepinline}{Nonrepresentable binding inlining}{from}{to}
1956
1957       \subsubsection[sec:normalization:specialize]{Function specialization}
1958         This transform removes arguments to user-defined functions that are
1959         not representable at runtime. This is done by creating a
1960         \emph{specialized} version of the function that only works for one
1961         particular value of that argument (in other words, the argument can be
1962         removed).
1963
1964         Specialization means to create a specialized version of the called
1965         function, with one argument already filled in. As a simple example, in
1966         the following program (this is not actual Core, since it directly uses
1967         a literal with the unrepresentable type \lam{GHC.Prim.Int\#}).
1968
1969         \startlambda
1970         f = λa.λb.a + b
1971         inc = λa.f a 1
1972         \stoplambda
1973
1974         We could specialize the function \lam{f} against the literal argument
1975         1, with the following result:
1976
1977         \startlambda
1978         f' = λa.a + 1
1979         inc = λa.f' a
1980         \stoplambda
1981
1982         In some way, this transformation is similar to β-reduction, but it
1983         operates across function boundaries. It is also similar to
1984         non-representable let binding inlining above, since it sort of
1985         \quote{inlines} an expression into a called function.
1986
1987         Special care must be taken when the argument has any free variables.
1988         If this is the case, the original argument should not be removed
1989         completely, but replaced by all the free variables of the expression.
1990         In this way, the original expression can still be evaluated inside the
1991         new function.
1992
1993         To prevent us from propagating the same argument over and over, a
1994         simple local variable reference is not propagated (since is has
1995         exactly one free variable, itself, we would only replace that argument
1996         with itself).
1997
1998         This shows that any free local variables that are not runtime
1999         representable cannot be brought into normal form by this transform. We
2000         rely on an inlining or β-reduction transformation to replace such a
2001         variable with an expression we can propagate again.
2002
2003         \starttrans
2004         x = E
2005         ~
2006         x Y0 ... Yi ... Yn                               \lam{Yi} is not representable
2007         ---------------------------------------------    \lam{Yi} is not a local variable reference
2008         x' Y0 ... Yi-1 f0 ...  fm Yi+1 ... Yn            \lam{f0 ... fm} are all free local vars of \lam{Yi}
2009         ~                                                \lam{T0 ... Tn} are the types of \lam{Y0 ... Yn}
2010         x' = λ(y0 :: T0) ... λ(yi-1 :: Ty-1). 
2011              λf0 ... λfm.
2012              λ(yi+1 :: Ty+1) ...  λ(yn :: Tn).       
2013                E y0 ... yi-1 Yi yi+1 ... yn   
2014         \stoptrans
2015
2016         This is a bit of a complex transformation. It transforms an
2017         application of the function \lam{x}, where one of the arguments
2018         (\lam{Y_i}) is not representable. A new
2019         function \lam{x'} is created that wraps the body of the old function.
2020         The body of the new function becomes a number of nested lambda
2021         abstractions, one for each of the original arguments that are left
2022         unchanged.
2023         
2024         The ith argument is replaced with the free variables of
2025         \lam{Y_i}. Note that we reuse the same binders as those used in
2026         \lam{Y_i}, since we can then just use \lam{Y_i} inside the new
2027         function body and have all of the variables it uses be in scope.
2028
2029         The argument that we are specializing for, \lam{Y_i}, is put inside
2030         the new function body. The old function body is applied to it. Since
2031         we use this new function only in place of an application with that
2032         particular argument \lam{Y_i}, behaviour should not change.
2033         
2034         Note that the types of the arguments of our new function are taken
2035         from the types of the \emph{actual} arguments (\lam{T0 ... Tn}). This
2036         means that any polymorphism in the arguments is removed, even when the
2037         corresponding explicit type lambda is not removed
2038         yet.
2039
2040         \todo{Examples. Perhaps reference the previous sections}
2041
2042   \section{Unsolved problems}
2043     The above system of transformations has been implemented in the prototype
2044     and seems to work well to compile simple and more complex examples of
2045     hardware descriptions. \todo{Ref christiaan?} However, this normalization
2046     system has not seen enough review and work to be complete and work for
2047     every Core expression that is supplied to it. A number of problems
2048     have already been identified and are discussed in this section.
2049
2050     \subsection[sec:normalization:duplicatework]{Work duplication}
2051         A possible problem of β-reduction is that it could duplicate work.
2052         When the expression applied is not a simple variable reference, but
2053         requires calculation and the binder the lambda abstraction binds to
2054         is used more than once, more hardware might be generated than strictly
2055         needed. 
2056
2057         As an example, consider the expression:
2058
2059         \startlambda
2060         (λx. x + x) (a * b)
2061         \stoplambda
2062
2063         When applying β-reduction to this expression, we get:
2064
2065         \startlambda
2066         (a * b) + (a * b)
2067         \stoplambda
2068
2069         which of course calculates \lam{(a * b)} twice.
2070         
2071         A possible solution to this would be to use the following alternative
2072         transformation, which is of course no longer normal β-reduction. The
2073         followin transformation has not been tested in the prototype, but is
2074         given here for future reference:
2075
2076         \starttrans
2077         (λx.E) M
2078         -----------------
2079         letrec x = M in E
2080         \stoptrans
2081         
2082         This does not seem like much of an improvement, but it does get rid of
2083         the lambda expression (and the associated higher-order value), while
2084         at the same time introducing a new let binding. Since the result of
2085         every application or case expression must be bound by a let expression
2086         in the intended normal form anyway, this is probably not a problem. If
2087         the argument happens to be a variable reference, then simple let
2088         binding removal (\in{section}[sec:normalization:simplelet]) will
2089         remove it, making the result identical to that of the original
2090         β-reduction transformation.
2091
2092         When also applying argument simplification to the above example, we
2093         get the following expression:
2094
2095         \startlambda
2096         let y = (a * b)
2097             z = (a * b)
2098         in y + z
2099         \stoplambda
2100
2101         Looking at this, we could imagine an alternative approach: Create a
2102         transformation that removes let bindings that bind identical values.
2103         In the above expression, the \lam{y} and \lam{z} variables could be
2104         merged together, resulting in the more efficient expression:
2105
2106         \startlambda
2107         let y = (a * b) in y + y
2108         \stoplambda
2109
2110       \subsection[sec:normalization:non-determinism]{Non-determinism}
2111         As an example, again consider the following expression:
2112
2113         \startlambda
2114         (λx. x + x) (a * b)
2115         \stoplambda
2116
2117         We can apply both β-reduction (\in{section}[sec:normalization:beta])
2118         as well as argument simplification
2119         (\in{section}[sec:normalization:argsimpl]) to this expression.
2120
2121         When applying argument simplification first and then β-reduction, we
2122         get the following expression:
2123
2124         \startlambda
2125         let y = (a * b) in y + y
2126         \stoplambda
2127
2128         When applying β-reduction first and then argument simplification, we
2129         get the following expression:
2130
2131         \startlambda
2132         let y = (a * b)
2133             z = (a * b)
2134         in y + z
2135         \stoplambda
2136
2137         As you can see, this is a different expression. This means that the
2138         order of expressions, does in fact change the resulting normal form,
2139         which is something that we would like to avoid. In this particular
2140         case one of the alternatives is even clearly more efficient, so we
2141         would of course like the more efficient form to be the normal form.
2142
2143         For this particular problem, the solutions for duplication of work
2144         seem from the previous section seem to fix the determinism of our
2145         transformation system as well. However, it is likely that there are
2146         other occurences of this problem.
2147
2148       \subsection[sec:normalization:castproblems]{Casts}
2149         We do not fully understand the use of cast expressions in Core, so
2150         there are probably expressions involving cast expressions that cannot
2151         be brought into intended normal form by this transformation system.
2152
2153         The uses of casts in the core system should be investigated more and
2154         transformations will probably need updating to handle them in all
2155         cases.
2156
2157       \subsection[sec:normalization:stateproblems]{Normalization of stateful descriptions}
2158         Currently, the intended normal form definition\refdef{intended
2159         normal form definition} offers enough freedom to describe all
2160         valid stateful descriptions, but is not limiting enough. It is
2161         possible to write descriptions which are in intended normal
2162         form, but cannot be translated into \VHDL\ in a meaningful way
2163         (\eg, a function that swaps two substates in its result, or a
2164         function that changes a substate itself instead of passing it to
2165         a subfunction).
2166
2167         It is now up to the programmer to not do anything funny with
2168         these state values, whereas the normalization just tries not to
2169         mess up the flow of state values. In practice, there are
2170         situations where a Core program that \emph{could} be a valid
2171         stateful description is not translateable by the prototype. This
2172         most often happens when statefulness is mixed with pattern
2173         matching, causing a state input to be unpacked multiple times or
2174         be unpacked and repacked only in some of the code paths.
2175
2176         Without going into detail about the exact problems (of which
2177         there are probably more than have shown up so far), it seems
2178         unlikely that these problems can be solved entirely by just
2179         improving the \VHDL\ state generation in the final stage. The
2180         normalization stage seems the best place to apply the rewriting
2181         needed to support more complex stateful descriptions. This does
2182         of course mean that the intended normal form definition must be
2183         extended as well to be more specific about how state handling
2184         should look like in normal form.
2185         \in{Section}[sec:prototype:statelimits] already contains a
2186         tight description of the limitations on the use of state
2187         variables, which could be adapted into the intended normal form.
2188
2189   \section[sec:normalization:properties]{Provable properties}
2190     When looking at the system of transformations outlined above, there are a
2191     number of questions that we can ask ourselves. The main question is of course:
2192     \quote{Does our system work as intended?}. We can split this question into a
2193     number of subquestions:
2194
2195     \startitemize[KR]
2196     \item[q:termination] Does our system \emph{terminate}? Since our system will
2197     keep running as long as transformations apply, there is an obvious risk that
2198     it will keep running indefinitely. This typically happens when one
2199     transformation produces a result that is transformed back to the original
2200     by another transformation, or when one or more transformations keep
2201     expanding some expression.
2202     \item[q:soundness] Is our system \emph{sound}? Since our transformations
2203     continuously modify the expression, there is an obvious risk that the final
2204     normal form will not be equivalent to the original program: Its meaning could
2205     have changed.
2206     \item[q:completeness] Is our system \emph{complete}? Since we have a complex
2207     system of transformations, there is an obvious risk that some expressions will
2208     not end up in our intended normal form, because we forgot some transformation.
2209     In other words: Does our transformation system result in our intended normal
2210     form for all possible inputs?
2211     \item[q:determinism] Is our system \emph{deterministic}? Since we have defined
2212     no particular order in which the transformation should be applied, there is an
2213     obvious risk that different transformation orderings will result in
2214     \emph{different} normal forms. They might still both be intended normal forms
2215     (if our system is \emph{complete}) and describe correct hardware (if our
2216     system is \emph{sound}), so this property is less important than the previous
2217     three: The translator would still function properly without it.
2218     \stopitemize
2219
2220     Unfortunately, the final transformation system has only been
2221     developed in the final part of the research, leaving no more time
2222     for verifying these properties. In fact, it is likely that the
2223     current transformation system still violates some of these
2224     properties in some cases and should be improved (or extra conditions
2225     on the input hardware descriptions should be formulated).
2226
2227     This is most likely the case with the completeness and determinism
2228     properties, perhaps als the termination property. The soundness
2229     property probably holds, since it is easier to manually verify (each
2230     transformation can be reviewed separately).
2231
2232     Even though no complete proofs have been made, some ideas for
2233     possible proof strategies are shown below.
2234
2235     \subsection{Graph representation}
2236       Before looking into how to prove these properties, we will look at
2237       transformation systems from a graph perspective. We will first define
2238       the graph view and then illustrate it using a simple example from lambda
2239       calculus (which is a different system than the Cλash normalization
2240       system). The nodes of the graph are all possible Core expressions. The
2241       (directed) edges of the graph are transformations. When a transformation
2242       α applies to an expression \lam{A} to produce an expression \lam{B}, we
2243       add an edge from the node for \lam{A} to the node for \lam{B}, labeled
2244       α.
2245
2246       \startuseMPgraphic{TransformGraph}
2247         save a, b, c, d;
2248
2249         % Nodes
2250         newCircle.a(btex \lam{(λx.λy. (+) x y) 1} etex);
2251         newCircle.b(btex \lam{λy. (+) 1 y} etex);
2252         newCircle.c(btex \lam{(λx.(+) x) 1} etex);
2253         newCircle.d(btex \lam{(+) 1} etex);
2254
2255         b.c = origin;
2256         c.c = b.c + (4cm, 0cm);
2257         a.c = midpoint(b.c, c.c) + (0cm, 4cm);
2258         d.c = midpoint(b.c, c.c) - (0cm, 3cm);
2259
2260         % β-conversion between a and b
2261         ncarc.a(a)(b) "name(bred)";
2262         ObjLabel.a(btex $\xrightarrow[normal]{}{β}$ etex) "labpathname(bred)", "labdir(rt)";
2263         ncarc.b(b)(a) "name(bexp)", "linestyle(dashed withdots)";
2264         ObjLabel.b(btex $\xleftarrow[normal]{}{β}$ etex) "labpathname(bexp)", "labdir(lft)";
2265
2266         % η-conversion between a and c
2267         ncarc.a(a)(c) "name(ered)";
2268         ObjLabel.a(btex $\xrightarrow[normal]{}{η}$ etex) "labpathname(ered)", "labdir(rt)";
2269         ncarc.c(c)(a) "name(eexp)", "linestyle(dashed withdots)";
2270         ObjLabel.c(btex $\xleftarrow[normal]{}{η}$ etex) "labpathname(eexp)", "labdir(lft)";
2271
2272         % η-conversion between b and d
2273         ncarc.b(b)(d) "name(ered)";
2274         ObjLabel.b(btex $\xrightarrow[normal]{}{η}$ etex) "labpathname(ered)", "labdir(rt)";
2275         ncarc.d(d)(b) "name(eexp)", "linestyle(dashed withdots)";
2276         ObjLabel.d(btex $\xleftarrow[normal]{}{η}$ etex) "labpathname(eexp)", "labdir(lft)";
2277
2278         % β-conversion between c and d
2279         ncarc.c(c)(d) "name(bred)";
2280         ObjLabel.c(btex $\xrightarrow[normal]{}{β}$ etex) "labpathname(bred)", "labdir(rt)";
2281         ncarc.d(d)(c) "name(bexp)", "linestyle(dashed withdots)";
2282         ObjLabel.d(btex $\xleftarrow[normal]{}{β}$ etex) "labpathname(bexp)", "labdir(lft)";
2283
2284         % Draw objects and lines
2285         drawObj(a, b, c, d);
2286       \stopuseMPgraphic
2287
2288       \placeexample[right][ex:TransformGraph]{Partial graph of a lambda calculus
2289       system with β and η reduction (solid lines) and expansion (dotted lines).}
2290           \boxedgraphic{TransformGraph}
2291
2292       Of course the graph for Cλash is unbounded, since we can construct an
2293       infinite amount of Core expressions. Also, there might potentially be
2294       multiple edges between two given nodes (with different labels), though
2295       this seems unlikely to actually happen in our system.
2296
2297       See \in{example}[ex:TransformGraph] for the graph representation of a very
2298       simple lambda calculus that contains just the expressions \lam{(λx.λy. (+) x
2299       y) 1}, \lam{λy. (+) 1 y}, \lam{(λx.(+) x) 1} and \lam{(+) 1}. The
2300       transformation system consists of β-reduction and η-reduction (solid edges) or
2301       β-expansion and η-expansion (dotted edges).
2302
2303       \todo{Define β-reduction and η-reduction?}
2304
2305       Note that the normal form of such a system consists of the set of nodes
2306       (expressions) without outgoing edges, since those are the expressions to which
2307       no transformation applies anymore. We call this set of nodes the \emph{normal
2308       set}. The set of nodes containing expressions in intended normal
2309       form \refdef{intended normal form} is called the \emph{intended
2310       normal set}.
2311
2312       From such a graph, we can derive some properties easily:
2313       \startitemize[KR]
2314         \item A system will \emph{terminate} if there is no walk (sequence of
2315         edges, or transformations) of infinite length in the graph (this
2316         includes cycles, but can also happen without cycles).
2317         \item Soundness is not easily represented in the graph.
2318         \item A system is \emph{complete} if all of the nodes in the normal set have
2319         the intended normal form. The inverse (that all of the nodes outside of
2320         the normal set are \emph{not} in the intended normal form) is not
2321         strictly required. In other words, our normal set must be a
2322         subset of the intended normal form, but they do not need to be
2323         the same set.
2324         form.
2325         \item A system is deterministic if all paths starting at a particular
2326         node, which end in a node in the normal set, end at the same node.
2327       \stopitemize
2328
2329       When looking at the \in{example}[ex:TransformGraph], we see that the system
2330       terminates for both the reduction and expansion systems (but note that, for
2331       expansion, this is only true because we have limited the possible
2332       expressions.  In complete lambda calculus, there would be a path from
2333       \lam{(λx.λy. (+) x y) 1} to \lam{(λx.λy.(λz.(+) z) x y) 1} to
2334       \lam{(λx.λy.(λz.(λq.(+) q) z) x y) 1} etc.)
2335
2336       If we would consider the system with both expansion and reduction, there
2337       would no longer be termination either, since there would be cycles all
2338       over the place.
2339
2340       The reduction and expansion systems have a normal set of containing just
2341       \lam{(+) 1} or \lam{(λx.λy. (+) x y) 1} respectively. Since all paths in
2342       either system end up in these normal forms, both systems are \emph{complete}.
2343       Also, since there is only one node in the normal set, it must obviously be
2344       \emph{deterministic} as well.
2345
2346     \subsection{Termination}
2347       In general, proving termination of an arbitrary program is a very
2348       hard problem. \todo{Ref about arbitrary termination} Fortunately,
2349       we only have to prove termination for our specific transformation
2350       system.
2351
2352       A common approach for these kinds of proofs is to associate a
2353       measure with each possible expression in our system. If we can
2354       show that each transformation strictly decreases this measure
2355       (\ie, the expression transformed to has a lower measure than the
2356       expression transformed from).  \todo{ref about measure-based
2357       termination proofs / analysis}
2358       
2359       A good measure for a system consisting of just β-reduction would
2360       be the number of lambda expressions in the expression. Since every
2361       application of β-reduction removes a lambda abstraction (and there
2362       is always a bounded number of lambda abstractions in every
2363       expression) we can easily see that a transformation system with
2364       just β-reduction will always terminate.
2365
2366       For our complete system, this measure would be fairly complex
2367       (probably the sum of a lot of things). Since the (conditions on)
2368       our transformations are pretty complex, we would need to include
2369       both simple things like the number of let expressions as well as
2370       more complex things like the number of case expressions that are
2371       not yet in normal form.
2372
2373       No real attempt has been made at finding a suitable measure for
2374       our system yet.
2375
2376     \subsection{Soundness}
2377       Soundness is a property that can be proven for each transformation
2378       separately. Since our system only runs separate transformations
2379       sequentially, if each of our transformations leaves the
2380       \emph{meaning} of the expression unchanged, then the entire system
2381       will of course leave the meaning unchanged and is thus
2382       \emph{sound}.
2383
2384       The current prototype has only been verified in an ad-hoc fashion
2385       by inspecting (the code for) each transformation. A more formal
2386       verification would be more appropriate.
2387
2388       To be able to formally show that each transformation properly
2389       preserves the meaning of every expression, we require an exact
2390       definition of the \emph{meaning} of every expression, so we can
2391       compare them. A definition of the operational semantics of \GHC's Core
2392       language is available \cite[sulzmann07], but this does not seem
2393       sufficient for our goals (but it is a good start).
2394
2395       It should be possible to have a single formal definition of
2396       meaning for Core for both normal Core compilation by \GHC\ and for
2397       our compilation to \VHDL. The main difference seems to be that in
2398       hardware every expression is always evaluated, while in software
2399       it is only evaluated if needed, but it should be possible to
2400       assign a meaning to core expressions that assumes neither.
2401       
2402       Since each of the transformations can be applied to any
2403       subexpression as well, there is a constraint on our meaning
2404       definition: The meaning of an expression should depend only on the
2405       meaning of subexpressions, not on the expressions themselves. For
2406       example, the meaning of the application in \lam{f (let x = 4 in
2407       x)} should be the same as the meaning of the application in \lam{f
2408       4}, since the argument subexpression has the same meaning (though
2409       the actual expression is different).
2410       
2411     \subsection{Completeness}
2412       Proving completeness is probably not hard, but it could be a lot
2413       of work. We have seen above that to prove completeness, we must
2414       show that the normal set of our graph representation is a subset
2415       of the intended normal set.
2416
2417       However, it is hard to systematically generate or reason about the
2418       normal set, since it is defined as any nodes to which no
2419       transformation applies. To determine this set, each transformation
2420       must be considered and when a transformation is added, the entire
2421       set should be re-evaluated. This means it is hard to show that
2422       each node in the normal set is also in the intended normal set.
2423       Reasoning about our intended normal set is easier, since we know
2424       how to generate it from its definition. \refdef{intended normal
2425       form definition}.
2426
2427       Fortunately, we can also prove the complement (which is
2428       equivalent, since $A \subseteq B \Leftrightarrow \overline{B}
2429       \subseteq \overline{A}$): Show that the set of nodes not in
2430       intended normal form is a subset of the set of nodes not in normal
2431       form. In other words, show that for every expression that is not
2432       in intended normal form, that there is at least one transformation
2433       that applies to it (since that means it is not in normal form
2434       either and since $A \subseteq C \Leftrightarrow \forall x (x \in A
2435       \rightarrow x \in C)$).
2436
2437       By systematically reviewing the entire Core language definition
2438       along with the intended normal form definition (both of which have
2439       a similar structure), it should be possible to identify all
2440       possible (sets of) core expressions that are not in intended
2441       normal form and identify a transformation that applies to it.
2442       
2443       This approach is especially useful for proving completeness of our
2444       system, since if expressions exist to which none of the
2445       transformations apply (\ie\ if the system is not yet complete), it
2446       is immediately clear which expressions these are and adding
2447       (or modifying) transformations to fix this should be relatively
2448       easy.
2449
2450       As observed above, applying this approach is a lot of work, since
2451       we need to check every (set of) transformation(s) separately.
2452
2453       \todo{Perhaps do a few steps of the proofs as proof-of-concept}
2454
2455 % vim: set sw=2 sts=2 expandtab: