X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=f1b53dfa7bc681969763e478045cec681ca62b09;hp=5647ae08426d9c54c1cc71fe22cd649f1fa458ea;hb=4703461b0093f5c9a83876fad9d21a34c7a28eb4;hpb=8515f491f83e63caa71de03c6e71b25df12aedb2

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 5647ae0..f1b53df 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -317,9 +317,7 @@
       \italic{normal} = \italic{lambda}
       \italic{lambda} = λvar.\italic{lambda} (representable(var))
                       | \italic{toplet} 
-      \italic{toplet} = let \italic{binding} in \italic{toplet} 
-                      | letrec [\italic{binding}] in \italic{toplet}
-                      | var (representable(varvar))
+      \italic{toplet} = letrec [\italic{binding}...] in var (representable(varvar))
       \italic{binding} = var = \italic{rhs} (representable(rhs))
                        -- State packing and unpacking by coercion
                        | var0 = var1 :: State ty (lvar(var1))
@@ -590,6 +588,8 @@
       In the following sections, we will be using a number of functions and
       notations, which we will define here.
 
+      TODO: Define substitution
+
       \subsubsection{Other concepts}
         A \emph{global variable} is any variable that is bound at the
         top level of a program, or an external module. A \emph{local variable} is any
@@ -784,8 +784,8 @@
 
       \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
-        it).
+        (which usually occurs when unused let binding removal removes the last
+        binding from it).
 
         \starttrans
         letrec in M
@@ -793,67 +793,70 @@
         M
         \stoptrans
 
+        TODO: Example
+
       \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
         resulting \small{VHDL} a lot shorter.
 
-        \starttrans
-        letnonrec
-          a = b
-        in
-          M
-        -----------------
-        M[b/a]
-        \stoptrans
-
         \starttrans
         letrec
+          a0 = E0
           \vdots
-          a = b
+          ai = b
           \vdots
+          an = En
         in
           M
-        -----------------
-        let
-          \vdots [b/a]
-          \vdots [b/a]
+        -----------------------------  \lam{b} is a variable reference
+        letrec
+          a0 = E0 [b/ai]
+          \vdots
+          ai-1 = Ei-1 [b/ai]
+          ai+1 = Ei+1 [b/ai]
+          \vdots
+          an = En [b/ai]
         in
-          M[b/a]
+          M[b/ai]
         \stoptrans
 
+        TODO: Example
+
       \subsubsection{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
+        (since unused 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 \small{VHDL} a lot shorter.
 
-        \starttrans
-        let a = E in M
-        ----------------------------    \lam{a} does not occur free in \lam{M}
-        M
-        \stoptrans
-
         \starttrans
         letrec
+          a0 = E0
           \vdots
-          a = E
+          ai = Ei
           \vdots
+          an = En
         in
-          M
-        ----------------------------    \lam{a} does not occur free in \lam{M}
+          M                             \lam{a} does not occur free in \lam{M}
+        ----------------------------    \forall j, 0 <= j <= n, j ≠ i (\lam{a} does not occur free in \lam{Ej})
         letrec
+          a0 = E0
           \vdots
+          ai-1 = Ei-1
+          ai+1 = Ei+1
           \vdots
+          an = En
         in
           M
         \stoptrans
 
+        TODO: Example
+
       \subsubsection{Cast propagation / simplification}
         This transform pushes casts down into the expression as far as possible.
         Since its exact role and need is not clear yet, this transformation is
@@ -862,7 +865,7 @@
       \subsubsection{Compiler generated top level binding inlining}
         TODO
 
-    \section{Program structure}
+    \subsection{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
@@ -904,14 +907,14 @@
         specialization).
 
         \starttrans
-        (let binds in E) M
+        (letrec binds in E) M
         -----------------
-        let binds in E M
+        letrec binds in E M
         \stoptrans
 
         % And an example
         \startbuffer[from]
-        ( let 
+        ( letrec
             val = 1
           in 
             add val
@@ -919,7 +922,7 @@
         \stopbuffer
 
         \startbuffer[to]
-        let 
+        letrec
           val = 1
         in 
           add val 3
@@ -955,10 +958,24 @@
 
         \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
-        this needed exactly?
+      \subsubsection{Let recursification}
+        This transformation makes all non-recursive lets recursive. In the
+        end, we want a single recursive let in our normalized program, so all
+        non-recursive lets can be converted. This also makes other
+        transformations simpler: They can simply assume all lets are
+        recursive.
+
+        \starttrans
+        let
+          a = E
+        in
+          M
+        ------------------------------------------
+        letrec
+          a = E
+        in
+          M
+        \stoptrans
 
       \subsubsection{Let flattening}
         This transformation puts nested lets in the same scope, by lifting the
@@ -966,21 +983,10 @@
         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
-        dederecursification 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)
+          x = (letrec bindings in M)
           \vdots
         in
           N
@@ -995,33 +1001,22 @@
         \stoptrans
 
         \startbuffer[from]
-        let
+        letrec
           a = letrec
             x = 1
             y = 2
           in
             x + y
         in
-          letrec
-            b = let c = 3 in a + c
-            d = 4
-          in
-            d + b
+          a
         \stopbuffer
         \startbuffer[to]
         letrec
           x = 1
           y = 2
+          a = x + y
         in
-          let
-            a = x + y
-          in
-            letrec
-              c = 3
-              b = a + c
-              d = 4
-            in
-              d + b
+          a
         \stopbuffer
 
         \transexample{Let flattening}{from}{to}
@@ -1051,7 +1046,7 @@
         ~                                \lam{E} is not a lambda abstraction
         E                                \lam{E} is not a let expression
         ---------------------------      \lam{E} is not a local variable reference
-        let x = E in x
+        letrec x = E in x
         \stoptrans
 
         \starttrans
@@ -1059,7 +1054,7 @@
         ~                                \lam{E} is representable
         E                                \lam{E} is not a let expression
         ---------------------------      \lam{E} is not a local variable reference
-        let x = E in x
+        letrec x = E in x
         \stoptrans
 
         \starttrans
@@ -1067,7 +1062,7 @@
         ~                                \lam{E} is representable
         E                                \lam{E} is not a local variable reference
         ---------------------------
-        let x = E in x
+        letrec x = E in x
         \stoptrans
 
         \startbuffer[from]
@@ -1075,7 +1070,7 @@
         \stopbuffer
 
         \startbuffer[to]
-        x = let x = add 1 2 in x
+        x = letrec x = add 1 2 in x
         \stopbuffer
 
         \transexample{Return value simplification}{from}{to}
@@ -1235,7 +1230,7 @@
         \starttrans
         M N
         --------------------    \lam{N} is of a representable type
-        let x = N in M x        \lam{N} is not a local variable reference
+        letrec x = N in M x     \lam{N} is not a local variable reference
         \stoptrans
 
         \startbuffer[from]
@@ -1243,7 +1238,7 @@
         \stopbuffer
 
         \startbuffer[to]
-        let x = add a 1 in add x 1
+        letrec x = add a 1 in add x 1
         \stopbuffer
 
         \transexample{Argument extraction}{from}{to}
@@ -1267,7 +1262,7 @@
         \starttrans
         M N                     \lam{M} is a (partial aplication of a) builtin function.
         ---------------------   \lam{f0 ... fn} = free local variables of \lam{N}
-        M x f0 ... fn           \lam{N :: a -> b}
+        M (x f0 ... fn)         \lam{N :: a -> b}
         ~                       \lam{N} is not a (partial application of) a top level function
         x = λf0 ... λfn.N
         \stoptrans
@@ -1279,16 +1274,18 @@
         \stopbuffer
 
         \startbuffer[to]
-        x0 = λb.λa.add a b
-        ~
-        map x0 xs
+        map (x0 b) xs
 
-        x1 = λb.add b
         map x1 ys
+        ~
+        x0 = λb.λa.add a b
+        x1 = λb.add b
         \stopbuffer
 
         \transexample{Function extraction}{from}{to}
 
+        Note that \lam{x0} and {x1} will still need normalization after this.
+
       \subsubsection{Argument propagation}
         This transform deals with arguments to user-defined functions that are
         not representable at runtime. This means these arguments cannot be
@@ -1303,7 +1300,7 @@
         inc = λa.f a 1
         \stoplambda
 
-        we could {\em propagate} the constant argument 1, with the following
+        We could {\em propagate} the constant argument 1, with the following
         result:
 
         \startlambda
@@ -1350,7 +1347,7 @@
         case E of
           alts
         -----------------        \lam{E} is not a local variable reference
-        let x = E in 
+        letrec x = E in 
           case E of
             alts
         \stoptrans
@@ -1362,7 +1359,7 @@
         \stopbuffer
 
         \startbuffer[to]
-        let x = foo a in
+        letrec x = foo a in
           case x of
             True -> a
             False -> b
@@ -1388,7 +1385,7 @@
           \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
+        letrec
           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
@@ -1430,7 +1427,7 @@
           (,) b c -> add b c
         \stopbuffer
         \startbuffer[to]
-        letnonrec
+        letrec
           b = case a of (,) b c -> b
           c = case a of (,) b c -> c
           x0 = add b c
@@ -1503,31 +1500,32 @@
         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 
+          a0 = E0
           \vdots
-          a = E
+          ai = Ei
           \vdots
+          an = En
         in
           M
-        --------------------------    \lam{E} has a non-representable type.
+        --------------------------    \lam{Ei} has a non-representable type.
         letrec
-          \vdots [E/a]
-          \vdots [E/a]
+          a0 = E0 [Ei/ai]
+          \vdots
+          ai-1 = Ei-1 [Ei/ai]
+          ai+1 = Ei+1 [Ei/ai]
+          \vdots
+          an = En [Ei/ai]
         in
-          M[E/a]
+          M[Ei/ai]
         \stoptrans
 
         \startbuffer[from]
         letrec
           a = smallInteger 10
-          inc = λa -> add a 1
+          inc = λb -> add b 1
           inc' = add 1
           x = fromInteger a 
         in
@@ -1538,10 +1536,10 @@
         letrec
           x = fromInteger (smallInteger 10)
         in
-          (λa -> add a 1) (add 1 x)
+          (λb -> add b 1) (add 1 x)
         \stopbuffer
 
-        \transexample{Let flattening}{from}{to}
+        \transexample{None representable binding inlining}{from}{to}
 
 
   \section{Provable properties}