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