+\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 [b/a]
+ \vdots [b/a]
+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 that have a non-representable type. Since
+we can never generate a signal assignment for these bindings (we cannot
+declare a signal assignment with a non-representable type, for obvious
+reasons), we have no choice but to inline the binding to remove it.
+
+If the binding is non-representable because it is a lambda abstraction, it is
+likely that it will inlined into an application and β-reduction will remove
+the lambda abstraction and turn it into a representable expression at the
+inline site. The same holds for partial applications, which can be turned into
+full applications by inlining.
+
+Other cases of non-representable bindings we see in practice are primitive
+Haskell types. In most cases, these will not result in a valid normalized
+output, but then the input would have been invalid to start with. There is one
+exception to this: When a builtin function is applied to a non-representable
+expression, things might work out in some cases. For example, when you write a
+literal \hs{SizedInt} in Haskell, like \hs{1 :: SizedInt D8}, this results in
+the following core: \lam{fromInteger (smallInteger 10)}, where for example
+\lam{10 :: GHC.Prim.Int\#} and \lam{smallInteger 10 :: Integer} have
+non-representable types. TODO: This/these paragraph(s) should probably become a
+separate discussion somewhere else.
+
+\starttrans
+letnonrec a = E in M
+-------------------------- \lam{E} has a non-representable type.
+M[E/a]
+\stoptrans
+
+\starttrans
+letrec
+ \vdots
+ a = E
+ \vdots
+in
+ M
+-------------------------- \lam{E} has a non-representable type.
+letrec
+ \vdots [E/a]
+ \vdots [E/a]
+in
+ M[E/a]
+\stoptrans
+
+\startbuffer[from]
+letrec
+ a = smallInteger 10
+ inc = λa -> add a 1
+ inc' = add 1
+ x = fromInteger a
+in
+ inc (inc' x)
+\stopbuffer
+
+\startbuffer[to]
+letrec
+ x = fromInteger (smallInteger 10)
+in
+ (λa -> add a 1) (add 1 x)
+\stopbuffer
+
+\transexample{Let flattening}{from}{to}
+
+\subsection{Compiler generated top level binding inlining}
+TODO
+
+\subsection{Scrutinee simplification}
+This transform ensures that the scrutinee of a case expression is always
+a simple variable reference.
+
+\starttrans
+case E of
+ alts
+----------------- \lam{E} is not a local variable reference
+let x = E in
+ case E of
+ alts
+\stoptrans
+
+\startbuffer[from]
+case (foo a) of
+ True -> a
+ False -> b
+\stopbuffer
+
+\startbuffer[to]
+let x = foo a in
+ case x of
+ True -> a
+ False -> b
+\stopbuffer
+
+\transexample{Let flattening}{from}{to}
+
+
+\subsection{Case simplification}
+This transformation ensures that all case expressions become normal form. This
+means they will become one of:
+\startitemize
+\item An extractor case with a single alternative that picks a single field
+from a datatype, \eg \lam{case x of (a, b) -> a}.
+\item A selector case with multiple alternatives and only wild binders, that
+makes a choice between expressions based on the constructor of another
+expression, \eg \lam{case x of Low -> a; High -> b}.
+\stopitemize
+
+\starttrans
+case E of
+ C0 v0,0 ... v0,m -> E0
+ \vdots
+ Cn vn,0 ... vn,m -> En
+--------------------------------------------------- \forall i \forall j, 0 <= i <= n, 0 <= i < m (\lam{wi,j} is a wild (unused) binder)
+letnonrec
+ v0,0 = case x of C0 v0,0 .. v0,m -> v0,0
+ \vdots
+ v0,m = case x of C0 v0,0 .. v0,m -> v0,m
+ x0 = E0
+ \dots
+ vn,m = case x of Cn vn,0 .. vn,m -> vn,m
+ xn = En
+in
+ case E of
+ C0 w0,0 ... w0,m -> x0
+ \vdots
+ Cn wn,0 ... wn,m -> xn
+\stoptrans
+
+TODO: This transformation specified like this is complicated and misses
+conditions to prevent looping with itself. Perhaps we should split it here for
+discussion?
+
+\startbuffer[from]
+case a of
+ True -> add b 1
+ False -> add b 2
+\stopbuffer
+
+\startbuffer[to]
+letnonrec
+ x0 = add b 1
+ x1 = add b 2
+in
+ case a of
+ True -> x0
+ False -> x1
+\stopbuffer
+
+\transexample{Selector case simplification}{from}{to}
+
+\startbuffer[from]
+case a of
+ (,) b c -> add b c
+\stopbuffer
+\startbuffer[to]
+letnonrec
+ b = case a of (,) b c -> b
+ c = case a of (,) b c -> c
+ x0 = add b c
+in
+ case a of
+ (,) w0 w1 -> x0
+\stopbuffer
+
+\transexample{Extractor case simplification}{from}{to}
+
+\subsection{Case removal}
+This transform removes any case statements with a single alternative and
+only wild binders.
+
+These "useless" case statements are usually leftovers from case simplification
+on extractor case (see the previous example).
+
+\starttrans
+case x of
+ C v0 ... vm -> E
+---------------------- \lam{\forall i, 0 <= i <= m} (\lam{vi} does not occur free in E)
+E
+\stoptrans
+
+\startbuffer[from]
+case a of
+ (,) w0 w1 -> x0
+\stopbuffer
+
+\startbuffer[to]
+x0
+\stopbuffer
+
+\transexample{Case removal}{from}{to}
+