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