Chapters/Normalization.tex

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