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