Core2Core.tex

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