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 % An (invisible) frame to hold a lambda expression
44 % Put a frame around lambda expressions, so they can have multiple
45 % lines and still appear inline.
46 % The align=right option really does left-alignment, but without the
47 % program will end up on a single line. The strut=no option prevents a
48 % bunch of empty space at the start of the frame.
49 \framed[offset=0mm,location=middle,strut=no,align=right,frame=off]{#1}
53 % Make \typebuffer uses the LAM pretty printer and a sans-serif font
54 % Also prevent any extra spacing above and below caused by the default
55 % before=\blank and after=\blank.
56 \setuptyping[option=LAM,style=sans,before=,after=]
57 % Prevent the arrow from ending up below the first frame (a \framed
58 % at the start of a line defaults to using vmode).
60 % Put the elements in frames, so they can have multiple lines and be
62 \lamframe{\typebuffer[#1]}
63 \lamframe{\Rightarrow}
64 \lamframe{\typebuffer[#2]}
65 % Reset the typing settings to their defaults
66 \setuptyping[option=none,style=\tttf]
69 % A helper to print a single example in the half the page width. The example
70 % text should be in a buffer whose name is given in an argument.
72 % The align=right option really does left-alignment, but without the program
73 % will end up on a single line. The strut=no option prevents a bunch of empty
74 % space at the start of the frame.
75 \define[1]\example{\framed[frameoffset=2mm,align=right,strut=no]{\typebuffer[#1]}}
77 % A transformation example
78 \definefloat[example][examples]
79 \setupcaption[example][location=top] % Put captions on top
81 \define[3]\transexample{
82 \placeexample[here]{#1}
83 \startcombination[2*1]
84 {\example{#2}}{Original program}
85 {\example{#3}}{Transformed program}
89 \define[3]\transexampleh{
90 \placeexample[here]{#1}
91 \startcombination[1*2]
92 {\example{#2}}{Original program}
93 {\example{#3}}{Transformed program}
97 % Define a custom description format for the builtinexprs below
98 \definedescription[builtindesc][headstyle=bold,style=normal,location=top]
101 \title {Core transformations for hardware generation}
104 \section{Introduction}
105 As a new approach to translating Core to VHDL, we investigate a number of
106 transformations on our Core program, which should bring the program into a
107 well-defined "canonical" form, which is subsequently trivial to translate to
110 The transformations as presented here are far from complete, but are meant as
111 an exploration of possible transformations. In the running example below, we
112 apply each of the transformations exactly once, in sequence. As will be
113 apparent from the end result, there will be additional transformations needed
114 to fully reach our goal, and some transformations must be applied more than
115 once. How exactly to (efficiently) do this, has not been investigated.
117 Lastly, I hope to be able to state a number of pre- and postconditions for
118 each transformation. If these can be proven for each transformation, and it
119 can be shown that there exists some ordering of transformations for which the
120 postcondition implies the canonical form, we can show that the transformations
121 do indeed transform any program (probably satisfying a number of
122 preconditions) to the canonical form.
125 The transformations described here have a well-defined goal: To bring the
126 program in a well-defined form that is directly translatable to hardware,
127 while fully preserving the semantics of the program.
129 This {\em canonical form} is again a Core program, but with a very specific
130 structure. A function in canonical form has nested lambda's at the top, which
131 produce a let expression. This let expression binds every function application
132 in the function and produces either a simple identifier or a tuple of
133 identifiers. Every bound value in the let expression is either a simple
134 function application or a case expression to extract a single element from a
135 tuple returned by a function.
137 An example of a program in canonical form would be:
140 -- All arguments are an inital lambda
142 -- There is one let expression at the top level
144 -- Calling some other user-defined function.
146 -- Extracting result values from a tuple
147 a = case s of (a, b) -> a
148 b = case s of (a, b) -> b
149 -- Some builtin expressions
152 -- Conditional connections
164 In this and all following programs, the following definitions are assumed to
168 data Bit = Low | High
170 foo :: Int -> (Bit, Bit)
171 add :: Int -> Int -> Int
172 sub :: Int -> Int -> Int
175 When looking at such a program from a hardware perspective, the top level
176 lambda's define the input ports. The value produced by the let expression are
177 the output ports. Each function application bound by the let expression
178 defines a component instantiation, where the input and output ports are mapped
179 to local signals or arguments. The tuple extracting case expressions don't map
182 \subsection{Canonical form definition}
183 Formally, the canonical form is a core program obeying the following
186 \startitemize[R,inmargin]
187 \item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
188 $fun$ is an identifier that will be bound as a global identifier.
189 \item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
190 $\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
191 \item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
192 \item $letbinds$ is a list with elements of the form
193 $\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
194 an identifier that will be bound as local identifier. The type of the bound
195 value must be a $hardware\;type$.
196 \item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
197 equivalent VHDL expression. Since there are many supported forms for this,
198 these are defined in a separate table.
199 \item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
200 where $fun$ is a global identifier and $x$ is a local identifier.
201 \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
202 be of a $hardware\;type$.
203 \item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
204 where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
206 \item A $hardware\;type$ is a type that can be directly translated to
207 hardware. This includes the types $Bit$, $SizedWord$, tuples containing
208 elements of $hardware\;type$s, and will include others. This explicitely
209 excludes function types.
212 TODO: Say something about uniqueness of identifiers
214 \subsection{Builtin expressions}
215 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
217 \startitemize[m,inmargin]
219 $tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
220 where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
221 e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
222 be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
223 \item TODO: Many more!
226 \section{Transformation passes}
228 In this section we describe the actual transformations. Here we're using
229 mostly Core-like notation, with a few notable points.
232 \item A core expression (in contrast with a transformation function, for
233 example), is enclosed in pipes. For example, $\app{transform}{\expr{\lam{z}{z+1}}}$
234 is the transform function applied to a lambda core expression.
236 Note that this notation might not be consistently applied everywhere. In
237 particular where a non-core function is used inside a core expression, things
238 get slightly confusing.
239 \item A bind is written as $\expr{\bind{x}{expr}}$. This means binding the identifier
240 $x$ to the expression $expr$.
241 \item In the core examples, the layout rule from Haskell is loosely applied.
242 It should be evident what was meant from indentation, even though it might nog
247 In the descriptions of transformations below, the following (slightly
248 contrived) example program will be used as the running example. Note that this
249 the example for the canonical form given above is the same program, but in
268 \subsection{Argument extraction}
269 This transformation makes sure that all of a bindings arguments are always
270 bound to variables at the top level of the bound value. Formally, we can
271 describe this transformation as follows.
273 \transform{Argument extraction}
275 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
277 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
278 \NC \app{transform'}{\expr{expr :: a \xrightarrow b}} \NC = \expr{\lam{x}{\app{transform'}{\expr{(\app{expr}{x})}}}} \NR
281 When applying this transformation to our running example, we get the following
302 foo = \x -> case x of True -> (\y -> mul y y); False -> id
305 foo = \x z -> (case x of True -> (\y -> mul y y); False -> id) z
308 \transexampleh{Argument extraction example}{from}{to}
310 \subsection{Application propagation}
311 This transformation is meant to propagate application expressions downwards
312 into expressions as far as possible. Formally, we can describe this
313 transformation as follows.
315 \transform{Application propagation}
317 \NC \app{transform}{\expr{\app{(\letexpr{binds}{expr})}{y}}} \NC = \expr{\letexpr{binds}{(\app{expr}{y})}}\NR
318 \NC \app{transform}{\expr{\app{(\lam{x}{expr})}{y}}} \NC = \app{\app{subs}{x \xRightarrow y}}{\expr{expr}}\NR
319 \NC \app{transform}{\expr{\app{(\case{x}{\alt{p}{e};...})}{y}}} \NC = \expr{\case{x}{\alt{p}{\app{e}{y}};...}}\;(for\;every\;alt)\NR
322 When applying this transformation to our running example, we get the following
342 foo = \x z -> (case x of True -> (\y -> mul y y); False -> id) z
345 foo = \x z -> case x of True -> mul z z; False -> id z
348 \transexampleh{Application propagation example}{from}{to}
350 \subsection{Introducing main scope}
351 This transformation is meant to introduce a single let expression that will be
352 the "main scope". This is the let expression as described under requirement
353 \ref[letexpr]. This let expression will contain only a single binding, which
354 binds the original expression to some identifier and then evalutes to just
355 this identifier (to comply with requirement \in[retexpr]).
357 Formally, we can describe the transformation as follows.
359 \transform{Main scope introduction}
361 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
363 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
364 \NC \app{transform'}{\expr{expr}} \NC = \expr{\letexpr{\bind{x}{expr}}{x}} \NR
367 When applying this transformation to our running example, we get the following
372 let r = (let s = foo x
389 \subsection{Scope flattening}
390 This transformation tries to flatten the topmost let expression in a bind,
391 {\em i.e.}, bind all identifiers in the same scope, and bind them to simple
392 expressions only (so simplify deeply nested expressions).
394 Formally, we can describe the transformation as follows.
396 \transform{Main scope introduction} { \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{\letexpr{binds}{expr}}} \NC = \expr{\letexpr{\app{concat . map . flatten}{binds}}{expr}}\NR
401 \NC \app{flatten}{\expr{\bind{x}{\letexpr{binds}{expr}}}} \NC = (\app{concat . map . flatten}{binds}) \cup \{\app{flatten}{\expr{\bind{x}{expr}}}\}\NR
402 \NC \app{flatten}{\expr{\bind{x}{\case{s}{alts}}}} \NC = \app{concat}{binds'} \cup \{\bind{x}{\case{s}{alts'}}\}\NR
403 \NC \NC \where{(binds', alts')=\app{unzip.map.(flattenalt s)}{alts}}\NR
404 \NC \app{\app{flattenalt}{s}}{\expr{\alt{\app{con}{x_0\;..\;x_n}}{expr}}} \NC = (extracts \cup \{\app{flatten}{bind}\}, alt)\NR
405 \NC \NC \where{extracts =\{\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_0}}},}\NR
406 \NC \NC \;..\;,\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_n}}}\} \NR
407 \NC \NC bind = \expr{\bind{y}{expr}}\NR
408 \NC \NC alt = \expr{\alt{\app{con}{\_\;..\;\_}}{y}}\NR
411 When applying this transformation to our running example, we get the following
419 a = case s of (a, b) -> a
420 b = case s of (a, b) -> b
435 \subsection{More transformations}
436 As noted before, the above transformations are not complete. Other needed
437 transformations include:
439 \item Inlining of local identifiers with a function type. Since these cannot
440 be represented in hardware directly, they must be transformed into something
441 else. Inlining them should always be possible without loss of semantics (TODO:
442 How true is this?) and can expose new possibilities for other transformations
443 passes (such as application propagation when inlining {\tt j} above).
444 \item A variation on inlining local identifiers is the propagation of
445 function arguments with a function type. This will probably be initiated when
446 transforming the caller (and not the callee), but it will also deal with
447 identifiers with a function type that are unrepresentable in hardware.
449 Special care must be taken here, since the expression that is propagated into
450 the callee comes from a different scope. The function typed argument must thus
451 be replaced by any identifiers from the callers scope that the propagated
454 Note that propagating an argument will change both a function's interface and
455 implementation. For this to work, a new function should be created instead of
456 modifying the original function, so any other callers will not be broken.
457 \item Something similar should happen with return values with function types.
458 \item Polymorphism must be removed from all user-defined functions. This is
459 again similar to propagation function typed arguments, since this will also
460 create duplicates of functions (for a specific type). This is an operation
461 that is commonly known as "specialization" and already happens in GHC (since
462 non-polymorph functions can be a lot faster than generic ones).
463 \item More builtin expressions should be added and these should be evaluated
464 by the compiler. For example, map, fold, +.