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   \startframedtext[width=\textwidth]
  32   #2
  33   \stopframedtext
  34 }
  35
  36 \define\conclusion{\blackrule[height=0.5pt,depth=0pt,width=.5\textwidth]}
  37 \define\nextrule{\vskip1cm}
  38
  39 \define[2]\transformold{
  40   %\placetransformation[here]{#1}
  41   \startframedtext[width=\textwidth]
  42   \startformula \startalign
  43   #2
  44   \stopalign \stopformula
  45   \stopframedtext
  46 }
  47
  48 % A shortcut for italicized e.g.
  49 \define[0]\eg{{\em e.g.}}
  50
  51 % Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
  52 \installprettytype [LAM] [LAM]
  53
  54 \definetyping[lambda][option=LAM,style=sans]
  55 \definetype[lam][option=LAM,style=sans]
  56
  57 % An (invisible) frame to hold a lambda expression
  58 \define[1]\lamframe{
  59         % Put a frame around lambda expressions, so they can have multiple
  60         % lines and still appear inline.
  61         % The align=right option really does left-alignment, but without the
  62         % program will end up on a single line. The strut=no option prevents a
  63         % bunch of empty space at the start of the frame.
  64         \framed[offset=0mm,location=middle,strut=no,align=right,frame=off]{#1}
  65 }
  66
  67 \define[2]\transbuf{
  68         % Make \typebuffer uses the LAM pretty printer and a sans-serif font
  69         % Also prevent any extra spacing above and below caused by the default
  70         % before=\blank and after=\blank.
  71         \setuptyping[option=LAM,style=sans,before=,after=]
  72         % Prevent the arrow from ending up below the first frame (a \framed
  73         % at the start of a line defaults to using vmode).
  74         \dontleavehmode
  75         % Put the elements in frames, so they can have multiple lines and be
  76         % middle-aligned
  77         \lamframe{\typebuffer[#1]}
  78         \lamframe{\Rightarrow}
  79         \lamframe{\typebuffer[#2]}
  80         % Reset the typing settings to their defaults
  81         \setuptyping[option=none,style=\tttf]
  82 }
  83 % This is the same as \transbuf above, but it accepts text directly instead
  84 % of through buffers. This only works for single lines, however.
  85 \define[2]\trans{
  86         \dontleavehmode
  87         \lamframe{\lam{#1}}
  88         \lamframe{\Rightarrow}
  89         \lamframe{\lam{#2}}
  90 }
  91
  92
  93 % A helper to print a single example in the half the page width. The example
  94 % text should be in a buffer whose name is given in an argument.
  95 %
  96 % The align=right option really does left-alignment, but without the program
  97 % will end up on a single line. The strut=no option prevents a bunch of empty
  98 % space at the start of the frame.
  99 \define[1]\example{
 100   \framed[offset=1mm,align=right,strut=no]{
 101     \setuptyping[option=LAM,style=sans,before=,after=]
 102     \typebuffer[#1]
 103     \setuptyping[option=none,style=\tttf]
 104   }
 105 }
 106
 107
 108 % A transformation example
 109 \definefloat[example][examples]
 110 \setupcaption[example][location=top] % Put captions on top
 111
 112 \define[3]\transexample{
 113   \placeexample[here]{#1}
 114   \startcombination[2*1]
 115     {\example{#2}}{Original program}
 116     {\example{#3}}{Transformed program}
 117   \stopcombination
 118 }
 119
 120 \define[3]\transexampleh{
 121 %  \placeexample[here]{#1}
 122 %  \startcombination[1*2]
 123 %    {\example{#2}}{Original program}
 124 %    {\example{#3}}{Transformed program}
 125 %  \stopcombination
 126 }
 127
 128 % Define a custom description format for the builtinexprs below
 129 \definedescription[builtindesc][headstyle=bold,style=normal,location=top]
 130
 131 \starttext
 132 \title {Core transformations for hardware generation}
 133 Matthijs Kooijman
 134
 135 \section{Introduction}
 136 As a new approach to translating Core to VHDL, we investigate a number of
 137 transformations on our Core program, which should bring the program into a
 138 well-defined "canonical" form, which is subsequently trivial to translate to
 139 VHDL.
 140
 141 The transformations as presented here are far from complete, but are meant as
 142 an exploration of possible transformations. In the running example below, we
 143 apply each of the transformations exactly once, in sequence. As will be
 144 apparent from the end result, there will be additional transformations needed
 145 to fully reach our goal, and some transformations must be applied more than
 146 once. How exactly to (efficiently) do this, has not been investigated.
 147
 148 Lastly, I hope to be able to state a number of pre- and postconditions for
 149 each transformation. If these can be proven for each transformation, and it
 150 can be shown that there exists some ordering of transformations for which the
 151 postcondition implies the canonical form, we can show that the transformations
 152 do indeed transform any program (probably satisfying a number of
 153 preconditions) to the canonical form.
 154
 155 \section{Goal}
 156 The transformations described here have a well-defined goal: To bring the
 157 program in a well-defined form that is directly translatable to hardware,
 158 while fully preserving the semantics of the program.
 159
 160 This {\em canonical form} is again a Core program, but with a very specific
 161 structure. A function in canonical form has nested lambda's at the top, which
 162 produce a let expression. This let expression binds every function application
 163 in the function and produces either a simple identifier or a tuple of
 164 identifiers. Every bound value in the let expression is either a simple
 165 function application or a case expression to extract a single element from a
 166 tuple returned by a function.
 167
 168 An example of a program in canonical form would be:
 169
 170 \starttyping
 171   -- All arguments are an inital lambda
 172   \x c d ->
 173   -- There is one let expression at the top level
 174   let
 175     -- Calling some other user-defined function.
 176     s = foo x
 177     -- Extracting result values from a tuple
 178     a = case s of (a, b) -> a
 179     b = case s of (a, b) -> b
 180     -- Some builtin expressions
 181     rh = add c d
 182     rhh = sub d c
 183     -- Conditional connections
 184     rl = case b of
 185       High -> rhh
 186       Low -> d
 187     r = case a of
 188       High -> rh
 189       Low -> rl
 190   in
 191     -- The actual result
 192     r
 193 \stoptyping
 194
 195 In this and all following programs, the following definitions are assumed to
 196 be available:
 197
 198 \starttyping
 199 data Bit = Low | High
 200
 201 foo :: Int -> (Bit, Bit)
 202 add :: Int -> Int -> Int
 203 sub :: Int -> Int -> Int
 204 \stoptyping
 205
 206 When looking at such a program from a hardware perspective, the top level
 207 lambda's define the input ports. The value produced by the let expression are
 208 the output ports. Each function application bound by the let expression
 209 defines a component instantiation, where the input and output ports are mapped
 210 to local signals or arguments. The tuple extracting case expressions don't map
 211 to
 212
 213 \subsection{Canonical form definition}
 214 Formally, the canonical form is a core program obeying the following
 215 constraints.
 216
 217 \startitemize[R,inmargin]
 218 \item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
 219 $fun$ is an identifier that will be bound as a global identifier.
 220 \item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
 221 $\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
 222 \item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
 223 \item $letbinds$ is a list with elements of the form
 224 $\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
 225 an identifier that will be bound as local identifier. The type of the bound
 226 value must be a $hardware\;type$.
 227 \item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
 228 equivalent VHDL expression. Since there are many supported forms for this,
 229 these are defined in a separate table.
 230 \item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
 231 where $fun$ is a global identifier and $x$ is a local identifier.
 232 \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
 233 be of a $hardware\;type$.
 234 \item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
 235 where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
 236 a local identifier.
 237 \item A $hardware\;type$ is a type that can be directly translated to
 238 hardware. This includes the types $Bit$, $SizedWord$, tuples containing
 239 elements of $hardware\;type$s, and will include others. This explicitely
 240 excludes function types.
 241 \stopitemize
 242
 243 TODO: Say something about uniqueness of identifiers
 244
 245 \subsection{Builtin expressions}
 246 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
 247
 248 \startitemize[m,inmargin]
 249 \item
 250 $tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
 251 where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
 252 e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
 253 be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
 254 \item TODO: Many more!
 255 \stopitemize
 256
 257 \section{Transformation passes}
 258
 259 In this section we describe the actual transformations. Here we're using
 260 mostly Core-like notation, with a few notable points.
 261
 262 \startitemize
 263 \item A core expression (in contrast with a transformation function, for
 264 example), is enclosed in pipes. For example, $\app{transform}{\expr{\lam{z}{z+1}}}$
 265 is the transform function applied to a lambda core expression.
 266
 267 Note that this notation might not be consistently applied everywhere. In
 268 particular where a non-core function is used inside a core expression, things
 269 get slightly confusing.
 270 \item A bind is written as $\expr{\bind{x}{expr}}$. This means binding the identifier
 271 $x$ to the expression $expr$.
 272 \item In the core examples, the layout rule from Haskell is loosely applied.
 273 It should be evident what was meant from indentation, even though it might nog
 274 be strictly correct.
 275 \stopitemize
 276
 277 \subsection{Example}
 278 In the descriptions of transformations below, the following (slightly
 279 contrived) example program will be used as the running example. Note that this
 280 the example for the canonical form given above is the same program, but in
 281 canonical form.
 282
 283 \starttyping
 284   \x ->
 285     let s = foo x
 286     in
 287       case s of
 288         (a, b) ->
 289           case a of
 290             High -> add
 291             Low -> let
 292               op' = case b of
 293                 High -> sub
 294                 Low  -> \c d -> c
 295               in
 296                 \c d -> op' d c
 297 \stoptyping
 298
 299 \subsection{η-abstraction}
 300 This transformation makes sure that all arguments of a function-typed
 301 expression are named, by introducing lambda expressions. When combined with
 302 β-reduction and function inlining below, all function-typed expressions should
 303 be lambda abstractions or global identifiers.
 304
 305 \transform{η-abstraction}
 306 {
 307 \lam{E :: * -> *}
 308
 309 \lam{E} is not the first argument of an application.
 310
 311 \lam{E} is not a lambda abstraction.
 312
 313 \lam{x} is a variable that does not occur free in E.
 314
 315 \conclusion
 316
 317 \trans{E}{λx.E x}
 318 }
 319
 320 \startbuffer[from]
 321 foo = λa -> case a of
 322   True -> λb.mul b b
 323   False -> id
 324 \stopbuffer
 325
 326 \startbuffer[to]
 327 foo = λa.λx -> (case a of
 328     True -> λb.mul b b
 329     False -> λy.id y) x
 330 \stopbuffer
 331
 332 \transexample{η-abstraction}{from}{to}
 333
 334 \subsection{Extended β-reduction}
 335 This transformation is meant to propagate application expressions downwards
 336 into expressions as far as possible. In lambda calculus, this reduction
 337 is known as β-reduction, but it is of course only defined for
 338 applications of lambda abstractions. We extend this reduction to also
 339 work for the rest of core (case and let expressions).
 340 \startbuffer[from]
 341 (case x of
 342   p1 -> E1
 343   \vdots
 344   pn -> En) M
 345 \stopbuffer
 346 \startbuffer[to]
 347 case x of
 348   p1 -> E1 M
 349   \vdots
 350   pn -> En M
 351 \stopbuffer
 352
 353 \transform{Extended β-reduction}
 354 {
 355 \conclusion
 356 \trans{(λx.E) M}{E[M/x]}
 357
 358 \nextrule
 359 \conclusion
 360 \trans{(let binds in E) M}{let binds in E M}
 361
 362 \nextrule
 363 \conclusion
 364 \transbuf{from}{to}
 365 }
 366
 367 \startbuffer[from]
 368 let a = (case x of
 369            True -> id
 370            False -> neg
 371         ) 1
 372     b = (let y = 3 in add y) 2
 373 in
 374   (λz.add 1 z) 3
 375 \stopbuffer
 376
 377 \startbuffer[to]
 378 let a = case x of
 379            True -> id 1
 380            False -> neg 1
 381     b = let y = 3 in add y 2
 382 in
 383   add 1 3
 384 \stopbuffer
 385
 386 \transexample{Extended β-reduction}{from}{to}
 387
 388 \subsection{Argument simplification}
 389 The transforms in this section deal with simplifying application
 390 arguments into normal form. The goal here is to:
 391
 392 \startitemize
 393  \item Make all arguments of user-defined functions (\eg, of which
 394  we have a function body) simple variable references of a runtime
 395  representable type.
 396  \item Make all arguments of builtin functions either:
 397    \startitemize
 398     \item A type argument.
 399     \item A dictionary argument.
 400     \item A type level expression.
 401     \item A variable reference of a runtime representable type.
 402     \item A variable reference or partial application of a function type.
 403    \stopitemize
 404 \stopitemize
 405
 406 \subsubsection{User-defined functions}
 407 We can divide the arguments of a user-defined function into two
 408 categories:
 409 \startitemize
 410   \item Runtime representable typed arguments (\eg bits or vectors).
 411   \item Non-runtime representable typed arguments.
 412 \stopitemize
 413
 414 The next two transformations will deal with each of these two kinds of argument respectively.
 415
 416 \subsubsubsection{Argument extraction}
 417 This transform deals with arguments to user-defined functions that
 418 are of a runtime representable type. These arguments can be preserved in
 419 the program, since they can be translated to input ports later on.
 420 However, since we can only connect signals to input ports, these
 421 arguments must be reduced to simple variables (for which signals will be
 422 produced).
 423
 424 TODO: It seems we can map an expression to a port, not only a signal.
 425 Perhaps this makes this transformation not needed?
 426 TODO: Say something about dataconstructors (without arguments, like True
 427 or False), which are variable references of a runtime representable
 428 type, but do not result in a signal.
 429
 430 To reduce a complex expression to a simple variable reference, we create
 431 a new let expression around the application, which binds the complex
 432 expression to a new variable. The original function is then applied to
 433 this variable.
 434
 435 \transform{Argument extract}
 436 {
 437 \lam{X} is a (partial application of) a user-defined function
 438
 439 \lam{Y} is of a hardware representable type
 440
 441 \lam{Y} is not a variable referene
 442
 443 \conclusion
 444
 445 \trans{X Y}{let z = Y in X z}
 446 }
 447 \subsubsubsection{Argument propagation}
 448 This transform deals with arguments to user-defined functions that are
 449 not representable at runtime. This means these arguments cannot be
 450 preserved in the final form and most be {\em propagated}.
 451
 452 Propagation means to create a specialized version of the called
 453 function, with the propagated argument already filled in. As a simple
 454 example, in the following program:
 455
 456 \startlambda
 457 f = λa.λb.a + b
 458 inc = λa.f a 1
 459 \stoplambda
 460
 461 we could {\em propagate} the constant argument 1, with the following
 462 result:
 463
 464 \startlambda
 465 f' = λa.a + 1
 466 inc = λa.f' a
 467 \stoplambda
 468
 469 Special care must be taken when the to-be-propagated expression has any
 470 free variables. If this is the case, the original argument should not be
 471 removed alltogether, but replaced by all the free variables of the
 472 expression. In this way, the original expression can still be evaluated
 473 inside the new function. Also, this brings us closer to our goal: All
 474 these free variables will be simple variable references.
 475
 476 To prevent us from propagating the same argument over and over, a simple
 477 local variable reference is not propagated (since is has exactly one
 478 free variable, itself, we would only replace that argument with itself).
 479
 480 This shows that any free local variables that are not runtime representable
 481 cannot be brought into normal form by this transform. We rely on an
 482 inlining transformation to replace such a variable with an expression we
 483 can propagate again.
 484
 485 TODO: Move these definitions somewhere sensible.
 486
 487 Definition: A global variable is any variable that is bound at the
 488 top level of a program. A local variable is any other variable.
 489
 490 Definition: A hardware representable type is a type that we can generate
 491 a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
 492 unsigned word, etc. Types that are not runtime representable notably
 493 include (but are not limited to): Types, dictionaries, functions.
 494
 495 Definition: A builtin function is a function for which a builtin
 496 hardware translation is available, because its actual definition is not
 497 translatable. A user-defined function is any other function.
 498
 499 \transform{Argument propagation}
 500 {
 501 \lam{x} is a global variable, bound to a user-defined function
 502
 503 \lam{x = E}
 504
 505 \lam{Y_i} is not of a runtime representable type
 506
 507 \lam{Y_i} is not a local variable reference
 508
 509 \conclusion
 510
 511 \lam{f0 ... fm} = free local vars of \lam{Y_i}
 512
 513 \lam{x'} is a new global variable
 514
 515 \lam{x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . E y0 ... yi-1 Yi yi+1 ... yn}
 516
 517 \trans{x Y0 ... Yi ... Yn}{x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn}
 518 }
 519
 520 TODO: The above definition looks too complicated... Can we find
 521 something more concise?
 522
 523 \subsubsection{Builtin functions}
 524
 525 argument categories:
 526
 527 function typed
 528
 529 type / dictionary / other
 530
 531 hardware representable
 532
 533 TODO
 534
 535 \subsection{Introducing main scope}
 536 This transformation is meant to introduce a single let expression that will be
 537 the "main scope". This is the let expression as described under requirement
 538 \ref[letexpr]. This let expression will contain only a single binding, which
 539 binds the original expression to some identifier and then evalutes to just
 540 this identifier (to comply with requirement \in[retexpr]).
 541
 542 Formally, we can describe the transformation as follows.
 543
 544 \transformold{Main scope introduction}
 545 {
 546 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
 547 \NR
 548 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
 549 \NC \app{transform'}{\expr{expr}} \NC = \expr{\letexpr{\bind{x}{expr}}{x}} \NR
 550 }
 551
 552 When applying this transformation to our running example, we get the following
 553 program.
 554
 555 \starttyping
 556   \x c d ->
 557     let r = (let s = foo x
 558               in
 559                 case s of
 560                   (a, b) ->
 561                     case a of
 562                       High -> add c d
 563                       Low -> let
 564                         op' = case b of
 565                           High -> sub
 566                           Low  -> \c d -> c
 567                         in
 568                           op' d c
 569             )
 570     in
 571       r
 572 \stoptyping
 573
 574 \subsection{Scope flattening}
 575 This transformation tries to flatten the topmost let expression in a bind,
 576 {\em i.e.}, bind all identifiers in the same scope, and bind them to simple
 577 expressions only (so simplify deeply nested expressions).
 578
 579 Formally, we can describe the transformation as follows.
 580
 581 \transformold{Main scope introduction} { \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
 582 \NR
 583 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
 584 \NC \app{transform'}{\expr{\letexpr{binds}{expr}}} \NC = \expr{\letexpr{\app{concat . map . flatten}{binds}}{expr}}\NR
 585 \NR
 586 \NC \app{flatten}{\expr{\bind{x}{\letexpr{binds}{expr}}}} \NC = (\app{concat . map . flatten}{binds}) \cup \{\app{flatten}{\expr{\bind{x}{expr}}}\}\NR
 587 \NC \app{flatten}{\expr{\bind{x}{\case{s}{alts}}}} \NC = \app{concat}{binds'} \cup \{\bind{x}{\case{s}{alts'}}\}\NR
 588 \NC                                                \NC  \where{(binds', alts')=\app{unzip.map.(flattenalt s)}{alts}}\NR
 589 \NC \app{\app{flattenalt}{s}}{\expr{\alt{\app{con}{x_0\;..\;x_n}}{expr}}} \NC = (extracts \cup \{\app{flatten}{bind}\}, alt)\NR
 590 \NC \NC \where{extracts =\{\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_0}}},}\NR
 591 \NC \NC \;..\;,\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_n}}}\} \NR
 592 \NC \NC bind = \expr{\bind{y}{expr}}\NR
 593 \NC \NC alt = \expr{\alt{\app{con}{\_\;..\;\_}}{y}}\NR
 594 }
 595
 596 When applying this transformation to our running example, we get the following
 597 program.
 598
 599 \starttyping
 600   \x c d ->
 601     let s = foo x
 602         r = case s of
 603               (_, _) -> y
 604         a = case s of (a, b) -> a
 605         b = case s of (a, b) -> b
 606         y = case a of
 607               High -> g
 608               Low -> h
 609         g = add c d
 610         h = op' d c
 611         op' = case b of
 612           High -> i
 613           Low  -> j
 614         i = sub
 615         j = \c d -> c
 616     in
 617       r
 618 \stoptyping
 619
 620 \subsection{More transformations}
 621 As noted before, the above transformations are not complete. Other needed
 622 transformations include:
 623 \startitemize
 624 \item Inlining of local identifiers with a function type. Since these cannot
 625 be represented in hardware directly, they must be transformed into something
 626 else. Inlining them should always be possible without loss of semantics (TODO:
 627 How true is this?) and can expose new possibilities for other transformations
 628 passes (such as application propagation when inlining {\tt j} above).
 629 \item A variation on inlining local identifiers is the propagation of
 630 function arguments with a function type. This will probably be initiated when
 631 transforming the caller (and not the callee), but it will also deal with
 632 identifiers with a function type that are unrepresentable in hardware.
 633
 634 Special care must be taken here, since the expression that is propagated into
 635 the callee comes from a different scope. The function typed argument must thus
 636 be replaced by any identifiers from the callers scope that the propagated
 637 expression uses.
 638
 639 Note that propagating an argument will change both a function's interface and
 640 implementation. For this to work, a new function should be created instead of
 641 modifying the original function, so any other callers will not be broken.
 642 \item Something similar should happen with return values with function types.
 643 \item Polymorphism must be removed from all user-defined functions. This is
 644 again similar to propagation function typed arguments, since this will also
 645 create duplicates of functions (for a specific type). This is an operation
 646 that is commonly known as "specialization" and already happens in GHC (since
 647 non-polymorph functions can be a lot faster than generic ones).
 648 \item More builtin expressions should be added and these should be evaluated
 649 by the compiler. For example, map, fold, +.
 650 \stopitemize
 651
 652 Initial example
 653
 654 \startlambda
 655   λx.
 656     let s = foo x
 657     in
 658       case s of
 659         (a, b) ->
 660           case a of
 661             High -> add
 662             Low -> let
 663               op' = case b of
 664                 High -> sub
 665                 Low  -> λc.λd.c
 666               in
 667                 λc.λd.op' d c
 668 \stoplambda
 669
 670 After top-level η-abstraction:
 671
 672 \startlambda
 673   λx.λc.λd.
 674     (let s = foo x
 675     in
 676       case s of
 677         (a, b) ->
 678           case a of
 679             High -> add
 680             Low -> let
 681               op' = case b of
 682                 High -> sub
 683                 Low  -> λc.λd.c
 684               in
 685                 λc.λd.op' d c
 686     ) c d
 687 \stoplambda
 688
 689 After (extended) β-reduction:
 690
 691 \startlambda
 692   λx.λc.λd.
 693     let s = foo x
 694     in
 695       case s of
 696         (a, b) ->
 697           case a of
 698             High -> add c d
 699             Low -> let
 700               op' = case b of
 701                 High -> sub
 702                 Low  -> λc.λd.c
 703               in
 704                 op' d c
 705 \stoplambda
 706
 707 After return value extraction:
 708
 709 \startlambda
 710   λx.λc.λd.
 711     let s = foo x
 712         r = case s of
 713               (a, b) ->
 714                 case a of
 715                   High -> add c d
 716                   Low -> let
 717                     op' = case b of
 718                       High -> sub
 719                       Low  -> λc.λd.c
 720                     in
 721                       op' d c
 722     in
 723       r
 724 \stoplambda
 725
 726 Scrutinee simplification does not apply.
 727
 728 After case binder wildening:
 729
 730 \startlambda
 731   λx.λc.λd.
 732     let s = foo x
 733         a = case s of (a, _) -> a
 734         b = case s of (_, b) -> b
 735         r = case s of (_, _) ->
 736               case a of
 737                 High -> add c d
 738                 Low -> let op' = case b of
 739                              High -> sub
 740                              Low  -> λc.λd.c
 741                        in
 742                          op' d c
 743     in
 744       r
 745 \stoplambda
 746
 747 After case value simplification
 748
 749 \startlambda
 750   λx.λc.λd.
 751     let s = foo x
 752         a = case s of (a, _) -> a
 753         b = case s of (_, b) -> b
 754         r = case s of (_, _) -> r'
 755         rh = add c d
 756         rl = let rll = λc.λd.c
 757                  op' = case b of
 758                    High -> sub
 759                    Low  -> rll
 760              in
 761                op' d c
 762         r' = case a of
 763                High -> rh
 764                Low -> rl
 765     in
 766       r
 767 \stoplambda
 768
 769 After let flattening:
 770
 771 \startlambda
 772   λx.λc.λd.
 773     let s = foo x
 774         a = case s of (a, _) -> a
 775         b = case s of (_, b) -> b
 776         r = case s of (_, _) -> r'
 777         rh = add c d
 778         rl = op' d c
 779         rll = λc.λd.c
 780         op' = case b of
 781           High -> sub
 782           Low  -> rll
 783         r' = case a of
 784                High -> rh
 785                Low -> rl
 786     in
 787       r
 788 \stoplambda
 789
 790 After function inlining:
 791
 792 \startlambda
 793   λx.λc.λd.
 794     let s = foo x
 795         a = case s of (a, _) -> a
 796         b = case s of (_, b) -> b
 797         r = case s of (_, _) -> r'
 798         rh = add c d
 799         rl = (case b of
 800           High -> sub
 801           Low  -> λc.λd.c) d c
 802         r' = case a of
 803           High -> rh
 804           Low -> rl
 805     in
 806       r
 807 \stoplambda
 808
 809 After (extended) β-reduction again:
 810
 811 \startlambda
 812   λx.λc.λd.
 813     let s = foo x
 814         a = case s of (a, _) -> a
 815         b = case s of (_, b) -> b
 816         r = case s of (_, _) -> r'
 817         rh = add c d
 818         rl = case b of
 819           High -> sub d c
 820           Low  -> d
 821         r' = case a of
 822           High -> rh
 823           Low -> rl
 824     in
 825       r
 826 \stoplambda
 827
 828 After case value simplification again:
 829
 830 \startlambda
 831   λx.λc.λd.
 832     let s = foo x
 833         a = case s of (a, _) -> a
 834         b = case s of (_, b) -> b
 835         r = case s of (_, _) -> r'
 836         rh = add c d
 837         rlh = sub d c
 838         rl = case b of
 839           High -> rlh
 840           Low  -> d
 841         r' = case a of
 842           High -> rh
 843           Low -> rl
 844     in
 845       r
 846 \stoplambda
 847
 848 After case removal:
 849
 850 \startlambda
 851   λx.λc.λd.
 852     let s = foo x
 853         a = case s of (a, _) -> a
 854         b = case s of (_, b) -> b
 855         r = r'
 856         rh = add c d
 857         rlh = sub d c
 858         rl = case b of
 859           High -> rlh
 860           Low  -> d
 861         r' = case a of
 862           High -> rh
 863           Low -> rl
 864     in
 865       r
 866 \stoplambda
 867
 868 After let bind removal:
 869
 870 \startlambda
 871   λx.λc.λd.
 872     let s = foo x
 873         a = case s of (a, _) -> a
 874         b = case s of (_, b) -> b
 875         rh = add c d
 876         rlh = sub d c
 877         rl = case b of
 878           High -> rlh
 879           Low  -> d
 880         r' = case a of
 881           High -> rh
 882           Low -> rl
 883     in
 884       r'
 885 \stoplambda
 886
 887 Application simplification is not applicable.
 888 \stoptext