From: Matthijs Kooijman Date: Mon, 2 Nov 2009 13:53:21 +0000 (+0100) Subject: Improve Normalization chapter a bit. X-Git-Tag: final-thesis~178 X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=commitdiff_plain;h=8515f491f83e63caa71de03c6e71b25df12aedb2 Improve Normalization chapter a bit. --- diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index d93717a..5647ae0 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -744,6 +744,15 @@ this notation are still a bit fuzzy, so comments are welcom. \subsection{General cleanup} + These transformations are general cleanup transformations, that aim to + make expressions simpler. These transformations usually clean up the + mess left behind by other transformations or clean up expressions to + expose new transformation opportunities for other transformations. + + Most of these transformations are standard optimizations in other + compilers as well. However, in our compiler, most of these are not just + optimizations, but they are required to get our program into normal + form. \subsubsection{β-reduction} β-reduction is a well known transformation from lambda calculus, where it is @@ -756,8 +765,6 @@ sure that most lambda abstractions will eventually be reducable by β-reduction. - TODO: Define substitution syntax - \starttrans (λx.E) M ----------------- @@ -775,64 +782,6 @@ \transexample{β-reduction}{from}{to} - \subsubsection{Application propagation} - This transformation is meant to propagate application expressions downwards - into expressions as far as possible. This allows partial applications inside - expressions to become fully applied and exposes new transformation - possibilities for other transformations (like β-reduction). - - \starttrans - let binds in E) M - ----------------- - let binds in E M - \stoptrans - - % And an example - \startbuffer[from] - ( let - val = 1 - in - add val - ) 3 - \stopbuffer - - \startbuffer[to] - let - val = 1 - in - add val 3 - \stopbuffer - - \transexample{Application propagation for a let expression}{from}{to} - - \starttrans - (case x of - p1 -> E1 - \vdots - pn -> En) M - ----------------- - case x of - p1 -> E1 M - \vdots - pn -> En M - \stoptrans - - % And an example - \startbuffer[from] - ( case x of - True -> id - False -> neg - ) 1 - \stopbuffer - - \startbuffer[to] - case x of - True -> id 1 - False -> neg 1 - \stopbuffer - - \transexample{Application propagation for a case expression}{from}{to} - \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 @@ -844,7 +793,7 @@ M \stoptrans - \subsubsection{Simple let binding removal} + \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 @@ -914,12 +863,17 @@ TODO \section{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 + value definitions in let bindings and making the final return value a + simple variable reference. \subsubsection{η-abstraction} This transformation makes sure that all arguments of a function-typed expression are named, by introducing lambda expressions. When combined with - β-reduction and function inlining below, all function-typed expressions should - be lambda abstractions or global identifiers. + β-reduction and non-representable binding inlining, all function-typed + expressions should be lambda abstractions or global identifiers. \starttrans E \lam{E :: a -> b} @@ -942,6 +896,65 @@ \transexample{η-abstraction}{from}{to} + \subsubsection{Application propagation} + This transformation is meant to propagate application expressions downwards + into expressions as far as possible. This allows partial applications inside + expressions to become fully applied and exposes new transformation + opportunities for other transformations (like β-reduction and + specialization). + + \starttrans + (let binds in E) M + ----------------- + let binds in E M + \stoptrans + + % And an example + \startbuffer[from] + ( let + val = 1 + in + add val + ) 3 + \stopbuffer + + \startbuffer[to] + let + val = 1 + in + add val 3 + \stopbuffer + + \transexample{Application propagation for a let expression}{from}{to} + + \starttrans + (case x of + p1 -> E1 + \vdots + pn -> En) M + ----------------- + case x of + p1 -> E1 M + \vdots + pn -> En M + \stoptrans + + % And an example + \startbuffer[from] + ( case x of + True -> id + False -> neg + ) 1 + \stopbuffer + + \startbuffer[to] + case x of + True -> id 1 + False -> neg 1 + \stopbuffer + + \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 @@ -956,7 +969,7 @@ 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 - rederecursification transformation will do this instead. + dederecursification transformation will do this instead. \starttrans letnonrec x = (let bindings in M) in N @@ -1025,6 +1038,14 @@ \lam{E}, any \lam{E} can be transformed, while we only mean the \lam{E} that is bound by \lam{x}. This might need some extra notes or something). + 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, of course. If the return value is not + representable because it has a function type, η-abstraction 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 representable anyway! + \starttrans x = E \lam{E} is representable ~ \lam{E} is not a lambda abstraction @@ -1445,12 +1466,18 @@ \transexample{Case removal}{from}{to} - \subsection{Monomorphisation} - TODO: Better name for this section - + \subsection{Removing polymorphism} Reference type-specialization (== argument propagation) - \subsubsection{Defunctionalization} + Reference polymporphic binding inlining (== non-representable binding + inlining). + + \subsection{Defunctionalization} + These transformations remove most higher order expressions from our + program, making it completely first-order (the only exception here is for + arguments to builtin functions, since we can't specialize builtin + function. TODO: Talk more about this somewhere). + Reference higher-order-specialization (== argument propagation) \subsubsection{Non-representable binding inlining}