X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=a1dec0a854efabd08ff58e32c07b2d3845dd99b4;hp=322b2401d6167a08b5ebfc0134e5d14bfd928eb5;hb=313351372e8c609c2875902d9c9a2b89f7c97032;hpb=736a0a7980ef55a90b3d439a49f71c74086eb002 diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 322b240..a1dec0a 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -36,7 +36,7 @@ to this form as the \emph{normal form} of the program. The formal definition of this normal form is quite simple: - \placedefinition{}{\startboxed A program is in \emph{normal form} if none of the + \placedefinition[force]{}{\startboxed A program is in \emph{normal form} if none of the transformations from this chapter apply.\stopboxed} Of course, this is an \quote{easy} definition of the normal form, since our @@ -65,26 +65,6 @@ other expression. \stopitemize - \todo{Intermezzo: functions vs plain values} - - A very simple example of a program in normal form is given in - \in{example}[ex:MulSum]. As you can see, all arguments to the function (which - will become input ports in the generated \VHDL) are at the outer level. - This means that the body of the inner lambda abstraction is never a - function, but always a plain value. - - As the body of the inner lambda abstraction, we see a single (recursive) - let expression, that binds two variables (\lam{mul} and \lam{sum}). These - variables will be signals in the generated \VHDL, bound to the output port - of the \lam{*} and \lam{+} components. - - The final line (the \quote{return value} of the function) selects the - \lam{sum} signal to be the output port of the function. This \quote{return - value} can always only be a variable reference, never a more complex - expression. - - \todo{Add generated VHDL} - \startbuffer[MulSum] alu :: Bit -> Word -> Word -> Word alu = λa.λb.λc. @@ -125,13 +105,33 @@ ncline(add)(sum); \stopuseMPgraphic - \placeexample[here][ex:MulSum]{Simple architecture consisting of a + \placeexample[][ex:MulSum]{Simple architecture consisting of a multiplier and a subtractor.} \startcombination[2*1] {\typebufferlam{MulSum}}{Core description in normal form.} {\boxedgraphic{MulSum}}{The architecture described by the normal form.} \stopcombination + \todo{Intermezzo: functions vs plain values} + + A very simple example of a program in normal form is given in + \in{example}[ex:MulSum]. As you can see, all arguments to the function (which + will become input ports in the generated \VHDL) are at the outer level. + This means that the body of the inner lambda abstraction is never a + function, but always a plain value. + + As the body of the inner lambda abstraction, we see a single (recursive) + let expression, that binds two variables (\lam{mul} and \lam{sum}). These + variables will be signals in the generated \VHDL, bound to the output port + of the \lam{*} and \lam{+} components. + + The final line (the \quote{return value} of the function) selects the + \lam{sum} signal to be the output port of the function. This \quote{return + value} can always only be a variable reference, never a more complex + expression. + + \todo{Add generated VHDL} + \in{Example}[ex:MulSum] showed a function that just applied two other functions (multiplication and addition), resulting in a simple architecture with two components and some connections. There is of @@ -196,7 +196,7 @@ ncline(mux)(res) "posA(out)"; \stopuseMPgraphic - \placeexample[here][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.} + \placeexample[][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.} \startcombination[2*1] {\typebufferlam{AddSubAlu}}{Core description in normal form.} {\boxedgraphic{AddSubAlu}}{The architecture described by the normal form.} @@ -307,7 +307,7 @@ \stopuseMPgraphic \todo{Don't split registers in this image?} - \placeexample[here][ex:NormalComplete]{Simple architecture consisting of an adder and a + \placeexample[][ex:NormalComplete]{Simple architecture consisting of an adder and a subtractor.} \startcombination[2*1] {\typebufferlam{NormalComplete}}{Core description in normal form.} @@ -318,12 +318,13 @@ \subsection[sec:normalization:intendednormalform]{Intended normal form definition} Now we have some intuition for the normal form, we can describe how we want - the normal form to look like in a slightly more formal manner. The following - EBNF-like description captures most of the intended structure (and - generates a subset of \GHC's core format). + the normal form to look like in a slightly more formal manner. The + EBNF-like description in \in{definition}[def:IntendedNormal] captures + most of the intended structure (and generates a subset of \GHC's core + format). - There are two things missing: cast expressions are sometimes - allowed by the prototype, but not specified here and the below + There are two things missing from this definition: cast expressions are + sometimes allowed by the prototype, but not specified here and the below definition allows uses of state that cannot be translated to \VHDL\ properly. These two problems are discussed in \in{section}[sec:normalization:castproblems] and @@ -472,8 +473,8 @@ \stopdesc To understand this notation better, the step by step application of - the η-abstraction transformation to a simple \small{ALU} will be - shown. Consider η-abstraction, which is a common transformation from + the η-expansion transformation to a simple \small{ALU} will be + shown. Consider η-expansion, which is a common transformation from labmda calculus, described using above notation as follows: \starttrans @@ -482,12 +483,12 @@ λx.E x \lam{E} is not a lambda abstraction. \stoptrans - η-abstraction is a well known transformation from lambda calculus. What + η-expansion is a well known transformation from lambda calculus. What this transformation does, is take any expression that has a function type and turn it into a lambda expression (giving an explicit name to the argument). There are some extra conditions that ensure that this transformation does not apply infinitely (which are not necessarily part - of the conventional definition of η-abstraction). + of the conventional definition of η-expansion). Consider the following function, in Core notation, which is a fairly obvious way to specify a simple \small{ALU} (Note that it is not yet in normal form, but @@ -631,7 +632,7 @@ \stoplambda The other alternative is left as an exercise to the reader. The final - function, after applying η-abstraction until it does no longer apply is: + function, after applying η-expansion until it does no longer apply is: \startlambda alu :: Bit -> Word -> Word -> Word @@ -819,41 +820,41 @@ \in{section}[sec:normalization:transformation]. \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 intended - normal form. - - \placeintermezzo{}{ - \defref{substitution notation} - \startframedtext[width=8cm,background=box,frame=no] - \startalignment[center] - {\tfa Substitution notation} - \stopalignment - \blank[medium] + \placeintermezzo{}{ + \defref{substitution notation} + \startframedtext[width=8cm,background=box,frame=no] + \startalignment[center] + {\tfa Substitution notation} + \stopalignment + \blank[medium] + + In some of the transformations in this chapter, we need to perform + substitution on an expression. Substitution means replacing every + occurence of some expression (usually a variable reference) with + another expression. + + There have been a lot of different notations used in literature for + specifying substitution. The notation that will be used in this report + is the following: - In some of the transformations in this chapter, we need to perform - substitution on an expression. Substitution means replacing every - occurence of some expression (usually a variable reference) with - another expression. + \startlambda + E[A=>B] + \stoplambda - There have been a lot of different notations used in literature for - specifying substitution. The notation that will be used in this report - is the following: + This means expression \lam{E} with all occurences of \lam{A} replaced + with \lam{B}. + \stopframedtext + } - \startlambda - E[A=>B] - \stoplambda + 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. - This means expression \lam{E} with all occurences of \lam{A} replaced - with \lam{B}. - \stopframedtext - } + 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 intended + normal form. \subsubsection[sec:normalization:beta]{β-reduction} β-reduction is a well known transformation from lambda calculus, where it is @@ -1098,7 +1099,7 @@ of the other value definitions in let bindings and making the final return value a simple variable reference. - \subsubsection[sec:normalization:eta]{η-abstraction} + \subsubsection[sec:normalization:eta]{η-expansion} This transformation makes sure that all arguments of a function-typed expression are named, by introducing lambda expressions. When combined with β-reduction and non-representable binding inlining, all function-typed @@ -1122,7 +1123,7 @@ False -> λy.id y) x \stopbuffer - \transexample{eta}{η-abstraction}{from}{to} + \transexample{eta}{η-expansion}{from}{to} \subsubsection[sec:normalization:appprop]{Application propagation} This transformation is meant to propagate application expressions downwards @@ -1283,7 +1284,7 @@ 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, η-abstraction + 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 @@ -1298,8 +1299,8 @@ \stoptrans \starttrans - x = λv0 ... λvn.E - ~ \lam{E} is representable + 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 @@ -1501,6 +1502,46 @@ \stopframedtext } + \subsubsection{Scrutinee binder removal} + This transformation removes (or rather, makes wild) the binder to + which the scrutinee is bound after evaluation. This is done by + replacing the bndr with the scrutinee in all alternatives. To prevent + duplication of work, this transformation is only applied when the + scrutinee is already a simple variable reference (but the previous + transformation ensures this will eventually be the case). The + scrutinee binder itself is replaced by a wild binder (which is no + longer displayed). + + Note that one could argue that this transformation can change the + meaning of the Core expression. In the regular Core semantics, a case + expression forces the evaluation of its scrutinee and can be used to + implement strict evaluation. However, in the generated \VHDL, + evaluation is always strict. So the semantics we assign to the Core + expression (which differ only at this particular point), this + transformation is completely valid. + + \starttrans + case x of bndr + alts + ----------------- \lam{x} is a local variable reference + case x of + alts[bndr=>x] + \stoptrans + + \startbuffer[from] + case x of y + True -> y + False -> not y + \stopbuffer + + \startbuffer[to] + case x of + True -> x + False -> not x + \stopbuffer + + \transexample{scrutbndrremove}{Scrutinee binder removal}{from}{to} + \subsubsection{Case normalization} This transformation ensures that all case expressions get a form that is allowed by the intended normal form. This means they @@ -1735,11 +1776,11 @@ lambda abstraction. To reduce all higher-order values to one of the above items, a number - of transformations we have already seen are used. The η-abstraction + of transformations we have already seen are used. The η-expansion transformation from \in{section}[sec:normalization:eta] ensures all function arguments are introduced by lambda abstraction on the highest level of a function. These lambda arguments are allowed because of - \in{item}[item:toplambda] above. After η-abstraction, our example + \in{item}[item:toplambda] above. After η-expansion, our example becomes a bit bigger: \startlambda @@ -1750,7 +1791,7 @@ ) q \stoplambda - η-abstraction also introduces extra applications (the application of + η-expansion also introduces extra applications (the application of the let expression to \lam{q} in the above example). These applications can then propagated down by the application propagation transformation (\in{section}[sec:normalization:appprop]). In our @@ -1769,8 +1810,8 @@ representable type). Completely applied top level functions (like the first alternative) are now no longer invalid (they fall under \in{item}[item:completeapp] above). (Completely) applied lambda - abstractions can be removed by β-abstraction. For our example, - applying β-abstraction results in the following: + abstractions can be removed by β-expansion. For our example, + applying β-expansion results in the following: \startlambda λy.λq.let double = λx. x + x in