Core2Core.tex

   1 \mainlanguage [en]
   2 \setuppapersize[A4][A4]
   3
   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
   6 % elegant...
   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]
  13 \stoptypescript
  14 \usetypescript [Custom]
  15
  16 % Use our custom typeface
  17 \switchtotypeface [Custom] [10pt]
  18
  19 % The function application operator, which expands to a space in math mode
  20 \define[1]\expr{|#1|}
  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}
  28 % A transformation
  29 \definefloat[transformation][transformations]
  30 \define[2]\transform{
  31   %\placetransformation[here]{#1}
  32   \startframedtext[width=\textwidth]
  33   \startformula \startalign
  34   #2
  35   \stopalign \stopformula
  36   \stopframedtext
  37 }
  38
  39 % A helper to print a single example in the half the page width. The example
  40 % text should be in a buffer whose name is given in an argument.
  41 %
  42 % The align=right option really does left-alignment, but without the program
  43 % will end up on a single line. The strut=no option prevents a bunch of empty
  44 % space at the start of the frame.
  45 \define[1]\example{\framed[frameoffset=2mm,align=right,strut=no]{\typebuffer[#1]}}
  46
  47 % A transformation example
  48 \definefloat[example][examples]
  49 \setupcaption[example][location=top] % Put captions on top
  50
  51 \define[3]\transexample{
  52   \placeexample[here]{#1}
  53   \startcombination[2*1]
  54     {\example{#2}}{Original program}
  55     {\example{#3}}{Transformed program}
  56   \stopcombination
  57 }
  58
  59 \define[3]\transexampleh{
  60   \placeexample[here]{#1}
  61   \startcombination[1*2]
  62     {\example{#2}}{Original program}
  63     {\example{#3}}{Transformed program}
  64   \stopcombination
  65 }
  66
  67 % Define a custom description format for the builtinexprs below
  68 \definedescription[builtindesc][headstyle=bold,style=normal,location=top]
  69
  70 \starttext
  71 \title {Core transformations for hardware generation}
  72 Matthijs Kooijman
  73
  74 \section{Introduction}
  75 As a new approach to translating Core to VHDL, we investigate a number of
  76 transformations on our Core program, which should bring the program into a
  77 well-defined "canonical" form, which is subsequently trivial to translate to
  78 VHDL.
  79
  80 The transformations as presented here are far from complete, but are meant as
  81 an exploration of possible transformations. In the running example below, we
  82 apply each of the transformations exactly once, in sequence. As will be
  83 apparent from the end result, there will be additional transformations needed
  84 to fully reach our goal, and some transformations must be applied more than
  85 once. How exactly to (efficiently) do this, has not been investigated.
  86
  87 Lastly, I hope to be able to state a number of pre- and postconditions for
  88 each transformation. If these can be proven for each transformation, and it
  89 can be shown that there exists some ordering of transformations for which the
  90 postcondition implies the canonical form, we can show that the transformations
  91 do indeed transform any program (probably satisfying a number of
  92 preconditions) to the canonical form.
  93
  94 \section{Goal}
  95 The transformations described here have a well-defined goal: To bring the
  96 program in a well-defined form that is directly translatable to hardware,
  97 while fully preserving the semantics of the program.
  98
  99 This {\em canonical form} is again a Core program, but with a very specific
 100 structure. A function in canonical form has nested lambda's at the top, which
 101 produce a let expression. This let expression binds every function application
 102 in the function and produces either a simple identifier or a tuple of
 103 identifiers. Every bound value in the let expression is either a simple
 104 function application or a case expression to extract a single element from a
 105 tuple returned by a function.
 106
 107 An example of a program in canonical form would be:
 108
 109 \starttyping
 110   -- All arguments are an inital lambda
 111   \x c d ->
 112   -- There is one let expression at the top level
 113   let
 114     -- Calling some other user-defined function.
 115     s = foo x
 116     -- Extracting result values from a tuple
 117     a = case s of (a, b) -> a
 118     b = case s of (a, b) -> b
 119     -- Some builtin expressions
 120     rh = add c d
 121     rhh = sub d c
 122     -- Conditional connections
 123     rl = case b of
 124       High -> rhh
 125       Low -> d
 126     r = case a of
 127       High -> rh
 128       Low -> rl
 129   in
 130     -- The actual result
 131     r
 132 \stoptyping
 133
 134 In this and all following programs, the following definitions are assumed to
 135 be available:
 136
 137 \starttyping
 138 data Bit = Low | High
 139
 140 foo :: Int -> (Bit, Bit)
 141 add :: Int -> Int -> Int
 142 sub :: Int -> Int -> Int
 143 \stoptyping
 144
 145 When looking at such a program from a hardware perspective, the top level
 146 lambda's define the input ports. The value produced by the let expression are
 147 the output ports. Each function application bound by the let expression
 148 defines a component instantiation, where the input and output ports are mapped
 149 to local signals or arguments. The tuple extracting case expressions don't map
 150 to
 151
 152 \subsection{Canonical form definition}
 153 Formally, the canonical form is a core program obeying the following
 154 constraints.
 155
 156 \startitemize[R,inmargin]
 157 \item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
 158 $fun$ is an identifier that will be bound as a global identifier.
 159 \item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
 160 $\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
 161 \item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
 162 \item $letbinds$ is a list with elements of the form
 163 $\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
 164 an identifier that will be bound as local identifier. The type of the bound
 165 value must be a $hardware\;type$.
 166 \item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
 167 equivalent VHDL expression. Since there are many supported forms for this,
 168 these are defined in a separate table.
 169 \item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
 170 where $fun$ is a global identifier and $x$ is a local identifier.
 171 \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
 172 be of a $hardware\;type$.
 173 \item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
 174 where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
 175 a local identifier.
 176 \item A $hardware\;type$ is a type that can be directly translated to
 177 hardware. This includes the types $Bit$, $SizedWord$, tuples containing
 178 elements of $hardware\;type$s, and will include others. This explicitely
 179 excludes function types.
 180 \stopitemize
 181
 182 TODO: Say something about uniqueness of identifiers
 183
 184 \subsection{Builtin expressions}
 185 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
 186
 187 \startitemize[m,inmargin]
 188 \item
 189 $tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
 190 where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
 191 e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
 192 be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
 193 \item TODO: Many more!
 194 \stopitemize
 195
 196 \section{Transformation passes}
 197
 198 In this section we describe the actual transformations. Here we're using
 199 mostly Core-like notation, with a few notable points.
 200
 201 \startitemize
 202 \item A core expression (in contrast with a transformation function, for
 203 example), is enclosed in pipes. For example, $\app{transform}{\expr{\lam{z}{z+1}}}$
 204 is the transform function applied to a lambda core expression.
 205
 206 Note that this notation might not be consistently applied everywhere. In
 207 particular where a non-core function is used inside a core expression, things
 208 get slightly confusing.
 209 \item A bind is written as $\expr{\bind{x}{expr}}$. This means binding the identifier
 210 $x$ to the expression $expr$.
 211 \item In the core examples, the layout rule from Haskell is loosely applied.
 212 It should be evident what was meant from indentation, even though it might nog
 213 be strictly correct.
 214 \stopitemize
 215
 216 \subsection{Example}
 217 In the descriptions of transformations below, the following (slightly
 218 contrived) example program will be used as the running example. Note that this
 219 the example for the canonical form given above is the same program, but in
 220 canonical form.
 221
 222 \starttyping
 223   \x ->
 224     let s = foo x
 225     in
 226       case s of
 227         (a, b) ->
 228           case a of
 229             High -> add
 230             Low -> let
 231               op' = case b of
 232                 High -> sub
 233                 Low  -> \c d -> c
 234               in
 235                 \c d -> op' d c
 236 \stoptyping
 237
 238 \subsection{Argument extraction}
 239 This transformation makes sure that all of a bindings arguments are always
 240 bound to variables at the top level of the bound value. Formally, we can
 241 describe this transformation as follows.
 242
 243 \transform{Argument extraction}
 244 {
 245 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
 246 \NR
 247 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
 248 \NC \app{transform'}{\expr{expr :: a \xrightarrow b}} \NC = \expr{\lam{x}{\app{transform'}{\expr{(\app{expr}{x})}}}} \NR
 249 }
 250
 251 When applying this transformation to our running example, we get the following
 252 program.
 253
 254 \starttyping
 255   \x c d ->
 256     (let s = foo x
 257     in
 258       case s of
 259         (a, b) ->
 260           case a of
 261             High -> add
 262             Low -> let
 263               op' = case b of
 264                 High -> sub
 265                 Low  -> \c d -> c
 266               in
 267                 \c d -> op' d c
 268     ) c d
 269 \stoptyping
 270
 271 \startbuffer[from]
 272 foo = \x -> case x of True -> (\y -> mul y y); False -> id
 273 \stopbuffer
 274 \startbuffer[to]
 275 foo = \x z -> (case x of True -> (\y -> mul y y); False -> id) z
 276 \stopbuffer
 277
 278 \transexampleh{Argument extraction example}{from}{to}
 279
 280 \subsection{Application propagation}
 281 This transformation is meant to propagate application expressions downwards
 282 into expressions as far as possible. Formally, we can describe this
 283 transformation as follows.
 284
 285 \transform{Application propagation}
 286 {
 287 \NC \app{transform}{\expr{\app{(\letexpr{binds}{expr})}{y}}} \NC = \expr{\letexpr{binds}{(\app{expr}{y})}}\NR
 288 \NC \app{transform}{\expr{\app{(\lam{x}{expr})}{y}}} \NC = \app{\app{subs}{x \xRightarrow y}}{\expr{expr}}\NR
 289 \NC \app{transform}{\expr{\app{(\case{x}{\alt{p}{e};...})}{y}}} \NC = \expr{\case{x}{\alt{p}{\app{e}{y}};...}}\;(for\;every\;alt)\NR
 290 }
 291
 292 When applying this transformation to our running example, we get the following
 293 program.
 294
 295 \starttyping
 296   \x c d ->
 297     let s = foo x
 298     in
 299       case s of
 300         (a, b) ->
 301           case a of
 302             High -> add c d
 303             Low -> let
 304               op' = case b of
 305                 High -> sub
 306                 Low  -> \c d -> c
 307               in
 308                 op' d c
 309 \stoptyping
 310
 311 \startbuffer[from]
 312 foo = \x z -> (case x of True -> (\y -> mul y y); False -> id) z
 313 \stopbuffer
 314 \startbuffer[to]
 315 foo = \x z -> case x of True -> mul z z; False -> id z
 316 \stopbuffer
 317
 318 \transexampleh{Application propagation example}{from}{to}
 319
 320 \subsection{Introducing main scope}
 321 This transformation is meant to introduce a single let expression that will be
 322 the "main scope". This is the let expression as described under requirement
 323 \ref[letexpr]. This let expression will contain only a single binding, which
 324 binds the original expression to some identifier and then evalutes to just
 325 this identifier (to comply with requirement \in[retexpr]).
 326
 327 Formally, we can describe the transformation as follows.
 328
 329 \transform{Main scope introduction}
 330 {
 331 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
 332 \NR
 333 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
 334 \NC \app{transform'}{\expr{expr}} \NC = \expr{\letexpr{\bind{x}{expr}}{x}} \NR
 335 }
 336
 337 When applying this transformation to our running example, we get the following
 338 program.
 339
 340 \starttyping
 341   \x c d ->
 342     let r = (let s = foo x
 343               in
 344                 case s of
 345                   (a, b) ->
 346                     case a of
 347                       High -> add c d
 348                       Low -> let
 349                         op' = case b of
 350                           High -> sub
 351                           Low  -> \c d -> c
 352                         in
 353                           op' d c
 354             )
 355     in
 356       r
 357 \stoptyping
 358
 359 \subsection{Scope flattening}
 360 This transformation tries to flatten the topmost let expression in a bind,
 361 {\em i.e.}, bind all identifiers in the same scope, and bind them to simple
 362 expressions only (so simplify deeply nested expressions).
 363
 364 Formally, we can describe the transformation as follows.
 365
 366 \transform{Main scope introduction} { \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
 367 \NR
 368 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
 369 \NC \app{transform'}{\expr{\letexpr{binds}{expr}}} \NC = \expr{\letexpr{\app{concat . map . flatten}{binds}}{expr}}\NR
 370 \NR
 371 \NC \app{flatten}{\expr{\bind{x}{\letexpr{binds}{expr}}}} \NC = (\app{concat . map . flatten}{binds}) \cup \{\app{flatten}{\expr{\bind{x}{expr}}}\}\NR
 372 \NC \app{flatten}{\expr{\bind{x}{\case{s}{alts}}}} \NC = \app{concat}{binds'} \cup \{\bind{x}{\case{s}{alts'}}\}\NR
 373 \NC                                                \NC  \where{(binds', alts')=\app{unzip.map.(flattenalt s)}{alts}}\NR
 374 \NC \app{\app{flattenalt}{s}}{\expr{\alt{\app{con}{x_0\;..\;x_n}}{expr}}} \NC = (extracts \cup \{\app{flatten}{bind}\}, alt)\NR
 375 \NC \NC \where{extracts =\{\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_0}}},}\NR
 376 \NC \NC \;..\;,\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_n}}}\} \NR
 377 \NC \NC bind = \expr{\bind{y}{expr}}\NR
 378 \NC \NC alt = \expr{\alt{\app{con}{\_\;..\;\_}}{y}}\NR
 379 }
 380
 381 When applying this transformation to our running example, we get the following
 382 program.
 383
 384 \starttyping
 385   \x c d ->
 386     let s = foo x
 387         r = case s of
 388               (_, _) -> y
 389         a = case s of (a, b) -> a
 390         b = case s of (a, b) -> b
 391         y = case a of
 392               High -> g
 393               Low -> h
 394         g = add c d
 395         h = op' d c
 396         op' = case b of
 397           High -> i
 398           Low  -> j
 399         i = sub
 400         j = \c d -> c
 401     in
 402       r
 403 \stoptyping
 404
 405 \subsection{More transformations}
 406 As noted before, the above transformations are not complete. Other needed
 407 transformations include:
 408 \startitemize
 409 \item Inlining of local identifiers with a function type. Since these cannot
 410 be represented in hardware directly, they must be transformed into something
 411 else. Inlining them should always be possible without loss of semantics (TODO:
 412 How true is this?) and can expose new possibilities for other transformations
 413 passes (such as application propagation when inlining {\tt j} above).
 414 \item A variation on inlining local identifiers is the propagation of
 415 function arguments with a function type. This will probably be initiated when
 416 transforming the caller (and not the callee), but it will also deal with
 417 identifiers with a function type that are unrepresentable in hardware.
 418
 419 Special care must be taken here, since the expression that is propagated into
 420 the callee comes from a different scope. The function typed argument must thus
 421 be replaced by any identifiers from the callers scope that the propagated
 422 expression uses.
 423
 424 Note that propagating an argument will change both a function's interface and
 425 implementation. For this to work, a new function should be created instead of
 426 modifying the original function, so any other callers will not be broken.
 427 \item Something similar should happen with return values with function types.
 428 \item Polymorphism must be removed from all user-defined functions. This is
 429 again similar to propagation function typed arguments, since this will also
 430 create duplicates of functions (for a specific type). This is an operation
 431 that is commonly known as "specialization" and already happens in GHC (since
 432 non-polymorph functions can be a lot faster than generic ones).
 433 \item More builtin expressions should be added and these should be evaluated
 434 by the compiler. For example, map, fold, +.
 435 \stopitemize
 436 \stoptext