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 number of nested let expressions. These let expressions binds a
56 number of simple expressions in the function and produces a simple identifier.
57 Every bound value in the let expression is either a simple function
58 application, a case expression to extract a single element from a tuple
59 returned by a function or a case expression to choose between two signals
60 based on some other signal.
62 This structure is easy to translate to VHDL, since each top level lambda will
63 be an input port, every bound value will become a concurrent statement (such
64 as a component instantiation or conditional signal assignment) and the result
65 variable will become the output port.
67 An example of a program in canonical form would be:
70 -- All arguments are an inital lambda
72 -- There are nested let expressions at top level
74 -- Unpack the state by coercion
75 s = sp :: (Word, Word)
76 -- Extract both registers from the state
77 r1 = case s of (fst, snd) -> fst
78 r2 = case s of (fst, snd) -> snd
79 -- Calling some other user-defined function.
81 -- Conditional connections
93 -- Packing the state by coercion
94 sp' = s' :: State (Word, Word)
95 -- Pack our return value
102 \subsection{Definitions}
103 In the following sections, we will be using a number of functions and
104 notations, which we will define here.
106 \subsubsection{Transformations}
107 The most important notation is the one for transformation, which looks like
114 ------------------------ expression conditions
120 Here, we describe a transformation. The most import parts are \lam{from} and
121 \lam{to}, which describe the Core expresssion that should be matched and the
122 expression that it should be replaced with. This matching can occur anywhere
123 in function that is being normalized, so it applies to any subexpression as
126 The \lam{expression conditions} list a number of conditions on the \lam{from}
127 expression that must hold for the transformation to apply.
129 Furthermore, there is some way to look into the environment (\eg, other top
130 level bindings). The \lam{context conditions} part specifies any number of
131 top level bindings that must be present for the transformation to apply.
132 Usually, this lists a top level binding that binds an identfier that is also
133 used in the \lam{from} expression, allowing us to "access" the value of a top
134 level binding in the \lam{to} expression (\eg, for inlining).
136 Finally, there is a way to influence the environment. The \lam{context
137 additions} part lists any number of new top level bindings that should be
140 If there are no \lam{context conditions} or \lam{context additions}, they can
141 be left out alltogether, along with the separator \lam{~}.
145 \subsubsection{Other concepts}
146 A \emph{global variable} is any variable that is bound at the
147 top level of a program, or an external module. A local variable is any other
148 variable (\eg, variables local to a function, which can be bound by lambda
149 abstractions, let expressions and case expressions).
151 A \emph{hardware representable} type is a type that we can generate
152 a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
153 unsigned word, etc. Types that are not runtime representable notably
154 include (but are not limited to): Types, dictionaries, functions.
156 A \emph{builtin function} is a function for which a builtin
157 hardware translation is available, because its actual definition is not
158 translatable. A user-defined function is any other function.
160 \subsubsection{Functions}
161 Here, we define a number of functions that can be used below to concisely
164 \emph{gvar(expr)} is true when \emph{expr} is a variable that references a
165 global variable. It is false when it references a local variable.
167 \emph{lvar(expr)} is the inverse of \emph{gvar}; it is true when \emph{expr}
168 references a local variable, false when it references a global variable.
170 \emph{representable(expr)} or \emph{representable(var)} is true when
171 \emph{expr} or \emph{var} has a type that is representable at runtime.
173 \subsection{Normal form definition}
174 We can describe this normal form in a slightly more formal manner. The
175 following EBNF-like description completely captures the intended structure
176 (and generates a subset of GHC's core format).
178 Some clauses have an expression listed in parentheses. These are conditions
179 that need to apply to the clause.
182 \italic{normal} = \italic{lambda}
183 \italic{lambda} = λvar.\italic{lambda} (representable(var))
185 \italic{toplet} = let \italic{binding} in \italic{toplet}
186 | letrec [\italic{binding}] in \italic{toplet}
187 | var (representable(varvar))
188 \italic{binding} = var = \italic{rhs} (representable(rhs))
189 -- State packing and unpacking by coercion
190 | var0 = var1 :: State ty (lvar(var1))
191 | var0 = var1 :: ty (var0 :: State ty) (lvar(var1))
192 \italic{rhs} = userapp
195 | case var of C a0 ... an -> ai (lvar(var))
197 | case var of (lvar(var))
198 DEFAULT -> var0 (lvar(var0))
199 C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, lvar(resvar))
200 \italic{userapp} = \italic{userfunc}
201 | \italic{userapp} {userarg}
202 \italic{userfunc} = var (gvar(var))
203 \italic{userarg} = var (lvar(var))
204 \italic{builtinapp} = \italic{builtinfunc}
205 | \italic{builtinapp} \italic{builtinarg}
206 \italic{builtinfunc} = var (bvar(var))
207 \italic{builtinarg} = \italic{coreexpr}
210 -- TODO: Limit builtinarg further
212 -- TODO: There can still be other casts around (which the code can handle,
213 e.g., ignore), which still need to be documented here.
215 -- TODO: Note about the selector case. It just supports Bit and Bool
216 currently, perhaps it should be generalized in the normal form?
218 When looking at such a program from a hardware perspective, the top level
219 lambda's define the input ports. The value produced by the let expression is
220 the output port. Most function applications bound by the let expression
221 define a component instantiation, where the input and output ports are mapped
222 to local signals or arguments. Some of the others use a builtin
223 construction (\eg the \lam{case} statement) or call a builtin function
224 (\eg \lam{add} or \lam{sub}). For these, a hardcoded VHDL translation is
227 \section{Transform passes}
228 In this section we describe the actual transforms. Here we're using
229 the core language in a notation that resembles lambda calculus.
231 Each of these transforms is meant to be applied to every (sub)expression
232 in a program, for as long as it applies. Only when none of the
233 expressions can be applied anymore, the program is in normal form. We
234 hope to be able to prove that this form will obey all of the constraints
235 defined above, but this has yet to happen (though it seems likely that
238 Each of the transforms will be described informally first, explaining
239 the need for and goal of the transform. Then, a formal definition is
240 given, using a familiar syntax from the world of logic. Each transform
241 is specified as a number of conditions (above the horizontal line) and a
242 number of conclusions (below the horizontal line). The details of using
243 this notation are still a bit fuzzy, so comments are welcom.
245 TODO: Formally describe the "apply to every (sub)expression" in terms of
246 rules with full transformations in the conditions.
248 \subsection{η-abstraction}
249 This transformation makes sure that all arguments of a function-typed
250 expression are named, by introducing lambda expressions. When combined with
251 β-reduction and function inlining below, all function-typed expressions should
252 be lambda abstractions or global identifiers.
256 -------------- \lam{E} is not the first argument of an application.
257 λx.E x \lam{E} is not a lambda abstraction.
258 \lam{x} is a variable that does not occur free in \lam{E}.
268 foo = λa.λx.(case a of
273 \transexample{η-abstraction}{from}{to}
275 \subsection{Extended β-reduction}
276 This transformation is meant to propagate application expressions downwards
277 into expressions as far as possible. In lambda calculus, this reduction
278 is known as β-reduction, but it is of course only defined for
279 applications of lambda abstractions. We extend this reduction to also
280 work for the rest of core (case and let expressions).
302 For lambda expressions:
315 b = (let y = 3 in add y) 2
325 b = let y = 3 in add y 2
330 \transexample{Extended β-reduction}{from}{to}
332 \subsection{Let derecursification}
333 This transformation is meant to make lets non-recursive whenever possible.
334 This might allow other optimizations to do their work better. TODO: Why is
337 \subsection{Let flattening}
338 This transformation puts nested lets in the same scope, by lifting the
339 binding(s) of the inner let into a new let around the outer let. Eventually,
340 this will cause all let bindings to appear in the same scope (they will all be
341 in scope for the function return value).
343 Note that this transformation does not try to be smart when faced with
344 recursive lets, it will just leave the lets recursive (possibly joining a
345 recursive and non-recursive let into a single recursive let). The let
346 rederursification transformation will do this instead.
349 letnonrec x = (let bindings in M) in N
350 ------------------------------------------
351 let bindings in (letnonrec x = M) in N
357 x = (let bindings in M)
361 ------------------------------------------
380 b = let c = 3 in a + c
401 \transexample{Let flattening}{from}{to}
403 \subsection{Empty let removal}
404 This transformation is simple: It removes recursive lets that have no bindings
405 (which usually occurs when let derecursification removes the last binding from
414 \subsection{Simple let binding removal}
415 This transformation inlines simple let bindings (\eg a = b).
417 This transformation is not needed to get into normal form, but makes the
418 resulting VHDL a lot shorter.
444 \subsection{Unused let binding removal}
445 This transformation removes let bindings that are never used. Usually,
446 the desugarer introduces some unused let bindings.
448 This normalization pass should really be unneeded to get into normal form
449 (since ununsed bindings are not forbidden by the normal form), but in practice
450 the desugarer or simplifier emits some unused bindings that cannot be
451 normalized (e.g., calls to a \type{PatError} (TODO: Check this name)). Also,
452 this transformation makes the resulting VHDL a lot shorter.
456 ---------------------------- \lam{a} does not occur free in \lam{M}
467 ---------------------------- \lam{a} does not occur free in \lam{M}
475 \subsection{Non-representable binding inlining}
476 This transform inlines let bindings that have a non-representable type. Since
477 we can never generate a signal assignment for these bindings (we cannot
478 declare a signal assignment with a non-representable type, for obvious
479 reasons), we have no choice but to inline the binding to remove it.
481 If the binding is non-representable because it is a lambda abstraction, it is
482 likely that it will inlined into an application and β-reduction will remove
483 the lambda abstraction and turn it into a representable expression at the
484 inline site. The same holds for partial applications, which can be turned into
485 full applications by inlining.
487 Other cases of non-representable bindings we see in practice are primitive
488 Haskell types. In most cases, these will not result in a valid normalized
489 output, but then the input would have been invalid to start with. There is one
490 exception to this: When a builtin function is applied to a non-representable
491 expression, things might work out in some cases. For example, when you write a
492 literal \hs{SizedInt} in Haskell, like \hs{1 :: SizedInt D8}, this results in
493 the following core: \lam{fromInteger (smallInteger 10)}, where for example
494 \lam{10 :: GHC.Prim.Int\#} and \lam{smallInteger 10 :: Integer} have
495 non-representable types. TODO: This/these paragraph(s) should probably become a
496 separate discussion somewhere else.
500 -------------------------- \lam{E} has a non-representable type.
511 -------------------------- \lam{E} has a non-representable type.
531 x = fromInteger (smallInteger 10)
533 (λa -> add a 1) (add 1 x)
536 \transexample{Let flattening}{from}{to}
538 \subsection{Compiler generated top level binding inlining}
541 \subsection{Scrutinee simplification}
542 This transform ensures that the scrutinee of a case expression is always
543 a simple variable reference.
548 ----------------- \lam{E} is not a local variable reference
567 \transexample{Let flattening}{from}{to}
570 \subsection{Case simplification}
571 This transformation ensures that all case expressions become normal form. This
572 means they will become one of:
574 \item An extractor case with a single alternative that picks a single field
575 from a datatype, \eg \lam{case x of (a, b) -> a}.
576 \item A selector case with multiple alternatives and only wild binders, that
577 makes a choice between expressions based on the constructor of another
578 expression, \eg \lam{case x of Low -> a; High -> b}.
583 C0 v0,0 ... v0,m -> E0
585 Cn vn,0 ... vn,m -> En
586 --------------------------------------------------- \forall i \forall j, 0 <= i <= n, 0 <= i < m (\lam{wi,j} is a wild (unused) binder)
588 v0,0 = case x of C0 v0,0 .. v0,m -> v0,0
590 v0,m = case x of C0 v0,0 .. v0,m -> v0,m
593 vn,m = case x of Cn vn,0 .. vn,m -> vn,m
597 C0 w0,0 ... w0,m -> x0
599 Cn wn,0 ... wn,m -> xn
602 TODO: This transformation specified like this is complicated and misses
603 conditions to prevent looping with itself. Perhaps we should split it here for
622 \transexample{Selector case simplification}{from}{to}
630 b = case a of (,) b c -> b
631 c = case a of (,) b c -> c
638 \transexample{Extractor case simplification}{from}{to}
640 \subsection{Case removal}
641 This transform removes any case statements with a single alternative and
644 These "useless" case statements are usually leftovers from case simplification
645 on extractor case (see the previous example).
650 ---------------------- \lam{\forall i, 0 <= i <= m} (\lam{vi} does not occur free in E)
663 \transexample{Case removal}{from}{to}
665 \subsection{Argument simplification}
666 The transforms in this section deal with simplifying application
667 arguments into normal form. The goal here is to:
670 \item Make all arguments of user-defined functions (\eg, of which
671 we have a function body) simple variable references of a runtime
672 representable type. This is needed, since these applications will be turned
673 into component instantiations.
674 \item Make all arguments of builtin functions one of:
676 \item A type argument.
677 \item A dictionary argument.
678 \item A type level expression.
679 \item A variable reference of a runtime representable type.
680 \item A variable reference or partial application of a function type.
684 When looking at the arguments of a user-defined function, we can
685 divide them into two categories:
687 \item Arguments with a runtime representable type (\eg bits or vectors).
689 These arguments can be preserved in the program, since they can
690 be translated to input ports later on. However, since we can
691 only connect signals to input ports, these arguments must be
692 reduced to simple variables (for which signals will be
693 produced). This is taken care of by the argument extraction
695 \item Non-runtime representable typed arguments.
697 These arguments cannot be preserved in the program, since we
698 cannot represent them as input or output ports in the resulting
699 VHDL. To remove them, we create a specialized version of the
700 called function with these arguments filled in. This is done by
701 the argument propagation transform.
703 Typically, these arguments are type and dictionary arguments that are
704 used to make functions polymorphic. By propagating these arguments, we
705 are essentially doing the same which GHC does when it specializes
706 functions: Creating multiple variants of the same function, one for
707 each type for which it is used. Other common non-representable
708 arguments are functions, e.g. when calling a higher order function
709 with another function or a lambda abstraction as an argument.
711 The reason for doing this is similar to the reasoning provided for
712 the inlining of non-representable let bindings above. In fact, this
713 argument propagation could be viewed as a form of cross-function
717 TODO: Check the following itemization.
719 When looking at the arguments of a builtin function, we can divide them
723 \item Arguments with a runtime representable type.
725 As we have seen with user-defined functions, these arguments can
726 always be reduced to a simple variable reference, by the
727 argument extraction transform. Performing this transform for
728 builtin functions as well, means that the translation of builtin
729 functions can be limited to signal references, instead of
730 needing to support all possible expressions.
732 \item Arguments with a function type.
734 These arguments are functions passed to higher order builtins,
735 like \lam{map} and \lam{foldl}. Since implementing these
736 functions for arbitrary function-typed expressions (\eg, lambda
737 expressions) is rather comlex, we reduce these arguments to
738 (partial applications of) global functions.
740 We can still support arbitrary expressions from the user code,
741 by creating a new global function containing that expression.
742 This way, we can simply replace the argument with a reference to
743 that new function. However, since the expression can contain any
744 number of free variables we also have to include partial
745 applications in our normal form.
747 This category of arguments is handled by the function extraction
749 \item Other unrepresentable arguments.
751 These arguments can take a few different forms:
752 \startdesc{Type arguments}
753 In the core language, type arguments can only take a single
754 form: A type wrapped in the Type constructor. Also, there is
755 nothing that can be done with type expressions, except for
756 applying functions to them, so we can simply leave type
757 arguments as they are.
759 \startdesc{Dictionary arguments}
760 In the core language, dictionary arguments are used to find
761 operations operating on one of the type arguments (mostly for
762 finding class methods). Since we will not actually evaluatie
763 the function body for builtin functions and can generate
764 code for builtin functions by just looking at the type
765 arguments, these arguments can be ignored and left as they
768 \startdesc{Type level arguments}
769 Sometimes, we want to pass a value to a builtin function, but
770 we need to know the value at compile time. Additionally, the
771 value has an impact on the type of the function. This is
772 encoded using type-level values, where the actual value of the
773 argument is not important, but the type encodes some integer,
774 for example. Since the value is not important, the actual form
775 of the expression does not matter either and we can leave
776 these arguments as they are.
778 \startdesc{Other arguments}
779 Technically, there is still a wide array of arguments that can
780 be passed, but does not fall into any of the above categories.
781 However, none of the supported builtin functions requires such
782 an argument. This leaves use with passing unsupported types to
783 a function, such as calling \lam{head} on a list of functions.
785 In these cases, it would be impossible to generate hardware
786 for such a function call anyway, so we can ignore these
789 The only way to generate hardware for builtin functions with
790 arguments like these, is to expand the function call into an
791 equivalent core expression (\eg, expand map into a series of
792 function applications). But for now, we choose to simply not
793 support expressions like these.
796 From the above, we can conclude that we can simply ignore these
797 other unrepresentable arguments and focus on the first two
801 \subsubsection{Argument simplification}
802 This transform deals with arguments to functions that
803 are of a runtime representable type. It ensures that they will all become
804 references to global variables, or local signals in the resulting VHDL.
806 TODO: It seems we can map an expression to a port, not only a signal.
807 Perhaps this makes this transformation not needed?
808 TODO: Say something about dataconstructors (without arguments, like True
809 or False), which are variable references of a runtime representable
810 type, but do not result in a signal.
812 To reduce a complex expression to a simple variable reference, we create
813 a new let expression around the application, which binds the complex
814 expression to a new variable. The original function is then applied to
819 -------------------- \lam{N} is of a representable type
820 let x = N in M x \lam{N} is not a local variable reference
828 let x = add a 1 in add x 1
831 \transexample{Argument extraction}{from}{to}
833 \subsubsection{Function extraction}
834 This transform deals with function-typed arguments to builtin functions.
835 Since these arguments cannot be propagated, we choose to extract them
836 into a new global function instead.
838 Any free variables occuring in the extracted arguments will become
839 parameters to the new global function. The original argument is replaced
840 with a reference to the new function, applied to any free variables from
841 the original argument.
843 This transformation is useful when applying higher order builtin functions
844 like \hs{map} to a lambda abstraction, for example. In this case, the code
845 that generates VHDL for \hs{map} only needs to handle top level functions and
846 partial applications, not any other expression (such as lambda abstractions or
847 even more complicated expressions).
850 M N \lam{M} is a (partial aplication of a) builtin function.
851 --------------------- \lam{f0 ... fn} = free local variables of \lam{N}
852 M x f0 ... fn \lam{N :: a -> b}
853 ~ \lam{N} is not a (partial application of) a top level function
858 map (λa . add a b) xs
872 \transexample{Function extraction}{from}{to}
874 \subsubsection{Argument propagation}
875 This transform deals with arguments to user-defined functions that are
876 not representable at runtime. This means these arguments cannot be
877 preserved in the final form and most be {\em propagated}.
879 Propagation means to create a specialized version of the called
880 function, with the propagated argument already filled in. As a simple
881 example, in the following program:
888 we could {\em propagate} the constant argument 1, with the following
896 Special care must be taken when the to-be-propagated expression has any
897 free variables. If this is the case, the original argument should not be
898 removed alltogether, but replaced by all the free variables of the
899 expression. In this way, the original expression can still be evaluated
900 inside the new function. Also, this brings us closer to our goal: All
901 these free variables will be simple variable references.
903 To prevent us from propagating the same argument over and over, a simple
904 local variable reference is not propagated (since is has exactly one
905 free variable, itself, we would only replace that argument with itself).
907 This shows that any free local variables that are not runtime representable
908 cannot be brought into normal form by this transform. We rely on an
909 inlining transformation to replace such a variable with an expression we
915 x Y0 ... Yi ... Yn \lam{Yi} is not of a runtime representable type
916 --------------------------------------------- \lam{Yi} is not a local variable reference
917 x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn \lam{f0 ... fm} = free local vars of \lam{Yi}
919 x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .
920 E y0 ... yi-1 Yi yi+1 ... yn
926 \subsection{Cast propagation / simplification}
927 This transform pushes casts down into the expression as far as possible. Since
928 its exact role and need is not clear yet, this transformation is not yet
931 \subsection{Return value simplification}
932 This transformation ensures that the return value of a function is always a
933 simple local variable reference.
935 Currently implemented using lambda simplification, let simplification, and
936 top simplification. Should change into something like the following, which
937 works only on the result of a function instead of any subexpression. This is
938 achieved by the contexts, like \lam{x = E}, though this is strictly not
939 correct (you could read this as "if there is any function \lam{x} that binds
940 \lam{E}, any \lam{E} can be transformed, while we only mean the \lam{E} that
941 is bound by \lam{x}. This might need some extra notes or something).
944 x = E \lam{E} is representable
945 ~ \lam{E} is not a lambda abstraction
946 E \lam{E} is not a let expression
947 --------------------------- \lam{E} is not a local variable reference
953 ~ \lam{E} is representable
954 E \lam{E} is not a let expression
955 --------------------------- \lam{E} is not a local variable reference
960 x = λv0 ... λvn.let ... in E
961 ~ \lam{E} is representable
962 E \lam{E} is not a local variable reference
963 ---------------------------
972 x = let x = add 1 2 in x
975 \transexample{Return value simplification}{from}{to}