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