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 \definetyping[lambda][option=LAM,style=sans]
44 % An (invisible) frame to hold a lambda expression
46 % Put a frame around lambda expressions, so they can have multiple
47 % lines and still appear inline.
48 % The align=right option really does left-alignment, but without the
49 % program will end up on a single line. The strut=no option prevents a
50 % bunch of empty space at the start of the frame.
51 \framed[offset=0mm,location=middle,strut=no,align=right,frame=off]{#1}
55 % Make \typebuffer uses the LAM pretty printer and a sans-serif font
56 % Also prevent any extra spacing above and below caused by the default
57 % before=\blank and after=\blank.
58 \setuptyping[option=LAM,style=sans,before=,after=]
59 % Prevent the arrow from ending up below the first frame (a \framed
60 % at the start of a line defaults to using vmode).
62 % Put the elements in frames, so they can have multiple lines and be
64 \lamframe{\typebuffer[#1]}
65 \lamframe{\Rightarrow}
66 \lamframe{\typebuffer[#2]}
67 % Reset the typing settings to their defaults
68 \setuptyping[option=none,style=\tttf]
71 % A helper to print a single example in the half the page width. The example
72 % text should be in a buffer whose name is given in an argument.
74 % The align=right option really does left-alignment, but without the program
75 % will end up on a single line. The strut=no option prevents a bunch of empty
76 % space at the start of the frame.
77 \define[1]\example{\framed[frameoffset=2mm,align=right,strut=no]{\typebuffer[#1]}}
79 % A transformation example
80 \definefloat[example][examples]
81 \setupcaption[example][location=top] % Put captions on top
83 \define[3]\transexample{
84 \placeexample[here]{#1}
85 \startcombination[2*1]
86 {\example{#2}}{Original program}
87 {\example{#3}}{Transformed program}
91 \define[3]\transexampleh{
92 \placeexample[here]{#1}
93 \startcombination[1*2]
94 {\example{#2}}{Original program}
95 {\example{#3}}{Transformed program}
99 % Define a custom description format for the builtinexprs below
100 \definedescription[builtindesc][headstyle=bold,style=normal,location=top]
103 \title {Core transformations for hardware generation}
106 \section{Introduction}
107 As a new approach to translating Core to VHDL, we investigate a number of
108 transformations on our Core program, which should bring the program into a
109 well-defined "canonical" form, which is subsequently trivial to translate to
112 The transformations as presented here are far from complete, but are meant as
113 an exploration of possible transformations. In the running example below, we
114 apply each of the transformations exactly once, in sequence. As will be
115 apparent from the end result, there will be additional transformations needed
116 to fully reach our goal, and some transformations must be applied more than
117 once. How exactly to (efficiently) do this, has not been investigated.
119 Lastly, I hope to be able to state a number of pre- and postconditions for
120 each transformation. If these can be proven for each transformation, and it
121 can be shown that there exists some ordering of transformations for which the
122 postcondition implies the canonical form, we can show that the transformations
123 do indeed transform any program (probably satisfying a number of
124 preconditions) to the canonical form.
127 The transformations described here have a well-defined goal: To bring the
128 program in a well-defined form that is directly translatable to hardware,
129 while fully preserving the semantics of the program.
131 This {\em canonical form} is again a Core program, but with a very specific
132 structure. A function in canonical form has nested lambda's at the top, which
133 produce a let expression. This let expression binds every function application
134 in the function and produces either a simple identifier or a tuple of
135 identifiers. Every bound value in the let expression is either a simple
136 function application or a case expression to extract a single element from a
137 tuple returned by a function.
139 An example of a program in canonical form would be:
142 -- All arguments are an inital lambda
144 -- There is one let expression at the top level
146 -- Calling some other user-defined function.
148 -- Extracting result values from a tuple
149 a = case s of (a, b) -> a
150 b = case s of (a, b) -> b
151 -- Some builtin expressions
154 -- Conditional connections
166 In this and all following programs, the following definitions are assumed to
170 data Bit = Low | High
172 foo :: Int -> (Bit, Bit)
173 add :: Int -> Int -> Int
174 sub :: Int -> Int -> Int
177 When looking at such a program from a hardware perspective, the top level
178 lambda's define the input ports. The value produced by the let expression are
179 the output ports. Each function application bound by the let expression
180 defines a component instantiation, where the input and output ports are mapped
181 to local signals or arguments. The tuple extracting case expressions don't map
184 \subsection{Canonical form definition}
185 Formally, the canonical form is a core program obeying the following
188 \startitemize[R,inmargin]
189 \item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
190 $fun$ is an identifier that will be bound as a global identifier.
191 \item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
192 $\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
193 \item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
194 \item $letbinds$ is a list with elements of the form
195 $\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
196 an identifier that will be bound as local identifier. The type of the bound
197 value must be a $hardware\;type$.
198 \item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
199 equivalent VHDL expression. Since there are many supported forms for this,
200 these are defined in a separate table.
201 \item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
202 where $fun$ is a global identifier and $x$ is a local identifier.
203 \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
204 be of a $hardware\;type$.
205 \item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
206 where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
208 \item A $hardware\;type$ is a type that can be directly translated to
209 hardware. This includes the types $Bit$, $SizedWord$, tuples containing
210 elements of $hardware\;type$s, and will include others. This explicitely
211 excludes function types.
214 TODO: Say something about uniqueness of identifiers
216 \subsection{Builtin expressions}
217 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
219 \startitemize[m,inmargin]
221 $tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
222 where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
223 e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
224 be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
225 \item TODO: Many more!
228 \section{Transformation passes}
230 In this section we describe the actual transformations. Here we're using
231 mostly Core-like notation, with a few notable points.
234 \item A core expression (in contrast with a transformation function, for
235 example), is enclosed in pipes. For example, $\app{transform}{\expr{\lam{z}{z+1}}}$
236 is the transform function applied to a lambda core expression.
238 Note that this notation might not be consistently applied everywhere. In
239 particular where a non-core function is used inside a core expression, things
240 get slightly confusing.
241 \item A bind is written as $\expr{\bind{x}{expr}}$. This means binding the identifier
242 $x$ to the expression $expr$.
243 \item In the core examples, the layout rule from Haskell is loosely applied.
244 It should be evident what was meant from indentation, even though it might nog
249 In the descriptions of transformations below, the following (slightly
250 contrived) example program will be used as the running example. Note that this
251 the example for the canonical form given above is the same program, but in
270 \subsection{Argument extraction}
271 This transformation makes sure that all of a bindings arguments are always
272 bound to variables at the top level of the bound value. Formally, we can
273 describe this transformation as follows.
275 \transform{Argument extraction}
277 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
279 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
280 \NC \app{transform'}{\expr{expr :: a \xrightarrow b}} \NC = \expr{\lam{x}{\app{transform'}{\expr{(\app{expr}{x})}}}} \NR
283 When applying this transformation to our running example, we get the following
304 foo = \x -> case x of True -> (\y -> mul y y); False -> id
307 foo = \x z -> (case x of True -> (\y -> mul y y); False -> id) z
310 \transexampleh{Argument extraction example}{from}{to}
312 \subsection{Application propagation}
313 This transformation is meant to propagate application expressions downwards
314 into expressions as far as possible. Formally, we can describe this
315 transformation as follows.
317 \transform{Application propagation}
319 \NC \app{transform}{\expr{\app{(\letexpr{binds}{expr})}{y}}} \NC = \expr{\letexpr{binds}{(\app{expr}{y})}}\NR
320 \NC \app{transform}{\expr{\app{(\lam{x}{expr})}{y}}} \NC = \app{\app{subs}{x \xRightarrow y}}{\expr{expr}}\NR
321 \NC \app{transform}{\expr{\app{(\case{x}{\alt{p}{e};...})}{y}}} \NC = \expr{\case{x}{\alt{p}{\app{e}{y}};...}}\;(for\;every\;alt)\NR
324 When applying this transformation to our running example, we get the following
344 foo = \x z -> (case x of True -> (\y -> mul y y); False -> id) z
347 foo = \x z -> case x of True -> mul z z; False -> id z
350 \transexampleh{Application propagation example}{from}{to}
352 \subsection{Introducing main scope}
353 This transformation is meant to introduce a single let expression that will be
354 the "main scope". This is the let expression as described under requirement
355 \ref[letexpr]. This let expression will contain only a single binding, which
356 binds the original expression to some identifier and then evalutes to just
357 this identifier (to comply with requirement \in[retexpr]).
359 Formally, we can describe the transformation as follows.
361 \transform{Main scope introduction}
363 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
365 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
366 \NC \app{transform'}{\expr{expr}} \NC = \expr{\letexpr{\bind{x}{expr}}{x}} \NR
369 When applying this transformation to our running example, we get the following
374 let r = (let s = foo x
391 \subsection{Scope flattening}
392 This transformation tries to flatten the topmost let expression in a bind,
393 {\em i.e.}, bind all identifiers in the same scope, and bind them to simple
394 expressions only (so simplify deeply nested expressions).
396 Formally, we can describe the transformation as follows.
398 \transform{Main scope introduction} { \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
400 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
401 \NC \app{transform'}{\expr{\letexpr{binds}{expr}}} \NC = \expr{\letexpr{\app{concat . map . flatten}{binds}}{expr}}\NR
403 \NC \app{flatten}{\expr{\bind{x}{\letexpr{binds}{expr}}}} \NC = (\app{concat . map . flatten}{binds}) \cup \{\app{flatten}{\expr{\bind{x}{expr}}}\}\NR
404 \NC \app{flatten}{\expr{\bind{x}{\case{s}{alts}}}} \NC = \app{concat}{binds'} \cup \{\bind{x}{\case{s}{alts'}}\}\NR
405 \NC \NC \where{(binds', alts')=\app{unzip.map.(flattenalt s)}{alts}}\NR
406 \NC \app{\app{flattenalt}{s}}{\expr{\alt{\app{con}{x_0\;..\;x_n}}{expr}}} \NC = (extracts \cup \{\app{flatten}{bind}\}, alt)\NR
407 \NC \NC \where{extracts =\{\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_0}}},}\NR
408 \NC \NC \;..\;,\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_n}}}\} \NR
409 \NC \NC bind = \expr{\bind{y}{expr}}\NR
410 \NC \NC alt = \expr{\alt{\app{con}{\_\;..\;\_}}{y}}\NR
413 When applying this transformation to our running example, we get the following
421 a = case s of (a, b) -> a
422 b = case s of (a, b) -> b
437 \subsection{More transformations}
438 As noted before, the above transformations are not complete. Other needed
439 transformations include:
441 \item Inlining of local identifiers with a function type. Since these cannot
442 be represented in hardware directly, they must be transformed into something
443 else. Inlining them should always be possible without loss of semantics (TODO:
444 How true is this?) and can expose new possibilities for other transformations
445 passes (such as application propagation when inlining {\tt j} above).
446 \item A variation on inlining local identifiers is the propagation of
447 function arguments with a function type. This will probably be initiated when
448 transforming the caller (and not the callee), but it will also deal with
449 identifiers with a function type that are unrepresentable in hardware.
451 Special care must be taken here, since the expression that is propagated into
452 the callee comes from a different scope. The function typed argument must thus
453 be replaced by any identifiers from the callers scope that the propagated
456 Note that propagating an argument will change both a function's interface and
457 implementation. For this to work, a new function should be created instead of
458 modifying the original function, so any other callers will not be broken.
459 \item Something similar should happen with return values with function types.
460 \item Polymorphism must be removed from all user-defined functions. This is
461 again similar to propagation function typed arguments, since this will also
462 create duplicates of functions (for a specific type). This is an operation
463 that is commonly known as "specialization" and already happens in GHC (since
464 non-polymorph functions can be a lot faster than generic ones).
465 \item More builtin expressions should be added and these should be evaluated
466 by the compiler. For example, map, fold, +.
487 After top-level η-abstraction:
506 After (extended) β-reduction:
524 After return value extraction:
543 Scrutinee simplification does not apply.
545 After case binder wildening:
550 a = case s of (a, _) -> a
551 b = case s of (_, b) -> b
552 r = case s of (_, _) ->
555 Low -> let op' = case b of
564 After case value simplification
569 a = case s of (a, _) -> a
570 b = case s of (_, b) -> b
571 r = case s of (_, _) -> r'
573 rl = let rll = λc.λd.c
586 After let flattening:
591 a = case s of (a, _) -> a
592 b = case s of (_, b) -> b
593 r = case s of (_, _) -> r'
607 After function inlining:
612 a = case s of (a, _) -> a
613 b = case s of (_, b) -> b
614 r = case s of (_, _) -> r'
626 After (extended) β-reduction again:
631 a = case s of (a, _) -> a
632 b = case s of (_, b) -> b
633 r = case s of (_, _) -> r'
645 After case value simplification again:
650 a = case s of (a, _) -> a
651 b = case s of (_, b) -> b
652 r = case s of (_, _) -> r'
670 a = case s of (a, _) -> a
671 b = case s of (_, b) -> b
685 After let bind removal:
690 a = case s of (a, _) -> a
691 b = case s of (_, b) -> b
704 Application simplification is not applicable.