Core2Core.tex

   1 \mainlanguage [en]
   2 \setuppapersize[A4][A4]
   3
   4 % Define a custom typescript. We could also have put the \definetypeface's
   5 % directly in the script, without a typescript, but I guess this is more
   6 % elegant...
   7 \starttypescript[Custom]
   8 % This is a sans font that supports greek symbols
   9 \definetypeface [Custom] [ss] [sans]  [iwona]                [default]
  10 \definetypeface [Custom] [rm] [serif] [antykwa-torunska]     [default]
  11 \definetypeface [Custom] [tt] [mono]  [modern]               [default]
  12 \definetypeface [Custom] [mm] [math]  [modern]               [default]
  13 \stoptypescript
  14 \usetypescript [Custom]
  15
  16 % Use our custom typeface
  17 \switchtotypeface [Custom] [10pt]
  18
  19 % The function application operator, which expands to a space in math mode
  20 \define[1]\expr{|#1|}
  21 \define[2]\app{#1\;#2}
  22 \define[2]\lam{λ#1 \xrightarrow #2}
  23 \define[2]\letexpr{{\bold let}\;#1\;{\bold in}\;#2}
  24 \define[2]\case{{\bold case}\;#1\;{\bold of}\;#2}
  25 \define[2]\alt{#1 \xrightarrow #2}
  26 \define[2]\bind{#1:#2}
  27 \define[1]\where{{\bold where}\;#1}
  28 % A transformation
  29 \definefloat[transformation][transformations]
  30 \define[2]\transform{
  31   \startframedtext[width=\textwidth]
  32   #2
  33   \stopframedtext
  34 }
  35
  36 \define\conclusion{\blackrule[height=0.5pt,depth=0pt,width=.5\textwidth]}
  37 \define\nextrule{\vskip1cm}
  38
  39 \define[2]\transformold{
  40   %\placetransformation[here]{#1}
  41   \startframedtext[width=\textwidth]
  42   \startformula \startalign
  43   #2
  44   \stopalign \stopformula
  45   \stopframedtext
  46 }
  47
  48 % Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
  49 \installprettytype [LAM] [LAM]
  50
  51 \definetyping[lambda][option=LAM,style=sans]
  52 \definetype[lam][option=LAM,style=sans]
  53
  54 % An (invisible) frame to hold a lambda expression
  55 \define[1]\lamframe{
  56         % Put a frame around lambda expressions, so they can have multiple
  57         % lines and still appear inline.
  58         % The align=right option really does left-alignment, but without the
  59         % program will end up on a single line. The strut=no option prevents a
  60         % bunch of empty space at the start of the frame.
  61         \framed[offset=0mm,location=middle,strut=no,align=right,frame=off]{#1}
  62 }
  63
  64 \define[2]\transbuf{
  65         % Make \typebuffer uses the LAM pretty printer and a sans-serif font
  66         % Also prevent any extra spacing above and below caused by the default
  67         % before=\blank and after=\blank.
  68         \setuptyping[option=LAM,style=sans,before=,after=]
  69         % Prevent the arrow from ending up below the first frame (a \framed
  70         % at the start of a line defaults to using vmode).
  71         \dontleavehmode
  72         % Put the elements in frames, so they can have multiple lines and be
  73         % middle-aligned
  74         \lamframe{\typebuffer[#1]}
  75         \lamframe{\Rightarrow}
  76         \lamframe{\typebuffer[#2]}
  77         % Reset the typing settings to their defaults
  78         \setuptyping[option=none,style=\tttf]
  79 }
  80 % This is the same as \transbuf above, but it accepts text directly instead
  81 % of through buffers. This only works for single lines, however.
  82 \define[2]\trans{
  83         \dontleavehmode
  84         \lamframe{\lam{#1}}
  85         \lamframe{\Rightarrow}
  86         \lamframe{\lam{#2}}
  87 }
  88
  89
  90 % A helper to print a single example in the half the page width. The example
  91 % text should be in a buffer whose name is given in an argument.
  92 %
  93 % The align=right option really does left-alignment, but without the program
  94 % will end up on a single line. The strut=no option prevents a bunch of empty
  95 % space at the start of the frame.
  96 \define[1]\example{
  97   \framed[offset=1mm,align=right,strut=no]{
  98     \setuptyping[option=LAM,style=sans,before=,after=]
  99     \typebuffer[#1]
 100     \setuptyping[option=none,style=\tttf]
 101   }
 102 }
 103
 104
 105 % A transformation example
 106 \definefloat[example][examples]
 107 \setupcaption[example][location=top] % Put captions on top
 108
 109 \define[3]\transexample{
 110   \placeexample[here]{#1}
 111   \startcombination[2*1]
 112     {\example{#2}}{Original program}
 113     {\example{#3}}{Transformed program}
 114   \stopcombination
 115 }
 116
 117 \define[3]\transexampleh{
 118 %  \placeexample[here]{#1}
 119 %  \startcombination[1*2]
 120 %    {\example{#2}}{Original program}
 121 %    {\example{#3}}{Transformed program}
 122 %  \stopcombination
 123 }
 124
 125 % Define a custom description format for the builtinexprs below
 126 \definedescription[builtindesc][headstyle=bold,style=normal,location=top]
 127
 128 \starttext
 129 \title {Core transformations for hardware generation}
 130 Matthijs Kooijman
 131
 132 \section{Introduction}
 133 As a new approach to translating Core to VHDL, we investigate a number of
 134 transformations on our Core program, which should bring the program into a
 135 well-defined "canonical" form, which is subsequently trivial to translate to
 136 VHDL.
 137
 138 The transformations as presented here are far from complete, but are meant as
 139 an exploration of possible transformations. In the running example below, we
 140 apply each of the transformations exactly once, in sequence. As will be
 141 apparent from the end result, there will be additional transformations needed
 142 to fully reach our goal, and some transformations must be applied more than
 143 once. How exactly to (efficiently) do this, has not been investigated.
 144
 145 Lastly, I hope to be able to state a number of pre- and postconditions for
 146 each transformation. If these can be proven for each transformation, and it
 147 can be shown that there exists some ordering of transformations for which the
 148 postcondition implies the canonical form, we can show that the transformations
 149 do indeed transform any program (probably satisfying a number of
 150 preconditions) to the canonical form.
 151
 152 \section{Goal}
 153 The transformations described here have a well-defined goal: To bring the
 154 program in a well-defined form that is directly translatable to hardware,
 155 while fully preserving the semantics of the program.
 156
 157 This {\em canonical form} is again a Core program, but with a very specific
 158 structure. A function in canonical form has nested lambda's at the top, which
 159 produce a let expression. This let expression binds every function application
 160 in the function and produces either a simple identifier or a tuple of
 161 identifiers. Every bound value in the let expression is either a simple
 162 function application or a case expression to extract a single element from a
 163 tuple returned by a function.
 164
 165 An example of a program in canonical form would be:
 166
 167 \starttyping
 168   -- All arguments are an inital lambda
 169   \x c d ->
 170   -- There is one let expression at the top level
 171   let
 172     -- Calling some other user-defined function.
 173     s = foo x
 174     -- Extracting result values from a tuple
 175     a = case s of (a, b) -> a
 176     b = case s of (a, b) -> b
 177     -- Some builtin expressions
 178     rh = add c d
 179     rhh = sub d c
 180     -- Conditional connections
 181     rl = case b of
 182       High -> rhh
 183       Low -> d
 184     r = case a of
 185       High -> rh
 186       Low -> rl
 187   in
 188     -- The actual result
 189     r
 190 \stoptyping
 191
 192 In this and all following programs, the following definitions are assumed to
 193 be available:
 194
 195 \starttyping
 196 data Bit = Low | High
 197
 198 foo :: Int -> (Bit, Bit)
 199 add :: Int -> Int -> Int
 200 sub :: Int -> Int -> Int
 201 \stoptyping
 202
 203 When looking at such a program from a hardware perspective, the top level
 204 lambda's define the input ports. The value produced by the let expression are
 205 the output ports. Each function application bound by the let expression
 206 defines a component instantiation, where the input and output ports are mapped
 207 to local signals or arguments. The tuple extracting case expressions don't map
 208 to
 209
 210 \subsection{Canonical form definition}
 211 Formally, the canonical form is a core program obeying the following
 212 constraints.
 213
 214 \startitemize[R,inmargin]
 215 \item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
 216 $fun$ is an identifier that will be bound as a global identifier.
 217 \item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
 218 $\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
 219 \item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
 220 \item $letbinds$ is a list with elements of the form
 221 $\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
 222 an identifier that will be bound as local identifier. The type of the bound
 223 value must be a $hardware\;type$.
 224 \item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
 225 equivalent VHDL expression. Since there are many supported forms for this,
 226 these are defined in a separate table.
 227 \item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
 228 where $fun$ is a global identifier and $x$ is a local identifier.
 229 \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
 230 be of a $hardware\;type$.
 231 \item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
 232 where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
 233 a local identifier.
 234 \item A $hardware\;type$ is a type that can be directly translated to
 235 hardware. This includes the types $Bit$, $SizedWord$, tuples containing
 236 elements of $hardware\;type$s, and will include others. This explicitely
 237 excludes function types.
 238 \stopitemize
 239
 240 TODO: Say something about uniqueness of identifiers
 241
 242 \subsection{Builtin expressions}
 243 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
 244
 245 \startitemize[m,inmargin]
 246 \item
 247 $tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
 248 where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
 249 e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
 250 be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
 251 \item TODO: Many more!
 252 \stopitemize
 253
 254 \section{Transformation passes}
 255
 256 In this section we describe the actual transformations. Here we're using
 257 mostly Core-like notation, with a few notable points.
 258
 259 \startitemize
 260 \item A core expression (in contrast with a transformation function, for
 261 example), is enclosed in pipes. For example, $\app{transform}{\expr{\lam{z}{z+1}}}$
 262 is the transform function applied to a lambda core expression.
 263
 264 Note that this notation might not be consistently applied everywhere. In
 265 particular where a non-core function is used inside a core expression, things
 266 get slightly confusing.
 267 \item A bind is written as $\expr{\bind{x}{expr}}$. This means binding the identifier
 268 $x$ to the expression $expr$.
 269 \item In the core examples, the layout rule from Haskell is loosely applied.
 270 It should be evident what was meant from indentation, even though it might nog
 271 be strictly correct.
 272 \stopitemize
 273
 274 \subsection{Example}
 275 In the descriptions of transformations below, the following (slightly
 276 contrived) example program will be used as the running example. Note that this
 277 the example for the canonical form given above is the same program, but in
 278 canonical form.
 279
 280 \starttyping
 281   \x ->
 282     let s = foo x
 283     in
 284       case s of
 285         (a, b) ->
 286           case a of
 287             High -> add
 288             Low -> let
 289               op' = case b of
 290                 High -> sub
 291                 Low  -> \c d -> c
 292               in
 293                 \c d -> op' d c
 294 \stoptyping
 295
 296 \subsection{η-abstraction}
 297 This transformation makes sure that all arguments of a function-typed
 298 expression are named, by introducing lambda expressions. When combined with
 299 β-reduction and function inlining below, all function-typed expressions should
 300 be lambda abstractions or global identifiers.
 301
 302 \transform{η-abstraction}
 303 {
 304 \lam{E :: * -> *}
 305
 306 \lam{E} is not the first argument of an application.
 307
 308 \lam{E} is not a lambda abstraction.
 309
 310 \lam{x} is a variable that does not occur free in E.
 311
 312 \conclusion
 313
 314 \trans{E}{λx.E x}
 315 }
 316
 317 \startbuffer[from]
 318 foo = λa -> case a of
 319   True -> λb.mul b b
 320   False -> id
 321 \stopbuffer
 322
 323 \startbuffer[to]
 324 foo = λa.λx -> (case a of
 325     True -> λb.mul b b
 326     False -> λy.id y) x
 327 \stopbuffer
 328
 329 \transexample{η-abstraction}{from}{to}
 330
 331 \subsection{Extended β-reduction}
 332 This transformation is meant to propagate application expressions downwards
 333 into expressions as far as possible. In lambda calculus, this reduction
 334 is known as β-reduction, but it is of course only defined for
 335 applications of lambda abstractions. We extend this reduction to also
 336 work for the rest of core (case and let expressions).
 337 \startbuffer[from]
 338 (case x of
 339   p1 -> E1
 340   \vdots
 341   pn -> En) M
 342 \stopbuffer
 343 \startbuffer[to]
 344 case x of
 345   p1 -> E1 M
 346   \vdots
 347   pn -> En M
 348 \stopbuffer
 349
 350 \transform{Extended β-reduction}
 351 {
 352 \conclusion
 353 \trans{(λx.E) M}{E[M/x]}
 354
 355 \nextrule
 356 \conclusion
 357 \trans{(let binds in E) M}{let binds in E M}
 358
 359 \nextrule
 360 \conclusion
 361 \transbuf{from}{to}
 362 }
 363
 364 \startbuffer[from]
 365 let a = (case x of
 366            True -> id
 367            False -> neg
 368         ) 1
 369     b = (let y = 3 in add y) 2
 370 in
 371   (λz.add 1 z) 3
 372 \stopbuffer
 373
 374 \startbuffer[to]
 375 let a = case x of
 376            True -> id 1
 377            False -> neg 1
 378     b = let y = 3 in add y 2
 379 in
 380   add 1 3
 381 \stopbuffer
 382
 383 \transexample{Extended β-reduction}{from}{to}
 384
 385 \subsection{Introducing main scope}
 386 This transformation is meant to introduce a single let expression that will be
 387 the "main scope". This is the let expression as described under requirement
 388 \ref[letexpr]. This let expression will contain only a single binding, which
 389 binds the original expression to some identifier and then evalutes to just
 390 this identifier (to comply with requirement \in[retexpr]).
 391
 392 Formally, we can describe the transformation as follows.
 393
 394 \transformold{Main scope introduction}
 395 {
 396 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
 397 \NR
 398 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
 399 \NC \app{transform'}{\expr{expr}} \NC = \expr{\letexpr{\bind{x}{expr}}{x}} \NR
 400 }
 401
 402 When applying this transformation to our running example, we get the following
 403 program.
 404
 405 \starttyping
 406   \x c d ->
 407     let r = (let s = foo x
 408               in
 409                 case s of
 410                   (a, b) ->
 411                     case a of
 412                       High -> add c d
 413                       Low -> let
 414                         op' = case b of
 415                           High -> sub
 416                           Low  -> \c d -> c
 417                         in
 418                           op' d c
 419             )
 420     in
 421       r
 422 \stoptyping
 423
 424 \subsection{Scope flattening}
 425 This transformation tries to flatten the topmost let expression in a bind,
 426 {\em i.e.}, bind all identifiers in the same scope, and bind them to simple
 427 expressions only (so simplify deeply nested expressions).
 428
 429 Formally, we can describe the transformation as follows.
 430
 431 \transformold{Main scope introduction} { \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
 432 \NR
 433 \NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
 434 \NC \app{transform'}{\expr{\letexpr{binds}{expr}}} \NC = \expr{\letexpr{\app{concat . map . flatten}{binds}}{expr}}\NR
 435 \NR
 436 \NC \app{flatten}{\expr{\bind{x}{\letexpr{binds}{expr}}}} \NC = (\app{concat . map . flatten}{binds}) \cup \{\app{flatten}{\expr{\bind{x}{expr}}}\}\NR
 437 \NC \app{flatten}{\expr{\bind{x}{\case{s}{alts}}}} \NC = \app{concat}{binds'} \cup \{\bind{x}{\case{s}{alts'}}\}\NR
 438 \NC                                                \NC  \where{(binds', alts')=\app{unzip.map.(flattenalt s)}{alts}}\NR
 439 \NC \app{\app{flattenalt}{s}}{\expr{\alt{\app{con}{x_0\;..\;x_n}}{expr}}} \NC = (extracts \cup \{\app{flatten}{bind}\}, alt)\NR
 440 \NC \NC \where{extracts =\{\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_0}}},}\NR
 441 \NC \NC \;..\;,\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_n}}}\} \NR
 442 \NC \NC bind = \expr{\bind{y}{expr}}\NR
 443 \NC \NC alt = \expr{\alt{\app{con}{\_\;..\;\_}}{y}}\NR
 444 }
 445
 446 When applying this transformation to our running example, we get the following
 447 program.
 448
 449 \starttyping
 450   \x c d ->
 451     let s = foo x
 452         r = case s of
 453               (_, _) -> y
 454         a = case s of (a, b) -> a
 455         b = case s of (a, b) -> b
 456         y = case a of
 457               High -> g
 458               Low -> h
 459         g = add c d
 460         h = op' d c
 461         op' = case b of
 462           High -> i
 463           Low  -> j
 464         i = sub
 465         j = \c d -> c
 466     in
 467       r
 468 \stoptyping
 469
 470 \subsection{More transformations}
 471 As noted before, the above transformations are not complete. Other needed
 472 transformations include:
 473 \startitemize
 474 \item Inlining of local identifiers with a function type. Since these cannot
 475 be represented in hardware directly, they must be transformed into something
 476 else. Inlining them should always be possible without loss of semantics (TODO:
 477 How true is this?) and can expose new possibilities for other transformations
 478 passes (such as application propagation when inlining {\tt j} above).
 479 \item A variation on inlining local identifiers is the propagation of
 480 function arguments with a function type. This will probably be initiated when
 481 transforming the caller (and not the callee), but it will also deal with
 482 identifiers with a function type that are unrepresentable in hardware.
 483
 484 Special care must be taken here, since the expression that is propagated into
 485 the callee comes from a different scope. The function typed argument must thus
 486 be replaced by any identifiers from the callers scope that the propagated
 487 expression uses.
 488
 489 Note that propagating an argument will change both a function's interface and
 490 implementation. For this to work, a new function should be created instead of
 491 modifying the original function, so any other callers will not be broken.
 492 \item Something similar should happen with return values with function types.
 493 \item Polymorphism must be removed from all user-defined functions. This is
 494 again similar to propagation function typed arguments, since this will also
 495 create duplicates of functions (for a specific type). This is an operation
 496 that is commonly known as "specialization" and already happens in GHC (since
 497 non-polymorph functions can be a lot faster than generic ones).
 498 \item More builtin expressions should be added and these should be evaluated
 499 by the compiler. For example, map, fold, +.
 500 \stopitemize
 501
 502 Initial example
 503
 504 \startlambda
 505   λx.
 506     let s = foo x
 507     in
 508       case s of
 509         (a, b) ->
 510           case a of
 511             High -> add
 512             Low -> let
 513               op' = case b of
 514                 High -> sub
 515                 Low  -> λc.λd.c
 516               in
 517                 λc.λd.op' d c
 518 \stoplambda
 519
 520 After top-level η-abstraction:
 521
 522 \startlambda
 523   λx.λc.λd.
 524     (let s = foo x
 525     in
 526       case s of
 527         (a, b) ->
 528           case a of
 529             High -> add
 530             Low -> let
 531               op' = case b of
 532                 High -> sub
 533                 Low  -> λc.λd.c
 534               in
 535                 λc.λd.op' d c
 536     ) c d
 537 \stoplambda
 538
 539 After (extended) β-reduction:
 540
 541 \startlambda
 542   λx.λc.λd.
 543     let s = foo x
 544     in
 545       case s of
 546         (a, b) ->
 547           case a of
 548             High -> add c d
 549             Low -> let
 550               op' = case b of
 551                 High -> sub
 552                 Low  -> λc.λd.c
 553               in
 554                 op' d c
 555 \stoplambda
 556
 557 After return value extraction:
 558
 559 \startlambda
 560   λx.λc.λd.
 561     let s = foo x
 562         r = case s of
 563               (a, b) ->
 564                 case a of
 565                   High -> add c d
 566                   Low -> let
 567                     op' = case b of
 568                       High -> sub
 569                       Low  -> λc.λd.c
 570                     in
 571                       op' d c
 572     in
 573       r
 574 \stoplambda
 575
 576 Scrutinee simplification does not apply.
 577
 578 After case binder wildening:
 579
 580 \startlambda
 581   λx.λc.λd.
 582     let s = foo x
 583         a = case s of (a, _) -> a
 584         b = case s of (_, b) -> b
 585         r = case s of (_, _) ->
 586               case a of
 587                 High -> add c d
 588                 Low -> let op' = case b of
 589                              High -> sub
 590                              Low  -> λc.λd.c
 591                        in
 592                          op' d c
 593     in
 594       r
 595 \stoplambda
 596
 597 After case value simplification
 598
 599 \startlambda
 600   λx.λc.λd.
 601     let s = foo x
 602         a = case s of (a, _) -> a
 603         b = case s of (_, b) -> b
 604         r = case s of (_, _) -> r'
 605         rh = add c d
 606         rl = let rll = λc.λd.c
 607                  op' = case b of
 608                    High -> sub
 609                    Low  -> rll
 610              in
 611                op' d c
 612         r' = case a of
 613                High -> rh
 614                Low -> rl
 615     in
 616       r
 617 \stoplambda
 618
 619 After let flattening:
 620
 621 \startlambda
 622   λx.λc.λd.
 623     let s = foo x
 624         a = case s of (a, _) -> a
 625         b = case s of (_, b) -> b
 626         r = case s of (_, _) -> r'
 627         rh = add c d
 628         rl = op' d c
 629         rll = λc.λd.c
 630         op' = case b of
 631           High -> sub
 632           Low  -> rll
 633         r' = case a of
 634                High -> rh
 635                Low -> rl
 636     in
 637       r
 638 \stoplambda
 639
 640 After function inlining:
 641
 642 \startlambda
 643   λx.λc.λd.
 644     let s = foo x
 645         a = case s of (a, _) -> a
 646         b = case s of (_, b) -> b
 647         r = case s of (_, _) -> r'
 648         rh = add c d
 649         rl = (case b of
 650           High -> sub
 651           Low  -> λc.λd.c) d c
 652         r' = case a of
 653           High -> rh
 654           Low -> rl
 655     in
 656       r
 657 \stoplambda
 658
 659 After (extended) β-reduction again:
 660
 661 \startlambda
 662   λx.λc.λd.
 663     let s = foo x
 664         a = case s of (a, _) -> a
 665         b = case s of (_, b) -> b
 666         r = case s of (_, _) -> r'
 667         rh = add c d
 668         rl = case b of
 669           High -> sub d c
 670           Low  -> d
 671         r' = case a of
 672           High -> rh
 673           Low -> rl
 674     in
 675       r
 676 \stoplambda
 677
 678 After case value simplification again:
 679
 680 \startlambda
 681   λx.λc.λd.
 682     let s = foo x
 683         a = case s of (a, _) -> a
 684         b = case s of (_, b) -> b
 685         r = case s of (_, _) -> r'
 686         rh = add c d
 687         rlh = sub d c
 688         rl = case b of
 689           High -> rlh
 690           Low  -> d
 691         r' = case a of
 692           High -> rh
 693           Low -> rl
 694     in
 695       r
 696 \stoplambda
 697
 698 After case removal:
 699
 700 \startlambda
 701   λx.λc.λd.
 702     let s = foo x
 703         a = case s of (a, _) -> a
 704         b = case s of (_, b) -> b
 705         r = r'
 706         rh = add c d
 707         rlh = sub d c
 708         rl = case b of
 709           High -> rlh
 710           Low  -> d
 711         r' = case a of
 712           High -> rh
 713           Low -> rl
 714     in
 715       r
 716 \stoplambda
 717
 718 After let bind removal:
 719
 720 \startlambda
 721   λx.λc.λd.
 722     let s = foo x
 723         a = case s of (a, _) -> a
 724         b = case s of (_, b) -> b
 725         rh = add c d
 726         rlh = sub d c
 727         rl = case b of
 728           High -> rlh
 729           Low  -> d
 730         r' = case a of
 731           High -> rh
 732           Low -> rl
 733     in
 734       r'
 735 \stoplambda
 736
 737 Application simplification is not applicable.
 738 \stoptext