core can describe expressions that do not have a direct hardware
interpretation.
- \todo{Describe core properties not supported in \VHDL, and describe how the
- \VHDL we want to generate should look like.}
-
\section{Normal form}
- \todo{Refresh or refer to distinct hardware per application principle}
The transformations described here have a well-defined goal: To bring the
program in a well-defined form that is directly translatable to hardware,
while fully preserving the semantics of the program. We refer to this form as
In particular, we define no particular order of transformations. Since
transformation order should not influence the resulting normal form,
- \todo{This is not really true, but would like it to be...} this leaves
- the implementation free to choose any application order that results in
- an efficient implementation.
+ this leaves the implementation free to choose any application order that
+ results in an efficient implementation. Unfortunately this is not
+ entirely true for the current set of transformations. See
+ \in{section}[sec:normalization:non-determinism] for a discussion of this
+ problem.
When applying a single transformation, we try to apply it to every (sub)expression
in a function, not just the top level function body. This allows us to
normal form.
\placeintermezzo{}{
+ \defref{substitution notation}
\startframedtext[width=8cm,background=box,frame=no]
\startalignment[center]
{\tfa Substitution notation}
This transformation is not needed to get an expression into intended
normal form (since these bindings are part of the intended normal
form), but makes the resulting \small{VHDL} a lot shorter.
-
+
+ \refdef{substitution notation}
\starttrans
letrec
a0 = E0
This propagation makes higher order values become applied (in
particular both of the alternatives of the case now have a
- representable type. Completely applied top level functions (like the
+ 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,
solves (part of) the polymorphism, higher order values and
unrepresentable literals in an expression.
+ \refdef{substitution notation}
\starttrans
letrec
a0 = E0
\todo{Examples. Perhaps reference the previous sections}
-
\section{Unsolved problems}
The above system of transformations has been implemented in the prototype
and seems to work well to compile simple and more complex examples of
let y = (a * b) in y + y
\stoplambda
- \subsection{Non-determinism}
+ \subsection[sec:normalization:non-determinism]{Non-determinism}
As an example, again consider the following expression:
\startlambda
transformations will probably need updating to handle them in all
cases.
+ \subsection[sec:normalization:stateproblems]{Normalization of stateful descriptions}
+ Currently, the intended normal form definition\refdef{intended
+ normal form definition} offers enough freedom to describe all
+ valid stateful descriptions, but is not limiting enough. It is
+ 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).
+
+ 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
+ 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.
+
+ Without going into detail about the exact problems (of which
+ there are probably more than have shown up so far), it seems
+ unlikely that these problems can be solved entirely by just
+ improving the \VHDL state generation in the final stage. The
+ normalization stage seems the best place to apply the rewriting
+ needed to support more complex stateful descriptions. This does
+ of course mean that the intended normal form definition must be
+ extended as well to be more specific about how state handling
+ should look like in normal form.
+ \in{Section}[sec:prototype:statelimits] already contains a
+ tight description of the limitations on the use of state
+ variables, which could be adapted into the intended normal form.
+
\section[sec:normalization:properties]{Provable properties}
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:
possible proof strategies are shown below.
\subsection{Graph representation}
- Before looking into how to prove these properties, we'll look at our
- transformation system from a graph perspective. The nodes of the graph are
- all possible Core expressions. The (directed) edges of the graph are
- transformations. When a transformation α applies to an expression \lam{A} to
- produce an expression \lam{B}, we add an edge from the node for \lam{A} to the
- node for \lam{B}, labeled α.
+ Before looking into how to prove these properties, we'll look at
+ transformation systems from a graph perspective. We will first define
+ the graph view and then illustrate it using a simple example from lambda
+ calculus (which is a different system than the Cλash normalization
+ system). The nodes of the graph are all possible Core expressions. The
+ (directed) edges of the graph are transformations. When a transformation
+ α applies to an expression \lam{A} to produce an expression \lam{B}, we
+ add an edge from the node for \lam{A} to the node for \lam{B}, labeled
+ α.
\startuseMPgraphic{TransformGraph}
save a, b, c, d;
system with β and η reduction (solid lines) and expansion (dotted lines).}
\boxedgraphic{TransformGraph}
- Of course our graph is unbounded, since we can construct an infinite amount of
- Core expressions. Also, there might potentially be multiple edges between two
- given nodes (with different labels), though seems unlikely to actually happen
- in our system.
+ Of course the graph for Cλash is unbounded, since we can construct an
+ infinite amount of Core expressions. Also, there might potentially be
+ multiple edges between two given nodes (with different labels), though
+ seems unlikely to actually happen in our system.
See \in{example}[ex:TransformGraph] for the graph representation of a very
simple lambda calculus that contains just the expressions \lam{(λx.λy. (+) x
Also, since there is only one node in the normal set, it must obviously be
\emph{deterministic} as well.
- \todo{Add content to these sections}
\subsection{Termination}
In general, proving termination of an arbitrary program is a very
hard problem. \todo{Ref about arbitrary termination} Fortunately,
projects / matthijs / master-project / report.git / blobdiff