Reorder and complete the list of transformations.

This does not add any content, except for updating β-reduction.

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index b91eb40edda218c60ccb1fc951a2da436490af10..e609cb3d2874655ea38297c8c75637368b1fa2d7 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -240,41 +240,44 @@ 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).
-\startbuffer[from]
+
+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
-\stopbuffer
-\startbuffer[to]
+-----------------
 case x of
   p1 -> E1 M
   \vdots
   pn -> En M
-\stopbuffer
+\stoptrans
 
-%\transform{Extended β-reduction}
-%{
-%\conclusion
-%\trans{(λx.E) M}{E[M/x]}
-%
-%\nextrule
-%\conclusion
-%\trans{(let binds in E) M}{let binds in E M}
-%
-%\nextrule
-%\conclusion
-%\transbuf{from}{to}
-%}
+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
+( 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]
@@ -288,6 +291,34 @@ in
 
 \transexample{Extended β-reduction}{from}{to}
 
+\subsection{Let derecursification}
+
+\subsection{Let flattening}
+This transform turns two nested lets (\lam{let x = (let ... in ...) in
+...}) into a single let.
+
+\subsection{Empty let removal}
+
+\subsection{Simple let binding removal}
+This transforms inlines simple let bindings (\eg a = b).
+
+\subsection{Unused let binding removal}
+
+\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:
@@ -526,61 +557,12 @@ x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .        \lam{f0 ... fm} = free local v
 x' y0 ... yi-1 f0 ...  fm Yi+1 ... Yn
 \stoptrans
 
-%\transform{Argument propagation}
-%{
-%\lam{x} is a global variable, bound to a user-defined function
-%
-%\lam{x = E}
-%
-%\lam{Y_i} is not of a runtime representable type
-%
-%\lam{Y_i} is not a local variable reference
-%
-%\conclusion
-%
-%\lam{f0 ... fm} = free local vars of \lam{Y_i}
-%
-%\lam{x'} is a new global variable
-%
-%\lam{x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . E y0 ... yi-1 Yi yi+1 ... yn}
-%
-%\trans{x Y0 ... Yi ... Yn}{x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn}
-%}
-%
-%TODO: The above definition looks too complicated... Can we find
-%something more concise?
-
-\subsection{Cast propagation}
+\subsection{Cast propagation / simplification}
 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{Return value simplification}
+Currently implemented using lambda simplification, let simplification, and
+top simplification. Should change.
 
 \subsection{Example sequence}