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
97 \italic{normal} = \italic{lambda}
98 \italic{lambda} = λvar.\italic{lambda} (representable(typeof(var)))
100 \italic{toplet} = let \italic{binding} in \italic{toplet}
101 | letrec [\italic{binding}] in \italic{toplet}
102 | var (representable(typeof(var)), fvar(var))
103 \italic{binding} = var = \italic{rhs} (representable(typeof(rhs)))
104 -- State packing and unpacking by coercion
105 | var0 = var1 :: State ty (fvar(var1))
106 | var0 = var1 :: ty (var0 :: State ty) (fvar(var1))
107 \italic{rhs} = userapp
110 | case var of C a0 ... an -> ai (fvar(var))
112 | case var of (fvar(var))
113 DEFAULT -> var0 (fvar(var0))
114 C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, fvar(resvar))
115 \italic{userapp} = \italic{userfunc}
116 | \italic{userapp} {userarg}
117 \italic{userfunc} = var (tvar(var))
118 \italic{userarg} = var (fvar(var))
119 \italic{builtinapp} = \italic{builtinfunc}
120 | \italic{builtinapp} \italic{builtinarg}
121 \italic{builtinfunc} = var (bvar(var))
122 \italic{builtinarg} = \italic{coreexpr}
125 -- TODO: Define tvar, fvar, typeof, representable
126 -- TODO: Limit builtinarg further
128 -- TODO: There can still be other casts around (which the code can handle,
129 e.g., ignore), which still need to be documented here.
131 -- TODO: Note about the selector case. It just supports Bit and Bool
132 currently, perhaps it should be generalized in the normal form?
134 When looking at such a program from a hardware perspective, the top level
135 lambda's define the input ports. The value produced by the let expression is
136 the output port. Most function applications bound by the let expression
137 define a component instantiation, where the input and output ports are mapped
138 to local signals or arguments. Some of the others use a builtin
139 construction (\eg the \lam{case} statement) or call a builtin function
140 (\eg \lam{add} or \lam{sub}). For these, a hardcoded VHDL translation is
143 \subsection{Normal definition}
144 Formally, the normal form is a core program obeying the following
145 constraints. TODO: Update this section, this is probably not completely
146 accurate or relevant anymore.
148 \startitemize[R,inmargin]
149 %\item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
150 %$fun$ is an identifier that will be bound as a global identifier.
151 %\item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
152 %$\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
153 %\item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
154 %\item $letbinds$ is a list with elements of the form
155 %$\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
156 %an identifier that will be bound as local identifier. The type of the bound
157 %value must be a $hardware\;type$.
158 %\item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
159 %equivalent VHDL expression. Since there are many supported forms for this,
160 %these are defined in a separate table.
161 %\item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
162 %where $fun$ is a global identifier and $x$ is a local identifier.
163 %\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
164 %be of a $hardware\;type$.
165 %\item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
166 %where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
168 %\item A $hardware\;type$ is a type that can be directly translated to
169 %hardware. This includes the types $Bit$, $SizedWord$, tuples containing
170 %elements of $hardware\;type$s, and will include others. This explicitely
171 %excludes function types.
174 TODO: Say something about uniqueness of identifiers
176 \subsection{Builtin expressions}
177 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
179 \startitemize[m,inmargin]
181 %$tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
182 %where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
183 %e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
184 %be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
185 %\item TODO: Many more!
188 \section{Transform passes}
190 In this section we describe the actual transforms. Here we're using
191 the core language in a notation that resembles lambda calculus.
193 Each of these transforms is meant to be applied to every (sub)expression
194 in a program, for as long as it applies. Only when none of the
195 expressions can be applied anymore, the program is in normal form. We
196 hope to be able to prove that this form will obey all of the constraints
197 defined above, but this has yet to happen (though it seems likely that
200 Each of the transforms will be described informally first, explaining
201 the need for and goal of the transform. Then, a formal definition is
202 given, using a familiar syntax from the world of logic. Each transform
203 is specified as a number of conditions (above the horizontal line) and a
204 number of conclusions (below the horizontal line). The details of using
205 this notation are still a bit fuzzy, so comments are welcom.
207 TODO: Formally describe the "apply to every (sub)expression" in terms of
208 rules with full transformations in the conditions.
210 \subsection{η-abstraction}
211 This transformation makes sure that all arguments of a function-typed
212 expression are named, by introducing lambda expressions. When combined with
213 β-reduction and function inlining below, all function-typed expressions should
214 be lambda abstractions or global identifiers.
218 -------------- \lam{E} is not the first argument of an application.
219 λx.E x \lam{E} is not a lambda abstraction.
220 \lam{x} is a variable that does not occur free in \lam{E}.
224 foo = λa -> case a of
230 foo = λa.λx -> (case a of
235 \transexample{η-abstraction}{from}{to}
237 \subsection{Extended β-reduction}
238 This transformation is meant to propagate application expressions downwards
239 into expressions as far as possible. In lambda calculus, this reduction
240 is known as β-reduction, but it is of course only defined for
241 applications of lambda abstractions. We extend this reduction to also
242 work for the rest of core (case and let expressions).
264 For lambda expressions:
277 b = (let y = 3 in add y) 2
287 b = let y = 3 in add y 2
292 \transexample{Extended β-reduction}{from}{to}
294 \subsection{Let derecursification}
295 This transformation is meant to make lets non-recursive whenever possible.
296 This might allow other optimizations to do their work better. TODO: Why is
299 \subsection{Let flattening}
300 This transformation puts nested lets in the same scope, by lifting the
301 binding(s) of the inner let into a new let around the outer let. Eventually,
302 this will cause all let bindings to appear in the same scope (they will all be
303 in scope for the function return value).
305 Note that this transformation does not try to be smart when faced with
306 recursive lets, it will just leave the lets recursive (possibly joining a
307 recursive and non-recursive let into a single recursive let). The let
308 rederursification transformation will do this instead.
311 letnonrec x = (let bindings in M) in N
312 ------------------------------------------
313 let bindings in (letnonrec x = M) in N
319 x = (let bindings in M)
323 ------------------------------------------
342 b = let c = 3 in a + c
363 \transexample{Let flattening}{from}{to}
365 \subsection{Empty let removal}
366 This transformation is simple: It removes recursive lets that have no bindings
367 (which usually occurs when let derecursification removes the last binding from
376 \subsection{Simple let binding removal}
377 This transformation inlines simple let bindings (\eg a = b).
379 This transformation is not needed to get into normal form, but makes the
380 resulting VHDL a lot shorter.
406 \subsection{Unused let binding removal}
407 This transformation removes let bindings that are never used. Usually,
408 the desugarer introduces some unused let bindings.
410 This normalization pass should really be unneeded to get into normal form
411 (since ununsed bindings are not forbidden by the normal form), but in practice
412 the desugarer or simplifier emits some unused bindings that cannot be
413 normalized (e.g., calls to a \type{PatError} (TODO: Check this name)). Also,
414 this transformation makes the resulting VHDL a lot shorter.
418 ---------------------------- \lam{a} does not occur free in \lam{M}
429 ---------------------------- \lam{a} does not occur free in \lam{M}
437 \subsection{Non-representable binding inlining}
438 This transform inlines let bindings of a funtion type. TODO: This should
439 be generelized to anything that is non representable at runtime, or
442 \subsection{Scrutinee simplification}
443 This transform ensures that the scrutinee of a case expression is always
444 a simple variable reference.
446 \subsection{Case simplification}
448 \subsection{Case removal}
449 This transform removes any case statements with a single alternative and
452 \subsection{Argument simplification}
453 The transforms in this section deal with simplifying application
454 arguments into normal form. The goal here is to:
457 \item Make all arguments of user-defined functions (\eg, of which
458 we have a function body) simple variable references of a runtime
460 \item Make all arguments of builtin functions either:
462 \item A type argument.
463 \item A dictionary argument.
464 \item A type level expression.
465 \item A variable reference of a runtime representable type.
466 \item A variable reference or partial application of a function type.
470 When looking at the arguments of a user-defined function, we can
471 divide them into two categories:
473 \item Arguments with a runtime representable type (\eg bits or vectors).
475 These arguments can be preserved in the program, since they can
476 be translated to input ports later on. However, since we can
477 only connect signals to input ports, these arguments must be
478 reduced to simple variables (for which signals will be
479 produced). This is taken care of by the argument extraction
481 \item Non-runtime representable typed arguments.
483 These arguments cannot be preserved in the program, since we
484 cannot represent them as input or output ports in the resulting
485 VHDL. To remove them, we create a specialized version of the
486 called function with these arguments filled in. This is done by
487 the argument propagation transform.
490 When looking at the arguments of a builtin function, we can divide them
494 \item Arguments with a runtime representable type.
496 As we have seen with user-defined functions, these arguments can
497 always be reduced to a simple variable reference, by the
498 argument extraction transform. Performing this transform for
499 builtin functions as well, means that the translation of builtin
500 functions can be limited to signal references, instead of
501 needing to support all possible expressions.
503 \item Arguments with a function type.
505 These arguments are functions passed to higher order builtins,
506 like \lam{map} and \lam{foldl}. Since implementing these
507 functions for arbitrary function-typed expressions (\eg, lambda
508 expressions) is rather comlex, we reduce these arguments to
509 (partial applications of) global functions.
511 We can still support arbitrary expressions from the user code,
512 by creating a new global function containing that expression.
513 This way, we can simply replace the argument with a reference to
514 that new function. However, since the expression can contain any
515 number of free variables we also have to include partial
516 applications in our normal form.
518 This category of arguments is handled by the function extraction
520 \item Other unrepresentable arguments.
522 These arguments can take a few different forms:
523 \startdesc{Type arguments}
524 In the core language, type arguments can only take a single
525 form: A type wrapped in the Type constructor. Also, there is
526 nothing that can be done with type expressions, except for
527 applying functions to them, so we can simply leave type
528 arguments as they are.
530 \startdesc{Dictionary arguments}
531 In the core language, dictionary arguments are used to find
532 operations operating on one of the type arguments (mostly for
533 finding class methods). Since we will not actually evaluatie
534 the function body for builtin functions and can generate
535 code for builtin functions by just looking at the type
536 arguments, these arguments can be ignored and left as they
539 \startdesc{Type level arguments}
540 Sometimes, we want to pass a value to a builtin function, but
541 we need to know the value at compile time. Additionally, the
542 value has an impact on the type of the function. This is
543 encoded using type-level values, where the actual value of the
544 argument is not important, but the type encodes some integer,
545 for example. Since the value is not important, the actual form
546 of the expression does not matter either and we can leave
547 these arguments as they are.
549 \startdesc{Other arguments}
550 Technically, there is still a wide array of arguments that can
551 be passed, but does not fall into any of the above categories.
552 However, none of the supported builtin functions requires such
553 an argument. This leaves use with passing unsupported types to
554 a function, such as calling \lam{head} on a list of functions.
556 In these cases, it would be impossible to generate hardware
557 for such a function call anyway, so we can ignore these
560 The only way to generate hardware for builtin functions with
561 arguments like these, is to expand the function call into an
562 equivalent core expression (\eg, expand map into a series of
563 function applications). But for now, we choose to simply not
564 support expressions like these.
567 From the above, we can conclude that we can simply ignore these
568 other unrepresentable arguments and focus on the first two
572 \subsubsection{Argument extraction}
573 This transform deals with arguments to functions that
574 are of a runtime representable type.
576 TODO: It seems we can map an expression to a port, not only a signal.
577 Perhaps this makes this transformation not needed?
578 TODO: Say something about dataconstructors (without arguments, like True
579 or False), which are variable references of a runtime representable
580 type, but do not result in a signal.
582 To reduce a complex expression to a simple variable reference, we create
583 a new let expression around the application, which binds the complex
584 expression to a new variable. The original function is then applied to
587 %\transform{Argument extract}
589 %\lam{Y} is of a hardware representable type
591 %\lam{Y} is not a variable referene
595 %\trans{X Y}{let z = Y in X z}
598 \subsubsection{Function extraction}
599 This transform deals with function-typed arguments to builtin functions.
600 Since these arguments cannot be propagated, we choose to extract them
601 into a new global function instead.
603 Any free variables occuring in the extracted arguments will become
604 parameters to the new global function. The original argument is replaced
605 with a reference to the new function, applied to any free variables from
606 the original argument.
608 %\transform{Function extraction}
610 %\lam{X} is a (partial application of) a builtin function
612 %\lam{Y} is not an application
614 %\lam{Y} is not a variable reference
618 %\lam{f0 ... fm} = free local vars of \lam{Y}
620 %\lam{y} is a new global variable
622 %\lam{y = λf0 ... fn.Y}
624 %\trans{X Y}{X (y f0 ... fn)}
627 \subsubsection{Argument propagation}
628 This transform deals with arguments to user-defined functions that are
629 not representable at runtime. This means these arguments cannot be
630 preserved in the final form and most be {\em propagated}.
632 Propagation means to create a specialized version of the called
633 function, with the propagated argument already filled in. As a simple
634 example, in the following program:
641 we could {\em propagate} the constant argument 1, with the following
649 Special care must be taken when the to-be-propagated expression has any
650 free variables. If this is the case, the original argument should not be
651 removed alltogether, but replaced by all the free variables of the
652 expression. In this way, the original expression can still be evaluated
653 inside the new function. Also, this brings us closer to our goal: All
654 these free variables will be simple variable references.
656 To prevent us from propagating the same argument over and over, a simple
657 local variable reference is not propagated (since is has exactly one
658 free variable, itself, we would only replace that argument with itself).
660 This shows that any free local variables that are not runtime representable
661 cannot be brought into normal form by this transform. We rely on an
662 inlining transformation to replace such a variable with an expression we
665 TODO: Move these definitions somewhere sensible.
667 Definition: A global variable is any variable that is bound at the
668 top level of a program. A local variable is any other variable.
670 Definition: A hardware representable type is a type that we can generate
671 a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
672 unsigned word, etc. Types that are not runtime representable notably
673 include (but are not limited to): Types, dictionaries, functions.
675 Definition: A builtin function is a function for which a builtin
676 hardware translation is available, because its actual definition is not
677 translatable. A user-defined function is any other function.
682 x Y0 ... Yi ... Yn \lam{Yi} is not of a runtime representable type
683 --------------------------------------------- \lam{Yi} is not a local variable reference
684 x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . \lam{f0 ... fm} = free local vars of \lam{Y_i}
685 E y0 ... yi-1 Yi yi+1 ... yn
687 x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn
690 \subsection{Cast propagation / simplification}
691 This transform pushes casts down into the expression as far as possible.
693 \subsection{Return value simplification}
694 Currently implemented using lambda simplification, let simplification, and
695 top simplification. Should change.
697 \subsection{Example sequence}
699 This section lists an example expression, with a sequence of transforms
700 applied to it. The exact transforms given here probably don't exactly
701 match the transforms given above anymore, but perhaps this can clarify
702 the big picture a bit.
704 TODO: Update or remove this section.
722 After top-level η-abstraction:
741 After (extended) β-reduction:
759 After return value extraction:
778 Scrutinee simplification does not apply.
780 After case binder wildening:
785 a = case s of (a, _) -> a
786 b = case s of (_, b) -> b
787 r = case s of (_, _) ->
790 Low -> let op' = case b of
799 After case value simplification
804 a = case s of (a, _) -> a
805 b = case s of (_, b) -> b
806 r = case s of (_, _) -> r'
808 rl = let rll = λc.λd.c
821 After let flattening:
826 a = case s of (a, _) -> a
827 b = case s of (_, b) -> b
828 r = case s of (_, _) -> r'
842 After function inlining:
847 a = case s of (a, _) -> a
848 b = case s of (_, b) -> b
849 r = case s of (_, _) -> r'
861 After (extended) β-reduction again:
866 a = case s of (a, _) -> a
867 b = case s of (_, b) -> b
868 r = case s of (_, _) -> r'
880 After case value simplification again:
885 a = case s of (a, _) -> a
886 b = case s of (_, b) -> b
887 r = case s of (_, _) -> r'
905 a = case s of (a, _) -> a
906 b = case s of (_, b) -> b
920 After let bind removal:
925 a = case s of (a, _) -> a
926 b = case s of (_, b) -> b
939 Application simplification is not applicable.