Improve Normalization chapter a bit.

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index d93717a1337e968253320a41d5a25cf32971ae7f..5647ae08426d9c54c1cc71fe22cd649f1fa458ea 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -744,6 +744,15 @@
     this notation are still a bit fuzzy, so comments are welcom.
 
     \subsection{General cleanup}
     this notation are still a bit fuzzy, so comments are welcom.
 
     \subsection{General cleanup}

+      These transformations are general cleanup transformations, that aim to
+      make expressions simpler. These transformations usually clean up the
+       mess left behind by other transformations or clean up expressions to
+       expose new transformation opportunities for other transformations.
+
+       Most of these transformations are standard optimizations in other
+       compilers as well. However, in our compiler, most of these are not just
+       optimizations, but they are required to get our program into normal
+       form.

 
       \subsubsection{β-reduction}
         β-reduction is a well known transformation from lambda calculus, where it is
 
       \subsubsection{β-reduction}
         β-reduction is a well known transformation from lambda calculus, where it is


@@ -756,8 +765,6 @@
         sure that most lambda abstractions will eventually be reducable by
         β-reduction.
 
         sure that most lambda abstractions will eventually be reducable by
         β-reduction.
 

-        TODO: Define substitution syntax
-

         \starttrans
         (λx.E) M
         -----------------
         \starttrans
         (λx.E) M
         -----------------


@@ -775,64 +782,6 @@
 
         \transexample{β-reduction}{from}{to}
 
 
         \transexample{β-reduction}{from}{to}
 

-      \subsubsection{Application propagation}
-        This transformation is meant to propagate application expressions downwards
-        into expressions as far as possible. This allows partial applications inside
-        expressions to become fully applied and exposes new transformation
-        possibilities for other transformations (like β-reduction).
-
-        \starttrans
-        let binds in E) M
-        -----------------
-        let binds in E M
-        \stoptrans
-
-        % And an example
-        \startbuffer[from]
-        ( let 
-            val = 1
-          in 
-            add val
-        ) 3
-        \stopbuffer
-
-        \startbuffer[to]
-        let 
-          val = 1
-        in 
-          add val 3
-        \stopbuffer
-
-        \transexample{Application propagation for a let expression}{from}{to}
-
-        \starttrans
-        (case x of
-          p1 -> E1
-          \vdots
-          pn -> En) M
-        -----------------
-        case x of
-          p1 -> E1 M
-          \vdots
-          pn -> En M
-        \stoptrans
-
-        % And an example
-        \startbuffer[from]
-        ( case x of 
-            True -> id
-            False -> neg
-        ) 1
-        \stopbuffer
-
-        \startbuffer[to]
-        case x of 
-          True -> id 1
-          False -> neg 1
-        \stopbuffer
-
-        \transexample{Application propagation for a case expression}{from}{to}
-

       \subsubsection{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
       \subsubsection{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


@@ -844,7 +793,7 @@
         M
         \stoptrans
 
         M
         \stoptrans
 

-        \subsubsection{Simple let binding removal}
+      \subsubsection{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
         This transformation inlines simple let bindings (\eg a = b).
 
         This transformation is not needed to get into normal form, but makes the


@@ -914,12 +863,17 @@
         TODO
 
     \section{Program structure}
         TODO
 
     \section{Program structure}

+      These transformations are aimed at normalizing the overall structure
+      into the intended form. This means ensuring there is a lambda abstraction
+      at the top for every argument (input port), putting all of the other
+      value definitions in let bindings and making the final return value a
+      simple variable reference.

 
       \subsubsection{η-abstraction}
         This transformation makes sure that all arguments of a function-typed
         expression are named, by introducing lambda expressions. When combined with
 
       \subsubsection{η-abstraction}
         This transformation makes sure that all arguments of a function-typed
         expression are named, by introducing lambda expressions. When combined with

-        β-reduction and function inlining below, all function-typed expressions should
-        be lambda abstractions or global identifiers.
+        β-reduction and non-representable binding inlining, all function-typed
+        expressions should be lambda abstractions or global identifiers.

 
         \starttrans
         E                 \lam{E :: a -> b}
 
         \starttrans
         E                 \lam{E :: a -> b}


@@ -942,6 +896,65 @@
 
         \transexample{η-abstraction}{from}{to}
 
 
         \transexample{η-abstraction}{from}{to}
 

+      \subsubsection{Application propagation}
+        This transformation is meant to propagate application expressions downwards
+        into expressions as far as possible. This allows partial applications inside
+        expressions to become fully applied and exposes new transformation
+        opportunities for other transformations (like β-reduction and
+        specialization).
+
+        \starttrans
+        (let binds in E) M
+        -----------------
+        let binds in E M
+        \stoptrans
+
+        % And an example
+        \startbuffer[from]
+        ( let 
+            val = 1
+          in 
+            add val
+        ) 3
+        \stopbuffer
+
+        \startbuffer[to]
+        let 
+          val = 1
+        in 
+          add val 3
+        \stopbuffer
+
+        \transexample{Application propagation for a let expression}{from}{to}
+
+        \starttrans
+        (case x of
+          p1 -> E1
+          \vdots
+          pn -> En) M
+        -----------------
+        case x of
+          p1 -> E1 M
+          \vdots
+          pn -> En M
+        \stoptrans
+
+        % And an example
+        \startbuffer[from]
+        ( case x of 
+            True -> id
+            False -> neg
+        ) 1
+        \stopbuffer
+
+        \startbuffer[to]
+        case x of 
+          True -> id 1
+          False -> neg 1
+        \stopbuffer
+
+        \transexample{Application propagation for a case expression}{from}{to}
+

       \subsubsection{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
       \subsubsection{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


@@ -956,7 +969,7 @@
         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
         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

-        rederecursification transformation will do this instead.
+        dederecursification transformation will do this instead.

 
         \starttrans
         letnonrec x = (let bindings in M) in N
 
         \starttrans
         letnonrec x = (let bindings in M) in N


@@ -1025,6 +1038,14 @@
         \lam{E}, any \lam{E} can be transformed, while we only mean the \lam{E} that
         is bound by \lam{x}. This might need some extra notes or something).
 
         \lam{E}, any \lam{E} can be transformed, while we only mean the \lam{E} that
         is bound by \lam{x}. This might need some extra notes or something).
 

+        Note that the return value is not simplified if its not representable.
+        Otherwise, this would cause a direct loop with the inlining of
+        unrepresentable bindings, of course. If the return value is not
+        representable because it has a function type, η-abstraction should
+        make sure that this transformation will eventually apply. If the value
+        is not representable for other reasons, the function result itself is
+        not representable, meaning this function is not representable anyway!
+

         \starttrans
         x = E                            \lam{E} is representable
         ~                                \lam{E} is not a lambda abstraction
         \starttrans
         x = E                            \lam{E} is representable
         ~                                \lam{E} is not a lambda abstraction


@@ -1445,12 +1466,18 @@
 
         \transexample{Case removal}{from}{to}
 
 
         \transexample{Case removal}{from}{to}
 

-  \subsection{Monomorphisation}
-    TODO: Better name for this section
-
+  \subsection{Removing polymorphism}

     Reference type-specialization (== argument propagation)
 
     Reference type-specialization (== argument propagation)
 

-  \subsubsection{Defunctionalization}
+    Reference polymporphic binding inlining (== non-representable binding
+    inlining).
+
+  \subsection{Defunctionalization}
+    These transformations remove most higher order expressions from our
+    program, making it completely first-order (the only exception here is for
+    arguments to builtin functions, since we can't specialize builtin
+    function. TODO: Talk more about this somewhere).
+

     Reference higher-order-specialization (== argument propagation)
 
       \subsubsection{Non-representable binding inlining}
     Reference higher-order-specialization (== argument propagation)
 
       \subsubsection{Non-representable binding inlining}