[matthijs/master-project/report.git] / Chapters / Normalization.tex

\chapter{Normalization}

% A helper to print a single example in the half the page width. The example
% text should be in a buffer whose name is given in an argument.
%
% The align=right option really does left-alignment, but without the program
% will end up on a single line. The strut=no option prevents a bunch of empty
% space at the start of the frame.
\define[1]\example{
  \framed[offset=1mm,align=right,strut=no]{
    \setuptyping[option=LAM,style=sans,before=,after=]
    \typebuffer[#1]
    \setuptyping[option=none,style=\tttf]
  }
}


% A transformation example
\definefloat[example][examples]
\setupcaption[example][location=top] % Put captions on top

\define[3]\transexample{
  \placeexample[here]{#1}
  \startcombination[2*1]
    {\example{#2}}{Original program}
    {\example{#3}}{Transformed program}
  \stopcombination
}
%
%\define[3]\transexampleh{
%%  \placeexample[here]{#1}
%%  \startcombination[1*2]
%%    {\example{#2}}{Original program}
%%    {\example{#3}}{Transformed program}
%%  \stopcombination
%}

The first step in the core to VHDL translation process, is normalization. We
aim to bring the core description into a simpler form, which we can
subsequently translate into VHDL easily. This normal form is needed because
the full core language is more expressive than VHDL in some areas and because
core can describe expressions that do not have a direct hardware
interpretation.

TODO: Describe core properties not supported in VHDL, and describe how the
VHDL we want to generate should look like.

\section{Goal}
The transformations described here have a well-defined goal: To bring the
program in a well-defined form that is directly translatable to hardware,
while fully preserving the semantics of the program.

This {\em normal form} is again a Core program, but with a very specific
structure. A function in normal form has nested lambda's at the top, which
produce a let expression. This let expression binds every function application
in the function and produces a simple identifier. Every bound value in
the let expression is either a simple function application or a case
expression to extract a single element from a tuple returned by a
function.

An example of a program in canonical form would be:

\startlambda
  -- All arguments are an inital lambda
  λa.λd.λsp.
  -- There are nested let expressions at top level
  let
    -- Unpack the state by coercion
    s = sp :: (Word, Word)
    -- Extract both registers from the state
    r1 = case s of (fst, snd) -> fst
    r2 = case s of (fst, snd) -> snd
    -- Calling some other user-defined function.
    d' = foo d
    -- Conditional connections
    out = case a of
      High -> r1
      Low -> r2
    r1' = case a of
      High -> d
      Low -> r1
    r2' = case a of
      High -> r2
      Low -> d
    -- Packing a tuple
    s' = (,) r1' r2'
    -- Packing the state by coercion
    sp' = s' :: State (Word, Word)
    -- Pack our return value
    res = (,) sp' out
  in
    -- The actual result
    res
\stoplambda

\startlambda
\italic{normal} = \italic{lambda}
\italic{lambda} = λvar.\italic{lambda} (representable(typeof(var)))
                | \italic{toplet} 
\italic{toplet} = let \italic{binding} in \italic{toplet} 
                | letrec [\italic{binding}] in \italic{toplet}
                | var (representable(typeof(var)), fvar(var))
\italic{binding} = var = \italic{rhs} (representable(typeof(rhs)))
                 -- State packing and unpacking by coercion
                 | var0 = var1 :: State ty (fvar(var1))
                 | var0 = var1 :: ty (var0 :: State ty) (fvar(var1))
\italic{rhs} = userapp
             | builtinapp
             -- Extractor case
             | case var of C a0 ... an -> ai (fvar(var))
             -- Selector case
             | case var of (fvar(var))
                DEFAULT -> var0 (fvar(var0))
                C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, fvar(resvar))
\italic{userapp} = \italic{userfunc}
                 | \italic{userapp} {userarg}
\italic{userfunc} = var (tvar(var))
\italic{userarg} = var (fvar(var))
\italic{builtinapp} = \italic{builtinfunc}
                    | \italic{builtinapp} \italic{builtinarg}
\italic{builtinfunc} = var (bvar(var))
\italic{builtinarg} = \italic{coreexpr}
\stoplambda

-- TODO: Define tvar, fvar, typeof, representable
-- TODO: Limit builtinarg further

-- TODO: There can still be other casts around (which the code can handle,
e.g., ignore), which still need to be documented here.

-- TODO: Note about the selector case. It just supports Bit and Bool
currently, perhaps it should be generalized in the normal form?

When looking at such a program from a hardware perspective, the top level
lambda's define the input ports. The value produced by the let expression is
the output port. Most function applications bound by the let expression
define a component instantiation, where the input and output ports are mapped
to local signals or arguments. Some of the others use a builtin
construction (\eg the \lam{case} statement) or call a builtin function
(\eg \lam{add} or \lam{sub}). For these, a hardcoded VHDL translation is
available.

\subsection{Normal definition}
Formally, the normal form is a core program obeying the following
constraints. TODO: Update this section, this is probably not completely
accurate or relevant anymore.

\startitemize[R,inmargin]
%\item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
%$fun$ is an identifier that will be bound as a global identifier.
%\item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
%$\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
%\item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
%\item $letbinds$ is a list with elements of the form
%$\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
%an identifier that will be bound as local identifier. The type of the bound
%value must be a $hardware\;type$.
%\item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
%equivalent VHDL expression. Since there are many supported forms for this,
%these are defined in a separate table.
%\item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
%where $fun$ is a global identifier and $x$ is a local identifier.
%\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
%be of a $hardware\;type$.
%\item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
%where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
%a local identifier.
%\item A $hardware\;type$ is a type that can be directly translated to
%hardware. This includes the types $Bit$, $SizedWord$, tuples containing
%elements of $hardware\;type$s, and will include others. This explicitely
%excludes function types.
\stopitemize

TODO: Say something about uniqueness of identifiers

\subsection{Builtin expressions}
A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.

\startitemize[m,inmargin]
%\item
%$tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
%where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
%e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
%be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
%\item TODO: Many more!
\stopitemize

\section{Transform passes}

In this section we describe the actual transforms. Here we're using
the core language in a notation that resembles lambda calculus.

Each of these transforms is meant to be applied to every (sub)expression
in a program, for as long as it applies. Only when none of the
expressions can be applied anymore, the program is in normal form. We
hope to be able to prove that this form will obey all of the constraints
defined above, but this has yet to happen (though it seems likely that
it will).

Each of the transforms will be described informally first, explaining
the need for and goal of the transform. Then, a formal definition is
given, using a familiar syntax from the world of logic. Each transform
is specified as a number of conditions (above the horizontal line) and a
number of conclusions (below the horizontal line). The details of using
this notation are still a bit fuzzy, so comments are welcom.

TODO: Formally describe the "apply to every (sub)expression" in terms of
rules with full transformations in the conditions.

\subsection{η-abstraction}
This transformation makes sure that all arguments of a function-typed
expression are named, by introducing lambda expressions. When combined with
β-reduction and function inlining below, all function-typed expressions should
be lambda abstractions or global identifiers.

\starttrans
E                 \lam{E :: * -> *}
--------------    \lam{E} is not the first argument of an application.
λx.E x            \lam{E} is not a lambda abstraction.
                  \lam{x} is a variable that does not occur free in \lam{E}.
\stoptrans

\startbuffer[from]
foo = λa -> case a of 
  True -> λb.mul b b
  False -> id
\stopbuffer

\startbuffer[to]
foo = λa.λx -> (case a of 
    True -> λb.mul b b
    False -> λy.id y) x
\stopbuffer

\transexample{η-abstraction}{from}{to}

\subsection{Extended β-reduction}
This transformation is meant to propagate application expressions downwards
into expressions as far as possible. In lambda calculus, this reduction
is known as β-reduction, but it is of course only defined for
applications of lambda abstractions. We extend this reduction to also
work for the rest of core (case and let expressions).

For let expressions:
\starttrans
let binds in E) M
-----------------
let binds in E M
\stoptrans

For case statements:
\starttrans
(case x of
  p1 -> E1
  \vdots
  pn -> En) M
-----------------
case x of
  p1 -> E1 M
  \vdots
  pn -> En M
\stoptrans

For lambda expressions:
\starttrans
(λx.E) M
-----------------
E[M/x]
\stoptrans

% And an example
\startbuffer[from]
( let a = (case x of 
            True -> id
            False -> neg
          ) 1
      b = (let y = 3 in add y) 2
  in
    (λz.add 1 z)
) 3
\stopbuffer

\startbuffer[to]
let a = case x of 
           True -> id 1
           False -> neg 1
    b = let y = 3 in add y 2
in
  add 1 3
\stopbuffer

\transexample{Extended β-reduction}{from}{to}

\subsection{Let derecursification}
This transformation is meant to make lets non-recursive whenever possible.
This might allow other optimizations to do their work better. TODO: Why is
this needed exactly?

\subsection{Let flattening}
This transformation puts nested lets in the same scope, by lifting the
binding(s) of the inner let into a new let around the outer let. Eventually,
this will cause all let bindings to appear in the same scope (they will all be
in scope for the function return value).

Note that this transformation does not try to be smart when faced with
recursive lets, it will just leave the lets recursive (possibly joining a
recursive and non-recursive let into a single recursive let). The let
rederursification transformation will do this instead.

\starttrans
letnonrec x = (let bindings in M) in N
------------------------------------------
let bindings in (letnonrec x = M) in N
\stoptrans

\starttrans
letrec 
  \vdots
  x = (let bindings in M)
  \vdots
in
  N
------------------------------------------
letrec
  \vdots
  bindings
  x = M
  \vdots
in
  N
\stoptrans

\startbuffer[from]
let
  a = letrec
    x = 1
    y = 2
  in
    x + y
in
  letrec
    b = let c = 3 in a + c
    d = 4
  in
    d + b
\stopbuffer
\startbuffer[to]
letrec
  x = 1
  y = 2
in
  let
    a = x + y
  in
    letrec
      c = 3
      b = a + c
      d = 4
    in
      d + b
\stopbuffer

\transexample{Let flattening}{from}{to}

\subsection{Empty let removal}
This transformation is simple: It removes recursive lets that have no bindings
(which usually occurs when let derecursification removes the last binding from
it).

\starttrans
letrec in M
--------------
M
\stoptrans

\subsection{Simple let binding removal}
This transformation inlines simple let bindings (\eg a = b).

This transformation is not needed to get into normal form, but makes the
resulting VHDL a lot shorter.

\starttrans
letnonrec
  a = b
in
  M
-----------------
M[b/a]
\stoptrans

\starttrans
letrec
  \vdots
  a = b
  \vdots
in
  M
-----------------
let
  \vdots
  \vdots
in
  M[b/a]
\stoptrans

\subsection{Unused let binding removal}
This transformation removes let bindings that are never used. Usually,
the desugarer introduces some unused let bindings.

This normalization pass should really be unneeded to get into normal form
(since ununsed bindings are not forbidden by the normal form), but in practice
the desugarer or simplifier emits some unused bindings that cannot be
normalized (e.g., calls to a \type{PatError} (TODO: Check this name)). Also,
this transformation makes the resulting VHDL a lot shorter.

\starttrans
let a = E in M
----------------------------    \lam{a} does not occur free in \lam{M}
M
\stoptrans

\starttrans
letrec
  \vdots
  a = E
  \vdots
in
  M
----------------------------    \lam{a} does not occur free in \lam{M}
letrec
  \vdots
  \vdots
in
  M
\stoptrans

\subsection{Non-representable binding inlining}
This transform inlines let bindings of a funtion type. TODO: This should
be generelized to anything that is non representable at runtime, or
something like that.

\subsection{Scrutinee simplification}
This transform ensures that the scrutinee of a case expression is always
a simple variable reference.

\subsection{Case simplification}

\subsection{Case removal}
This transform removes any case statements with a single alternative and
only wild binders.

\subsection{Argument simplification}
The transforms in this section deal with simplifying application
arguments into normal form. The goal here is to:

\startitemize
 \item Make all arguments of user-defined functions (\eg, of which
 we have a function body) simple variable references of a runtime
 representable type.
 \item Make all arguments of builtin functions either:
   \startitemize
    \item A type argument.
    \item A dictionary argument.
    \item A type level expression.
    \item A variable reference of a runtime representable type.
    \item A variable reference or partial application of a function type.
   \stopitemize
\stopitemize

When looking at the arguments of a user-defined function, we can
divide them into two categories:
\startitemize
  \item Arguments with a runtime representable type (\eg bits or vectors).

        These arguments can be preserved in the program, since they can
        be translated to input ports later on.  However, since we can
        only connect signals to input ports, these arguments must be
        reduced to simple variables (for which signals will be
        produced). This is taken care of by the argument extraction
        transform.
  \item Non-runtime representable typed arguments.
        
        These arguments cannot be preserved in the program, since we
        cannot represent them as input or output ports in the resulting
        VHDL. To remove them, we create a specialized version of the
        called function with these arguments filled in. This is done by
        the argument propagation transform.
\stopitemize

When looking at the arguments of a builtin function, we can divide them
into categories: 

\startitemize
  \item Arguments with a runtime representable type.
        
        As we have seen with user-defined functions, these arguments can
        always be reduced to a simple variable reference, by the
        argument extraction transform. Performing this transform for
        builtin functions as well, means that the translation of builtin
        functions can be limited to signal references, instead of
        needing to support all possible expressions.

  \item Arguments with a function type.
        
        These arguments are functions passed to higher order builtins,
        like \lam{map} and \lam{foldl}. Since implementing these
        functions for arbitrary function-typed expressions (\eg, lambda
        expressions) is rather comlex, we reduce these arguments to
        (partial applications of) global functions.
        
        We can still support arbitrary expressions from the user code,
        by creating a new global function containing that expression.
        This way, we can simply replace the argument with a reference to
        that new function. However, since the expression can contain any
        number of free variables we also have to include partial
        applications in our normal form.

        This category of arguments is handled by the function extraction
        transform.
  \item Other unrepresentable arguments.
        
        These arguments can take a few different forms:
        \startdesc{Type arguments}
          In the core language, type arguments can only take a single
          form: A type wrapped in the Type constructor. Also, there is
          nothing that can be done with type expressions, except for
          applying functions to them, so we can simply leave type
          arguments as they are.
        \stopdesc
        \startdesc{Dictionary arguments}
          In the core language, dictionary arguments are used to find
          operations operating on one of the type arguments (mostly for
          finding class methods). Since we will not actually evaluatie
          the function body for builtin functions and can generate
          code for builtin functions by just looking at the type
          arguments, these arguments can be ignored and left as they
          are.
        \stopdesc
        \startdesc{Type level arguments}
          Sometimes, we want to pass a value to a builtin function, but
          we need to know the value at compile time. Additionally, the
          value has an impact on the type of the function. This is
          encoded using type-level values, where the actual value of the
          argument is not important, but the type encodes some integer,
          for example. Since the value is not important, the actual form
          of the expression does not matter either and we can leave
          these arguments as they are.
        \stopdesc
        \startdesc{Other arguments}
          Technically, there is still a wide array of arguments that can
          be passed, but does not fall into any of the above categories.
          However, none of the supported builtin functions requires such
          an argument. This leaves use with passing unsupported types to
          a function, such as calling \lam{head} on a list of functions.

          In these cases, it would be impossible to generate hardware
          for such a function call anyway, so we can ignore these
          arguments.

          The only way to generate hardware for builtin functions with
          arguments like these, is to expand the function call into an
          equivalent core expression (\eg, expand map into a series of
          function applications). But for now, we choose to simply not
          support expressions like these.
        \stopdesc

        From the above, we can conclude that we can simply ignore these
        other unrepresentable arguments and focus on the first two
        categories instead.
\stopitemize

\subsubsection{Argument extraction}
This transform deals with arguments to functions that
are of a runtime representable type. 

TODO: It seems we can map an expression to a port, not only a signal.
Perhaps this makes this transformation not needed?
TODO: Say something about dataconstructors (without arguments, like True
or False), which are variable references of a runtime representable
type, but do not result in a signal.

To reduce a complex expression to a simple variable reference, we create
a new let expression around the application, which binds the complex
expression to a new variable. The original function is then applied to
this variable.

%\transform{Argument extract}
%{
%\lam{Y} is of a hardware representable type
%
%\lam{Y} is not a variable referene
%
%\conclusion
%
%\trans{X Y}{let z = Y in X z}
%}

\subsubsection{Function extraction}
This transform deals with function-typed arguments to builtin functions.
Since these arguments cannot be propagated, we choose to extract them
into a new global function instead.

Any free variables occuring in the extracted arguments will become
parameters to the new global function. The original argument is replaced
with a reference to the new function, applied to any free variables from
the original argument.

%\transform{Function extraction}
%{
%\lam{X} is a (partial application of) a builtin function
%
%\lam{Y} is not an application
%
%\lam{Y} is not a variable reference
%
%\conclusion
%
%\lam{f0 ... fm} = free local vars of \lam{Y}
%
%\lam{y} is a new global variable
%
%\lam{y = λf0 ... fn.Y}
%
%\trans{X Y}{X (y f0 ... fn)}
%}

\subsubsection{Argument propagation}
This transform deals with arguments to user-defined functions that are
not representable at runtime. This means these arguments cannot be
preserved in the final form and most be {\em propagated}.

Propagation means to create a specialized version of the called
function, with the propagated argument already filled in. As a simple
example, in the following program:

\startlambda
f = λa.λb.a + b
inc = λa.f a 1
\stoplambda

we could {\em propagate} the constant argument 1, with the following
result:

\startlambda
f' = λa.a + 1
inc = λa.f' a
\stoplambda

Special care must be taken when the to-be-propagated expression has any
free variables. If this is the case, the original argument should not be
removed alltogether, but replaced by all the free variables of the
expression. In this way, the original expression can still be evaluated
inside the new function. Also, this brings us closer to our goal: All
these free variables will be simple variable references.

To prevent us from propagating the same argument over and over, a simple
local variable reference is not propagated (since is has exactly one
free variable, itself, we would only replace that argument with itself).

This shows that any free local variables that are not runtime representable
cannot be brought into normal form by this transform. We rely on an
inlining transformation to replace such a variable with an expression we
can propagate again.

TODO: Move these definitions somewhere sensible.

Definition: A global variable is any variable that is bound at the
top level of a program. A local variable is any other variable.

Definition: A hardware representable type is a type that we can generate
a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
unsigned word, etc. Types that are not runtime representable notably
include (but are not limited to): Types, dictionaries, functions.

Definition: A builtin function is a function for which a builtin
hardware translation is available, because its actual definition is not
translatable. A user-defined function is any other function.

\starttrans
x = E
~
x Y0 ... Yi ... Yn                               \lam{Yi} is not of a runtime representable type
---------------------------------------------    \lam{Yi} is not a local variable reference
x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .        \lam{f0 ... fm} = free local vars of \lam{Y_i}
      E y0 ... yi-1 Yi yi+1 ... yn   
~
x' y0 ... yi-1 f0 ...  fm Yi+1 ... Yn
\stoptrans

\subsection{Cast propagation / simplification}
This transform pushes casts down into the expression as far as possible.

\subsection{Return value simplification}
Currently implemented using lambda simplification, let simplification, and
top simplification. Should change.

\subsection{Example sequence}

This section lists an example expression, with a sequence of transforms
applied to it. The exact transforms given here probably don't exactly
match the transforms given above anymore, but perhaps this can clarify
the big picture a bit.

TODO: Update or remove this section.

\startlambda
  λx.
    let s = foo x
    in
      case s of
        (a, b) ->
          case a of
            High -> add
            Low -> let
              op' = case b of
                High -> sub
                Low  -> λc.λd.c
              in
                λc.λd.op' d c
\stoplambda

After top-level η-abstraction:

\startlambda
  λx.λc.λd.
    (let s = foo x
    in
      case s of
        (a, b) ->
          case a of
            High -> add
            Low -> let
              op' = case b of
                High -> sub
                Low  -> λc.λd.c
              in
                λc.λd.op' d c
    ) c d
\stoplambda

After (extended) β-reduction:

\startlambda
  λx.λc.λd.
    let s = foo x
    in
      case s of
        (a, b) ->
          case a of
            High -> add c d
            Low -> let
              op' = case b of
                High -> sub
                Low  -> λc.λd.c
              in
                op' d c
\stoplambda

After return value extraction:

\startlambda
  λx.λc.λd.
    let s = foo x
        r = case s of
              (a, b) ->
                case a of
                  High -> add c d
                  Low -> let
                    op' = case b of
                      High -> sub
                      Low  -> λc.λd.c
                    in
                      op' d c
    in
      r
\stoplambda

Scrutinee simplification does not apply.

After case binder wildening:

\startlambda
  λx.λc.λd.
    let s = foo x
        a = case s of (a, _) -> a
        b = case s of (_, b) -> b
        r = case s of (_, _) ->
              case a of
                High -> add c d
                Low -> let op' = case b of
                             High -> sub
                             Low  -> λc.λd.c
                       in
                         op' d c
    in
      r
\stoplambda

After case value simplification

\startlambda
  λx.λc.λd.
    let s = foo x
        a = case s of (a, _) -> a
        b = case s of (_, b) -> b
        r = case s of (_, _) -> r'
        rh = add c d
        rl = let rll = λc.λd.c
                 op' = case b of
                   High -> sub
                   Low  -> rll
             in
               op' d c
        r' = case a of
               High -> rh
               Low -> rl
    in
      r
\stoplambda

After let flattening:

\startlambda
  λx.λc.λd.
    let s = foo x
        a = case s of (a, _) -> a
        b = case s of (_, b) -> b
        r = case s of (_, _) -> r'
        rh = add c d
        rl = op' d c
        rll = λc.λd.c
        op' = case b of
          High -> sub
          Low  -> rll
        r' = case a of
               High -> rh
               Low -> rl
    in
      r
\stoplambda

After function inlining:

\startlambda
  λx.λc.λd.
    let s = foo x
        a = case s of (a, _) -> a
        b = case s of (_, b) -> b
        r = case s of (_, _) -> r'
        rh = add c d
        rl = (case b of
          High -> sub
          Low  -> λc.λd.c) d c
        r' = case a of
          High -> rh
          Low -> rl
    in
      r
\stoplambda

After (extended) β-reduction again:

\startlambda
  λx.λc.λd.
    let s = foo x
        a = case s of (a, _) -> a
        b = case s of (_, b) -> b
        r = case s of (_, _) -> r'
        rh = add c d
        rl = case b of
          High -> sub d c
          Low  -> d
        r' = case a of
          High -> rh
          Low -> rl
    in
      r
\stoplambda

After case value simplification again:

\startlambda
  λx.λc.λd.
    let s = foo x
        a = case s of (a, _) -> a
        b = case s of (_, b) -> b
        r = case s of (_, _) -> r'
        rh = add c d
        rlh = sub d c
        rl = case b of
          High -> rlh
          Low  -> d
        r' = case a of
          High -> rh
          Low -> rl
    in
      r
\stoplambda

After case removal:

\startlambda
  λx.λc.λd.
    let s = foo x
        a = case s of (a, _) -> a
        b = case s of (_, b) -> b
        r = r'
        rh = add c d
        rlh = sub d c
        rl = case b of
          High -> rlh
          Low  -> d
        r' = case a of
          High -> rh
          Low -> rl
    in
      r
\stoplambda

After let bind removal:

\startlambda
  λx.λc.λd.
    let s = foo x
        a = case s of (a, _) -> a
        b = case s of (_, b) -> b
        rh = add c d
        rlh = sub d c
        rl = case b of
          High -> rlh
          Low  -> d
        r' = case a of
          High -> rh
          Low -> rl
    in
      r'
\stoplambda

Application simplification is not applicable.