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