Fix the return value simplification transformation.

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index a1dec0a854efabd08ff58e32c07b2d3845dd99b4..a811bfef339e1d613fc6aa25496ab68c92a3ef61 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -1273,45 +1273,54 @@
         This transformation ensures that the return value of a function is always a
         simple local variable reference.
 
         This transformation ensures that the return value of a function is always a
         simple local variable reference.
 

-        This transformation only applies to the entire body of a
-        function instead of any subexpression in a function. This is
-        achieved by the contexts, like \lam{x = E}, though this is
-        strictly not correct (you could read this as "if there is any
-        function \lam{x} that binds \lam{E}, any \lam{E} can be
-        transformed, while we only mean the \lam{E} that is bound by
-        \lam{x}).
-
-        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. If the return value is
-        not representable because it has a function type, η-expansion
-        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 translatable anyway.
+        The basic idea of this transformation is to take the body of a
+        function and bind it with a let expression (so the body of that let
+        expression becomes a variable reference that can be used as the output
+        port). If the body of the function happens to have lambda abstractions
+        at the top level (which is allowed by the intended normal
+        form\refdef{intended normal form definition}), we take the body of the
+        inner lambda instead. If that happens to be a let expression already
+        (which is allowed by the intended normal form), we take the body of
+        that let (which is not allowed to be anything but a variable reference
+        according the the intended normal form).
+
+        This transformation uses the context conditions in a special way.
+        These contexts, like \lam{x = λv1 ... λvn.E}, are above the dotted
+        line and provide a condition on the environment (\ie\ they require a
+        certain top level binding to be present). These ensure that
+        expressions are only transformed when they are in the functions
+        \quote{return value} directly. This means the context conditions have
+        to interpreted in the right way: not \quote{if there is any function
+        \lam{x} that binds \lam{E}, any \lam{E} can be transformed}, but we
+        mean only the \lam{E} that is bound by \lam{x}).
+
+        Be careful when reading the transformations: Not the entire function
+        from the context is transformed, just a part of it.
+
+        Note that the return value is not simplified if it is not representable.
+        Otherwise, this would cause a loop with the inlining of
+        unrepresentable bindings in
+        \in{section}[sec:normalization:nonrepinline]. If the return value is
+        not representable because it has a function type, η-expansion 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 translatable
+        anyway.

 
         \starttrans
 
         \starttrans

-        x = E                            \lam{E} is representable
-        ~                                \lam{E} is not a lambda abstraction
-        E                                \lam{E} is not a let expression
-        ---------------------------      \lam{E} is not a local variable reference
-        letrec x = E in x
-        \stoptrans
-
-        \starttrans
-        x = λv0 ... λvn.E                \lam{E} is representable
-        ~                                \lam{E} is not a lambda abstraction
-        E                                \lam{E} is not a let expression
-        ---------------------------      \lam{E} is not a local variable reference
-        letrec x = E in x
+        x = λv1 ... λvn.E                \lam{n} can be zero
+        ~                                \lam{E} is representable
+        E                                \lam{E} is not a lambda abstraction
+        ---------------------------      \lam{E} is not a let expression
+        letrec y = E in y                \lam{E} is not a local variable reference

         \stoptrans
 
         \starttrans
         \stoptrans
 
         \starttrans

-        x = λv0 ... λvn.let ... in E
-        ~                                \lam{E} is representable
-        E                                \lam{E} is not a local variable reference
-        -----------------------------
-        letrec x = E in x
+        x = λv1 ... λvn.letrec binds in E     \lam{n} can be zero
+        ~                                     \lam{E} is representable
+        letrec binds in E                     \lam{E} is not a local variable reference
+        ------------------------------------
+        letrec binds; y = E in y

         \stoptrans
 
         \startbuffer[from]
         \stoptrans
 
         \startbuffer[from]


@@ -1319,12 +1328,40 @@
         \stopbuffer
 
         \startbuffer[to]
         \stopbuffer
 
         \startbuffer[to]

-        x = letrec x = add 1 2 in x
+        x = letrec y = add 1 2 in y

         \stopbuffer
 
         \transexample{retvalsimpl}{Return value simplification}{from}{to}
         \stopbuffer
 
         \transexample{retvalsimpl}{Return value simplification}{from}{to}

+
+        \startbuffer[from]
+        x = λa. add 1 a
+        \stopbuffer
+
+        \startbuffer[to]
+        x = λa. letrec 
+          y = add 1 a 
+        in
+          y
+        \stopbuffer
+
+        \transexample{retvalsimpllam}{Return value simplification with a lambda abstraction}{from}{to}

         
         

-        \todo{More examples}
+        \startbuffer[from]
+        x = letrec
+          a = add 1 2 
+        in 
+          add a 3
+        \stopbuffer
+
+        \startbuffer[to]
+        x = letrec
+          a = add 1 2 
+          y = add a 3 
+        in
+          y
+        \stopbuffer
+
+        \transexample{retvalsimpllet}{Return value simplification with a let expression}{from}{to}

 
     \subsection[sec:normalization:argsimpl]{Representable arguments simplification}
       This section contains just a single transformation that deals with
 
     \subsection[sec:normalization:argsimpl]{Representable arguments simplification}
       This section contains just a single transformation that deals with


@@ -1971,7 +2008,7 @@
         to specialize away any unrepresentable literals that are used as
         function arguments. The following two transformations do exactly this.
 
         to specialize away any unrepresentable literals that are used as
         function arguments. The following two transformations do exactly this.
 

-      \subsubsection{Non-representable binding inlining}
+      \subsubsection[sec:normalization:nonrepinline]{Non-representable binding inlining}

         This transform inlines let bindings that are bound to a
         non-representable value. Since we can never generate a signal
         assignment for these bindings (we cannot declare a signal assignment
         This transform inlines let bindings that are bound to a
         non-representable value. Since we can never generate a signal
         assignment for these bindings (we cannot declare a signal assignment