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 % Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
  40 \installprettytype [LAM] [LAM]
  41
  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.
  44 %
  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]}}
  49
  50 % A transformation example
  51 \definefloat[example][examples]
  52 \setupcaption[example][location=top] % Put captions on top
  53
  54 \define[3]\transexample{
  55   \placeexample[here]{#1}
  56   \startcombination[2*1]
  57     {\example{#2}}{Original program}
  58     {\example{#3}}{Transformed program}
  59   \stopcombination
  60 }
  61
  62 \define[3]\transexampleh{
  63   \placeexample[here]{#1}
  64   \startcombination[1*2]
  65     {\example{#2}}{Original program}
  66     {\example{#3}}{Transformed program}
  67   \stopcombination
  68 }
  69
  70 % Define a custom description format for the builtinexprs below
  71 \definedescription[builtindesc][headstyle=bold,style=normal,location=top]
  72
  73 \starttext
  74 \title {Core transformations for hardware generation}
  75 Matthijs Kooijman
  76
  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
  81 VHDL.
  82
  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.
  89
  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.
  96
  97 \section{Goal}
  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.
 101
 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.
 109
 110 An example of a program in canonical form would be:
 111
 112 \starttyping
 113   -- All arguments are an inital lambda
 114   \x c d ->
 115   -- There is one let expression at the top level
 116   let
 117     -- Calling some other user-defined function.
 118     s = foo x
 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
 123     rh = add c d
 124     rhh = sub d c
 125     -- Conditional connections
 126     rl = case b of
 127       High -> rhh
 128       Low -> d
 129     r = case a of
 130       High -> rh
 131       Low -> rl
 132   in
 133     -- The actual result
 134     r
 135 \stoptyping
 136
 137 In this and all following programs, the following definitions are assumed to
 138 be available:
 139
 140 \starttyping
 141 data Bit = Low | High
 142
 143 foo :: Int -> (Bit, Bit)
 144 add :: Int -> Int -> Int
 145 sub :: Int -> Int -> Int
 146 \stoptyping
 147
 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
 153 to
 154
 155 \subsection{Canonical form definition}
 156 Formally, the canonical form is a core program obeying the following
 157 constraints.
 158
 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
 178 a local identifier.
 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.
 183 \stopitemize
 184
 185 TODO: Say something about uniqueness of identifiers
 186
 187 \subsection{Builtin expressions}
 188 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
 189
 190 \startitemize[m,inmargin]
 191 \item
 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!
 197 \stopitemize
 198
 199 \section{Transformation passes}
 200
 201 In this section we describe the actual transformations. Here we're using
 202 mostly Core-like notation, with a few notable points.
 203
 204 \startitemize
 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.
 208
 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
 216 be strictly correct.
 217 \stopitemize
 218
 219 \subsection{Example}
 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
 223 canonical form.
 224
 225 \starttyping
 226   \x ->
 227     let s = foo x
 228     in
 229       case s of
 230         (a, b) ->
 231           case a of
 232             High -> add
 233             Low -> let
 234               op' = case b of
 235                 High -> sub
 236                 Low  -> \c d -> c
 237               in
 238                 \c d -> op' d c
 239 \stoptyping
 240
 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.
 245
 246 \transform{Argument extraction}
 247 {
 248 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
 249 \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
 252 }
 253
 254 When applying this transformation to our running example, we get the following
 255 program.
 256
 257 \starttyping
 258   \x c d ->
 259     (let s = foo x
 260     in
 261       case s of
 262         (a, b) ->
 263           case a of
 264             High -> add
 265             Low -> let
 266               op' = case b of
 267                 High -> sub
 268                 Low  -> \c d -> c
 269               in
 270                 \c d -> op' d c
 271     ) c d
 272 \stoptyping
 273
 274 \startbuffer[from]
 275 foo = \x -> case x of True -> (\y -> mul y y); False -> id
 276 \stopbuffer
 277 \startbuffer[to]
 278 foo = \x z -> (case x of True -> (\y -> mul y y); False -> id) z
 279 \stopbuffer
 280
 281 \transexampleh{Argument extraction example}{from}{to}
 282
 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.
 287
 288 \transform{Application propagation}
 289 {
 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
 293 }
 294
 295 When applying this transformation to our running example, we get the following
 296 program.
 297
 298 \starttyping
 299   \x c d ->
 300     let s = foo x
 301     in
 302       case s of
 303         (a, b) ->
 304           case a of
 305             High -> add c d
 306             Low -> let
 307               op' = case b of
 308                 High -> sub
 309                 Low  -> \c d -> c
 310               in
 311                 op' d c
 312 \stoptyping
 313
 314 \startbuffer[from]
 315 foo = \x z -> (case x of True -> (\y -> mul y y); False -> id) z
 316 \stopbuffer
 317 \startbuffer[to]
 318 foo = \x z -> case x of True -> mul z z; False -> id z
 319 \stopbuffer
 320
 321 \transexampleh{Application propagation example}{from}{to}
 322
 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]).
 329
 330 Formally, we can describe the transformation as follows.
 331
 332 \transform{Main scope introduction}
 333 {
 334 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
 335 \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
 338 }
 339
 340 When applying this transformation to our running example, we get the following
 341 program.
 342
 343 \starttyping
 344   \x c d ->
 345     let r = (let s = foo x
 346               in
 347                 case s of
 348                   (a, b) ->
 349                     case a of
 350                       High -> add c d
 351                       Low -> let
 352                         op' = case b of
 353                           High -> sub
 354                           Low  -> \c d -> c
 355                         in
 356                           op' d c
 357             )
 358     in
 359       r
 360 \stoptyping
 361
 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).
 366
 367 Formally, we can describe the transformation as follows.
 368
 369 \transform{Main scope introduction} { \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
 370 \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
 373 \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
 382 }
 383
 384 When applying this transformation to our running example, we get the following
 385 program.
 386
 387 \starttyping
 388   \x c d ->
 389     let s = foo x
 390         r = case s of
 391               (_, _) -> y
 392         a = case s of (a, b) -> a
 393         b = case s of (a, b) -> b
 394         y = case a of
 395               High -> g
 396               Low -> h
 397         g = add c d
 398         h = op' d c
 399         op' = case b of
 400           High -> i
 401           Low  -> j
 402         i = sub
 403         j = \c d -> c
 404     in
 405       r
 406 \stoptyping
 407
 408 \subsection{More transformations}
 409 As noted before, the above transformations are not complete. Other needed
 410 transformations include:
 411 \startitemize
 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.
 421
 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
 425 expression uses.
 426
 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, +.
 438 \stopitemize
 439 \stoptext