-\subsection{Introducing main scope}
-This transformation is meant to introduce a single let expression that will be
-the "main scope". This is the let expression as described under requirement
-\ref[letexpr]. This let expression will contain only a single binding, which
-binds the original expression to some identifier and then evalutes to just
-this identifier (to comply with requirement \in[retexpr]).
-
-Formally, we can describe the transformation as follows.
-
-\transformold{Main scope introduction}
-{
-\NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
-\NR
-\NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
-\NC \app{transform'}{\expr{expr}} \NC = \expr{\letexpr{\bind{x}{expr}}{x}} \NR
-}
-
-When applying this transformation to our running example, we get the following
-program.
-
-\starttyping
- \x c d ->
- let r = (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
- )
- in
- r
-\stoptyping
-
-\subsection{Scope flattening}
-This transformation tries to flatten the topmost let expression in a bind,
-{\em i.e.}, bind all identifiers in the same scope, and bind them to simple
-expressions only (so simplify deeply nested expressions).
-
-Formally, we can describe the transformation as follows.
-
-\transformold{Main scope introduction} { \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
-\NR
-\NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
-\NC \app{transform'}{\expr{\letexpr{binds}{expr}}} \NC = \expr{\letexpr{\app{concat . map . flatten}{binds}}{expr}}\NR
-\NR
-\NC \app{flatten}{\expr{\bind{x}{\letexpr{binds}{expr}}}} \NC = (\app{concat . map . flatten}{binds}) \cup \{\app{flatten}{\expr{\bind{x}{expr}}}\}\NR
-\NC \app{flatten}{\expr{\bind{x}{\case{s}{alts}}}} \NC = \app{concat}{binds'} \cup \{\bind{x}{\case{s}{alts'}}\}\NR
-\NC \NC \where{(binds', alts')=\app{unzip.map.(flattenalt s)}{alts}}\NR
-\NC \app{\app{flattenalt}{s}}{\expr{\alt{\app{con}{x_0\;..\;x_n}}{expr}}} \NC = (extracts \cup \{\app{flatten}{bind}\}, alt)\NR
-\NC \NC \where{extracts =\{\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_0}}},}\NR
-\NC \NC \;..\;,\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_n}}}\} \NR
-\NC \NC bind = \expr{\bind{y}{expr}}\NR
-\NC \NC alt = \expr{\alt{\app{con}{\_\;..\;\_}}{y}}\NR
-}
-
-When applying this transformation to our running example, we get the following
-program.
-
-\starttyping
- \x c d ->
- let s = foo x
- r = case s of
- (_, _) -> y
- a = case s of (a, b) -> a
- b = case s of (a, b) -> b
- y = case a of
- High -> g
- Low -> h
- g = add c d
- h = op' d c
- op' = case b of
- High -> i
- Low -> j
- i = sub
- j = \c d -> c
- in
- r
-\stoptyping
-
-\subsection{More transformations}
-As noted before, the above transformations are not complete. Other needed
-transformations include:
-\startitemize
-\item Inlining of local identifiers with a function type. Since these cannot
-be represented in hardware directly, they must be transformed into something
-else. Inlining them should always be possible without loss of semantics (TODO:
-How true is this?) and can expose new possibilities for other transformations
-passes (such as application propagation when inlining {\tt j} above).
-\item A variation on inlining local identifiers is the propagation of
-function arguments with a function type. This will probably be initiated when
-transforming the caller (and not the callee), but it will also deal with
-identifiers with a function type that are unrepresentable in hardware.
-
-Special care must be taken here, since the expression that is propagated into
-the callee comes from a different scope. The function typed argument must thus
-be replaced by any identifiers from the callers scope that the propagated
-expression uses.
-
-Note that propagating an argument will change both a function's interface and
-implementation. For this to work, a new function should be created instead of
-modifying the original function, so any other callers will not be broken.
-\item Something similar should happen with return values with function types.
-\item Polymorphism must be removed from all user-defined functions. This is
-again similar to propagation function typed arguments, since this will also
-create duplicates of functions (for a specific type). This is an operation
-that is commonly known as "specialization" and already happens in GHC (since
-non-polymorph functions can be a lot faster than generic ones).
-\item More builtin expressions should be added and these should be evaluated
-by the compiler. For example, map, fold, +.
-\stopitemize
-
-Initial example
+\subsection{Cast propagation}
+This transform pushes casts down into the expression as far as possible.
+\subsection{Let recursification}
+This transform makes all lets recursive.
+\subsection{Let simplification}
+This transform makes the result value of all let expressions a simple
+variable reference.
+\subsection{Let flattening}
+This transform turns two nested lets (\lam{let x = (let ... in ...) in
+...}) into a single let.
+\subsection{Simple let binding removal}
+This transforms inlines simple let bindings (\eg a = b).
+\subsection{Function 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 binder wildening}
+This transform replaces all binders of a each case alternative with a
+wild binder (\ie, one that is never referred to). This will possibly
+introduce a number of new "selector" case statements, that only select
+one element from an algebraic datatype and bind it to a variable.
+\subsection{Case value simplification}
+This transform simplifies the result value of each case alternative by
+binding the value in a let expression and replacing the value by a
+simple variable reference.
+\subsection{Case removal}
+This transform removes any case statements with a single alternative and
+only wild binders.
+
+\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.