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