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
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.
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
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.}
\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.}
\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
\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
\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
projects / matthijs / master-project / report.git / blobdiff