- 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
- -- All arguments are an inital lambda (address, data, packed state)
+ -- All arguments are an inital lambda
+ -- (address, data, packed state)
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
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
\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
\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
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.
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.
\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.
\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{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{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
Without this transformation, there would be a \lam{(+)} entity
in the \VHDL\ which would just add its inputs. This generates a
Without this transformation, there would be a \lam{(+)} entity
in the \VHDL\ which would just add its inputs. This generates 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
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
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.
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.
- 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
\item A selector case with multiple alternatives and only wild binders, that
makes a choice between expressions based on the constructor of another
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
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
there are probably expressions involving cast expressions that cannot
be brought into intended normal form by this transformation system.
there are probably expressions involving cast expressions that cannot
be brought into intended normal form by this transformation system.
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
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
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
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
Since each of the transformations can be applied to any
subexpression as well, there is a constraint on our meaning
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
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
normal form and identify a transformation that applies to it.
This approach is especially useful for proving completeness of our
normal form and identify a transformation that applies to it.
This approach is especially useful for proving completeness of our