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.
49 \define[0]\eg{{\em e.g.}}
51 % Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
52 \installprettytype [LAM] [LAM]
54 \definetyping[lambda][option=LAM,style=sans]
55 \definetype[lam][option=LAM,style=sans]
57 % An (invisible) frame to hold a lambda expression
59 % Put a frame around lambda expressions, so they can have multiple
60 % lines and still appear inline.
61 % The align=right option really does left-alignment, but without the
62 % program will end up on a single line. The strut=no option prevents a
63 % bunch of empty space at the start of the frame.
64 \framed[offset=0mm,location=middle,strut=no,align=right,frame=off]{#1}
68 % Make \typebuffer uses the LAM pretty printer and a sans-serif font
69 % Also prevent any extra spacing above and below caused by the default
70 % before=\blank and after=\blank.
71 \setuptyping[option=LAM,style=sans,before=,after=]
72 % Prevent the arrow from ending up below the first frame (a \framed
73 % at the start of a line defaults to using vmode).
75 % Put the elements in frames, so they can have multiple lines and be
77 \lamframe{\typebuffer[#1]}
78 \lamframe{\Rightarrow}
79 \lamframe{\typebuffer[#2]}
80 % Reset the typing settings to their defaults
81 \setuptyping[option=none,style=\tttf]
83 % This is the same as \transbuf above, but it accepts text directly instead
84 % of through buffers. This only works for single lines, however.
88 \lamframe{\Rightarrow}
93 % A helper to print a single example in the half the page width. The example
94 % text should be in a buffer whose name is given in an argument.
96 % The align=right option really does left-alignment, but without the program
97 % will end up on a single line. The strut=no option prevents a bunch of empty
98 % space at the start of the frame.
100 \framed[offset=1mm,align=right,strut=no]{
101 \setuptyping[option=LAM,style=sans,before=,after=]
103 \setuptyping[option=none,style=\tttf]
108 % A transformation example
109 \definefloat[example][examples]
110 \setupcaption[example][location=top] % Put captions on top
112 \define[3]\transexample{
113 \placeexample[here]{#1}
114 \startcombination[2*1]
115 {\example{#2}}{Original program}
116 {\example{#3}}{Transformed program}
120 \define[3]\transexampleh{
121 % \placeexample[here]{#1}
122 % \startcombination[1*2]
123 % {\example{#2}}{Original program}
124 % {\example{#3}}{Transformed program}
128 % Define a custom description format for the builtinexprs below
129 \definedescription[builtindesc][headstyle=bold,style=normal,location=top]
132 \title {Core transformations for hardware generation}
135 \section{Introduction}
136 As a new approach to translating Core to VHDL, we investigate a number of
137 transformations on our Core program, which should bring the program into a
138 well-defined "canonical" form, which is subsequently trivial to translate to
141 The transformations as presented here are far from complete, but are meant as
142 an exploration of possible transformations. In the running example below, we
143 apply each of the transformations exactly once, in sequence. As will be
144 apparent from the end result, there will be additional transformations needed
145 to fully reach our goal, and some transformations must be applied more than
146 once. How exactly to (efficiently) do this, has not been investigated.
148 Lastly, I hope to be able to state a number of pre- and postconditions for
149 each transformation. If these can be proven for each transformation, and it
150 can be shown that there exists some ordering of transformations for which the
151 postcondition implies the canonical form, we can show that the transformations
152 do indeed transform any program (probably satisfying a number of
153 preconditions) to the canonical form.
156 The transformations described here have a well-defined goal: To bring the
157 program in a well-defined form that is directly translatable to hardware,
158 while fully preserving the semantics of the program.
160 This {\em canonical form} is again a Core program, but with a very specific
161 structure. A function in canonical form has nested lambda's at the top, which
162 produce a let expression. This let expression binds every function application
163 in the function and produces either a simple identifier or a tuple of
164 identifiers. Every bound value in the let expression is either a simple
165 function application or a case expression to extract a single element from a
166 tuple returned by a function.
168 An example of a program in canonical form would be:
171 -- All arguments are an inital lambda
173 -- There is one let expression at the top level
175 -- Calling some other user-defined function.
177 -- Extracting result values from a tuple
178 a = case s of (a, b) -> a
179 b = case s of (a, b) -> b
180 -- Some builtin expressions
183 -- Conditional connections
195 In this and all following programs, the following definitions are assumed to
199 data Bit = Low | High
201 foo :: Int -> (Bit, Bit)
202 add :: Int -> Int -> Int
203 sub :: Int -> Int -> Int
206 When looking at such a program from a hardware perspective, the top level
207 lambda's define the input ports. The value produced by the let expression are
208 the output ports. Each function application bound by the let expression
209 defines a component instantiation, where the input and output ports are mapped
210 to local signals or arguments. The tuple extracting case expressions don't map
213 \subsection{Canonical form definition}
214 Formally, the canonical form is a core program obeying the following
217 \startitemize[R,inmargin]
218 \item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
219 $fun$ is an identifier that will be bound as a global identifier.
220 \item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
221 $\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
222 \item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
223 \item $letbinds$ is a list with elements of the form
224 $\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
225 an identifier that will be bound as local identifier. The type of the bound
226 value must be a $hardware\;type$.
227 \item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
228 equivalent VHDL expression. Since there are many supported forms for this,
229 these are defined in a separate table.
230 \item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
231 where $fun$ is a global identifier and $x$ is a local identifier.
232 \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
233 be of a $hardware\;type$.
234 \item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
235 where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
237 \item A $hardware\;type$ is a type that can be directly translated to
238 hardware. This includes the types $Bit$, $SizedWord$, tuples containing
239 elements of $hardware\;type$s, and will include others. This explicitely
240 excludes function types.
243 TODO: Say something about uniqueness of identifiers
245 \subsection{Builtin expressions}
246 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
248 \startitemize[m,inmargin]
250 $tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
251 where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
252 e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
253 be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
254 \item TODO: Many more!
257 \section{Transformation passes}
259 In this section we describe the actual transformations. Here we're using
260 mostly Core-like notation, with a few notable points.
263 \item A core expression (in contrast with a transformation function, for
264 example), is enclosed in pipes. For example, $\app{transform}{\expr{\lam{z}{z+1}}}$
265 is the transform function applied to a lambda core expression.
267 Note that this notation might not be consistently applied everywhere. In
268 particular where a non-core function is used inside a core expression, things
269 get slightly confusing.
270 \item A bind is written as $\expr{\bind{x}{expr}}$. This means binding the identifier
271 $x$ to the expression $expr$.
272 \item In the core examples, the layout rule from Haskell is loosely applied.
273 It should be evident what was meant from indentation, even though it might nog
278 In the descriptions of transformations below, the following (slightly
279 contrived) example program will be used as the running example. Note that this
280 the example for the canonical form given above is the same program, but in
299 \subsection{η-abstraction}
300 This transformation makes sure that all arguments of a function-typed
301 expression are named, by introducing lambda expressions. When combined with
302 β-reduction and function inlining below, all function-typed expressions should
303 be lambda abstractions or global identifiers.
305 \transform{η-abstraction}
309 \lam{E} is not the first argument of an application.
311 \lam{E} is not a lambda abstraction.
313 \lam{x} is a variable that does not occur free in E.
321 foo = λa -> case a of
327 foo = λa.λx -> (case a of
332 \transexample{η-abstraction}{from}{to}
334 \subsection{Extended β-reduction}
335 This transformation is meant to propagate application expressions downwards
336 into expressions as far as possible. In lambda calculus, this reduction
337 is known as β-reduction, but it is of course only defined for
338 applications of lambda abstractions. We extend this reduction to also
339 work for the rest of core (case and let expressions).
353 \transform{Extended β-reduction}
356 \trans{(λx.E) M}{E[M/x]}
360 \trans{(let binds in E) M}{let binds in E M}
372 b = (let y = 3 in add y) 2
381 b = let y = 3 in add y 2
386 \transexample{Extended β-reduction}{from}{to}
388 \subsection{Argument simplification}
389 The transforms in this section deal with simplifying application
390 arguments into normal form. The goal here is to:
393 \item Make all arguments of user-defined functions (\eg, of which
394 we have a function body) simple variable references of a runtime
396 \item Make all arguments of builtin functions either:
398 \item A type argument.
399 \item A dictionary argument.
400 \item A type level expression.
401 \item A variable reference of a runtime representable type.
402 \item A variable reference or partial application of a function type.
406 \subsubsection{User-defined functions}
407 We can divide the arguments of a user-defined function into two
410 \item Runtime representable typed arguments (\eg bits or vectors).
411 \item Non-runtime representable typed arguments.
414 The next two transformations will deal with each of these two kinds of argument respectively.
416 \subsubsubsection{Argument extraction}
417 This transform deals with arguments to user-defined functions that
418 are of a runtime representable type. These arguments can be preserved in
419 the program, since they can be translated to input ports later on.
420 However, since we can only connect signals to input ports, these
421 arguments must be reduced to simple variables (for which signals will be
424 TODO: It seems we can map an expression to a port, not only a signal.
425 Perhaps this makes this transformation not needed?
426 TODO: Say something about dataconstructors (without arguments, like True
427 or False), which are variable references of a runtime representable
428 type, but do not result in a signal.
430 To reduce a complex expression to a simple variable reference, we create
431 a new let expression around the application, which binds the complex
432 expression to a new variable. The original function is then applied to
435 \transform{Argument extract}
437 \lam{X} is a (partial application of) a user-defined function
439 \lam{Y} is of a hardware representable type
441 \lam{Y} is not a variable referene
445 \trans{X Y}{let z = Y in X z}
447 \subsubsubsection{Argument propagation}
448 This transform deals with arguments to user-defined functions that are
449 not representable at runtime. This means these arguments cannot be
450 preserved in the final form and most be {\em propagated}.
452 Propagation means to create a specialized version of the called
453 function, with the propagated argument already filled in. As a simple
454 example, in the following program:
461 we could {\em propagate} the constant argument 1, with the following
469 Special care must be taken when the to-be-propagated expression has any
470 free variables. If this is the case, the original argument should not be
471 removed alltogether, but replaced by all the free variables of the
472 expression. In this way, the original expression can still be evaluated
473 inside the new function. Also, this brings us closer to our goal: All
474 these free variables will be simple variable references.
476 To prevent us from propagating the same argument over and over, a simple
477 local variable reference is not propagated (since is has exactly one
478 free variable, itself, we would only replace that argument with itself).
480 This shows that any free local variables that are not runtime representable
481 cannot be brought into normal form by this transform. We rely on an
482 inlining transformation to replace such a variable with an expression we
485 TODO: Move these definitions somewhere sensible.
487 Definition: A global variable is any variable that is bound at the
488 top level of a program. A local variable is any other variable.
490 Definition: A hardware representable type is a type that we can generate
491 a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
492 unsigned word, etc. Types that are not runtime representable notably
493 include (but are not limited to): Types, dictionaries, functions.
495 Definition: A builtin function is a function for which a builtin
496 hardware translation is available, because its actual definition is not
497 translatable. A user-defined function is any other function.
499 \transform{Argument propagation}
501 \lam{x} is a global variable, bound to a user-defined function
505 \lam{Y_i} is not of a runtime representable type
507 \lam{Y_i} is not a local variable reference
511 \lam{f0 ... fm} = free local vars of \lam{Y_i}
513 \lam{x'} is a new global variable
515 \lam{x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . E y0 ... yi-1 Yi yi+1 ... yn}
517 \trans{x Y0 ... Yi ... Yn}{x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn}
520 TODO: The above definition looks too complicated... Can we find
521 something more concise?
523 \subsubsection{Builtin functions}
529 type / dictionary / other
531 hardware representable
535 \subsection{Introducing main scope}
536 This transformation is meant to introduce a single let expression that will be
537 the "main scope". This is the let expression as described under requirement
538 \ref[letexpr]. This let expression will contain only a single binding, which
539 binds the original expression to some identifier and then evalutes to just
540 this identifier (to comply with requirement \in[retexpr]).
542 Formally, we can describe the transformation as follows.
544 \transformold{Main scope introduction}
546 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
548 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
549 \NC \app{transform'}{\expr{expr}} \NC = \expr{\letexpr{\bind{x}{expr}}{x}} \NR
552 When applying this transformation to our running example, we get the following
557 let r = (let s = foo x
574 \subsection{Scope flattening}
575 This transformation tries to flatten the topmost let expression in a bind,
576 {\em i.e.}, bind all identifiers in the same scope, and bind them to simple
577 expressions only (so simplify deeply nested expressions).
579 Formally, we can describe the transformation as follows.
581 \transformold{Main scope introduction} { \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
583 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
584 \NC \app{transform'}{\expr{\letexpr{binds}{expr}}} \NC = \expr{\letexpr{\app{concat . map . flatten}{binds}}{expr}}\NR
586 \NC \app{flatten}{\expr{\bind{x}{\letexpr{binds}{expr}}}} \NC = (\app{concat . map . flatten}{binds}) \cup \{\app{flatten}{\expr{\bind{x}{expr}}}\}\NR
587 \NC \app{flatten}{\expr{\bind{x}{\case{s}{alts}}}} \NC = \app{concat}{binds'} \cup \{\bind{x}{\case{s}{alts'}}\}\NR
588 \NC \NC \where{(binds', alts')=\app{unzip.map.(flattenalt s)}{alts}}\NR
589 \NC \app{\app{flattenalt}{s}}{\expr{\alt{\app{con}{x_0\;..\;x_n}}{expr}}} \NC = (extracts \cup \{\app{flatten}{bind}\}, alt)\NR
590 \NC \NC \where{extracts =\{\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_0}}},}\NR
591 \NC \NC \;..\;,\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_n}}}\} \NR
592 \NC \NC bind = \expr{\bind{y}{expr}}\NR
593 \NC \NC alt = \expr{\alt{\app{con}{\_\;..\;\_}}{y}}\NR
596 When applying this transformation to our running example, we get the following
604 a = case s of (a, b) -> a
605 b = case s of (a, b) -> b
620 \subsection{More transformations}
621 As noted before, the above transformations are not complete. Other needed
622 transformations include:
624 \item Inlining of local identifiers with a function type. Since these cannot
625 be represented in hardware directly, they must be transformed into something
626 else. Inlining them should always be possible without loss of semantics (TODO:
627 How true is this?) and can expose new possibilities for other transformations
628 passes (such as application propagation when inlining {\tt j} above).
629 \item A variation on inlining local identifiers is the propagation of
630 function arguments with a function type. This will probably be initiated when
631 transforming the caller (and not the callee), but it will also deal with
632 identifiers with a function type that are unrepresentable in hardware.
634 Special care must be taken here, since the expression that is propagated into
635 the callee comes from a different scope. The function typed argument must thus
636 be replaced by any identifiers from the callers scope that the propagated
639 Note that propagating an argument will change both a function's interface and
640 implementation. For this to work, a new function should be created instead of
641 modifying the original function, so any other callers will not be broken.
642 \item Something similar should happen with return values with function types.
643 \item Polymorphism must be removed from all user-defined functions. This is
644 again similar to propagation function typed arguments, since this will also
645 create duplicates of functions (for a specific type). This is an operation
646 that is commonly known as "specialization" and already happens in GHC (since
647 non-polymorph functions can be a lot faster than generic ones).
648 \item More builtin expressions should be added and these should be evaluated
649 by the compiler. For example, map, fold, +.
670 After top-level η-abstraction:
689 After (extended) β-reduction:
707 After return value extraction:
726 Scrutinee simplification does not apply.
728 After case binder wildening:
733 a = case s of (a, _) -> a
734 b = case s of (_, b) -> b
735 r = case s of (_, _) ->
738 Low -> let op' = case b of
747 After case value simplification
752 a = case s of (a, _) -> a
753 b = case s of (_, b) -> b
754 r = case s of (_, _) -> r'
756 rl = let rll = λc.λd.c
769 After let flattening:
774 a = case s of (a, _) -> a
775 b = case s of (_, b) -> b
776 r = case s of (_, _) -> r'
790 After function inlining:
795 a = case s of (a, _) -> a
796 b = case s of (_, b) -> b
797 r = case s of (_, _) -> r'
809 After (extended) β-reduction again:
814 a = case s of (a, _) -> a
815 b = case s of (_, b) -> b
816 r = case s of (_, _) -> r'
828 After case value simplification again:
833 a = case s of (a, _) -> a
834 b = case s of (_, b) -> b
835 r = case s of (_, _) -> r'
853 a = case s of (a, _) -> a
854 b = case s of (_, b) -> b
868 After let bind removal:
873 a = case s of (a, _) -> a
874 b = case s of (_, b) -> b
887 Application simplification is not applicable.