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 %\placetransformation[here]{#1}
32 \startframedtext[width=\textwidth]
33 \startformula \startalign
35 \stopalign \stopformula
39 % Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
40 \installprettytype [LAM] [LAM]
42 % A helper to print a single example in the half the page width. The example
43 % text should be in a buffer whose name is given in an argument.
45 % The align=right option really does left-alignment, but without the program
46 % will end up on a single line. The strut=no option prevents a bunch of empty
47 % space at the start of the frame.
48 \define[1]\example{\framed[frameoffset=2mm,align=right,strut=no]{\typebuffer[#1]}}
50 % A transformation example
51 \definefloat[example][examples]
52 \setupcaption[example][location=top] % Put captions on top
54 \define[3]\transexample{
55 \placeexample[here]{#1}
56 \startcombination[2*1]
57 {\example{#2}}{Original program}
58 {\example{#3}}{Transformed program}
62 \define[3]\transexampleh{
63 \placeexample[here]{#1}
64 \startcombination[1*2]
65 {\example{#2}}{Original program}
66 {\example{#3}}{Transformed program}
70 % Define a custom description format for the builtinexprs below
71 \definedescription[builtindesc][headstyle=bold,style=normal,location=top]
74 \title {Core transformations for hardware generation}
77 \section{Introduction}
78 As a new approach to translating Core to VHDL, we investigate a number of
79 transformations on our Core program, which should bring the program into a
80 well-defined "canonical" form, which is subsequently trivial to translate to
83 The transformations as presented here are far from complete, but are meant as
84 an exploration of possible transformations. In the running example below, we
85 apply each of the transformations exactly once, in sequence. As will be
86 apparent from the end result, there will be additional transformations needed
87 to fully reach our goal, and some transformations must be applied more than
88 once. How exactly to (efficiently) do this, has not been investigated.
90 Lastly, I hope to be able to state a number of pre- and postconditions for
91 each transformation. If these can be proven for each transformation, and it
92 can be shown that there exists some ordering of transformations for which the
93 postcondition implies the canonical form, we can show that the transformations
94 do indeed transform any program (probably satisfying a number of
95 preconditions) to the canonical form.
98 The transformations described here have a well-defined goal: To bring the
99 program in a well-defined form that is directly translatable to hardware,
100 while fully preserving the semantics of the program.
102 This {\em canonical form} is again a Core program, but with a very specific
103 structure. A function in canonical form has nested lambda's at the top, which
104 produce a let expression. This let expression binds every function application
105 in the function and produces either a simple identifier or a tuple of
106 identifiers. Every bound value in the let expression is either a simple
107 function application or a case expression to extract a single element from a
108 tuple returned by a function.
110 An example of a program in canonical form would be:
113 -- All arguments are an inital lambda
115 -- There is one let expression at the top level
117 -- Calling some other user-defined function.
119 -- Extracting result values from a tuple
120 a = case s of (a, b) -> a
121 b = case s of (a, b) -> b
122 -- Some builtin expressions
125 -- Conditional connections
137 In this and all following programs, the following definitions are assumed to
141 data Bit = Low | High
143 foo :: Int -> (Bit, Bit)
144 add :: Int -> Int -> Int
145 sub :: Int -> Int -> Int
148 When looking at such a program from a hardware perspective, the top level
149 lambda's define the input ports. The value produced by the let expression are
150 the output ports. Each function application bound by the let expression
151 defines a component instantiation, where the input and output ports are mapped
152 to local signals or arguments. The tuple extracting case expressions don't map
155 \subsection{Canonical form definition}
156 Formally, the canonical form is a core program obeying the following
159 \startitemize[R,inmargin]
160 \item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
161 $fun$ is an identifier that will be bound as a global identifier.
162 \item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
163 $\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
164 \item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
165 \item $letbinds$ is a list with elements of the form
166 $\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
167 an identifier that will be bound as local identifier. The type of the bound
168 value must be a $hardware\;type$.
169 \item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
170 equivalent VHDL expression. Since there are many supported forms for this,
171 these are defined in a separate table.
172 \item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
173 where $fun$ is a global identifier and $x$ is a local identifier.
174 \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
175 be of a $hardware\;type$.
176 \item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
177 where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
179 \item A $hardware\;type$ is a type that can be directly translated to
180 hardware. This includes the types $Bit$, $SizedWord$, tuples containing
181 elements of $hardware\;type$s, and will include others. This explicitely
182 excludes function types.
185 TODO: Say something about uniqueness of identifiers
187 \subsection{Builtin expressions}
188 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
190 \startitemize[m,inmargin]
192 $tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
193 where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
194 e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
195 be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
196 \item TODO: Many more!
199 \section{Transformation passes}
201 In this section we describe the actual transformations. Here we're using
202 mostly Core-like notation, with a few notable points.
205 \item A core expression (in contrast with a transformation function, for
206 example), is enclosed in pipes. For example, $\app{transform}{\expr{\lam{z}{z+1}}}$
207 is the transform function applied to a lambda core expression.
209 Note that this notation might not be consistently applied everywhere. In
210 particular where a non-core function is used inside a core expression, things
211 get slightly confusing.
212 \item A bind is written as $\expr{\bind{x}{expr}}$. This means binding the identifier
213 $x$ to the expression $expr$.
214 \item In the core examples, the layout rule from Haskell is loosely applied.
215 It should be evident what was meant from indentation, even though it might nog
220 In the descriptions of transformations below, the following (slightly
221 contrived) example program will be used as the running example. Note that this
222 the example for the canonical form given above is the same program, but in
241 \subsection{Argument extraction}
242 This transformation makes sure that all of a bindings arguments are always
243 bound to variables at the top level of the bound value. Formally, we can
244 describe this transformation as follows.
246 \transform{Argument extraction}
248 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
250 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
251 \NC \app{transform'}{\expr{expr :: a \xrightarrow b}} \NC = \expr{\lam{x}{\app{transform'}{\expr{(\app{expr}{x})}}}} \NR
254 When applying this transformation to our running example, we get the following
275 foo = \x -> case x of True -> (\y -> mul y y); False -> id
278 foo = \x z -> (case x of True -> (\y -> mul y y); False -> id) z
281 \transexampleh{Argument extraction example}{from}{to}
283 \subsection{Application propagation}
284 This transformation is meant to propagate application expressions downwards
285 into expressions as far as possible. Formally, we can describe this
286 transformation as follows.
288 \transform{Application propagation}
290 \NC \app{transform}{\expr{\app{(\letexpr{binds}{expr})}{y}}} \NC = \expr{\letexpr{binds}{(\app{expr}{y})}}\NR
291 \NC \app{transform}{\expr{\app{(\lam{x}{expr})}{y}}} \NC = \app{\app{subs}{x \xRightarrow y}}{\expr{expr}}\NR
292 \NC \app{transform}{\expr{\app{(\case{x}{\alt{p}{e};...})}{y}}} \NC = \expr{\case{x}{\alt{p}{\app{e}{y}};...}}\;(for\;every\;alt)\NR
295 When applying this transformation to our running example, we get the following
315 foo = \x z -> (case x of True -> (\y -> mul y y); False -> id) z
318 foo = \x z -> case x of True -> mul z z; False -> id z
321 \transexampleh{Application propagation example}{from}{to}
323 \subsection{Introducing main scope}
324 This transformation is meant to introduce a single let expression that will be
325 the "main scope". This is the let expression as described under requirement
326 \ref[letexpr]. This let expression will contain only a single binding, which
327 binds the original expression to some identifier and then evalutes to just
328 this identifier (to comply with requirement \in[retexpr]).
330 Formally, we can describe the transformation as follows.
332 \transform{Main scope introduction}
334 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
336 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
337 \NC \app{transform'}{\expr{expr}} \NC = \expr{\letexpr{\bind{x}{expr}}{x}} \NR
340 When applying this transformation to our running example, we get the following
345 let r = (let s = foo x
362 \subsection{Scope flattening}
363 This transformation tries to flatten the topmost let expression in a bind,
364 {\em i.e.}, bind all identifiers in the same scope, and bind them to simple
365 expressions only (so simplify deeply nested expressions).
367 Formally, we can describe the transformation as follows.
369 \transform{Main scope introduction} { \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
371 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
372 \NC \app{transform'}{\expr{\letexpr{binds}{expr}}} \NC = \expr{\letexpr{\app{concat . map . flatten}{binds}}{expr}}\NR
374 \NC \app{flatten}{\expr{\bind{x}{\letexpr{binds}{expr}}}} \NC = (\app{concat . map . flatten}{binds}) \cup \{\app{flatten}{\expr{\bind{x}{expr}}}\}\NR
375 \NC \app{flatten}{\expr{\bind{x}{\case{s}{alts}}}} \NC = \app{concat}{binds'} \cup \{\bind{x}{\case{s}{alts'}}\}\NR
376 \NC \NC \where{(binds', alts')=\app{unzip.map.(flattenalt s)}{alts}}\NR
377 \NC \app{\app{flattenalt}{s}}{\expr{\alt{\app{con}{x_0\;..\;x_n}}{expr}}} \NC = (extracts \cup \{\app{flatten}{bind}\}, alt)\NR
378 \NC \NC \where{extracts =\{\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_0}}},}\NR
379 \NC \NC \;..\;,\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_n}}}\} \NR
380 \NC \NC bind = \expr{\bind{y}{expr}}\NR
381 \NC \NC alt = \expr{\alt{\app{con}{\_\;..\;\_}}{y}}\NR
384 When applying this transformation to our running example, we get the following
392 a = case s of (a, b) -> a
393 b = case s of (a, b) -> b
408 \subsection{More transformations}
409 As noted before, the above transformations are not complete. Other needed
410 transformations include:
412 \item Inlining of local identifiers with a function type. Since these cannot
413 be represented in hardware directly, they must be transformed into something
414 else. Inlining them should always be possible without loss of semantics (TODO:
415 How true is this?) and can expose new possibilities for other transformations
416 passes (such as application propagation when inlining {\tt j} above).
417 \item A variation on inlining local identifiers is the propagation of
418 function arguments with a function type. This will probably be initiated when
419 transforming the caller (and not the callee), but it will also deal with
420 identifiers with a function type that are unrepresentable in hardware.
422 Special care must be taken here, since the expression that is propagated into
423 the callee comes from a different scope. The function typed argument must thus
424 be replaced by any identifiers from the callers scope that the propagated
427 Note that propagating an argument will change both a function's interface and
428 implementation. For this to work, a new function should be created instead of
429 modifying the original function, so any other callers will not be broken.
430 \item Something similar should happen with return values with function types.
431 \item Polymorphism must be removed from all user-defined functions. This is
432 again similar to propagation function typed arguments, since this will also
433 create duplicates of functions (for a specific type). This is an operation
434 that is commonly known as "specialization" and already happens in GHC (since
435 non-polymorph functions can be a lot faster than generic ones).
436 \item More builtin expressions should be added and these should be evaluated
437 by the compiler. For example, map, fold, +.