From: Matthijs Kooijman Date: Tue, 8 Dec 2009 14:01:04 +0000 (+0100) Subject: Fix the return value simplification transformation. X-Git-Tag: final-thesis~34 X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=commitdiff_plain;h=898bdb75483e570effe1a926592fc938419d83e9;hp=2a5206c6b7117f5342fba4a256e2e08621d6f752 Fix the return value simplification transformation. --- diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index a1dec0a..a811bfe 100644 --- 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 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] @@ -1319,12 +1328,40 @@ \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 @@ -1971,7 +2008,7 @@ 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