1 \chapter{Normalization}
3 % A helper to print a single example in the half the page width. The example
4 % text should be in a buffer whose name is given in an argument.
6 % The align=right option really does left-alignment, but without the program
7 % will end up on a single line. The strut=no option prevents a bunch of empty
8 % space at the start of the frame.
10 \framed[offset=1mm,align=right,strut=no]{
11 \setuptyping[option=LAM,style=sans,before=,after=]
13 \setuptyping[option=none,style=\tttf]
18 % A transformation example
19 \definefloat[example][examples]
20 \setupcaption[example][location=top] % Put captions on top
22 \define[3]\transexample{
23 \placeexample[here]{#1}
24 \startcombination[2*1]
25 {\example{#2}}{Original program}
26 {\example{#3}}{Transformed program}
30 %\define[3]\transexampleh{
31 %% \placeexample[here]{#1}
32 %% \startcombination[1*2]
33 %% {\example{#2}}{Original program}
34 %% {\example{#3}}{Transformed program}
38 The first step in the core to VHDL translation process, is normalization. We
39 aim to bring the core description into a simpler form, which we can
40 subsequently translate into VHDL easily. This normal form is needed because
41 the full core language is more expressive than VHDL in some areas and because
42 core can describe expressions that do not have a direct hardware
45 TODO: Describe core properties not supported in VHDL, and describe how the
46 VHDL we want to generate should look like.
49 The transformations described here have a well-defined goal: To bring the
50 program in a well-defined form that is directly translatable to hardware,
51 while fully preserving the semantics of the program.
53 This {\em normal form} is again a Core program, but with a very specific
54 structure. A function in normal form has nested lambda's at the top, which
55 produce a let expression. This let expression binds every function application
56 in the function and produces a simple identifier. Every bound value in
57 the let expression is either a simple function application or a case
58 expression to extract a single element from a tuple returned by a
61 An example of a program in canonical form would be:
64 -- All arguments are an inital lambda
66 -- There are nested let expressions at top level
68 -- Unpack the state by coercion
69 s = sp :: (Word, Word)
70 -- Extract both registers from the state
71 r1 = case s of (fst, snd) -> fst
72 r2 = case s of (fst, snd) -> snd
73 -- Calling some other user-defined function.
75 -- Conditional connections
87 -- Packing the state by coercion
88 sp' = s' :: State (Word, Word)
89 -- Pack our return value
96 When looking at such a program from a hardware perspective, the top level
97 lambda's define the input ports. The value produced by the let expression is
98 the output port. Most function applications bound by the let expression
99 define a component instantiation, where the input and output ports are mapped
100 to local signals or arguments. Some of the others use a builtin
101 construction (\eg the \lam{case} statement) or call a builtin function
102 (\eg \lam{add} or \lam{sub}). For these, a hardcoded VHDL translation is
105 \subsection{Normal definition}
106 Formally, the normal form is a core program obeying the following
107 constraints. TODO: Update this section, this is probably not completely
108 accurate or relevant anymore.
110 \startitemize[R,inmargin]
111 %\item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
112 %$fun$ is an identifier that will be bound as a global identifier.
113 %\item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
114 %$\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
115 %\item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
116 %\item $letbinds$ is a list with elements of the form
117 %$\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
118 %an identifier that will be bound as local identifier. The type of the bound
119 %value must be a $hardware\;type$.
120 %\item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
121 %equivalent VHDL expression. Since there are many supported forms for this,
122 %these are defined in a separate table.
123 %\item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
124 %where $fun$ is a global identifier and $x$ is a local identifier.
125 %\item[retexpr] A $retexpr$ has the form $\expr{x}$ or $\expr{tupexpr}$, where $x$ is a local identifier that is bound as an $argument$ or $result$. A $retexpr$ must
126 %be of a $hardware\;type$.
127 %\item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
128 %where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
130 %\item A $hardware\;type$ is a type that can be directly translated to
131 %hardware. This includes the types $Bit$, $SizedWord$, tuples containing
132 %elements of $hardware\;type$s, and will include others. This explicitely
133 %excludes function types.
136 TODO: Say something about uniqueness of identifiers
138 \subsection{Builtin expressions}
139 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
141 \startitemize[m,inmargin]
143 %$tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
144 %where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
145 %e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
146 %be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
147 %\item TODO: Many more!
150 \section{Transform passes}
152 In this section we describe the actual transforms. Here we're using
153 the core language in a notation that resembles lambda calculus.
155 Each of these transforms is meant to be applied to every (sub)expression
156 in a program, for as long as it applies. Only when none of the
157 expressions can be applied anymore, the program is in normal form. We
158 hope to be able to prove that this form will obey all of the constraints
159 defined above, but this has yet to happen (though it seems likely that
162 Each of the transforms will be described informally first, explaining
163 the need for and goal of the transform. Then, a formal definition is
164 given, using a familiar syntax from the world of logic. Each transform
165 is specified as a number of conditions (above the horizontal line) and a
166 number of conclusions (below the horizontal line). The details of using
167 this notation are still a bit fuzzy, so comments are welcom.
169 TODO: Formally describe the "apply to every (sub)expression" in terms of
170 rules with full transformations in the conditions.
172 \subsection{η-abstraction}
173 This transformation makes sure that all arguments of a function-typed
174 expression are named, by introducing lambda expressions. When combined with
175 β-reduction and function inlining below, all function-typed expressions should
176 be lambda abstractions or global identifiers.
180 -------------- \lam{E} is not the first argument of an application.
181 λx.E x \lam{E} is not a lambda abstraction.
182 \lam{x} is a variable that does not occur free in \lam{E}.
186 foo = λa -> case a of
192 foo = λa.λx -> (case a of
197 \transexample{η-abstraction}{from}{to}
199 \subsection{Extended β-reduction}
200 This transformation is meant to propagate application expressions downwards
201 into expressions as far as possible. In lambda calculus, this reduction
202 is known as β-reduction, but it is of course only defined for
203 applications of lambda abstractions. We extend this reduction to also
204 work for the rest of core (case and let expressions).
218 %\transform{Extended β-reduction}
221 %\trans{(λx.E) M}{E[M/x]}
225 %\trans{(let binds in E) M}{let binds in E M}
237 b = (let y = 3 in add y) 2
246 b = let y = 3 in add y 2
251 \transexample{Extended β-reduction}{from}{to}
253 \subsection{Argument simplification}
254 The transforms in this section deal with simplifying application
255 arguments into normal form. The goal here is to:
258 \item Make all arguments of user-defined functions (\eg, of which
259 we have a function body) simple variable references of a runtime
261 \item Make all arguments of builtin functions either:
263 \item A type argument.
264 \item A dictionary argument.
265 \item A type level expression.
266 \item A variable reference of a runtime representable type.
267 \item A variable reference or partial application of a function type.
271 When looking at the arguments of a user-defined function, we can
272 divide them into two categories:
274 \item Arguments with a runtime representable type (\eg bits or vectors).
276 These arguments can be preserved in the program, since they can
277 be translated to input ports later on. However, since we can
278 only connect signals to input ports, these arguments must be
279 reduced to simple variables (for which signals will be
280 produced). This is taken care of by the argument extraction
282 \item Non-runtime representable typed arguments.
284 These arguments cannot be preserved in the program, since we
285 cannot represent them as input or output ports in the resulting
286 VHDL. To remove them, we create a specialized version of the
287 called function with these arguments filled in. This is done by
288 the argument propagation transform.
291 When looking at the arguments of a builtin function, we can divide them
295 \item Arguments with a runtime representable type.
297 As we have seen with user-defined functions, these arguments can
298 always be reduced to a simple variable reference, by the
299 argument extraction transform. Performing this transform for
300 builtin functions as well, means that the translation of builtin
301 functions can be limited to signal references, instead of
302 needing to support all possible expressions.
304 \item Arguments with a function type.
306 These arguments are functions passed to higher order builtins,
307 like \lam{map} and \lam{foldl}. Since implementing these
308 functions for arbitrary function-typed expressions (\eg, lambda
309 expressions) is rather comlex, we reduce these arguments to
310 (partial applications of) global functions.
312 We can still support arbitrary expressions from the user code,
313 by creating a new global function containing that expression.
314 This way, we can simply replace the argument with a reference to
315 that new function. However, since the expression can contain any
316 number of free variables we also have to include partial
317 applications in our normal form.
319 This category of arguments is handled by the function extraction
321 \item Other unrepresentable arguments.
323 These arguments can take a few different forms:
324 \startdesc{Type arguments}
325 In the core language, type arguments can only take a single
326 form: A type wrapped in the Type constructor. Also, there is
327 nothing that can be done with type expressions, except for
328 applying functions to them, so we can simply leave type
329 arguments as they are.
331 \startdesc{Dictionary arguments}
332 In the core language, dictionary arguments are used to find
333 operations operating on one of the type arguments (mostly for
334 finding class methods). Since we will not actually evaluatie
335 the function body for builtin functions and can generate
336 code for builtin functions by just looking at the type
337 arguments, these arguments can be ignored and left as they
340 \startdesc{Type level arguments}
341 Sometimes, we want to pass a value to a builtin function, but
342 we need to know the value at compile time. Additionally, the
343 value has an impact on the type of the function. This is
344 encoded using type-level values, where the actual value of the
345 argument is not important, but the type encodes some integer,
346 for example. Since the value is not important, the actual form
347 of the expression does not matter either and we can leave
348 these arguments as they are.
350 \startdesc{Other arguments}
351 Technically, there is still a wide array of arguments that can
352 be passed, but does not fall into any of the above categories.
353 However, none of the supported builtin functions requires such
354 an argument. This leaves use with passing unsupported types to
355 a function, such as calling \lam{head} on a list of functions.
357 In these cases, it would be impossible to generate hardware
358 for such a function call anyway, so we can ignore these
361 The only way to generate hardware for builtin functions with
362 arguments like these, is to expand the function call into an
363 equivalent core expression (\eg, expand map into a series of
364 function applications). But for now, we choose to simply not
365 support expressions like these.
368 From the above, we can conclude that we can simply ignore these
369 other unrepresentable arguments and focus on the first two
373 \subsubsection{Argument extraction}
374 This transform deals with arguments to functions that
375 are of a runtime representable type.
377 TODO: It seems we can map an expression to a port, not only a signal.
378 Perhaps this makes this transformation not needed?
379 TODO: Say something about dataconstructors (without arguments, like True
380 or False), which are variable references of a runtime representable
381 type, but do not result in a signal.
383 To reduce a complex expression to a simple variable reference, we create
384 a new let expression around the application, which binds the complex
385 expression to a new variable. The original function is then applied to
388 %\transform{Argument extract}
390 %\lam{Y} is of a hardware representable type
392 %\lam{Y} is not a variable referene
396 %\trans{X Y}{let z = Y in X z}
399 \subsubsection{Function extraction}
400 This transform deals with function-typed arguments to builtin functions.
401 Since these arguments cannot be propagated, we choose to extract them
402 into a new global function instead.
404 Any free variables occuring in the extracted arguments will become
405 parameters to the new global function. The original argument is replaced
406 with a reference to the new function, applied to any free variables from
407 the original argument.
409 %\transform{Function extraction}
411 %\lam{X} is a (partial application of) a builtin function
413 %\lam{Y} is not an application
415 %\lam{Y} is not a variable reference
419 %\lam{f0 ... fm} = free local vars of \lam{Y}
421 %\lam{y} is a new global variable
423 %\lam{y = λf0 ... fn.Y}
425 %\trans{X Y}{X (y f0 ... fn)}
428 \subsubsection{Argument propagation}
429 This transform deals with arguments to user-defined functions that are
430 not representable at runtime. This means these arguments cannot be
431 preserved in the final form and most be {\em propagated}.
433 Propagation means to create a specialized version of the called
434 function, with the propagated argument already filled in. As a simple
435 example, in the following program:
442 we could {\em propagate} the constant argument 1, with the following
450 Special care must be taken when the to-be-propagated expression has any
451 free variables. If this is the case, the original argument should not be
452 removed alltogether, but replaced by all the free variables of the
453 expression. In this way, the original expression can still be evaluated
454 inside the new function. Also, this brings us closer to our goal: All
455 these free variables will be simple variable references.
457 To prevent us from propagating the same argument over and over, a simple
458 local variable reference is not propagated (since is has exactly one
459 free variable, itself, we would only replace that argument with itself).
461 This shows that any free local variables that are not runtime representable
462 cannot be brought into normal form by this transform. We rely on an
463 inlining transformation to replace such a variable with an expression we
466 TODO: Move these definitions somewhere sensible.
468 Definition: A global variable is any variable that is bound at the
469 top level of a program. A local variable is any other variable.
471 Definition: A hardware representable type is a type that we can generate
472 a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
473 unsigned word, etc. Types that are not runtime representable notably
474 include (but are not limited to): Types, dictionaries, functions.
476 Definition: A builtin function is a function for which a builtin
477 hardware translation is available, because its actual definition is not
478 translatable. A user-defined function is any other function.
483 x Y0 ... Yi ... Yn \lam{Yi} is not of a runtime representable type
484 --------------------------------------------- \lam{Yi} is not a local variable reference
485 x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . \lam{f0 ... fm} = free local vars of \lam{Y_i}
486 E y0 ... yi-1 Yi yi+1 ... yn
488 x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn
491 %\transform{Argument propagation}
493 %\lam{x} is a global variable, bound to a user-defined function
497 %\lam{Y_i} is not of a runtime representable type
499 %\lam{Y_i} is not a local variable reference
503 %\lam{f0 ... fm} = free local vars of \lam{Y_i}
505 %\lam{x'} is a new global variable
507 %\lam{x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . E y0 ... yi-1 Yi yi+1 ... yn}
509 %\trans{x Y0 ... Yi ... Yn}{x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn}
512 %TODO: The above definition looks too complicated... Can we find
513 %something more concise?
515 \subsection{Cast propagation}
516 This transform pushes casts down into the expression as far as possible.
517 \subsection{Let recursification}
518 This transform makes all lets recursive.
519 \subsection{Let simplification}
520 This transform makes the result value of all let expressions a simple
522 \subsection{Let flattening}
523 This transform turns two nested lets (\lam{let x = (let ... in ...) in
524 ...}) into a single let.
525 \subsection{Simple let binding removal}
526 This transforms inlines simple let bindings (\eg a = b).
527 \subsection{Function inlining}
528 This transform inlines let bindings of a funtion type. TODO: This should
529 be generelized to anything that is non representable at runtime, or
531 \subsection{Scrutinee simplification}
532 This transform ensures that the scrutinee of a case expression is always
533 a simple variable reference.
534 \subsection{Case binder wildening}
535 This transform replaces all binders of a each case alternative with a
536 wild binder (\ie, one that is never referred to). This will possibly
537 introduce a number of new "selector" case statements, that only select
538 one element from an algebraic datatype and bind it to a variable.
539 \subsection{Case value simplification}
540 This transform simplifies the result value of each case alternative by
541 binding the value in a let expression and replacing the value by a
542 simple variable reference.
543 \subsection{Case removal}
544 This transform removes any case statements with a single alternative and
547 \subsection{Example sequence}
549 This section lists an example expression, with a sequence of transforms
550 applied to it. The exact transforms given here probably don't exactly
551 match the transforms given above anymore, but perhaps this can clarify
552 the big picture a bit.
554 TODO: Update or remove this section.
572 After top-level η-abstraction:
591 After (extended) β-reduction:
609 After return value extraction:
628 Scrutinee simplification does not apply.
630 After case binder wildening:
635 a = case s of (a, _) -> a
636 b = case s of (_, b) -> b
637 r = case s of (_, _) ->
640 Low -> let op' = case b of
649 After case value simplification
654 a = case s of (a, _) -> a
655 b = case s of (_, b) -> b
656 r = case s of (_, _) -> r'
658 rl = let rll = λc.λd.c
671 After let flattening:
676 a = case s of (a, _) -> a
677 b = case s of (_, b) -> b
678 r = case s of (_, _) -> r'
692 After function inlining:
697 a = case s of (a, _) -> a
698 b = case s of (_, b) -> b
699 r = case s of (_, _) -> r'
711 After (extended) β-reduction again:
716 a = case s of (a, _) -> a
717 b = case s of (_, b) -> b
718 r = case s of (_, _) -> r'
730 After case value simplification again:
735 a = case s of (a, _) -> a
736 b = case s of (_, b) -> b
737 r = case s of (_, _) -> r'
755 a = case s of (a, _) -> a
756 b = case s of (_, b) -> b
770 After let bind removal:
775 a = case s of (a, _) -> a
776 b = case s of (_, b) -> b
789 Application simplification is not applicable.