Make the normal form use only recursive lets again.
authorMatthijs Kooijman <matthijs@stdin.nl>
Wed, 4 Nov 2009 11:47:34 +0000 (12:47 +0100)
committerMatthijs Kooijman <matthijs@stdin.nl>
Wed, 4 Nov 2009 11:48:33 +0000 (12:48 +0100)
Previously, both recursive and non-recursive lets were allowed, which made
a lot of transformations a lot more complex. Now, all lets are made
recursive again, which makes things simpler.

Also do some other miscellaneous fixes in the Normalization chapter.

Chapters/Normalization.tex

index 5647ae08426d9c54c1cc71fe22cd649f1fa458ea..f1b53dfa7bc681969763e478045cec681ca62b09 100644 (file)
       \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))
       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
 
       \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
         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
       \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
         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
         \stopbuffer
 
         \startbuffer[to]
-        let 
+        letrec
           val = 1
         in 
           add val 3
 
         \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
         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
         \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}
         ~                                \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
         ~                                \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
         ~                                \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]
         \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}
         \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]
         \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}
         \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
         \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
         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
         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
         \stopbuffer
 
         \startbuffer[to]
-        let x = foo a in
+        letrec x = foo a in
           case x of
             True -> a
             False -> b
           \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
           (,) 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
         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
         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}