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
 244 For let expressions:
 245 \starttrans
 246 let binds in E) M
 247 -----------------
 248 let binds in E M
 249 \stoptrans
 250
 251 For case statements:
 252 \starttrans
 253 (case x of
 254   p1 -> E1
 255   \vdots
 256   pn -> En) M
 257 -----------------
 258 case x of
 259   p1 -> E1 M
 260   \vdots
 261   pn -> En M
 262 \stoptrans
 263
 264 For lambda expressions:
 265 \starttrans
 266 (λx.E) M
 267 -----------------
 268 E[M/x]
 269 \stoptrans
 270
 271 % And an example
 272 \startbuffer[from]
 273 ( let a = (case x of
 274             True -> id
 275             False -> neg
 276           ) 1
 277       b = (let y = 3 in add y) 2
 278   in
 279     (λz.add 1 z)
 280 ) 3
 281 \stopbuffer
 282
 283 \startbuffer[to]
 284 let a = case x of
 285            True -> id 1
 286            False -> neg 1
 287     b = let y = 3 in add y 2
 288 in
 289   add 1 3
 290 \stopbuffer
 291
 292 \transexample{Extended β-reduction}{from}{to}
 293
 294 \subsection{Let derecursification}
 295
 296 \subsection{Let flattening}
 297 This transform turns two nested lets (\lam{let x = (let ... in ...) in
 298 ...}) into a single let.
 299
 300 \subsection{Empty let removal}
 301
 302 \subsection{Simple let binding removal}
 303 This transforms inlines simple let bindings (\eg a = b).
 304
 305 \subsection{Unused let binding removal}
 306
 307 \subsection{Non-representable binding inlining}
 308 This transform inlines let bindings of a funtion type. TODO: This should
 309 be generelized to anything that is non representable at runtime, or
 310 something like that.
 311
 312 \subsection{Scrutinee simplification}
 313 This transform ensures that the scrutinee of a case expression is always
 314 a simple variable reference.
 315
 316 \subsection{Case simplification}
 317
 318 \subsection{Case removal}
 319 This transform removes any case statements with a single alternative and
 320 only wild binders.
 321
 322 \subsection{Argument simplification}
 323 The transforms in this section deal with simplifying application
 324 arguments into normal form. The goal here is to:
 325
 326 \startitemize
 327  \item Make all arguments of user-defined functions (\eg, of which
 328  we have a function body) simple variable references of a runtime
 329  representable type.
 330  \item Make all arguments of builtin functions either:
 331    \startitemize
 332     \item A type argument.
 333     \item A dictionary argument.
 334     \item A type level expression.
 335     \item A variable reference of a runtime representable type.
 336     \item A variable reference or partial application of a function type.
 337    \stopitemize
 338 \stopitemize
 339
 340 When looking at the arguments of a user-defined function, we can
 341 divide them into two categories:
 342 \startitemize
 343   \item Arguments with a runtime representable type (\eg bits or vectors).
 344
 345         These arguments can be preserved in the program, since they can
 346         be translated to input ports later on.  However, since we can
 347         only connect signals to input ports, these arguments must be
 348         reduced to simple variables (for which signals will be
 349         produced). This is taken care of by the argument extraction
 350         transform.
 351   \item Non-runtime representable typed arguments.
 352
 353         These arguments cannot be preserved in the program, since we
 354         cannot represent them as input or output ports in the resulting
 355         VHDL. To remove them, we create a specialized version of the
 356         called function with these arguments filled in. This is done by
 357         the argument propagation transform.
 358 \stopitemize
 359
 360 When looking at the arguments of a builtin function, we can divide them
 361 into categories:
 362
 363 \startitemize
 364   \item Arguments with a runtime representable type.
 365
 366         As we have seen with user-defined functions, these arguments can
 367         always be reduced to a simple variable reference, by the
 368         argument extraction transform. Performing this transform for
 369         builtin functions as well, means that the translation of builtin
 370         functions can be limited to signal references, instead of
 371         needing to support all possible expressions.
 372
 373   \item Arguments with a function type.
 374
 375         These arguments are functions passed to higher order builtins,
 376         like \lam{map} and \lam{foldl}. Since implementing these
 377         functions for arbitrary function-typed expressions (\eg, lambda
 378         expressions) is rather comlex, we reduce these arguments to
 379         (partial applications of) global functions.
 380
 381         We can still support arbitrary expressions from the user code,
 382         by creating a new global function containing that expression.
 383         This way, we can simply replace the argument with a reference to
 384         that new function. However, since the expression can contain any
 385         number of free variables we also have to include partial
 386         applications in our normal form.
 387
 388         This category of arguments is handled by the function extraction
 389         transform.
 390   \item Other unrepresentable arguments.
 391
 392         These arguments can take a few different forms:
 393         \startdesc{Type arguments}
 394           In the core language, type arguments can only take a single
 395           form: A type wrapped in the Type constructor. Also, there is
 396           nothing that can be done with type expressions, except for
 397           applying functions to them, so we can simply leave type
 398           arguments as they are.
 399         \stopdesc
 400         \startdesc{Dictionary arguments}
 401           In the core language, dictionary arguments are used to find
 402           operations operating on one of the type arguments (mostly for
 403           finding class methods). Since we will not actually evaluatie
 404           the function body for builtin functions and can generate
 405           code for builtin functions by just looking at the type
 406           arguments, these arguments can be ignored and left as they
 407           are.
 408         \stopdesc
 409         \startdesc{Type level arguments}
 410           Sometimes, we want to pass a value to a builtin function, but
 411           we need to know the value at compile time. Additionally, the
 412           value has an impact on the type of the function. This is
 413           encoded using type-level values, where the actual value of the
 414           argument is not important, but the type encodes some integer,
 415           for example. Since the value is not important, the actual form
 416           of the expression does not matter either and we can leave
 417           these arguments as they are.
 418         \stopdesc
 419         \startdesc{Other arguments}
 420           Technically, there is still a wide array of arguments that can
 421           be passed, but does not fall into any of the above categories.
 422           However, none of the supported builtin functions requires such
 423           an argument. This leaves use with passing unsupported types to
 424           a function, such as calling \lam{head} on a list of functions.
 425
 426           In these cases, it would be impossible to generate hardware
 427           for such a function call anyway, so we can ignore these
 428           arguments.
 429
 430           The only way to generate hardware for builtin functions with
 431           arguments like these, is to expand the function call into an
 432           equivalent core expression (\eg, expand map into a series of
 433           function applications). But for now, we choose to simply not
 434           support expressions like these.
 435         \stopdesc
 436
 437         From the above, we can conclude that we can simply ignore these
 438         other unrepresentable arguments and focus on the first two
 439         categories instead.
 440 \stopitemize
 441
 442 \subsubsection{Argument extraction}
 443 This transform deals with arguments to functions that
 444 are of a runtime representable type.
 445
 446 TODO: It seems we can map an expression to a port, not only a signal.
 447 Perhaps this makes this transformation not needed?
 448 TODO: Say something about dataconstructors (without arguments, like True
 449 or False), which are variable references of a runtime representable
 450 type, but do not result in a signal.
 451
 452 To reduce a complex expression to a simple variable reference, we create
 453 a new let expression around the application, which binds the complex
 454 expression to a new variable. The original function is then applied to
 455 this variable.
 456
 457 %\transform{Argument extract}
 458 %{
 459 %\lam{Y} is of a hardware representable type
 460 %
 461 %\lam{Y} is not a variable referene
 462 %
 463 %\conclusion
 464 %
 465 %\trans{X Y}{let z = Y in X z}
 466 %}
 467
 468 \subsubsection{Function extraction}
 469 This transform deals with function-typed arguments to builtin functions.
 470 Since these arguments cannot be propagated, we choose to extract them
 471 into a new global function instead.
 472
 473 Any free variables occuring in the extracted arguments will become
 474 parameters to the new global function. The original argument is replaced
 475 with a reference to the new function, applied to any free variables from
 476 the original argument.
 477
 478 %\transform{Function extraction}
 479 %{
 480 %\lam{X} is a (partial application of) a builtin function
 481 %
 482 %\lam{Y} is not an application
 483 %
 484 %\lam{Y} is not a variable reference
 485 %
 486 %\conclusion
 487 %
 488 %\lam{f0 ... fm} = free local vars of \lam{Y}
 489 %
 490 %\lam{y} is a new global variable
 491 %
 492 %\lam{y = λf0 ... fn.Y}
 493 %
 494 %\trans{X Y}{X (y f0 ... fn)}
 495 %}
 496
 497 \subsubsection{Argument propagation}
 498 This transform deals with arguments to user-defined functions that are
 499 not representable at runtime. This means these arguments cannot be
 500 preserved in the final form and most be {\em propagated}.
 501
 502 Propagation means to create a specialized version of the called
 503 function, with the propagated argument already filled in. As a simple
 504 example, in the following program:
 505
 506 \startlambda
 507 f = λa.λb.a + b
 508 inc = λa.f a 1
 509 \stoplambda
 510
 511 we could {\em propagate} the constant argument 1, with the following
 512 result:
 513
 514 \startlambda
 515 f' = λa.a + 1
 516 inc = λa.f' a
 517 \stoplambda
 518
 519 Special care must be taken when the to-be-propagated expression has any
 520 free variables. If this is the case, the original argument should not be
 521 removed alltogether, but replaced by all the free variables of the
 522 expression. In this way, the original expression can still be evaluated
 523 inside the new function. Also, this brings us closer to our goal: All
 524 these free variables will be simple variable references.
 525
 526 To prevent us from propagating the same argument over and over, a simple
 527 local variable reference is not propagated (since is has exactly one
 528 free variable, itself, we would only replace that argument with itself).
 529
 530 This shows that any free local variables that are not runtime representable
 531 cannot be brought into normal form by this transform. We rely on an
 532 inlining transformation to replace such a variable with an expression we
 533 can propagate again.
 534
 535 TODO: Move these definitions somewhere sensible.
 536
 537 Definition: A global variable is any variable that is bound at the
 538 top level of a program. A local variable is any other variable.
 539
 540 Definition: A hardware representable type is a type that we can generate
 541 a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
 542 unsigned word, etc. Types that are not runtime representable notably
 543 include (but are not limited to): Types, dictionaries, functions.
 544
 545 Definition: A builtin function is a function for which a builtin
 546 hardware translation is available, because its actual definition is not
 547 translatable. A user-defined function is any other function.
 548
 549 \starttrans
 550 x = E
 551 ~
 552 x Y0 ... Yi ... Yn                               \lam{Yi} is not of a runtime representable type
 553 ---------------------------------------------    \lam{Yi} is not a local variable reference
 554 x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .        \lam{f0 ... fm} = free local vars of \lam{Y_i}
 555       E y0 ... yi-1 Yi yi+1 ... yn
 556 ~
 557 x' y0 ... yi-1 f0 ...  fm Yi+1 ... Yn
 558 \stoptrans
 559
 560 \subsection{Cast propagation / simplification}
 561 This transform pushes casts down into the expression as far as possible.
 562
 563 \subsection{Return value simplification}
 564 Currently implemented using lambda simplification, let simplification, and
 565 top simplification. Should change.
 566
 567 \subsection{Example sequence}
 568
 569 This section lists an example expression, with a sequence of transforms
 570 applied to it. The exact transforms given here probably don't exactly
 571 match the transforms given above anymore, but perhaps this can clarify
 572 the big picture a bit.
 573
 574 TODO: Update or remove this section.
 575
 576 \startlambda
 577   λx.
 578     let s = foo x
 579     in
 580       case s of
 581         (a, b) ->
 582           case a of
 583             High -> add
 584             Low -> let
 585               op' = case b of
 586                 High -> sub
 587                 Low  -> λc.λd.c
 588               in
 589                 λc.λd.op' d c
 590 \stoplambda
 591
 592 After top-level η-abstraction:
 593
 594 \startlambda
 595   λx.λc.λd.
 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     ) c d
 609 \stoplambda
 610
 611 After (extended) β-reduction:
 612
 613 \startlambda
 614   λx.λc.λd.
 615     let s = foo x
 616     in
 617       case s of
 618         (a, b) ->
 619           case a of
 620             High -> add c d
 621             Low -> let
 622               op' = case b of
 623                 High -> sub
 624                 Low  -> λc.λd.c
 625               in
 626                 op' d c
 627 \stoplambda
 628
 629 After return value extraction:
 630
 631 \startlambda
 632   λx.λc.λd.
 633     let s = foo x
 634         r = case s of
 635               (a, b) ->
 636                 case a of
 637                   High -> add c d
 638                   Low -> let
 639                     op' = case b of
 640                       High -> sub
 641                       Low  -> λc.λd.c
 642                     in
 643                       op' d c
 644     in
 645       r
 646 \stoplambda
 647
 648 Scrutinee simplification does not apply.
 649
 650 After case binder wildening:
 651
 652 \startlambda
 653   λx.λc.λd.
 654     let s = foo x
 655         a = case s of (a, _) -> a
 656         b = case s of (_, b) -> b
 657         r = case s of (_, _) ->
 658               case a of
 659                 High -> add c d
 660                 Low -> let op' = case b of
 661                              High -> sub
 662                              Low  -> λc.λd.c
 663                        in
 664                          op' d c
 665     in
 666       r
 667 \stoplambda
 668
 669 After case value simplification
 670
 671 \startlambda
 672   λx.λc.λd.
 673     let s = foo x
 674         a = case s of (a, _) -> a
 675         b = case s of (_, b) -> b
 676         r = case s of (_, _) -> r'
 677         rh = add c d
 678         rl = let rll = λc.λd.c
 679                  op' = case b of
 680                    High -> sub
 681                    Low  -> rll
 682              in
 683                op' d c
 684         r' = case a of
 685                High -> rh
 686                Low -> rl
 687     in
 688       r
 689 \stoplambda
 690
 691 After let flattening:
 692
 693 \startlambda
 694   λx.λc.λd.
 695     let s = foo x
 696         a = case s of (a, _) -> a
 697         b = case s of (_, b) -> b
 698         r = case s of (_, _) -> r'
 699         rh = add c d
 700         rl = op' d c
 701         rll = λc.λd.c
 702         op' = case b of
 703           High -> sub
 704           Low  -> rll
 705         r' = case a of
 706                High -> rh
 707                Low -> rl
 708     in
 709       r
 710 \stoplambda
 711
 712 After function inlining:
 713
 714 \startlambda
 715   λx.λc.λd.
 716     let s = foo x
 717         a = case s of (a, _) -> a
 718         b = case s of (_, b) -> b
 719         r = case s of (_, _) -> r'
 720         rh = add c d
 721         rl = (case b of
 722           High -> sub
 723           Low  -> λc.λd.c) d c
 724         r' = case a of
 725           High -> rh
 726           Low -> rl
 727     in
 728       r
 729 \stoplambda
 730
 731 After (extended) β-reduction again:
 732
 733 \startlambda
 734   λx.λc.λd.
 735     let s = foo x
 736         a = case s of (a, _) -> a
 737         b = case s of (_, b) -> b
 738         r = case s of (_, _) -> r'
 739         rh = add c d
 740         rl = case b of
 741           High -> sub d c
 742           Low  -> d
 743         r' = case a of
 744           High -> rh
 745           Low -> rl
 746     in
 747       r
 748 \stoplambda
 749
 750 After case value simplification again:
 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 = case s of (_, _) -> 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 case 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         r = r'
 778         rh = add c d
 779         rlh = sub d c
 780         rl = case b of
 781           High -> rlh
 782           Low  -> d
 783         r' = case a of
 784           High -> rh
 785           Low -> rl
 786     in
 787       r
 788 \stoplambda
 789
 790 After let bind removal:
 791
 792 \startlambda
 793   λx.λc.λd.
 794     let s = foo x
 795         a = case s of (a, _) -> a
 796         b = case s of (_, b) -> b
 797         rh = add c d
 798         rlh = sub d c
 799         rl = case b of
 800           High -> rlh
 801           Low  -> d
 802         r' = case a of
 803           High -> rh
 804           Low -> rl
 805     in
 806       r'
 807 \stoplambda
 808
 809 Application simplification is not applicable.