stateful functions at a time, the final state consists of nested two-tuples.
The final \hs{()} in the state originates from the fact that the \hs{return}
function has no real state, but is part of the composition. We could have left
-out the return statement (and the \hs{outb <-} part) to make \hs{foo}'s return
+out the return expression (and the \hs{outb <-} part) to make \hs{foo}'s return
value equal to \hs{funcb}'s, but this approach makes it clearer what is
happening.
is calculated as well, but only saved when the right clock has an up
transition.
-As you can see, there is some code duplication in the case statement that
+As you can see, there is some code duplication in the case expression that
selects the right clock. One of the advantages of an explicit approach like
this, is that some of this duplication can be extracted away into helper
functions. For example, we could imagine a \hs{select_clock} function, which
The main cost of this approach will probably be extra complexity in the
compiler: The paths (state) data can take become very non-trivial, and it
-is probably hard to properly analyze these paths and produce the intended VHDL
-description.
+is probably hard to properly analyze these paths and produce the
+intended \VHDL description.
\section{Multiple cycle descriptions}
In the current Cλash prototype, every description is a single-cycle
This is of course a very intrusive solution. Every type must become member
of this typeclass, and there is now some member in every type that is a
special don't care value. Guaranteeing the obvious don't care semantics
- also becomes harder, since every pattern match or case statement must now
+ also becomes harder, since every pattern match or case expressions must now
also take care of the don't care value (this might actually be an
advantage, since it forces designers to specify how to handle don't care
for different operations).
These options should be explored further to see if they provide feasible
methods for describing don't care conditions. Possibly there are completely
other methods which work better.
+
+\section{Correctness proofs of the normalization system}
+As stated in \in{section}[sec:normalization:properties], there are a
+number of properties we would like to see verified about the
+normalization system. In particular, the \emph{termination} and
+\emph{completeness} of the system would be a good candidate for future
+research. Specifying formal semantics for the Core language in
+order to verify the \emph{soundness} of the system would be an even more
+challenging task.
+% vim: set sw=2 sts=2 expandtab:
projects / matthijs / master-project / report.git / blobdiff