Fix the return value simplification transformation.
authorMatthijs Kooijman <matthijs@stdin.nl>
Tue, 8 Dec 2009 14:01:04 +0000 (15:01 +0100)
committerMatthijs Kooijman <matthijs@stdin.nl>
Tue, 8 Dec 2009 14:01:04 +0000 (15:01 +0100)
Chapters/Normalization.tex

index a1dec0a..a811bfe 100644 (file)
         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
-        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
-        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]
         \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}
+
+        \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
         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