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