2 \setuppapersize[A4][A4]
4 % Define a custom typescript. We could also have put the \definetypeface's
5 % directly in the script, without a typescript, but I guess this is more
7 \starttypescript[Custom]
8 % This is a sans font that supports greek symbols
9 \definetypeface [Custom] [ss] [sans] [iwona] [default]
10 \definetypeface [Custom] [rm] [serif] [antykwa-torunska] [default]
11 \definetypeface [Custom] [tt] [mono] [modern] [default]
12 \definetypeface [Custom] [mm] [math] [modern] [default]
14 \usetypescript [Custom]
16 % Use our custom typeface
17 \switchtotypeface [Custom] [10pt]
19 % The function application operator, which expands to a space in math mode
21 \define[2]\app{#1\;#2}
22 \define[2]\lam{λ#1 \xrightarrow #2}
23 \define[2]\letexpr{{\bold let}\;#1\;{\bold in}\;#2}
24 \define[2]\case{{\bold case}\;#1\;{\bold of}\;#2}
25 \define[2]\alt{#1 \xrightarrow #2}
26 \define[2]\bind{#1:#2}
27 \define[1]\where{{\bold where}\;#1}
29 \definefloat[transformation][transformations]
31 \startframedtext[width=\textwidth]
36 \define\conclusion{\blackrule[height=0.5pt,depth=0pt,width=.5\textwidth]}
37 \define\nextrule{\vskip1cm}
39 \define[2]\transformold{
40 %\placetransformation[here]{#1}
41 \startframedtext[width=\textwidth]
42 \startformula \startalign
44 \stopalign \stopformula
48 % A shortcut for italicized e.g. and i.e.
49 \define[0]\eg{{\em e.g.}}
50 \define[0]\ie{{\em i.e.}}
54 [location=hanging,hang=20,width=broad]
55 %command=\hskip-1cm,margin=1cm]
57 % Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
58 \installprettytype [LAM] [LAM]
60 \definetyping[lambda][option=LAM,style=sans]
61 \definetype[lam][option=LAM,style=sans]
63 \installprettytype [TRANS] [TRANS]
64 \definetyping[trans][option=TRANS,style=normal,before=,after=]
66 % An (invisible) frame to hold a lambda expression
68 % Put a frame around lambda expressions, so they can have multiple
69 % lines and still appear inline.
70 % The align=right option really does left-alignment, but without the
71 % program will end up on a single line. The strut=no option prevents a
72 % bunch of empty space at the start of the frame.
73 \framed[offset=0mm,location=middle,strut=no,align=right,frame=off]{#1}
77 % Make \typebuffer uses the LAM pretty printer and a sans-serif font
78 % Also prevent any extra spacing above and below caused by the default
79 % before=\blank and after=\blank.
80 \setuptyping[option=LAM,style=sans,before=,after=]
81 % Prevent the arrow from ending up below the first frame (a \framed
82 % at the start of a line defaults to using vmode).
84 % Put the elements in frames, so they can have multiple lines and be
86 \lamframe{\typebuffer[#1]}
87 \lamframe{\Rightarrow}
88 \lamframe{\typebuffer[#2]}
89 % Reset the typing settings to their defaults
90 \setuptyping[option=none,style=\tttf]
92 % This is the same as \transbuf above, but it accepts text directly instead
93 % of through buffers. This only works for single lines, however.
97 \lamframe{\Rightarrow}
102 % A helper to print a single example in the half the page width. The example
103 % text should be in a buffer whose name is given in an argument.
105 % The align=right option really does left-alignment, but without the program
106 % will end up on a single line. The strut=no option prevents a bunch of empty
107 % space at the start of the frame.
109 \framed[offset=1mm,align=right,strut=no]{
110 \setuptyping[option=LAM,style=sans,before=,after=]
112 \setuptyping[option=none,style=\tttf]
117 % A transformation example
118 \definefloat[example][examples]
119 \setupcaption[example][location=top] % Put captions on top
121 \define[3]\transexample{
122 \placeexample[here]{#1}
123 \startcombination[2*1]
124 {\example{#2}}{Original program}
125 {\example{#3}}{Transformed program}
129 \define[3]\transexampleh{
130 % \placeexample[here]{#1}
131 % \startcombination[1*2]
132 % {\example{#2}}{Original program}
133 % {\example{#3}}{Transformed program}
137 % Define a custom description format for the builtinexprs below
138 \definedescription[builtindesc][headstyle=bold,style=normal,location=top]
141 \title {Core transformations for hardware generation}
144 \section{Introduction}
145 As a new approach to translating Core to VHDL, we investigate a number of
146 transforms on our Core program, which should bring the program into a
147 well-defined {\em normal} form, which is subsequently trivial to
150 The transforms as presented here are far from complete, but are meant as
151 an exploration of possible transformations.
154 The transformations described here have a well-defined goal: To bring the
155 program in a well-defined form that is directly translatable to hardware,
156 while fully preserving the semantics of the program.
158 This {\em normal form} is again a Core program, but with a very specific
159 structure. A function in normal form has nested lambda's at the top, which
160 produce a let expression. This let expression binds every function application
161 in the function and produces a simple identifier. Every bound value in
162 the let expression is either a simple function application or a case
163 expression to extract a single element from a tuple returned by a
166 An example of a program in canonical form would be:
169 -- All arguments are an inital lambda
171 -- There is one let expression at the top level
173 -- Calling some other user-defined function.
175 -- Extracting result values from a tuple
176 a = case s of (a, b) -> a
177 b = case s of (a, b) -> b
178 -- Some builtin expressions
181 -- Conditional connections
193 When looking at such a program from a hardware perspective, the top level
194 lambda's define the input ports. The value produced by the let expression is
195 the output port. Most function applications bound by the let expression
196 define a component instantiation, where the input and output ports are mapped
197 to local signals or arguments. Some of the others use a builtin
198 construction (\eg the \lam{case} statement) or call a builtin function
199 (\eg \lam{add} or \lam{sub}). For these, a hardcoded VHDL translation is
202 \subsection{Normal definition}
203 Formally, the normal form is a core program obeying the following
204 constraints. TODO: Update this section, this is probably not completely
205 accurate or relevant anymore.
207 \startitemize[R,inmargin]
208 \item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
209 $fun$ is an identifier that will be bound as a global identifier.
210 \item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
211 $\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
212 \item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
213 \item $letbinds$ is a list with elements of the form
214 $\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
215 an identifier that will be bound as local identifier. The type of the bound
216 value must be a $hardware\;type$.
217 \item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
218 equivalent VHDL expression. Since there are many supported forms for this,
219 these are defined in a separate table.
220 \item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
221 where $fun$ is a global identifier and $x$ is a local identifier.
222 \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
223 be of a $hardware\;type$.
224 \item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
225 where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
227 \item A $hardware\;type$ is a type that can be directly translated to
228 hardware. This includes the types $Bit$, $SizedWord$, tuples containing
229 elements of $hardware\;type$s, and will include others. This explicitely
230 excludes function types.
233 TODO: Say something about uniqueness of identifiers
235 \subsection{Builtin expressions}
236 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
238 \startitemize[m,inmargin]
240 $tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
241 where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
242 e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
243 be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
244 \item TODO: Many more!
247 \section{Transform passes}
249 In this section we describe the actual transforms. Here we're using
250 the core language in a notation that resembles lambda calculus.
252 Each of these transforms is meant to be applied to every (sub)expression
253 in a program, for as long as it applies. Only when none of the
254 expressions can be applied anymore, the program is in normal form. We
255 hope to be able to prove that this form will obey all of the constraints
256 defined above, but this has yet to happen (though it seems likely that
259 Each of the transforms will be described informally first, explaining
260 the need for and goal of the transform. Then, a formal definition is
261 given, using a familiar syntax from the world of logic. Each transform
262 is specified as a number of conditions (above the horizontal line) and a
263 number of conclusions (below the horizontal line). The details of using
264 this notation are still a bit fuzzy, so comments are welcom.
266 TODO: Formally describe the "apply to every (sub)expression" in terms of
267 rules with full transformations in the conditions.
269 \subsection{η-abstraction}
270 This transformation makes sure that all arguments of a function-typed
271 expression are named, by introducing lambda expressions. When combined with
272 β-reduction and function inlining below, all function-typed expressions should
273 be lambda abstractions or global identifiers.
277 -------------- \lam{E} is not the first argument of an application.
278 λx.E x \lam{E} is not a lambda abstraction.
279 \lam{x} is a variable that does not occur free in \lam{E}.
283 foo = λa -> case a of
289 foo = λa.λx -> (case a of
294 \transexample{η-abstraction}{from}{to}
296 \subsection{Extended β-reduction}
297 This transformation is meant to propagate application expressions downwards
298 into expressions as far as possible. In lambda calculus, this reduction
299 is known as β-reduction, but it is of course only defined for
300 applications of lambda abstractions. We extend this reduction to also
301 work for the rest of core (case and let expressions).
315 \transform{Extended β-reduction}
318 \trans{(λx.E) M}{E[M/x]}
322 \trans{(let binds in E) M}{let binds in E M}
334 b = (let y = 3 in add y) 2
343 b = let y = 3 in add y 2
348 \transexample{Extended β-reduction}{from}{to}
350 \subsection{Argument simplification}
351 The transforms in this section deal with simplifying application
352 arguments into normal form. The goal here is to:
355 \item Make all arguments of user-defined functions (\eg, of which
356 we have a function body) simple variable references of a runtime
358 \item Make all arguments of builtin functions either:
360 \item A type argument.
361 \item A dictionary argument.
362 \item A type level expression.
363 \item A variable reference of a runtime representable type.
364 \item A variable reference or partial application of a function type.
368 When looking at the arguments of a user-defined function, we can
369 divide them into two categories:
371 \item Arguments with a runtime representable type (\eg bits or vectors).
373 These arguments can be preserved in the program, since they can
374 be translated to input ports later on. However, since we can
375 only connect signals to input ports, these arguments must be
376 reduced to simple variables (for which signals will be
377 produced). This is taken care of by the argument extraction
379 \item Non-runtime representable typed arguments.
381 These arguments cannot be preserved in the program, since we
382 cannot represent them as input or output ports in the resulting
383 VHDL. To remove them, we create a specialized version of the
384 called function with these arguments filled in. This is done by
385 the argument propagation transform.
388 When looking at the arguments of a builtin function, we can divide them
392 \item Arguments with a runtime representable type.
394 As we have seen with user-defined functions, these arguments can
395 always be reduced to a simple variable reference, by the
396 argument extraction transform. Performing this transform for
397 builtin functions as well, means that the translation of builtin
398 functions can be limited to signal references, instead of
399 needing to support all possible expressions.
401 \item Arguments with a function type.
403 These arguments are functions passed to higher order builtins,
404 like \lam{map} and \lam{foldl}. Since implementing these
405 functions for arbitrary function-typed expressions (\eg, lambda
406 expressions) is rather comlex, we reduce these arguments to
407 (partial applications of) global functions.
409 We can still support arbitrary expressions from the user code,
410 by creating a new global function containing that expression.
411 This way, we can simply replace the argument with a reference to
412 that new function. However, since the expression can contain any
413 number of free variables we also have to include partial
414 applications in our normal form.
416 This category of arguments is handled by the function extraction
418 \item Other unrepresentable arguments.
420 These arguments can take a few different forms:
421 \startdesc{Type arguments}
422 In the core language, type arguments can only take a single
423 form: A type wrapped in the Type constructor. Also, there is
424 nothing that can be done with type expressions, except for
425 applying functions to them, so we can simply leave type
426 arguments as they are.
428 \startdesc{Dictionary arguments}
429 In the core language, dictionary arguments are used to find
430 operations operating on one of the type arguments (mostly for
431 finding class methods). Since we will not actually evaluatie
432 the function body for builtin functions and can generate
433 code for builtin functions by just looking at the type
434 arguments, these arguments can be ignored and left as they
437 \startdesc{Type level arguments}
438 Sometimes, we want to pass a value to a builtin function, but
439 we need to know the value at compile time. Additionally, the
440 value has an impact on the type of the function. This is
441 encoded using type-level values, where the actual value of the
442 argument is not important, but the type encodes some integer,
443 for example. Since the value is not important, the actual form
444 of the expression does not matter either and we can leave
445 these arguments as they are.
447 \startdesc{Other arguments}
448 Technically, there is still a wide array of arguments that can
449 be passed, but does not fall into any of the above categories.
450 However, none of the supported builtin functions requires such
451 an argument. This leaves use with passing unsupported types to
452 a function, such as calling \lam{head} on a list of functions.
454 In these cases, it would be impossible to generate hardware
455 for such a function call anyway, so we can ignore these
458 The only way to generate hardware for builtin functions with
459 arguments like these, is to expand the function call into an
460 equivalent core expression (\eg, expand map into a series of
461 function applications). But for now, we choose to simply not
462 support expressions like these.
465 From the above, we can conclude that we can simply ignore these
466 other unrepresentable arguments and focus on the first two
470 \subsubsection{Argument extraction}
471 This transform deals with arguments to functions that
472 are of a runtime representable type.
474 TODO: It seems we can map an expression to a port, not only a signal.
475 Perhaps this makes this transformation not needed?
476 TODO: Say something about dataconstructors (without arguments, like True
477 or False), which are variable references of a runtime representable
478 type, but do not result in a signal.
480 To reduce a complex expression to a simple variable reference, we create
481 a new let expression around the application, which binds the complex
482 expression to a new variable. The original function is then applied to
485 \transform{Argument extract}
487 \lam{Y} is of a hardware representable type
489 \lam{Y} is not a variable referene
493 \trans{X Y}{let z = Y in X z}
496 \subsubsection{Function extraction}
497 This transform deals with function-typed arguments to builtin functions.
498 Since these arguments cannot be propagated, we choose to extract them
499 into a new global function instead.
501 Any free variables occuring in the extracted arguments will become
502 parameters to the new global function. The original argument is replaced
503 with a reference to the new function, applied to any free variables from
504 the original argument.
506 \transform{Function extraction}
508 \lam{X} is a (partial application of) a builtin function
510 \lam{Y} is not an application
512 \lam{Y} is not a variable reference
516 \lam{f0 ... fm} = free local vars of \lam{Y}
518 \lam{y} is a new global variable
520 \lam{y = λf0 ... fn.Y}
522 \trans{X Y}{X (y f0 ... fn)}
525 \subsubsection{Argument propagation}
526 This transform deals with arguments to user-defined functions that are
527 not representable at runtime. This means these arguments cannot be
528 preserved in the final form and most be {\em propagated}.
530 Propagation means to create a specialized version of the called
531 function, with the propagated argument already filled in. As a simple
532 example, in the following program:
539 we could {\em propagate} the constant argument 1, with the following
547 Special care must be taken when the to-be-propagated expression has any
548 free variables. If this is the case, the original argument should not be
549 removed alltogether, but replaced by all the free variables of the
550 expression. In this way, the original expression can still be evaluated
551 inside the new function. Also, this brings us closer to our goal: All
552 these free variables will be simple variable references.
554 To prevent us from propagating the same argument over and over, a simple
555 local variable reference is not propagated (since is has exactly one
556 free variable, itself, we would only replace that argument with itself).
558 This shows that any free local variables that are not runtime representable
559 cannot be brought into normal form by this transform. We rely on an
560 inlining transformation to replace such a variable with an expression we
563 TODO: Move these definitions somewhere sensible.
565 Definition: A global variable is any variable that is bound at the
566 top level of a program. A local variable is any other variable.
568 Definition: A hardware representable type is a type that we can generate
569 a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
570 unsigned word, etc. Types that are not runtime representable notably
571 include (but are not limited to): Types, dictionaries, functions.
573 Definition: A builtin function is a function for which a builtin
574 hardware translation is available, because its actual definition is not
575 translatable. A user-defined function is any other function.
580 x Y0 ... Yi ... Yn \lam{Y_i} is not of a runtime representable type
581 --------------------------------------------- \lam{Y_i} is not a local variable reference
582 x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . \lam{f0 ... fm} = free local vars of \lam{Y_i}
583 E y0 ... yi-1 Yi yi+1 ... yn
585 x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn
588 \transform{Argument propagation}
590 \lam{x} is a global variable, bound to a user-defined function
594 \lam{Y_i} is not of a runtime representable type
596 \lam{Y_i} is not a local variable reference
600 \lam{f0 ... fm} = free local vars of \lam{Y_i}
602 \lam{x'} is a new global variable
604 \lam{x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . E y0 ... yi-1 Yi yi+1 ... yn}
606 \trans{x Y0 ... Yi ... Yn}{x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn}
609 TODO: The above definition looks too complicated... Can we find
610 something more concise?
612 \subsection{Cast propagation}
613 This transform pushes casts down into the expression as far as possible.
614 \subsection{Let recursification}
615 This transform makes all lets recursive.
616 \subsection{Let simplification}
617 This transform makes the result value of all let expressions a simple
619 \subsection{Let flattening}
620 This transform turns two nested lets (\lam{let x = (let ... in ...) in
621 ...}) into a single let.
622 \subsection{Simple let binding removal}
623 This transforms inlines simple let bindings (\eg a = b).
624 \subsection{Function inlining}
625 This transform inlines let bindings of a funtion type. TODO: This should
626 be generelized to anything that is non representable at runtime, or
628 \subsection{Scrutinee simplification}
629 This transform ensures that the scrutinee of a case expression is always
630 a simple variable reference.
631 \subsection{Case binder wildening}
632 This transform replaces all binders of a each case alternative with a
633 wild binder (\ie, one that is never referred to). This will possibly
634 introduce a number of new "selector" case statements, that only select
635 one element from an algebraic datatype and bind it to a variable.
636 \subsection{Case value simplification}
637 This transform simplifies the result value of each case alternative by
638 binding the value in a let expression and replacing the value by a
639 simple variable reference.
640 \subsection{Case removal}
641 This transform removes any case statements with a single alternative and
644 \subsection{Example sequence}
646 This section lists an example expression, with a sequence of transforms
647 applied to it. The exact transforms given here probably don't exactly
648 match the transforms given above anymore, but perhaps this can clarify
649 the big picture a bit.
651 TODO: Update or remove this section.
669 After top-level η-abstraction:
688 After (extended) β-reduction:
706 After return value extraction:
725 Scrutinee simplification does not apply.
727 After case binder wildening:
732 a = case s of (a, _) -> a
733 b = case s of (_, b) -> b
734 r = case s of (_, _) ->
737 Low -> let op' = case b of
746 After case value simplification
751 a = case s of (a, _) -> a
752 b = case s of (_, b) -> b
753 r = case s of (_, _) -> r'
755 rl = let rll = λc.λd.c
768 After let flattening:
773 a = case s of (a, _) -> a
774 b = case s of (_, b) -> b
775 r = case s of (_, _) -> r'
789 After function inlining:
794 a = case s of (a, _) -> a
795 b = case s of (_, b) -> b
796 r = case s of (_, _) -> r'
808 After (extended) β-reduction again:
813 a = case s of (a, _) -> a
814 b = case s of (_, b) -> b
815 r = case s of (_, _) -> r'
827 After case value simplification again:
832 a = case s of (a, _) -> a
833 b = case s of (_, b) -> b
834 r = case s of (_, _) -> r'
852 a = case s of (a, _) -> a
853 b = case s of (_, b) -> b
867 After let bind removal:
872 a = case s of (a, _) -> a
873 b = case s of (_, b) -> b
886 Application simplification is not applicable.