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).
 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
 (case x of
   p1 -> E1
   \vdots
   pn -> En) M

-\stopbuffer
-\startbuffer[to]
+-----------------

 case x of
   p1 -> E1 M
   \vdots
   pn -> En M
 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]
 \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]
 \stopbuffer
 
 \startbuffer[to]


@@ -288,6 +291,34 @@ in
 
 \transexample{Extended β-reduction}{from}{to}
 
 
 \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:
 \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
 
 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.
 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}
 
 
 \subsection{Example sequence}