X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=2768ba2c0a2c89e87e989471bd5d7a3c53ea5e4c;hp=fba2c4a47d22b6fb09527fbd4f94ff40e87fd162;hb=05ab912a6a0d53892521265750b313126ab442af;hpb=9e91ba5d56c3626ace094e8074c6b6a1106f5d3f diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index fba2c4a..2768ba2 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.} @@ -1299,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 @@ -1502,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