+ Since this expression is at top level, it does not occur at a function
+ position of an application. However, The expression is a lambda abstraction,
+ so this transformation does not apply.
+
+ The next expression we could apply this transformation to, is the body of
+ the lambda abstraction:
+
+\startlambda
+case opcode of
+ Low -> (+)
+ High -> (-)
+\stoplambda
+
+ The type of this expression is \lam{Word -> Word -> Word}, which again
+ matches \lam{a -> b}. The expression is the body of a lambda expression, so
+ it does not occur at a function position of an application. Finally, the
+ expression is not a lambda abstraction but a case expression, so all the
+ conditions match. There are no context conditions to match, so the
+ transformation applies.
+
+ By now, the placeholder \lam{E} is bound to the entire expression. The
+ placeholder \lam{x}, which occurs in the replacement template, is not bound
+ yet, so we need to generate a fresh binder for that. Let's use the binder
+ \lam{a}. This results in the following replacement expression:
+
+\startlambda
+λa.(case opcode of
+ Low -> (+)
+ High -> (-)) a
+\stoplambda
+
+ Continuing with this expression, we see that the transformation does not
+ apply again (it is a lambda expression). Next we look at the body of this
+ labmda abstraction:
+
+\startlambda
+(case opcode of
+ Low -> (+)
+ High -> (-)) a
+\stoplambda
+
+ Here, the transformation does apply, binding \lam{E} to the entire
+ expression and \lam{x} to the fresh binder \lam{b}, resulting in the
+ replacement:
+
+\startlambda
+λb.(case opcode of
+ Low -> (+)
+ High -> (-)) a b
+\stoplambda
+
+ Again, the transformation does not apply to this lambda abstraction, so we
+ look at its body. For brevity, we'll put the case statement on one line from
+ now on.
+
+\startlambda
+(case opcode of Low -> (+); High -> (-)) a b
+\stoplambda
+
+ The type of this expression is \lam{Word}, so it does not match \lam{a -> b}
+ and the transformation does not apply. Next, we have two options for the
+ next expression to look at: The function position and argument position of
+ the application. The expression in the argument position is \lam{b}, which
+ has type \lam{Word}, so the transformation does not apply. The expression in
+ the function position is:
+
+\startlambda
+(case opcode of Low -> (+); High -> (-)) a
+\stoplambda
+
+ Obviously, the transformation does not apply here, since it occurs in
+ function position. In the same way the transformation does not apply to both
+ components of this expression (\lam{case opcode of Low -> (+); High -> (-)}
+ and \lam{a}), so we'll skip to the components of the case expression: The
+ scrutinee and both alternatives. Since the opcode is not a function, it does
+ not apply here, and we'll leave both alternatives as an exercise to the
+ reader. The final function, after all these transformations becomes:
+
+\startlambda
+alu :: Bit -> Word -> Word -> Word
+alu = λopcode.λa.b. (case opcode of
+ Low -> λa1.λb1 (+) a1 b1
+ High -> λa2.λb2 (-) a2 b2) a b
+\stoplambda
+
+ In this case, the transformation does not apply anymore, though this might
+ not always be the case (e.g., the application of a transformation on a
+ subexpression might open up possibilities to apply the transformation
+ further up in the expression).
+
+\subsection{Transformation application}
+In this chapter we define a number of transformations, but how will we apply
+these? As stated before, our normal form is reached as soon as no
+transformation applies anymore. This means our application strategy is to
+simply apply any transformation that applies, and continuing to do that with
+the result of each transformation.
+
+In particular, we define no particular order of transformations. Since
+transformation order should not influence the resulting normal form (see TODO
+ref), this leaves the implementation free to choose any application order that
+results in an efficient implementation.
+
+When applying a single transformation, we try to apply it to every (sub)expression
+in a function, not just the top level function. This allows us to keep the
+transformation descriptions concise and powerful.
+
+\subsection{Definitions}
+In the following sections, we will be using a number of functions and
+notations, which we will define here.
+
+\subsubsection{Other concepts}
+A \emph{global variable} is any variable that is bound at the
+top level of a program, or an external module. A \emph{local variable} is any
+other variable (\eg, variables local to a function, which can be bound by
+lambda abstractions, let expressions and pattern matches of case
+alternatives). Note that this is a slightly different notion of global versus
+local than what \small{GHC} uses internally.
+\defref{global variable} \defref{local variable}
+
+A \emph{hardware representable} (or just \emph{representable}) type or value
+is (a value of) 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.
+\defref{representable}
+
+A \emph{builtin function} is a function supplied by the Cλash framework, whose
+implementation is not valid Cλash. The implementation is of course valid
+Haskell, for simulation, but it is not expressable in Cλash.
+\defref{builtin function} \defref{user-defined function}
+
+For these functions, Cλash has a \emph{builtin hardware translation}, so calls
+to these functions can still be translated. These are functions like
+\lam{map}, \lam{hwor} and \lam{length}.
+
+A \emph{user-defined} function is a function for which we do have a Cλash
+implementation available.