\stopcombination
}
- The first step in the core to \small{VHDL} translation process, is normalization. We
- aim to bring the core description into a simpler form, which we can
+ The first step in the Core to \small{VHDL} translation process, is normalization. We
+ aim to bring the Core description into a simpler form, which we can
subsequently translate into \small{VHDL} easily. This normal form is needed because
- the full core language is more expressive than \small{VHDL} in some
+ the full Core language is more expressive than \small{VHDL} in some
areas (higher-order expressions, limited polymorphism using type
- classes, etc.) and because core can describe expressions that do not
+ classes, etc.) and because Core can describe expressions that do not
have a direct hardware interpretation.
\section{Normal form}
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.}
-> State (Word, Word)
-> (State (Word, Word), Word)
- -- All arguments are an inital lambda (address, data, packed state)
+ -- All arguments are an inital lambda
+ -- (address, data, packed state)
regbank = λa.λd.λsp.
-- There are nested let expressions at top level
let
\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
{\defref{intended normal form definition}
\typebufferlam{IntendedNormal}}
- When looking at such a program from a hardware perspective, the
- top level lambda abstractions define the input ports. Lambda
- abstractions cannot appear anywhere else. The variable reference
- in the body of the recursive let expression is the output port.
- Most function applications bound by the let expression define a
- component instantiation, where the input and output ports are
- mapped to local signals or arguments. Some of the others use a
- built-in construction (\eg\ the \lam{case} expression) or call a
- built-in function (\eg\ \lam{+} or \lam{map}). For these, a
- hardcoded \small{VHDL} translation is available.
+ When looking at such a program from a hardware perspective, the top
+ level lambda abstractions (\italic{lambda}) define the input ports.
+ Lambda abstractions cannot appear anywhere else. The variable reference
+ in the body of the recursive let expression (\italic{toplet}) is the
+ output port. Most binders bound by the let expression define a
+ component instantiation (\italic{userapp}), where the input and output
+ ports are mapped to local signals (\italic{userarg}). Some of the others
+ use a built-in construction (\eg\ the \lam{case} expression) or call a
+ built-in function (\italic{builtinapp}) such as \lam{+} or \lam{map}.
+ For these, a hardcoded \small{VHDL} translation is available.
\section[sec:normalization:transformation]{Transformation notation}
To be able to concisely present transformations, we use a specific format
\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
λ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
\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
dictionaries, functions.
\defref{representable}
- A \emph{built-in function} is a function supplied by the Cλash framework, whose
- implementation is not valid Cλash. The implementation is of course valid
- Haskell, for simulation, but it is not expressable in Cλash.
- \defref{built-in function} \defref{user-defined function}
+ A \emph{built-in function} is a function supplied by the Cλash
+ framework, whose implementation is not used to generate \VHDL. This is
+ either because it is no valid Cλash (like most list functions that need
+ recursion) or because a Cλash implementation would be unwanted (for the
+ addition operator, for example, we would rather use the \VHDL addition
+ operator to let the synthesis tool decide what kind of adder to use
+ instead of explicitly describing one in Cλash). \defref{built-in
+ function}
+
+ These are functions like \lam{map}, \lam{hwor}, \lam{+} and \lam{length}.
- For these functions, Cλash has a \emph{built-in hardware translation}, so calls
- to these functions can still be translated. These are functions like
- \lam{map}, \lam{hwor} and \lam{length}.
+ For these functions, Cλash has a \emph{built-in hardware translation},
+ so calls to these functions can still be translated. Built-in functions
+ must have a valid Haskell implementation, of course, to allow
+ simulation.
- A \emph{user-defined} function is a function for which we do have a Cλash
- implementation available.
+ A \emph{user-defined} function is a function for which no built-in
+ translation is available and whose definition will thus need to be
+ translated to Cλash. \defref{user-defined function}
\subsubsection[sec:normalization:predicates]{Predicates}
Here, we define a number of predicates that can be used below to concisely
\subsection[sec:normalization:uniq]{Binder uniqueness}
A common problem in transformation systems, is binder uniqueness. When not
considering this problem, it is easy to create transformations that mix up
- bindings and cause name collisions. Take for example, the following core
+ bindings and cause name collisions. Take for example, the following Core
expression:
\startlambda
unique. This is done by generating a fresh binder for every binder used. This
also replaces binders that did not cause any conflict, but it does ensure that
all binders within the function are generated by the same unique supply.
- \refdef{fresh binder}
\item Whenever a new binder must be generated, we generate a fresh binder that
is guaranteed to be different from \emph{all binders generated so far}. This
can thus never introduce duplication and will maintain the invariant.
\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]
+
+ 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:
- \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.
+ \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
\in{Example}[ex:trans:toplevelinline] shows a typical application of
the addition operator generated by \GHC. The type and dictionary
arguments used here are described in
- \in{Section}[section:prototype:polymorphism].
+ \in{Section}[sec:prototype:coretypes].
Without this transformation, there would be a \lam{(+)} entity
in the \VHDL\ which would just add its inputs. This generates a
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
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
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, η-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 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
+ x = λv1 ... λvn.E \lam{n} can be zero
~ \lam{E} is representable
- E \lam{E} is not a let expression
- --------------------------- \lam{E} is not a local variable reference
- letrec x = E in x
+ 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]
\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
function type. Since these can be any expression, there is no
transformation needed. Note that this category is exactly all
expressions that are not transformed by the transformations for the
- previous two categories. This means that \emph{any} core expression
+ previous two categories. This means that \emph{any} Core expression
that is used as an argument to a built-in function will be either
transformed into one of the above categories, or end up in this
categorie. In any case, the result is in normal form.
\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
\startitemize
\item An extractor case with a single alternative that picks a field
- from a datatype, \eg\ \lam{case x of (a, b) -> a}.
+ from a datatype, \eg\ \lam{case x of (a, b) ->
+ a}.\defref{extractor case}
\item A selector case with multiple alternatives and only wild binders, that
makes a choice between expressions based on the constructor of another
- expression, \eg\ \lam{case x of Low -> a; High -> b}.
+ expression, \eg\ \lam{case x of Low -> a; High ->
+ b}.\defref{selector case}
\stopitemize
For an arbitrary case, that has \lam{n} alternatives, with
actual transformations.
\subsubsection{Removing Polymorphism}
- As noted in \in{section}[sec:prototype:polymporphism],
+ As noted in \in{section}[sec:prototype:coretypes],
polymorphism is made explicit in Core through type and
dictionary arguments. To remove the polymorphism from a
function, we can simply specialize the polymorphic function for
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
) 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
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
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
there are probably expressions involving cast expressions that cannot
be brought into intended normal form by this transformation system.
- The uses of casts in the core system should be investigated more and
+ The uses of casts in the Core system should be investigated more and
transformations will probably need updating to handle them in all
cases.
\todo{Define β-reduction and η-reduction?}
- Note that the normal form of such a system consists of the set of nodes
- (expressions) without outgoing edges, since those are the expressions to which
- no transformation applies anymore. We call this set of nodes the \emph{normal
- set}. The set of nodes containing expressions in intended normal
- form \refdef{intended normal form} is called the \emph{intended
- normal set}.
+ In such a graph a node (expression) is in normal form if it has no
+ outgoing edges (meaning no transformation applies to it). The set of
+ nodes without outgoing edges is called the \emph{normal set}. Similarly,
+ the set of nodes containing expressions in intended normal form
+ \refdef{intended normal form definition} is called the \emph{intended normal set}.
From such a graph, we can derive some properties easily:
\startitemize[KR]
our compilation to \VHDL. The main difference seems to be that in
hardware every expression is always evaluated, while in software
it is only evaluated if needed, but it should be possible to
- assign a meaning to core expressions that assumes neither.
+ assign a meaning to Core expressions that assumes neither.
Since each of the transformations can be applied to any
subexpression as well, there is a constraint on our meaning
By systematically reviewing the entire Core language definition
along with the intended normal form definition (both of which have
a similar structure), it should be possible to identify all
- possible (sets of) core expressions that are not in intended
+ possible (sets of) Core expressions that are not in intended
normal form and identify a transformation that applies to it.
This approach is especially useful for proving completeness of our
projects / matthijs / master-project / report.git / blobdiff