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 % Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
49 \installprettytype [LAM] [LAM]
51 \definetyping[lambda][option=LAM,style=sans]
52 \definetype[lam][option=LAM,style=sans]
54 % An (invisible) frame to hold a lambda expression
56 % Put a frame around lambda expressions, so they can have multiple
57 % lines and still appear inline.
58 % The align=right option really does left-alignment, but without the
59 % program will end up on a single line. The strut=no option prevents a
60 % bunch of empty space at the start of the frame.
61 \framed[offset=0mm,location=middle,strut=no,align=right,frame=off]{#1}
65 % Make \typebuffer uses the LAM pretty printer and a sans-serif font
66 % Also prevent any extra spacing above and below caused by the default
67 % before=\blank and after=\blank.
68 \setuptyping[option=LAM,style=sans,before=,after=]
69 % Prevent the arrow from ending up below the first frame (a \framed
70 % at the start of a line defaults to using vmode).
72 % Put the elements in frames, so they can have multiple lines and be
74 \lamframe{\typebuffer[#1]}
75 \lamframe{\Rightarrow}
76 \lamframe{\typebuffer[#2]}
77 % Reset the typing settings to their defaults
78 \setuptyping[option=none,style=\tttf]
80 % This is the same as \transbuf above, but it accepts text directly instead
81 % of through buffers. This only works for single lines, however.
85 \lamframe{\Rightarrow}
90 % A helper to print a single example in the half the page width. The example
91 % text should be in a buffer whose name is given in an argument.
93 % The align=right option really does left-alignment, but without the program
94 % will end up on a single line. The strut=no option prevents a bunch of empty
95 % space at the start of the frame.
97 \framed[offset=1mm,align=right,strut=no]{
98 \setuptyping[option=LAM,style=sans,before=,after=]
100 \setuptyping[option=none,style=\tttf]
105 % A transformation example
106 \definefloat[example][examples]
107 \setupcaption[example][location=top] % Put captions on top
109 \define[3]\transexample{
110 \placeexample[here]{#1}
111 \startcombination[2*1]
112 {\example{#2}}{Original program}
113 {\example{#3}}{Transformed program}
117 \define[3]\transexampleh{
118 % \placeexample[here]{#1}
119 % \startcombination[1*2]
120 % {\example{#2}}{Original program}
121 % {\example{#3}}{Transformed program}
125 % Define a custom description format for the builtinexprs below
126 \definedescription[builtindesc][headstyle=bold,style=normal,location=top]
129 \title {Core transformations for hardware generation}
132 \section{Introduction}
133 As a new approach to translating Core to VHDL, we investigate a number of
134 transformations on our Core program, which should bring the program into a
135 well-defined "canonical" form, which is subsequently trivial to translate to
138 The transformations as presented here are far from complete, but are meant as
139 an exploration of possible transformations. In the running example below, we
140 apply each of the transformations exactly once, in sequence. As will be
141 apparent from the end result, there will be additional transformations needed
142 to fully reach our goal, and some transformations must be applied more than
143 once. How exactly to (efficiently) do this, has not been investigated.
145 Lastly, I hope to be able to state a number of pre- and postconditions for
146 each transformation. If these can be proven for each transformation, and it
147 can be shown that there exists some ordering of transformations for which the
148 postcondition implies the canonical form, we can show that the transformations
149 do indeed transform any program (probably satisfying a number of
150 preconditions) to the canonical form.
153 The transformations described here have a well-defined goal: To bring the
154 program in a well-defined form that is directly translatable to hardware,
155 while fully preserving the semantics of the program.
157 This {\em canonical form} is again a Core program, but with a very specific
158 structure. A function in canonical form has nested lambda's at the top, which
159 produce a let expression. This let expression binds every function application
160 in the function and produces either a simple identifier or a tuple of
161 identifiers. Every bound value in the let expression is either a simple
162 function application or a case expression to extract a single element from a
163 tuple returned by a function.
165 An example of a program in canonical form would be:
168 -- All arguments are an inital lambda
170 -- There is one let expression at the top level
172 -- Calling some other user-defined function.
174 -- Extracting result values from a tuple
175 a = case s of (a, b) -> a
176 b = case s of (a, b) -> b
177 -- Some builtin expressions
180 -- Conditional connections
192 In this and all following programs, the following definitions are assumed to
196 data Bit = Low | High
198 foo :: Int -> (Bit, Bit)
199 add :: Int -> Int -> Int
200 sub :: Int -> Int -> Int
203 When looking at such a program from a hardware perspective, the top level
204 lambda's define the input ports. The value produced by the let expression are
205 the output ports. Each function application bound by the let expression
206 defines a component instantiation, where the input and output ports are mapped
207 to local signals or arguments. The tuple extracting case expressions don't map
210 \subsection{Canonical form definition}
211 Formally, the canonical form is a core program obeying the following
214 \startitemize[R,inmargin]
215 \item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
216 $fun$ is an identifier that will be bound as a global identifier.
217 \item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
218 $\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
219 \item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
220 \item $letbinds$ is a list with elements of the form
221 $\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
222 an identifier that will be bound as local identifier. The type of the bound
223 value must be a $hardware\;type$.
224 \item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
225 equivalent VHDL expression. Since there are many supported forms for this,
226 these are defined in a separate table.
227 \item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
228 where $fun$ is a global identifier and $x$ is a local identifier.
229 \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
230 be of a $hardware\;type$.
231 \item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
232 where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
234 \item A $hardware\;type$ is a type that can be directly translated to
235 hardware. This includes the types $Bit$, $SizedWord$, tuples containing
236 elements of $hardware\;type$s, and will include others. This explicitely
237 excludes function types.
240 TODO: Say something about uniqueness of identifiers
242 \subsection{Builtin expressions}
243 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
245 \startitemize[m,inmargin]
247 $tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
248 where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
249 e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
250 be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
251 \item TODO: Many more!
254 \section{Transformation passes}
256 In this section we describe the actual transformations. Here we're using
257 mostly Core-like notation, with a few notable points.
260 \item A core expression (in contrast with a transformation function, for
261 example), is enclosed in pipes. For example, $\app{transform}{\expr{\lam{z}{z+1}}}$
262 is the transform function applied to a lambda core expression.
264 Note that this notation might not be consistently applied everywhere. In
265 particular where a non-core function is used inside a core expression, things
266 get slightly confusing.
267 \item A bind is written as $\expr{\bind{x}{expr}}$. This means binding the identifier
268 $x$ to the expression $expr$.
269 \item In the core examples, the layout rule from Haskell is loosely applied.
270 It should be evident what was meant from indentation, even though it might nog
275 In the descriptions of transformations below, the following (slightly
276 contrived) example program will be used as the running example. Note that this
277 the example for the canonical form given above is the same program, but in
296 \subsection{η-abstraction}
297 This transformation makes sure that all arguments of a function-typed
298 expression are named, by introducing lambda expressions. When combined with
299 β-reduction and function inlining below, all function-typed expressions should
300 be lambda abstractions or global identifiers.
302 \transform{η-abstraction}
306 \lam{E} is not the first argument of an application.
308 \lam{E} is not a lambda abstraction.
310 \lam{x} is a variable that does not occur free in E.
318 foo = λa -> case a of
324 foo = λa.λx -> (case a of
329 \transexample{η-abstraction}{from}{to}
331 \subsection{Extended β-reduction}
332 This transformation is meant to propagate application expressions downwards
333 into expressions as far as possible. In lambda calculus, this reduction
334 is known as β-reduction, but it is of course only defined for
335 applications of lambda abstractions. We extend this reduction to also
336 work for the rest of core (case and let expressions).
350 \transform{Extended β-reduction}
353 \trans{(λx.E) M}{E[M/x]}
357 \trans{(let binds in E) M}{let binds in E M}
369 b = (let y = 3 in add y) 2
378 b = let y = 3 in add y 2
383 \transexample{Extended β-reduction}{from}{to}
385 \subsection{Introducing main scope}
386 This transformation is meant to introduce a single let expression that will be
387 the "main scope". This is the let expression as described under requirement
388 \ref[letexpr]. This let expression will contain only a single binding, which
389 binds the original expression to some identifier and then evalutes to just
390 this identifier (to comply with requirement \in[retexpr]).
392 Formally, we can describe the transformation as follows.
394 \transformold{Main scope introduction}
396 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
398 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
399 \NC \app{transform'}{\expr{expr}} \NC = \expr{\letexpr{\bind{x}{expr}}{x}} \NR
402 When applying this transformation to our running example, we get the following
407 let r = (let s = foo x
424 \subsection{Scope flattening}
425 This transformation tries to flatten the topmost let expression in a bind,
426 {\em i.e.}, bind all identifiers in the same scope, and bind them to simple
427 expressions only (so simplify deeply nested expressions).
429 Formally, we can describe the transformation as follows.
431 \transformold{Main scope introduction} { \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
433 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
434 \NC \app{transform'}{\expr{\letexpr{binds}{expr}}} \NC = \expr{\letexpr{\app{concat . map . flatten}{binds}}{expr}}\NR
436 \NC \app{flatten}{\expr{\bind{x}{\letexpr{binds}{expr}}}} \NC = (\app{concat . map . flatten}{binds}) \cup \{\app{flatten}{\expr{\bind{x}{expr}}}\}\NR
437 \NC \app{flatten}{\expr{\bind{x}{\case{s}{alts}}}} \NC = \app{concat}{binds'} \cup \{\bind{x}{\case{s}{alts'}}\}\NR
438 \NC \NC \where{(binds', alts')=\app{unzip.map.(flattenalt s)}{alts}}\NR
439 \NC \app{\app{flattenalt}{s}}{\expr{\alt{\app{con}{x_0\;..\;x_n}}{expr}}} \NC = (extracts \cup \{\app{flatten}{bind}\}, alt)\NR
440 \NC \NC \where{extracts =\{\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_0}}},}\NR
441 \NC \NC \;..\;,\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_n}}}\} \NR
442 \NC \NC bind = \expr{\bind{y}{expr}}\NR
443 \NC \NC alt = \expr{\alt{\app{con}{\_\;..\;\_}}{y}}\NR
446 When applying this transformation to our running example, we get the following
454 a = case s of (a, b) -> a
455 b = case s of (a, b) -> b
470 \subsection{More transformations}
471 As noted before, the above transformations are not complete. Other needed
472 transformations include:
474 \item Inlining of local identifiers with a function type. Since these cannot
475 be represented in hardware directly, they must be transformed into something
476 else. Inlining them should always be possible without loss of semantics (TODO:
477 How true is this?) and can expose new possibilities for other transformations
478 passes (such as application propagation when inlining {\tt j} above).
479 \item A variation on inlining local identifiers is the propagation of
480 function arguments with a function type. This will probably be initiated when
481 transforming the caller (and not the callee), but it will also deal with
482 identifiers with a function type that are unrepresentable in hardware.
484 Special care must be taken here, since the expression that is propagated into
485 the callee comes from a different scope. The function typed argument must thus
486 be replaced by any identifiers from the callers scope that the propagated
489 Note that propagating an argument will change both a function's interface and
490 implementation. For this to work, a new function should be created instead of
491 modifying the original function, so any other callers will not be broken.
492 \item Something similar should happen with return values with function types.
493 \item Polymorphism must be removed from all user-defined functions. This is
494 again similar to propagation function typed arguments, since this will also
495 create duplicates of functions (for a specific type). This is an operation
496 that is commonly known as "specialization" and already happens in GHC (since
497 non-polymorph functions can be a lot faster than generic ones).
498 \item More builtin expressions should be added and these should be evaluated
499 by the compiler. For example, map, fold, +.
520 After top-level η-abstraction:
539 After (extended) β-reduction:
557 After return value extraction:
576 Scrutinee simplification does not apply.
578 After case binder wildening:
583 a = case s of (a, _) -> a
584 b = case s of (_, b) -> b
585 r = case s of (_, _) ->
588 Low -> let op' = case b of
597 After case value simplification
602 a = case s of (a, _) -> a
603 b = case s of (_, b) -> b
604 r = case s of (_, _) -> r'
606 rl = let rll = λc.λd.c
619 After let flattening:
624 a = case s of (a, _) -> a
625 b = case s of (_, b) -> b
626 r = case s of (_, _) -> r'
640 After function inlining:
645 a = case s of (a, _) -> a
646 b = case s of (_, b) -> b
647 r = case s of (_, _) -> r'
659 After (extended) β-reduction again:
664 a = case s of (a, _) -> a
665 b = case s of (_, b) -> b
666 r = case s of (_, _) -> r'
678 After case value simplification again:
683 a = case s of (a, _) -> a
684 b = case s of (_, b) -> b
685 r = case s of (_, _) -> r'
703 a = case s of (a, _) -> a
704 b = case s of (_, b) -> b
718 After let bind removal:
723 a = case s of (a, _) -> a
724 b = case s of (_, b) -> b
737 Application simplification is not applicable.