Add content to a bunch more transformations.

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index e609cb3d2874655ea38297c8c75637368b1fa2d7..059ba43c99482828c059de70e1943be972680bd5 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -292,17 +292,147 @@ in
 \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 transform turns two nested lets (\lam{let x = (let ... in ...) in
-...}) into a single let.
+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 transforms inlines simple let bindings (\eg a = b).
+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