\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}
-> State (Word, Word)
-> (State (Word, Word), Word)
- -- All arguments are an inital lambda (address, data, packed state)
+ -- All arguments are an initial lambda
+ -- (address, data, packed state)
regbank = λa.λd.λsp.
-- There are nested let expressions at top level
let
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
EBNF-like description in \in{definition}[def:IntendedNormal] captures
- most of the intended structure (and generates a subset of \GHC's core
+ most of the intended structure (and generates a subset of \GHC's Core
format).
There are two things missing from this definition: cast expressions are
| \italic{builtinapp}
\stopbuffer
- \placedefinition[][def:IntendedNormal]{Definition of the intended nnormal form using an \small{EBNF}-like syntax.}
+ \placedefinition[][def:IntendedNormal]{Definition of the intended normal form using an \small{EBNF}-like syntax.}
{\defref{intended normal form definition}
\typebufferlam{IntendedNormal}}
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.
+ For these, a hard-coded \small{VHDL} translation is available.
\section[sec:normalization:transformation]{Transformation notation}
To be able to concisely present transformations, we use a specific format
Nevertheless, we will more precisely specify their meaning below:
\startdesc{<original expression>} The expression pattern that will be matched
- against (subexpressions of) the expression to be transformed. We call this a
+ against (sub-expressions of) the expression to be transformed. We call this a
pattern, because it can contain \emph{placeholders} (variables), which match
any expression or binder. Any such placeholder is said to be \emph{bound} to
the expression it matches. It is convention to use an uppercase letter (\eg\
To understand this notation better, the step by step application of
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:
+ lambda calculus, described using above notation as follows:
\starttrans
E \lam{E :: a -> b}
High -> (-)
\stoplambda
- There are a few subexpressions in this function to which we could possibly
+ There are a few sub-expressions in this function to which we could possibly
apply the transformation. Since the pattern of the transformation is only
the placeholder \lam{E}, any expression will match that. Whether the
transformation applies to an expression is thus solely decided by the
We look at the \lam{<original expression>} pattern, which is \lam{E}.
This means we bind \lam{E} to \lam{(+)}. We then replace the expression
- with the \lam{<transformed expression>}, replacing all occurences of
+ with the \lam{<transformed expression>}, replacing all occurrences of
\lam{E} with \lam{(+)}. In the \lam{<transformed expression>}, the This gives us the replacement expression:
\lam{λx.(+) x} (A lambda expression binding \lam{x}, with a body that
applies the addition operator to \lam{x}).
A \emph{hardware representable} (or just \emph{representable}) type or value
is (a value of) a type that we can generate a signal for in hardware. For
example, a bit, a vector of bits, a 32 bit unsigned word, etc. Values that are
- not runtime representable notably include (but are not limited to): types,
+ not run-time representable notably include (but are not limited to): types,
dictionaries, functions.
\defref{representable}
\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
\stoplambda
Now, we have replaced the \lam{a} binder with a reference to the \lam{x}
- binder. No harm done here. But note that we see multiple occurences of the
- \lam{c} binder. The first is a binding occurence, to which the second refers.
+ binder. No harm done here. But note that we see multiple occurrences of the
+ \lam{c} binder. The first is a binding occurrence, to which the second refers.
The last, however refers to \emph{another} instance of \lam{c}, which is
bound somewhere outside of this expression. Now, if we would apply beta
reduction without taking heed of binder uniqueness, we would get:
can be accessed.
There are a number of ways to solve this. \small{GHC} has isolated this
- problem to their binder substitution code, which performs \emph{deshadowing}
+ problem to their binder substitution code, which performs \emph{de-shadowing}
during its expression traversal. This means that any binding that shadows
another binding on a higher level is replaced by a new binder that does not
shadow any other binding. This non-shadowing invariant is enough to prevent
In our transformation system, maintaining this non-shadowing invariant is
a bit harder to do (mostly due to implementation issues, the prototype
- does not use \small{GHC}'s subsitution code). Also, the following points
+ does not use \small{GHC}'s substitution code). Also, the following points
can be observed.
\startitemize
- \item Deshadowing does not guarantee overall uniqueness. For example, the
+ \item De-shadowing does not guarantee overall uniqueness. For example, the
following (slightly contrived) expression shows the identifier \lam{x} bound in
- two seperate places (and to different values), even though no shadowing
+ two separate places (and to different values), even though no shadowing
occurs.
\startlambda
unique.
\item When we know that all binders in an expression are unique, moving around
- or removing a subexpression will never cause any binder conflicts. If we have
- some way to generate fresh binders, introducing new subexpressions will not
+ or removing a sub-expression will never cause any binder conflicts. If we have
+ some way to generate fresh binders, introducing new sub-expressions will not
cause any problems either. The only way to cause conflicts is thus to
- duplicate an existing subexpression.
+ duplicate an existing sub-expression.
\stopitemize
Given the above, our prototype maintains a unique binder invariant. This
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 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
+ occurrence of some expression (usually a variable reference) with
another expression.
There have been a lot of different notations used in literature for
E[A=>B]
\stoplambda
- This means expression \lam{E} with all occurences of \lam{A} replaced
+ This means expression \lam{E} with all occurrences of \lam{A} replaced
with \lam{B}.
\stopframedtext
}
In our transformation system, this step helps to remove unwanted lambda
abstractions (basically all but the ones at the top level). Other
transformations (application propagation, non-representable inlining) make
- sure that most lambda abstractions will eventually be reducable by
+ sure that most lambda abstractions will eventually be reducible by
β-reduction.
Note that β-reduction also works on type lambda abstractions and type
applications as well. This means the substitution below also works on
- type variables, in the case that the binder is a type variable and teh
+ type variables, in the case that the binder is a type variable and the
expression applied to is a type.
\starttrans
This transform takes simple top level bindings generated by the
\small{GHC} compiler. \small{GHC} sometimes generates very simple
\quote{wrapper} bindings, which are bound to just a variable
- reference, or contain just a (partial) function appliation with
+ reference, or contain just a (partial) function application with
the type and dictionary arguments filled in (such as the
\lam{(+)} in the example below).
\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
allowed in \VHDL\ architecture names\footnote{Technically, it is
allowed to use non-alphanumerics when using extended
identifiers, but it seems that none of the tooling likes
- extended identifiers in filenames, so it effectively does not
+ extended identifiers in file names, so it effectively does not
work.}, so the entity would be called \quote{w7aA7f} or
- something similarly meaningless and autogenerated).
+ something similarly meaningless and auto-generated).
\subsection{Program structure}
These transformations are aimed at normalizing the overall structure
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, η-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.
+ 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 \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
+ x = λv1 ... λvn.E \lam{n} can be zero
+ ~ \lam{E} is representable
+ 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
\refdef{global variable}
Note that references to \emph{global variables} (like a top level
- function without arguments, but also an argumentless dataconstructors
+ function without arguments, but also an argumentless data-constructors
like \lam{True}) are also simplified. Only local variables generate
signals in the resulting architecture. Even though argumentless
- dataconstructors generate constants in generated \VHDL\ code and could be
+ data-constructors generate constants in generated \VHDL\ code and could be
mapped to an input port directly, they are still simplified to make the
normal form more regular.
reference.
\item (A partial application of) a top level function (either built-in on
user-defined). The function extraction transformation described in
- this section takes care of turning every functiontyped argument into
+ this section takes care of turning every function-typed argument into
(a partial application of) a top level function.
\item Any expression that is not representable and does not have a
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.
+ category. In any case, the result is in normal form.
\stopitemize
As noted, the argument simplification will handle any representable
translation rules needed for built-in functions, since they only need
to handle (partial applications of) top level functions.
- Any free variables occuring in the extracted arguments will become
+ Any free variables occurring in the extracted arguments will become
parameters to the new global function. The original argument is replaced
with a reference to the new function, applied to any free variables from
the original argument.
even more complicated expressions).
\starttrans
- M N \lam{M} is (a partial aplication of) a built-in function.
+ M N \lam{M} is (a partial application of) a built-in function.
--------------------- \lam{f0 ... fn} are all free local variables of \lam{N}
M (x f0 ... fn) \lam{N :: a -> b}
~ \lam{N} is not a (partial application of) a top level function
Note that the function \lam{f} will still need normalization after
this.
- \subsection{Case normalisation}
+ \subsection{Case normalization}
The transformations in this section ensure that case statements end up
in normal form.
False -> b
\stopbuffer
- \transexample{letflat}{Case normalisation}{from}{to}
+ \transexample{letflat}{Case normalization}{from}{to}
\placeintermezzo{}{
The Haskell syntax offers the underscore as a wild binder that
cannot even be referenced (It can be seen as introducing a new,
- anonymous, binder everytime it is used).
+ anonymous, binder every time it is used).
In these transformations, the term wild binder will sometimes be
used to indicate that a binder must not be referenced.
\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
let bindings for each of the alternatives' value and a single
selector case to select the right value out of these.
- Technically, the defintion of this transformation would require
+ Technically, the definition of this transformation would require
that the constructor for every alternative has exactly the same
amount (\lam{m}) of arguments, but of course this transformation
also applies when this is not the case.
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
\startlambda
f 1 2
\stoplambda
- the subexpression \lam{f 1} has a function type. But this is
+ the sub-expression \lam{f 1} has a function type. But this is
allowed, since it is inside a complete application.
\stopitemize
first argument and applies that function twice to the second argument.
Again, we have made the function monomorphic for clarity, even though
this function would be a lot more useful if it was polymorphic. The
- function \lam{main} uses \lam{twice} to apply a lambda epression twice.
+ function \lam{main} uses \lam{twice} to apply a lambda expression twice.
When faced with a user defined function, a body is available for that
function. This means we could create a specialized version of the
twice). This is discussed in more detail in
\in{section}[sec:normalization:duplicatework].
- \subsubsection{Literals}
+ \subsubsection[sec:normalization:literals]{Literals}
There are a limited number of literals available in Haskell and Core.
\refdef{enumerated types} When using (enumerating) algebraic
- datatypes, a literal is just a reference to the corresponding data
+ data-types, a literal is just a reference to the corresponding data
constructor, which has a representable type (the algebraic datatype)
and can be translated directly. This also holds for literals of the
\hs{Bool} Haskell type, which is just an enumerated type.
literals for all three integer types supported (\hs{SizedWord},
\hs{SizedInt} and \hs{RangedWord}). This is implemented using
Haskell's \hs{Num} type class, which offers a \hs{fromInteger} method
- that converts any \hs{Integer} to the Cλash datatypes.
+ that converts any \hs{Integer} to the Cλash data-types.
When \GHC\ sees integer literals, it will automatically insert calls to
the \hs{fromInteger} method in the resulting Core expression. For
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
(λb -> add b 1) (add 1 x)
\stopbuffer
- \transexample{nonrepinline}{Nonrepresentable binding inlining}{from}{to}
+ \transexample{nonrepinline}{Non-representable binding inlining}{from}{to}
\subsubsection[sec:normalization:specialize]{Function specialization}
This transform removes arguments to user-defined functions that are
- not representable at runtime. This is done by creating a
+ not representable at run-time. This is done by creating a
\emph{specialized} version of the function that only works for one
particular value of that argument (in other words, the argument can be
removed).
exactly one free variable, itself, we would only replace that argument
with itself).
- This shows that any free local variables that are not runtime
+ This shows that any free local variables that are not run-time
representable cannot be brought into normal form by this transform. We
rely on an inlining or β-reduction transformation to replace such a
variable with an expression we can propagate again.
The argument that we are specializing for, \lam{Y_i}, is put inside
the new function body. The old function body is applied to it. Since
we use this new function only in place of an application with that
- particular argument \lam{Y_i}, behaviour should not change.
+ particular argument \lam{Y_i}, behavior should not change.
Note that the types of the arguments of our new function are taken
from the types of the \emph{actual} arguments (\lam{T0 ... Tn}). This
A possible solution to this would be to use the following alternative
transformation, which is of course no longer normal β-reduction. The
- followin transformation has not been tested in the prototype, but is
+ following transformation has not been tested in the prototype, but is
given here for future reference:
\starttrans
For this particular problem, the solutions for duplication of work
seem from the previous section seem to fix the determinism of our
transformation system as well. However, it is likely that there are
- other occurences of this problem.
+ other occurrences of this problem.
\subsection[sec:normalization:castproblems]{Casts}
We do not fully understand the use of cast expressions in Core, so
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.
possible to write descriptions which are in intended normal
form, but cannot be translated into \VHDL\ in a meaningful way
(\eg, a function that swaps two substates in its result, or a
- function that changes a substate itself instead of passing it to
- a subfunction).
+ function that changes a sub-state itself instead of passing it to
+ a sub-function).
It is now up to the programmer to not do anything funny with
these state values, whereas the normalization just tries not to
mess up the flow of state values. In practice, there are
situations where a Core program that \emph{could} be a valid
- stateful description is not translateable by the prototype. This
+ stateful description is not translatable by the prototype. This
most often happens when statefulness is mixed with pattern
matching, causing a state input to be unpacked multiple times or
be unpacked and repacked only in some of the code paths.
When looking at the system of transformations outlined above, there are a
number of questions that we can ask ourselves. The main question is of course:
\quote{Does our system work as intended?}. We can split this question into a
- number of subquestions:
+ number of sub-questions:
\startitemize[KR]
\item[q:termination] Does our system \emph{terminate}? Since our system will
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} is called the \emph{intended normal set}.
+ \refdef{intended normal form definition} is called the \emph{intended normal set}.
From such a graph, we can derive some properties easily:
\startitemize[KR]
will of course leave the meaning unchanged and is thus
\emph{sound}.
- The current prototype has only been verified in an ad-hoc fashion
+ The current prototype has only been verified in an ad hoc fashion
by inspecting (the code for) each transformation. A more formal
verification would be more appropriate.
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
+ sub-expression as well, there is a constraint on our meaning
definition: the meaning of an expression should depend only on the
- meaning of subexpressions, not on the expressions themselves. For
+ meaning of sub-expressions, not on the expressions themselves. For
example, the meaning of the application in \lam{f (let x = 4 in
x)} should be the same as the meaning of the application in \lam{f
- 4}, since the argument subexpression has the same meaning (though
+ 4}, since the argument sub-expression has the same meaning (though
the actual expression is different).
\subsection{Completeness}
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
we need to check every (set of) transformation(s) separately.
\todo{Perhaps do a few steps of the proofs as proof-of-concept}
+ \subsection{Determinism}
+ A well-known technique for proving determinism in lambda calculus
+ and other reduction systems, is using the Church-Rosser property
+ \cite[church36]. A reduction system has the CR property if and only if:
+
+ \placedefinition[here]{Church-Rosser theorem}
+ {\lam{\forall A, B, C \exists D (A ->> B ∧ A ->> C => B ->> D ∧ C ->> D)}}
+
+ Here, \lam{A ->> B} means \lam{A} \emph{reduces to} \lam{B}. In
+ other words, there is a set of transformations that can transform
+ \lam{A} to \lam{B}. \lam{=>} is used to mean \emph{implies}.
+
+ For a transformation system holding the Church-Rosser property, it
+ is easy to show that it is in fact deterministic. Showing that this
+ property actually holds is a harder problem, but has been
+ done for some reduction systems in the lambda calculus
+ \cite[klop80]\ \cite[barendregt84]. Doing the same for our
+ transformation system is probably more complicated, but not
+ impossible.
% vim: set sw=2 sts=2 expandtab:
projects / matthijs / master-project / report.git / blobdiff