ForSyDe-3.0: doc/www/files/tutorial/tutorial.html
<html><head><meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1"><title>ForSyDe tutorial</title><link rel="stylesheet" href="fptools.css" type="text/css"><meta name="generator" content="DocBook XSL Stylesheets V1.73.2"></head><body bgcolor="white" text="black" link="#0000FF" vlink="#840084" alink="#0000FF"><div class="article" lang="en"><div class="titlepage"><div><div><h2 class="title"><a name="ForSyDe-tutorial"></a>ForSyDe tutorial</h2></div><div><div class="author"><h3 class="author"><span class="firstname">Alfonso</span> <span class="surname">Acosta</span></h3><div class="affiliation"><span class="org">
<span class="orgname">Royal Institute of Technology (KTH)</span>
<span class="orgdiv">System, Architecture and Methodology (SAM) group</span>
<div class="address"><p><span class="city">Stockholm</span>, <span class="country">Sweden</span></p></div>
</span></div><code class="email"><<a class="email" href="mailto:alfonsoa@kth.se">alfonsoa@kth.se</a>></code></div></div><div><p class="pubdate">2008-09-20</p></div><div><div class="revhistory"><table border="1" width="100%" summary="Revision history"><tr><th align="left" valign="top" colspan="2"><b>Revision History</b></th></tr><tr><td align="left">Revision 0.2</td><td align="left">2008-09-20</td></tr><tr><td align="left" colspan="2">Complete draft.</td></tr><tr><td align="left">Revision 0.1</td><td align="left">2008-08-15</td></tr><tr><td align="left" colspan="2">First version.</td></tr></table></div></div></div><hr></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="section"><a href="#intro">1. Disclaimer and Prerequisites</a></span></dt><dt><span class="section"><a href="#install">2. Installing ForSyDe</a></span></dt><dt><span class="section"><a href="#introForSYDe">3. Introduction to ForSyDe</a></span></dt><dd><dl><dt><span class="section"><a href="#id1251676">3.1. Signals</a></span></dt><dt><span class="section"><a href="#id1251727">3.2. Processes</a></span></dt><dt><span class="section"><a href="#id1251867">3.3. Process Constructors</a></span></dt><dt><span class="section"><a href="#id1251871">3.4. Models of Computation and Domain Interfaces</a></span></dt></dl></dd><dt><span class="section"><a href="#DEvsSE">4. Deep-embedded vs Shallow-embedded signals</a></span></dt><dt><span class="section"><a href="#DE">5. Using deep-embedded Signals</a></span></dt><dd><dl><dt><span class="section"><a href="#combinational">5.1. Combinational Systems</a></span></dt><dt><span class="section"><a href="#sequential">5.2. Sequential Systems</a></span></dt><dt><span class="section"><a href="#components">5.3. Using components</a></span></dt><dt><span class="section"><a href="#VHDL">5.4. VHDL Backend</a></span></dt><dt><span class="section"><a href="#GraphML">5.5. GraphML Backend</a></span></dt></dl></dd><dt><span class="section"><a href="#SE">6. Shallow-embedded signals</a></span></dt><dt><span class="appendix"><a href="#FSVec">A. <code class="literal">FSVec</code>s: Vectors parameterized in size</a></span></dt><dd><dl><dt><span class="section"><a href="#id1255404">1. Goal</a></span></dt><dt><span class="section"><a href="#id1255478">2. How?</a></span></dt><dt><span class="section"><a href="#id1255502">3. Type-level decimal numerals</a></span></dt><dt><span class="section"><a href="#id1255520">4. Fixed Sized Vectors themselves</a></span></dt><dt><span class="section"><a href="#id1255822">5. <code class="code">FSVec</code> issues</a></span></dt></dl></dd></dl></div><div class="section" lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a name="intro"></a>1. Disclaimer and Prerequisites</h2></div></div></div><p>
This document has been devised as a practical hands-on
introduction to the use of ForSyDe's implementation. Thus, it is
intentionally informal and non-exhaustive. If you are interested
in ForSyDe's theoretical foundations please refer to the <a class="ulink" href="http://www.ict.kth.se/org/ict/ecs/sam/projects/forsyde/www/index.html#documentation" target="_top">Documentation
section</a> in our <a class="ulink" href="http://www.ict.kth.se/org/ict/ecs/sam/projects/forsyde/www/" target="_top">website</a>.
</p><p>
In order to take full advantage of this tutorial, it is
essential to have a good background in the <a class="ulink" href="http://www.haskell.org" target="_top">Haskell</a> programming
language. Familiarity with some Haskell extensions (<a class="ulink" href="http://www.haskell.org/th" target="_top">Template Haskell</a>,
<a class="ulink" href="http://haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#functional-dependencies" target="_top">Multiparameter
Type Classes with Functional Dependencies</a>, <a class="ulink" href="http://haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#instance-decls" target="_top">Undecidable
and Overlapping Instances</a>) might help but is not vital.
</p></div><div class="section" lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a name="install"></a>2. Installing ForSyDe</h2></div></div></div><p>
ForSyDe is implemented as a Haskell-embedded Domain Specific
Language (DSL). As intimidating as the previous phrase might
sound, from a practical point of view it only means that, to all
effects, ForSyDe is simply a Haskell library.
</p><p>
As it was already stated in <a class="xref" href="#intro" title="1. Disclaimer and Prerequisites">Section 1, “Disclaimer and Prerequisites”</a>, ForSyDe
relies on many Haskell extensions, some of which are exclusive
to GHC. For that reason, a recent version of GHC is required to
build ForSyDe<sup>[<a name="id1251533" href="#ftn.id1251533" class="footnote">1</a>]</sup>.
</p><p>
ForSyDe's library is available on Haskell's <a class="ulink" href="http://hackage.haskell.org" target="_top">HackageDB</a>, a
popular repository of Haskell <a class="ulink" href="http://www.haskell.org/cabal" target="_top">Cabal</a> packages.
If ForSyDe is the first Cabal package you install or your memory
needs to be refreshed in this matter, you should read <a class="ulink" href="http://haskell.org/haskellwiki/Cabal/How_to_install_a_Cabal_package" target="_top">"How
to install a Cabal package"</a>.
</p><p>
At the time being, ForSyDe depends on the <a class="ulink" href="http://hackage.haskell.org/cgi-bin/hackage-scripts/package/type-level" target="_top"><code class="code">type-level</code></a>
and <a class="ulink" href="http://hackage.haskell.org/cgi-bin/hackage-scripts/package/parameterized-data" target="_top"><code class="code">parameterized-data</code></a>
packages to offer numerically-parametrized vectors, and on some
other packages normally distributed with GHC (e.g. <a class="ulink" href="http://hackage.haskell.org/cgi-bin/hackage-scripts/package/mtl" target="_top"><code class="code">mtl</code></a>
..)
</p></div><div class="section" lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a name="introForSYDe"></a>3. Introduction to ForSyDe</h2></div></div></div><p>
This section is a short introduction to some basic concepts
surrounding ForSyDe which are vital to understand how to use its
implementation. If you cannot wait to get your hands dirty and begin
with the implementation examples, go directly to <a class="xref" href="#DEvsSE" title="4. Deep-embedded vs Shallow-embedded signals">Section 4, “Deep-embedded vs Shallow-embedded signals”</a>.
</p><p>
ForSyDe, which stands for Formal System Design, is a
methodology aimed at raising the abstraction level in which
systems (e.g. System on Chip Systems, Hardware or Software) are designed.
</p><p>
ForSyDe systems are modelled as networks of <span class="emphasis"><em>processes</em></span>
interconnected by <span class="emphasis"><em>signals</em></span>. In
addition, the designer is allowed to use processes belonging to
different <span class="emphasis"><em>Models of Computation</em></span>.
</p><p>
In order to understand how systems are modelled, it is important to
get familiar with the concepts outlined above.
</p><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="id1251676"></a>3.1. Signals</h3></div></div></div><p>
Signals can be intuitively defined as
streams of information which flow through the different
processes forming a system.
</p><p>
For example, this is a signal containing the first 10 positive numbers
</p><div class="example"><a name="id1251694"></a><p class="title"><b>Example 1. Signal containing the first 10 positive numbers</b></p><div class="example-contents"><1,2,3,4,5,6,7,8,9,10></div></div><br class="example-break"><p>
More formally, a signal is a sequence of events where each
event has a tag and a value. In ForSyDe, the tag of an event
is implicitly given by the event's position on the list. For
instance, the sample signal above is formed by integer values
which are identical to the signal implicit tags.
</p><p>
It is important to note that signals are homogeneous (i.e. a
signal cannot carry values belonging to different types)
</p><div class="note" style="margin-left: 0.5in; margin-right: 0.5in;"><h3 class="title">Note</h3>The interpretation of tags, as we will see, is determined
by the <span class="emphasis"><em>Model of Computation</em></span> used, e.g. an
identical tag of two events in different signals does not
necessarily imply that these events happen at the same
time. </div></div><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="id1251727"></a>3.2. Processes</h3></div></div></div><p>
Processes are pure functions on signals, i.e. for a given set of input signals a process always gets the same
set of output signals.
</p><div class="figure"><a name="processfun"></a><p class="title"><b>Figure 1. Processes viewed as functions</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="360"><tr><td align="center" valign="middle"><object data="figures/processfun.svg" type="image/svg+xml" width="360" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"><p>
They can also be viewed as a black box which performs computations over its input signals and
forward the results to adjacent processes through output signals.
</p><div class="figure"><a name="processbox"></a><p class="title"><b>Figure 2. Processes viewed as boxes</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="225"><tr><td align="center" valign="middle"><object data="figures/processbox.svg" type="image/svg+xml" width="225" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"><p>
Note that this still allows processes to have internal
state. A process does not necessarily react identically the
same event applied at different times. But it will produce the same, possibly infinite, output signals
when confronted with identical, possibly infinite, input signals.
</p><p>
One of the simplest examples one can think of, is a process which merely adds one to every value in its
only input signal: <span class="emphasis"><em>plus1</em></span>.
</p><div class="example"><a name="id1251834"></a><p class="title"><b>Example 2. The <span class="emphasis"><em>plus1</em></span> process</b></p><div class="example-contents">
plus1(<v<sub>1</sub>, v<sub>2</sub>, v<sub>3</sub>, ...>) =
<v<sub>1</sub>+1, v<sub>2</sub>+1, v<sub>3</sub>+1, ...>)
</div></div><br class="example-break"></div><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="id1251867"></a>3.3. Process Constructors</h3></div></div></div><p>
In ForSyDe, all processes, even <span class="emphasis"><em>plus1</em></span>, must be created from
<span class="emphasis"><em>process constructors</em></span>. A process constructor takes zero or more
functions and/or values which determine the initial state and behaviour of the process to be created.
</p><div class="figure"><a name="processcons"></a><p class="title"><b>Figure 3. A process constructor</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="270"><tr><td align="center" valign="middle"><object data="figures/processcons.svg" type="image/svg+xml" width="270" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"><p>
The ForSyDe methodology offers a set of well-defined
process constructors. For example, certain process constructors are aimed at creating
synchronous systems. Synchronous systems are governed by a global clock and all processes consume and produce
exactly one signal event in each clock-cycle.
</p><p>
For instance, <span class="emphasis"><em>mapSY</em></span>, (where the suffix
<span class="emphasis"><em>SY</em></span> stands for
<span class="emphasis"><em>SY</em></span>ncrhonous) is a
combinational<sup>[<a name="id1251950" href="#ftn.id1251950" class="footnote">2</a>]</sup> process constructor.
<span class="emphasis"><em>mapSY</em></span> takes a function
<span class="emphasis"><em>f</em></span> and creates a process with one input
and output signal, resulting from the application of
<span class="emphasis"><em>f</em></span> to every value in the input.
</p><div class="figure"><a name="mapSY"></a><p class="title"><b>Figure 4. The synchronous, combinational map process constructor: <span class="emphasis"><em>mapSY</em></span></b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="495"><tr><td align="center" valign="middle"><object data="figures/mapSY.svg" type="image/svg+xml" width="495" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"><p>
<span class="emphasis"><em>plus1</em></span> can, in fact, be defined in terms of
<span class="emphasis"><em>mapSY</em></span> as <span class="emphasis"><em>plus1 = mapSY
(+1)</em></span>.
</p><p>
ForSyDe also supports synchronous, sequential
systems. However, it does not allow loops formed exclusively
by combinational processes, also known as
<span class="emphasis"><em>combinational loops</em></span>, <span class="emphasis"><em>zero-delay
loops</em></span> or <span class="emphasis"><em>feedback loops</em></span>, since
their behaviour is not always decidable. Even with that,
combinational loops are still possible if they contain at
least one process formed by the
<span class="emphasis"><em>delaySY<sub>k</sub></em></span>
(<span class="emphasis"><em>k</em></span> > 0) constructor, which is defined as follows.
</p><div class="figure"><a name="delaySY"></a><p class="title"><b>Figure 5. The synchronous, sequential delay process constructor: <span class="emphasis"><em>delaySY</em></span></b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="495"><tr><td align="center" valign="middle"><object data="figures/delaySY.svg" type="image/svg+xml" width="495" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"><p>
<span class="emphasis"><em>delaySY<sub>k</sub></em></span> takes an
initial value <span class="emphasis"><em>s<sub>0</sub></em></span>
and creates a process which appends
<span class="emphasis"><em>s<sub>0</sub></em></span>, replicated
<span class="emphasis"><em>k</em></span> times, to its input
signal. <span class="emphasis"><em>delaySY</em></span> provides the basic
mechanism with which to build sequential systems.
</p><p>
Both <span class="emphasis"><em>mapSY</em></span> and
<span class="emphasis"><em>delaySY<sub>k</sub></em></span> are
considered primitive process constructors, since they cannot
be defined in terms of simpler ones. Primitive constructors
can be combined, forming derived process
constructors. For instance, <span class="emphasis"><em>sourceSY</em></span> is
the result of combining
<span class="emphasis"><em>delaySY<sub>1</sub></em></span> (normally
denoted simply as <span class="emphasis"><em>delaSY</em></span>) and
<span class="emphasis"><em>mapSY</em></span>.
</p><div class="figure"><a name="sourceSY"></a><p class="title"><b>Figure 6. The <span class="emphasis"><em>sourceSY</em></span> derived process constructor</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="450"><tr><td align="center" valign="middle"><object data="figures/sourceSY.svg" type="image/svg+xml" width="450" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"><p>
<span class="emphasis"><em>sourceSY</em></span> takes an initial value <span class="emphasis"><em>s<sub>0</sub></em></span>
and a function <span class="emphasis"><em>f</em></span>, and creates a sequential process with no
inputs and just one output, resulting from the reiterated application of <span class="emphasis"><em>f</em></span>
to <span class="emphasis"><em>s<sub>0</sub></em></span>.
</p><p>
For example, <span class="emphasis"><em>sourceSY</em></span>(1,(+1)), is a
counter with <span class="emphasis"><em>1</em></span> as its initial value.
</p><p>
ForSyDe supplies many other process constructors (e.g. <code class="code">zipWithSY</code>, <code class="code">mealySY</code> ...). However, a thoroughly description
is out of the scope of this tutorial.
</p></div><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="id1251871"></a>3.4. Models of Computation and Domain Interfaces</h3></div></div></div><p>
A <span class="emphasis"><em>Model of Computation</em></span> (MoC), also known
as <span class="emphasis"><em>Computational Model</em></span>, establishes a set of
constraints on the possible processes and signals contained by
a system. A system is said to belong to certain
<span class="emphasis"><em>MoC</em></span> if it satisfies its
constraints.
</p><p>
The behaviour of a process is observed in its
<span class="emphasis"><em>evaluation</em></span>. The evaluation is divided
in atomic steps called <span class="emphasis"><em>evaluation
cycles</em></span>, during which the process produces and
consumes signal values. MoCs specify how and when evaluation
cycles are fired.
</p><p>
ForSyDe currently offers 3 MoCs.
</p><div class="itemizedlist"><ul type="disc"><li><p>
The <span class="strong"><strong>Synchronous MoC</strong></span> was
already mentioned in previous section. All systems
contain an implicit global clock. Its cycle matches
the evaluation cycle of all the system processes, during which
they must consume and produce exactly one value on every
input and output signal.
</p></li><li><p>
<span class="strong"><strong>Untimed
MoC</strong></span>. Communication between processes can be
thought as a specific variant of asynchronous, blocking
message passing. There is no notion of time or global
clock.
</p><p>
Contrary to the Synchronous MoC, in which all the system
processes evaluate in parallel during every cycle,
untimed processes are fired individually. A process only
evaluates when all their inputs have a minimum number of
values ready to be read. That number may vary between
inputs, but is fixed for each of them. On the other hand,
the number of values produced by output signals
may vary independently between evaluation cycles.
</p></li><li><p>
The <span class="strong"><strong>Continuous MoC</strong></span>
models continuous signals representing them as
continuous one-variable, piecewise functions.
</p><div class="figure"><a name="id1252356"></a><p class="title"><b>Figure 7. Continuous signal</b></p><div class="figure-contents">
< (sin(x),[-10,0)), (-sin(x),[0,10)) >
<div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="360"><tr><td align="center" valign="middle"><object data="figures/piecewise_sin.svg" type="image/svg+xml" width="360" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"></li></ul></div><p>
ForSyDe specifies a set of process constructors for each MoC. A
ForSyDe system is thus guaranteed to belong to a MoC if it was
built using constructors from one of those sets.
</p><p>
Nevertheless, it is possible to build heterogeneous systems,
i.e. systems which mix different MoCs. For that purpose,
ForSyDe provides special<sup>[<a name="id1252412" href="#ftn.id1252412" class="footnote">3</a>]</sup> processes in
charge of connecting two subsystems which belong to different
MoCs or which have different timing specifications (e.g. two
Synchronous subsystems with a different clock period).
</p></div></div><div class="section" lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a name="DEvsSE"></a>4. Deep-embedded vs Shallow-embedded signals</h2></div></div></div><p>
As we already mentioned, ForSyDe is implemented as a
Domain Specific Embedded Language (DSL) on top of Haskell.
Actually, ForSyDe offers two different DSL flavours
according to how signals are modelled.
</p><div class="itemizedlist"><ul type="disc"><li><p>
<span class="strong"><strong>Shallow-embedded signals</strong></span>
(<a class="ulink" href="http://hackage.haskell.org/packages/archive/ForSyDe/3.0/doc/html/ForSyDe-Shallow-Signal.htm" target="_top"><code class="code">ForSyDe.Shallow.Signal</code></a>)
are modelled as streams of data isomorphic to lists.
</p><pre class="programlisting">
data Signal a = NullS | a :- Signal a
</pre><p>
Systems built with them are unfortunately restricted to
simulation, however, shallow-embedded signals provide a
rapid-prototyping framework with which to experiment with
Models of Computation.
</p></li><li><p>
<span class="strong"><strong>Deep-embedded signals</strong></span>
(<a class="ulink" href="http://hackage.haskell.org/packages/archive/ForSyDe/3.0/doc/html/ForSyDe-Signal.htm" target="_top"><code class="code">ForSyDe.Signal</code></a>)
are used in a similar way to shallow-embedded signals but
are modelled as an abstract data type which, transparently
to the end user, keeps track of the system
structure<sup>[<a name="id1252502" href="#ftn.id1252502" class="footnote">4</a>]</sup>. Based on that structural
information, ForSyDe's embedded compiler can perform
different analysis and transformations such as simulating
the system or translating it to other target languages
(e.g. VHDL and GraphML).
</p><p>
As a drawback, the deep-embedded API can only currently
build systems belonging to the Synchronous MoC and domain
interfaces are not yet supported. This limitation is,
however, likely to change in the future.
</p></li></ul></div></div><div class="section" lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a name="DE"></a>5. Using deep-embedded Signals</h2></div></div></div><p>
In this section we go through a few simple sample systems
built with ForSyDe's deep-embedded API. We will create both
combinational and sequential systems all belonging to the
Synchronous MoC (the only MoC currently supported by this API).
</p><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="combinational"></a>5.1. Combinational Systems</h3></div></div></div><p>
A system or process is combinational if its outputs are
stateless, i.e. they don't depend on past system events.
</p><div class="section" lang="en"><div class="titlepage"><div><div><h4 class="title"><a name="plus1"></a>5.1.1. A naive combinational system: <span class="emphasis"><em>plus1</em></span></h4></div></div></div><p>
We are going to implement <span class="emphasis"><em>plus1</em></span>, ForSyDe's <span class="emphasis"><em>Hello World</em></span>, a
system with takes integer values, adds 1 to them and forwards the result
through its output signal.
</p><p>
As we mentioned previously, the <span class="emphasis"><em>plus1</em></span>
process can be created in terms of the
<span class="emphasis"><em>mapSY</em></span> process constructor. Here is the
signature of <code class="code">mapSY</code> in the deep-embedded API.
</p><pre class="programlisting">
mapSY :: (ProcType a, ProcType b) =>
ProcId -> ProcFun (a -> b) -> Signal a -> Signal b
</pre><p>
<code class="code">mapSY</code> works similarly to Haskell's
<code class="code">map</code> function. It creates a process which applies a
function to every value in a signal. Let's have a closer look
at its arguments.
</p><div class="variablelist"><dl><dt><span class="term"><code class="code">ProcId</code></span></dt><dd>
The process identifier, simply a textual tag which
univocally identifies the process created (<code class="code">type ProcId
= String</code>).
</dd><dt><span class="term"><code class="code">ProcFun (a->b)</code></span></dt><dd><p>
A process function. The function which will be applied to every element in the input signal. In the
case of <code class="code">plus1</code> we will need a function computationally equivalent to <code class="code">(+1)</code>.
</p><p>
Both <code class="code">a</code> and <code class="code">b</code> must be instances
of <code class="code">ProcType</code> (read Process Type).
<code class="code">ProcType</code> is used by ForSyDe's embedded
compiler to extract type and structure information of expressions.
</p></dd><dt><span class="term"><code class="code">Signal a</code></span></dt><dd>
Input signal.
</dd><dt><span class="term"><code class="code">Signal b</code></span></dt><dd>
Output signal.
</dd></dl></div>
Now, we are ready to start implementing <span class="emphasis"><em>plus1</em></span>.
<pre class="programlisting">
{-# LANGUAGE TemplateHaskell #-}
module Plus1 where
import ForSyDe
import Data.Int (Int32)
</pre><p>
We need to import ForSyDe's library and
<code class="code">Int32</code>. Since deep-embedded systems might be
later translated to hardware, it is required to be specific
about the size of integers used (the size of <code class="code">Int</code> is
platform-specific). Additionally, in all ForSyDe
deep-embedded designs we need to tell GHC to enable the <a class="ulink" href="http://www.haskell.org/th/" target="_top">Template
Haskell</a> (TH) extension, here is why:
</p><pre class="programlisting">
-- A process function which adds one to its input
addOnef :: ProcFun (Int32 -> Int32)
addOnef = $(newProcFun [d|addOnef :: Int32 -> Int32
addOnef n = n + 1 |])
</pre><p>
In the code above, we declared the <code class="code">ProcFun</code> needed
by <code class="code">mapSY</code>. It simply takes an <code class="code">Int32</code> value
and adds 1 to it.
</p><p>
Instead of creating a specific DSL to express computations
in the deep-embedded model, ForSyDe uses TH to allow using
plain Haskell. In principle, <code class="code">ProcFun</code>s can make
use of any Haskell feature supported by TH. However, such
features might not be supported or make sense for certain
backends (e.g. lists and thus, list comprehensions, are
difficult to support in VHDL). Thus, in this tutorial we will
create systems which are compatible with every backend. For example,
writing <code class="code">addOnef = (+1)</code> instead of <code class="code">addOnef n = n +1</code>
is more compact, however the VHDL backend does not currently support
sections nor points-free notation.
</p><p>
In order to use ForSyDe it is not vital to understand what is
really happening, but, for those curious about it, here is how
the TH trick works. First, the <code class="code">[d| .. |]</code> brackets
enclosing the function declaration lift its AST (Abstract
Syntax Tree). Then, the AST is used by <code class="code">newProcFun</code>
to splice (expand in TH's terminology) a <code class="code">ProcFun</code>.
It is important to note that everything happens at compile-time.
</p><p>
Here is the rest of the system definition.
</p><pre class="programlisting">
-- System function (simply a process in this case) which uses addOnef
plus1Proc :: Signal Int32 -> Signal Int32
plus1Proc = mapSY "plus1Proc" addOnef
-- System definition associated to the system function
plus1SysDef :: SysDef (Signal Int32 -> Signal Int32)
plus1SysDef = newSysDef plus1Proc "plus1" ["inSignal"] ["outSignal"]
</pre><p>
First, we use <code class="code">mapSY</code> to create process. Then we create the final definition
of the <span class="emphasis"><em>plus1</em></span> system with <code class="code">newSysDef</code>. Here is its type signature.
</p><pre class="programlisting">
newSysDef :: (SysFun f) => f -> SysId -> [PortId] -> [PortId] -> SysDef f
</pre><div class="variablelist"><dl><dt><span class="term"><code class="code">f</code></span></dt><dd>
A <code class="code">SysFun</code> (system function) describing the
system. It results from the combination of one or more
processes. ForSyDe uses a trick similar to <a class="ulink" href="http://www.haskell.org/ghc/docs/latest/html/libraries/base/Text-Printf.html" target="_top"><code class="code">Text.Printf</code></a>
in order to emulate variadic functions (different systems
are obviously allowed to have different number of inputs
and outputs).
</dd><dt><span class="term"><code class="code">SysId</code></span></dt><dd>
Textual tag identifying the system. <code class="code">type SysId = String</code>.
</dd><dt><span class="term"><code class="code">[PortId]</code></span></dt><dd>
List of port identifiers for the system inputs and outputs. <code class="code">type PortId = String</code>.
</dd></dl></div><p>
Now we can simulate our system, or, as we will see later on, translate it to VHDL or GraphML.
</p><pre class="programlisting">
simulate :: SysFunToSimFun sysFun simFun => SysDef sysFun -> simFun
</pre><p>
<code class="code">simulate</code> transforms our system definition into a
list-based function with the help of a multiparameter
typeclass, <code class="code">SysFunToSimFun</code>, in charge of
implementing the <span class="emphasis"><em>type-level</em></span> translation of the system
signals to lists.
</p><pre class="screen">
<code class="prompt">$</code> ghci Plus1.hs
<code class="prompt">*Plus1></code> let simPlus1 = simulate plus1SysDef
<code class="prompt">*Plus1></code> :t simPlus1
simPlus1 :: [Int32] -> [Int32]
<code class="prompt">*Plus1></code> simPlus1 [1..10]
[2,3,4,5,6,7,8,9,10,11]
</pre><p>
Simulation is lazy, allowing to work with infinite signals.
</p><pre class="screen">
<code class="prompt">*Plus1></code> take 10 $ simPlus1 [1,1..]
[2,2,2,2,2,2,2,2,2,2]
</pre><p>
It is important to remark that ForSyDe does not support
systems containing <span class="emphasis"><em>combinational loops</em></span>.
If such a loop is found, an error will be reported.
</p><p>
For example, here is a system containing a combinational
loop, built with a mutually recursive call between two
processes adding one to their inputs.
</p><pre class="programlisting">
combLoopSysDef :: SysDef (Signal Int32)
combLoopSysDef = newSysDef s "combLoop" [] ["out"]
where s = mapSY "addOne1" addOnef s'
s' = mapSY "addOne2" addOnef s
</pre><p>
As we mentioned, <code class="code">combLoopSysDef</code> cannot be simulated.
</p><pre class="screen">
*Plus1> simulate combLoopSysDef
*** Exception: detected combinational loop
</pre></div><div class="section" lang="en"><div class="titlepage"><div><div><h4 class="title"><a name="id1253066"></a>5.1.2. Keypad encoder</h4></div></div></div><p>
Here is a slightly more complex example. We have a keypad with
4 arrow buttons connected to our synchronous system. The
key-presses are sent in the form of a 4-bit vector. Each bit
indicates whether the corresponding button is pressed (high
value) or not (low value) according to the diagram below.
</p><div class="figure"><a name="encoderfig"></a><p class="title"><b>Figure 8. Keypad encoder</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="225"><tr><td align="center" valign="middle"><object data="figures/encoder.svg" type="image/svg+xml" width="225" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"><p>
In order to work more comfortably and forget about multiple
key-strokes at once, we want to encode each key-press event
with a specific Haskell type: <code class="code">data Direction = Left |
Down | Right | Up</code>.
</p><p>
Of course, keys are not necessarily pressed all the time.
Thus, instead of encoding the input vector into a signal of
<code class="code">Direction</code> we will output signals of
<code class="code">AbstExt Direction</code>.
</p><pre class="programlisting">
data AbstExt a = Abst | Prst a
</pre><p>
<code class="code">AbstExt</code> (read absent-extended) is ForSyDe's
equivalent to the popular Haskell type <code class="code">Maybe</code>.
It is used to introduce absent values in signals, in our
particular case it will denote an absence of key presses.
</p>
Here is the definition of <code class="code">Direction</code> together with
the necessary imports for the definition of the whole system.
<pre class="programlisting">
{-# LANGUAGE TemplateHaskell, DeriveDataTypeable #-}
module Encoder where
import ForSyDe
import Language.Haskell.TH.Lift (deriveLift1)
import Prelude hiding (Left, Right)
import Data.Generics (Data,Typeable)
import Data.Param.FSVec
import Data.TypeLevel.Num hiding ((==))
data Direction = Left | Down | Right | Up
deriving (Typeable, Data, Show)
$(deriveLift1 ''Direction)
</pre><p>
There are a few things worth remarking
</p><div class="itemizedlist"><ul type="disc"><li><p>
Since we are defining new constructors named <code class="code">Left</code> and <code class="code">Right</code>, to avoid clashes
with the identically-named constructors of <code class="code">Either</code> we hide their import from
the <code class="code">Prelude</code>.
</p></li><li><p>
We are defining a custom enumerated
datatype<sup>[<a name="id1253225" href="#ftn.id1253225" class="footnote">5</a>]</sup> (<code class="code">Direction</code>)
whose values will be carried by system signals. All
the values used in a system, and
<code class="code">Direction</code> in particular, must be
instances of the private typeclass
<code class="code">ProcType</code>.
</p><pre class="programlisting">
class (Data a, Lift a) => ProcType a
-- Some existing (overlapping) instances of ProcType
instance (Data a, Lift a) => ProcType a
instance ProcType a => ProcType (AbstExt a)
instance (ProcType a, ProcType b) => ProcType (a,b)
...
</pre><p>
The <code class="code">ProcType</code> constraint is required,
among other reasons, to provide type and structural
information of datatypes to ForSyDe's embedded
compiler. The overlapping instances are needed to
obtain datatype information regardless of
the nesting of values in other supported datastructures.
</p><p>
Due to the <code class="code">(Data a, Lift a) => ProcType a</code>
instance all we need to do in order to use our custom
enumerated datatypes with ForSyDe is creating
instances of <code class="code">Data</code> (which implicitly
requires an instantiation of <code class="code">Typeable</code>)
and Template Haskell's <code class="code">Lift</code> class.
</p><p>
Fortunately, thanks to a GHC extension it is possible
to derive instances for <code class="code">Typeable</code> and
<code class="code">Data</code> (hence the
<code class="code">DeriveDataTypeable</code> language
pragma). Additionally, ForSyDe provides a Template
Haskell module
<code class="code">Language.Haskell.TH.Lift</code><sup>[<a name="id1253310" href="#ftn.id1253310" class="footnote">6</a>]</sup> to automatically generate
instances of <code class="code">Lift</code>. In this case, since we
needed to instantiate a single datatype, we used
<code class="code">deriveLift1</code>.
</p></li><li><p>
The rest of the imports (<code class="code">Data.Param.FSVec</code>
and <code class="code">Data.TypeLevel.Num</code>) come from the
<a class="ulink" href="http://hackage.haskell.org/cgi-bin/hackage-scripts/package/parameterized-data" target="_top"><code class="code">parameterized-data</code></a>
and
<a class="ulink" href="http://hackage.haskell.org/cgi-bin/hackage-scripts/package/type-level" target="_top"><code class="code">type-level</code></a>
packages in order to support fixed-sized vectors.
</p></li></ul></div><p>
</p><p>
Here is the code of the process function, needed to encode the button presses:
</p><pre class="programlisting">
encoderFun :: ProcFun (FSVec D4 Bit -> AbstExt Direction)
encoderFun = $(newProcFun
[d| encode :: FSVec D4 Bit -> AbstExt Direction
encode v = if v ! d0 == H then Prst Left else
if v ! d1 == H then Prst Down else
if v ! d2 == H then Prst Right else
if v ! d3 == H then Prst Up else Abst |])
</pre><p>
The code should be self-explanatory, it makes use of the
type <code class="code">ForSyDe.Bit.Bit</code>, with data constructors
<code class="code">L</code> (low) and <code class="code">H</code> (high), and of
vectors of size 4 (hence the <code class="code">D4</code> type
parameter). In order to get a deeper insight on how
<code class="code">FSVec</code>s work, check <a class="xref" href="#FSVec" title="A. FSVecs: Vectors parameterized in size">Appendix A, <i><code class="literal">FSVec</code>s: Vectors parameterized in size</i></a>. It
is important to note that the system does not take
simultaneous key-strokes in account, choosing the direction
with higher precedence (i.e. situated in the outermost <code class="code">if</code>
expression). Also, using pattern matching with multiple
function clauses instead of nested <code class="code">if</code>
expressions would had been more clear. However, the VHDL
backend currently only supports one clause.
</p><p>
Here is the remaining code needed to build the rest of the system.
</p><pre class="programlisting">
encoderProc :: Signal (FSVec D4 Bit) -> Signal (AbstExt Direction)
encoderProc = mapSY "encoder" encoderFun
encoderSysDef :: SysDef (Signal (FSVec D4 Bit) -> Signal (AbstExt Direction))
encoderSysDef = newSysDef encoderProc "KeypadEncoder" ["arrowBits"] ["direction"]
</pre><p>
Finally, we can evaluate some simulations.
</p><pre class="screen">
<code class="prompt">$</code> ghci -XTemplateHaskell Encoder.hs
<code class="prompt">*Encoder></code> let simEncoder = simulate encoderSysDef
<code class="prompt">*Encoder></code> :t simEncoder
simEncoder :: [FSVec D4 Bit] -> [AbstExt Direction]
<code class="prompt">*Encoder></code> simEncoder [$(vectorTH [L,H,L,L]), $(vectorTH [L,L,L,L])]
[Down,_]
</pre></div></div><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="sequential"></a>5.2. Sequential Systems</h3></div></div></div><p>
Now we are going to have a look at a couple of sequential systems, whose outputs, contrary to combinational systems,
can depend on the system history (i.e. can have a state).
</p><div class="section" lang="en"><div class="titlepage"><div><div><h4 class="title"><a name="counter"></a>5.2.1. A naive sequential system: <span class="emphasis"><em>counter</em></span></h4></div></div></div><p>
Our goal is to generate a signal whose values match its tags
or, more intuitively, a counter from 1 to infinity.
</p><p>
This is clearly a sequential system since its output signal
is not stateless, each output value depends on the previous
one.
</p><pre class="programlisting">
{-# LANGUAGE TemplateHaskell #-}
module Counter where
import ForSyDe
import Data.Int (Int32)
import Plus1 (addOnef)
counterProc :: Signal Int32
counterProc = out'
where out = mapSY "addOneProc" addOnef out'
out' = delaySY "delayOne" 1 out
counterSysDef :: SysDef (Signal Int32)
counterSysDef = newSysDef counterProc "counter" [] ["count"]
</pre><p>
We reuse <code class="code">addOnef</code> from previous examples. The counter is built by the mutually recursive calls of
<code class="code">mapSY</code> and <code class="code">delaySY</code> which should be interpreted as parallel equations.
</p><p>
Again, we can lazily simulate the system.
</p><pre class="screen">
<code class="prompt">$</code> ghci Counter.hs
<code class="prompt">*Counter></code> :t simulate counterSysDef
simulate counterSysDef :: [Int32]
<code class="prompt">*Plus1></code> simulate counterSysDef
[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17
^C Interrupted
</pre><p>
Actually, the definition of <code class="code">counterProc</code> can be
simplified by using <code class="code">sourceSY</code>, getting the following
equivalent declaration.
</p><pre class="programlisting">
counterProc :: Signal Int32
counterProc = sourceSY "counterProc" addOnef 1
</pre></div><div class="section" lang="en"><div class="titlepage"><div><div><h4 class="title"><a name="id1253588"></a>5.2.2. Serial full adder</h4></div></div></div><p>
A serial full adder which adds two streams of bits is a,
still simple, but more elaborated example of a sequential
system. Our system will receive pairs of bits which will be
added together, taking the resulting carry of last cycle in
account.
</p><p>
We are going to implement it as a Mealy FSM (Finite State Machine) following the diagram below.
</p><div class="figure"><a name="fullAdderfig"></a><p class="title"><b>Figure 9. Full Adder: Mealy Machine</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="315"><tr><td align="center" valign="middle"><object data="figures/fullAdderMealy.svg" type="image/svg+xml" width="315" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"><p>
ForSyDe provides derived process constructors to implement FSMs, in this case we will be using
<code class="code">mealySY</code>.
</p><pre class="programlisting">
mealySY :: (ProcType c, ProcType b, ProcType a) =>
ProcId
-> ProcFun (a -> b -> a)
-> ProcFun (a -> b -> c)
-> a
-> Signal b
-> Signal c
</pre><div class="variablelist"><dl><dt><span class="term"><code class="code">ProcId</code></span></dt><dd>
The process identifier, used in the same way as in the
rest of the process constructors
(e.g. <code class="code">mapSY</code> and <code class="code">delaySY</code>).
</dd><dt><span class="term"><code class="code">ProcFun (a- > b -> a)</code></span></dt><dd><p>
A process function in charge of calculating next state
based on current state and current input.
</p></dd><dt><span class="term"><code class="code">ProcFun (a -> b -> c)</code></span></dt><dd><p>
A process function in charge of calculating current output
based on current state and current input.
</p></dd><dt><span class="term"><code class="code">a</code></span></dt><dd><p>
Initial state.
</p></dd><dt><span class="term"><code class="code">Signal b</code></span></dt><dd>
Input Signal.
</dd><dt><span class="term"><code class="code">Signal c</code></span></dt><dd>
Output Signal.
</dd></dl></div><p>
Here is the Haskell code, which should be straightforward to understand.
</p><pre class="programlisting">
{-# LANGUAGE TemplateHaskell #-}
module FullAdder where
import ForSyDe
faNextState :: ProcFun (Bit -> (Bit,Bit) -> Bit)
faNextState = $(newProcFun
[d| faNextState :: Bit -> (Bit,Bit) -> Bit
faNextState st input =
if st == L then
case input of
(H, H) -> H
_ -> L
else
case input of
(L,L) -> L
_ -> H
|])
faOut :: ProcFun (Bit -> (Bit,Bit) -> Bit)
faOut= $(newProcFun
[d| faOut :: Bit -> (Bit,Bit) -> Bit
faOut st input =
if st == L then
case input of
(L, L) -> L
(L, H) -> H
(H, L) -> H
(H, H) -> L
else
case input of
(L, L) -> H
(L, H) -> L
(H, L) -> L
(H, H) -> H
|])
faProc :: Signal (Bit,Bit) -> Signal Bit
faProc = mealySY "addProc" faNextState faOut L
faSysDef :: SysDef (Signal (Bit,Bit) -> Signal Bit)
faSysDef = newSysDef faProc "fullAdder" ["op1", "op2"] ["res"]
</pre>
Here is a little test.
<pre class="screen">
*FullAdder> let simfa = simulate faSysDef
*FullAdder> simfa [(L,L),(L,H),(H,H),(L,L)]
[L,H,L,H]
*FullAdder>
</pre></div></div><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="components"></a>5.3. Using components</h3></div></div></div><p>
A desired characteristic of any system design language is
the possibility of creating hierarchical models.
</p><p>
In ForSyDe's deep-embedded DSL, hierarchical design is implemented through components, let's see
an example.
</p><div class="figure"><a name="seqaddfour"></a><p class="title"><b>Figure 10. <span class="emphasis"><em>AddFour</em></span> system</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="540"><tr><td align="center" valign="middle"><object data="figures/SeqAddFour.svg" type="image/svg+xml" width="540" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"><p>
The system above which, admittedly, would not be of much use
in the real world, adds 4 to its input in serial steps of 1.
</p><p>
Instead of creating 4 different processes and connecting them
together, we can reuse the design of <span class="emphasis"><em>plus1</em></span>
placing 4 identical components.
</p><p>
ForSyDe provides a primitive to create components or instances
of a system: <code class="code">instantiate</code>.
</p><pre class="programlisting">
instantiate :: (SysFun f) => ProcId -> SysDef f -> f
</pre><p>
<code class="code">instantiate</code> creates a component out of a system
definition. A component can be considered a special process
(hence the <code class="code">ProcId</code> parameter) containing an
instance of its parent system (the system from which it is
created).
</p><p>
Instances behave identically to their parents and can be combined with
other system processes.
</p><p>
For example, here we create and simulate an instance of <span class="emphasis"><em>plus1</em></span>
</p><pre class="screen">
$ ghci Plus1.hs
*Plus1> :t plus1SysDef
plus1SysDef :: SysDef (Signal Int32 -> Signal Int32)
*Plus1> let plus1Comp1 = instantiate "plus1_1" plus1SysDef
*Plus1> :t plus1Comp1
plus1SysDef :: Signal Int32 -> Signal Int32
*Plus1> let nestedPlus1 = newSysDef plus1Comp1 "nestedPlus1" ["in1"] ["out1"]
*Plus1> simulate nestedPlus1 $ [1,2,3,4]
[2,3,4,5]
</pre><p>
And here is the definition of the <span class="emphasis"><em>AddFour</em></span> system.
</p><pre class="programlisting">
module AddFour where
import Plus1 (plus1SysDef)
import ForSyDe
import Data.Int (Int32)
addFourProc :: Signal Int32 -> Signal Int32
addFourProc = plus1Comp "plus1_1" .
plus1Comp "plus1_2" .
plus1Comp "plus1_3" .
plus1Comp "plus1_4"
where plus1Comp id = instantiate id plus1SysDef
addFourSysDef :: SysDef (Signal Int32 -> Signal Int32)
addFourSysDef = newSysDef addFourProc "addFour" ["in1"] ["out1"]
</pre><p>
Components, just like any other process, are functions over
signals. This allows using all the combinatorial power of
Haskell. In this particular case we have just used function
composition.
</p><p>
Here is the general workflow of ForSyDe modelling, including
the use of components.
</p><div class="figure"><a name="cwf"></a><p class="title"><b>Figure 11. Component workflow</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="540"><tr><td align="center" valign="middle"><object data="figures/compflow.svg" type="image/svg+xml" width="540" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"><div class="orderedlist"><ol type="1"><li><p>
The designer describes computations using process functions (<code class="code">ProcFun</code>s).
</p></li><li><p>
Those process functions, possibly with other constants,
are passed to process constructors in order to build
processes which are combined together,
creating the main process function.
</p></li><li><p>
The system function is transformed into a system definition by <code class="code">newSysDef</code>.
</p></li><li><p>
The system definition can be
</p><div class="itemizedlist"><ul type="disc"><li>
passed to ForSyDe's embedded compiler, capable of simulating or
translating it to other target languages (VHDL or GraphML at the time being).
</li><li>
used to create components, bringing us back to step 2.
</li></ul></div><p>
</p></li></ol></div></div><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="VHDL"></a>5.4. VHDL Backend</h3></div></div></div><p>
ForSyDe's embedded compiler is able to translate system definitions to VHDL. That is
done through the <code class="code">writeVHDL</code>* functions.
</p><pre class="programlisting">
writeVHDL :: SysDef a -> IO ()
writeVHDLOps :: VHDLOps -> SysDef a -> IO ()
</pre><p>
For example, this is how we would generate the VHDL definition
of <span class="emphasis"><em>AddFour</em></span> and write it to disk.
</p><pre class="screen">
$ ghci AddFour.hs
*AddFour> writeVHDL addFourSysDef
*AddFour> :q
Leaving GHCi.
$ ls -R addFour
vhdl
addFour/vhdl:
addFour_lib work
addFour/vhdl/addFour_lib:
addFour_lib.vhd
addFour/vhdl/work:
addFour.vhd plus1.vhd
</pre><p>
Here is a diagram of the filetree generated for <code class="code">addFour</code>.
</p><div class="figure"><a name="VHDLTree"></a><p class="title"><b>Figure 12. VHDL filetree of <code class="code">addFour</code></b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="315"><tr><td align="center" valign="middle"><object data="figures/VHDLTree.svg" type="image/svg+xml" width="315" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"><p>
<code class="code">writeVHDL</code> generates a VHDL filetree pending from current
working directory. Assuming <code class="code">$SYSNAME</code> is the
system's name (<code class="code">addFour</code> in this particular case):
</p><div class="itemizedlist"><ul type="disc"><li><p>
The main VHDL entity and architecture is written in <code class="code">$SYSNAME/vhdl/work/$SYSNAME.vhdl</code>.
</p></li><li><p>
The VHDL translation of other systems included through component instantiation is also written under
<code class="code">$SYSNAME/vhdl/work/</code>. In the case of the <code class="code">addFour</code> system, the compiler also
generates the file <code class="code">plus1.vhd</code>.
</p></li><li><p>
A global VHDL library, <code class="code">forsyde_lib.vhd</code>, is
bundled with ForSyDe's distribution and contains the
translation of basic monomorphic Haskell types to VHDL. It
is installed under the <code class="code">data</code> directory of
ForSyDe's Cabal package, whose location is
system-dependent.
</p></li><li><p>
Since VHDL lacks support for <span class="emphasis"><em>parametric
polymorphism</em></span>, the translation of polymorphic
types and functions is done on a per-system basis
(i.e. each different possible monotype of a polymorphic
Haskell type triggers a different translation). Thus, the
result of that translation is put in
<code class="code">$SYSNAME/vhdl/lib/$SYSNAME_lib.vhd</code> and not
<code class="code">forsyde_lib.vhd</code>.
</p></li></ul></div><p>
It is important to remember that, even if ForSyDe signals are polymorphic and
<code class="code">ProcFun</code>s can include any Haskell function definition,
some backends might be limited. In the case of the VHDL backend:
</p><div class="itemizedlist"><ul type="disc"><li><p>
Accepted <code class="code">Signal</code> types. <code class="code">Signal a</code> is a valid
signal for the VHDL backend if <code class="code">a</code> belongs to:
</p><div class="orderedlist"><ol type="1"><li><p>
Primitive types: <code class="code">Data.Int</code>{<code class="code">8</code>, <code class="code">16</code>, <code class="code">32</code>}, <code class="code">Bool</code>,
<code class="code">ForSyDe.Bit</code>.
</p></li><li><p>
Custom types: enumerated<sup>[<a name="id1254317" href="#ftn.id1254317" class="footnote">7</a>]</sup> types.
</p></li><li><p>
The following containers, which can hold any primitive
or custom type and can be unrestrictively nested:
<code class="code">Data.Param.FSVec</code>, tuples of unlimited
size<sup>[<a name="id1254337" href="#ftn.id1254337" class="footnote">8</a>]</sup>,
</p></li></ol></div></li><li><p>
Although this will hopefully change in the future, the
declarations contained by <code class="code">ProcFun</code>s must
be fairly simple. For instance:
</p><div class="orderedlist"><ol type="1"><li><p>
Points-free notation is not admitted.
</p></li><li><p>
They can only contain a clause, multiple clauses are not accepted.
</p></li></ol></div></li></ul></div><p>
Getting back to the function interface of the VHDL backend, it
is possible to provide certain compilation options, namely to
integrate Altera's <span class="emphasis"><em>Quartus II</em></span> and
<span class="emphasis"><em>Modelsim</em></span> in our workflow. For that
purpose we will use <code class="code">writeVHDLOps</code>.
</p><p>
For example, we can generate a <code class="code">Quartus II</code> project
and compile the generated VHDL code setting certain configuration
options such as the pin-mapping and the FGPA model to be used.
</p><pre class="programlisting">
compileQuartus :: IO ()
compileQuartus = writeVHDLOps vhdlOps addFourSysDef
where vhdlOps = defaultVHDLOps{execQuartus=Just quartusOps}
quartusOps = QuartusOps{action=FullCompilation,
fMax=Just 50, -- in MHz
fpgaFamiliyDevice=Just ("CycloneII",
Just "EP2C35F672C6"),
-- Three sample pin assignments
pinAssigs=[("in1[0]", "PIN_W1"),
("in1[1]", "PIN_W2"),
("in1[2]", "PIN_W3")]}
</pre><p>
The code above generates the VHDL code for the
<code class="code">addFour</code> system, subsequently creating a Quartus
project and running a full compilation of the project. We set
a minimum acceptable clock frequency of 50 MHz, the FPGA
family (<code class="code">CycloneII</code>), specific device
(<code class="code">EP2C35F672C6</code>) and some pin assignments, which,
for briefness' sake are not sufficient.
</p><p>
It is important to note that, when needed, Quartus will
split input and output port identifiers into several logical
names corresponding to individual bits (e.g in1[0]). Thus, it
might be necessary to open Quartus in order to find out what
logical names to use in pin assignments.
</p><p>
In addition to <span class="emphasis"><em>Quartus II</em></span>, the VHDL
backend is able to interface with
<span class="emphasis"><em>ModelSim</em></span>. For example, the following
function shows how can we automatically compile the generated
VHDL code with ModelSim.
</p><pre class="programlisting">
compileModelSim :: IO ()
compileModelSim = writeVHDLOps vhdlOps addFourSysDef
where vhdlOps = defaultVHDLOps{compileModelsim=True}
</pre><p>
It is also possible to run test benches in ModelSim.
</p><pre class="programlisting">
writeAndModelsimVHDL :: (SysFunToIOSimFun sysF simF) =>
Maybe Int -> SysDef sysF -> simF
writeAndModelsimVHDLOps :: (SysFunToIOSimFun sysF simF) =>
VHDLOps -> Maybe Int -> SysDef sysF -> simF
</pre>
Here are two examples:
<pre class="screen">
$ ghci AddFour.hs
*AddFour> let vhdlSim = writeAndModelsimVHDL Nothing addFourSysDef
*AddFour> :t vhdlSim
vhdlSim :: [Int32] -> IO [Int32]
*AddFour> vhdlSim [1..10]
[4,5,6,7,8,9,10,11,12,13,14]
</pre><p>
In the example above, we simulate <code class="code">addFour</code> without supplying a limit in the number of cycles to
simulate. <code class="code">writeAndModelsimVHDL</code> is strict, so, without a limit it will only work
with finite input stimuli.
</p><pre class="screen">
$ ghci Counter.hs
*Counter> writeAndModelsimVHDL (Just 20) counterSysDef
[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]
</pre><p>
In this case the system does not have any inputs and thus the simulation implicitly results in infinite
output stimuli. Thus, it is necessary to set a limit in the number of cycles to simulate.
</p><p>
In a general way, the <code class="code">writeAndModelsimVHDL</code>* functions, generate a
simulation function which will
</p><div class="orderedlist"><ol type="1"><li><p>
Generate a VHDL model (implicitly using the
<code class="code">writeVHDL</code>* functions).
</p></li><li><p>
Compile the resulting model with ModelSim.
</p></li><li><p>
Marshal the provided input stimuli from Haskell to VHDL
and generate a testbench in
<code class="code">$SYSNAME/vhdl/test/$SYSNAME_tb.vhd</code>.
</p></li><li><p>
Simulate the testbench with ModelSim and unmarshal the
results back to Haskell.
</p></li></ol></div><p>
<code class="code">writeAndModelsimVHDL</code>* give equivalent results to <code class="code">simulate</code>, with a few caveats.
</p><div class="itemizedlist"><ul type="disc"><li><p>
<code class="code">writeAndModelsimVHDL</code>*, unlike
<code class="code">simulate</code>, are strict, and thus do not
support infinite stimuli. For that reason, it is
possible to set the number of cycles to simulate
(<code class="code">Maybe Int</code> parameter).
</p></li><li><p>
<code class="code">writeAndModelsimVHDL</code>* , provide <code class="code">IO</code> simulation functions
whereas <code class="code">simulate</code> is pure.
</p></li><li><p>
<code class="code">writeAndModelsimVHDL</code>* suffer all the limitations of the VHDL backend whereas
<code class="code">simulate</code> can cope with any system.
</p></li></ul></div></div><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="GraphML"></a>5.5. GraphML Backend</h3></div></div></div><p>
It is possible to use ForSyDe's GraphML backend in order to
</p><div class="orderedlist"><ol type="1"><li><p>
Generate an XML-based intermediate representation of
a system for further processing.
</p></li><li><p>
Obtain system diagrams.
</p></li></ol></div><p>
ForSyDe provides the following functions, similar to the ones of the VHDL backend.
</p><pre class="programlisting">
writeGraphML :: SysDef a -> IO ()
writeGraphMLOps :: GraphMLOps -> SysDef a -> IO ()
</pre><p>
For example, here is how we would generate the GraphML translation of <code class="code">addFour</code>
</p><pre class="screen">
$ ghci AddFour.hs
*AddFour> writeGraphML addFourSysDef
*AddFour> :q
Leaving GHCi.
$ ls -R addFour
graphml
addFour/graphml:
addFour.graphml plus1.graphml
</pre><p>
As we can see, a <code class="code">.graphml</code> file is generated for each
system involved. In this case, one for the main system
(<code class="code">addFour.graphml</code>) and another one for <code class="code">plus1</code>
which was instantiated by <code class="code">addFour</code>.
</p><p>
In order to embed ForSyDe metainformation, the GraphML backend
makes use of the following <a class="ulink" href="http://graphml.graphdrawing.org/primer/graphml-primer.html#Attributes" target="_top">GraphML-Attributes</a>:
</p><pre class="screen">
<key id="process_type" for="node" attr.name="process_type" attr.type="string"/>
<key id="value_arg" for="node" attr.name="value_arg" attr.type="string"/>
<key id="procfun_arg" for="node" attr.name="procfun_arg" attr.type="string"/>
<key id="instance_parent" for="node" attr.name="instance_parent" attr.type="string"/>
</pre><p>
The keys above are used to tag nodes in different ways.
</p><div class="itemizedlist"><ul type="disc"><li><p>
<span class="strong"><strong><code class="code">process_type</code></strong></span> indicates what process constructor was used
to create a process node or if the node is an input or output port.
</p></li><li><p>
<span class="strong"><strong><code class="code">value_arg</code></strong></span> contains a value passed to a process
constructor.
</p></li><li><p>
<span class="strong"><strong><code class="code">procfun_arg</code></strong></span> contains a value passed to a process
constructor.
</p></li><li><p>
<span class="strong"><strong><code class="code">instance_parent</code></strong></span> is specific to component nodes
and indicates the name of the parent system from which the component was instanciated.
</p></li></ul></div><div class="section" lang="en"><div class="titlepage"><div><div><h4 class="title"><a name="id1254817"></a>5.5.1. Obtaining diagrams of ForSyDe</h4></div></div></div><p>
The GraphML definition does not provide a way to specify the
graphical representation of graphs (e.g. edge and node
shapes, colours, textual tags ...)
</p><p>
For that reason, <a class="ulink" href="http://www.yworks.com" target="_top"><span class="emphasis"><em>yWorks</em></span></a>, a company
offering graph visualization products, created yFiles-GraphML, an extension to the GraphML
schema which adds graphical information.
</p><p>
yWorks also distributes <a class="ulink" href="http://www.yworks.com/en/products_yed_about.html" target="_top"><span class="emphasis"><em>yEd</em></span></a>,
a free (as in beer) multiplatform graph editor with
impressive automatic layout features.
</p><p>
Here is an example on how to generate and edit
yFiles-GraphML diagrams from ForSyDe systems. For this
purpose, we will use our <span class="emphasis"><em>counter</em></span> system.
</p><pre class="screen">
$ ghci Counter.hs
*Counter> writeGraphMLOps defaultGraphMLOps{yFilesMarkup=True} counterSysDef
*Counter> :q
$ ls -R counter
graphml
counter/graphml:
counter.graphml sourceSY_counterProc.graphml
</pre><p>
<code class="code">sourceSY_counterProc.graphml</code> contains the <span class="emphasis"><em>sourceSY</em></span> process
used in the counter. Let's view its representation with yEd.
</p><p>
This is the unorganized representation we get right after opening <code class="code">sourceSY_counterProc.graphml</code>
with yEd.
</p><div class="figure"><a name="sourceSY_counterProc1"></a><p class="title"><b>Figure 13. Initial yEd representation</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="225"><tr><td align="center" valign="middle"><object data="figures/sourceSY_counterProc1.svg" type="image/svg+xml" width="225" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"><p>
All nodes are overlapped because the GraphML-yFiles backend
does not perform any kind of node placement nor edge
routing. yEd, however, does a very good job in this regard.
</p><p>
Before running a layout algorithm it is convenient to set
port constraints on the graph nodes. This is a workaround to
make yEd faithfully represent shared signals
(signals coming from the same process output), otherwise yEd
will treat them as different outputs. The GraphML format
(and GraphML-yFiles) allows edge sharing through the use of
<a class="link" href=""><span class="emphasis"><em>ports</em></span></a>,
however, yEd does not currently respect them. Our current
solution is to set a location for the edge ends in the
GraphML backend and lock that location through yEd port
constraints.
</p><p>
In order to set the port constraints we will go to
<span class="emphasis"><em>Tools -> Constraints -> Port
Constraints</em></span>.
</p><p>
The port constraints menu will initially look like this.
</p><div class="figure"><a name="portConstraints1"></a><p class="title"><b>Figure 14. Port constraints default options</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="360"><tr><td align="center" valign="middle"><img src="figures/portConstraints1.png" align="middle" width="360" alt="Port constraints default options"></td></tr></table></div></div></div><br class="figure-break"><p>
These are the options we need to set in order to fix all
ports. Remember to click on OK after setting them.
</p><div class="figure"><a name="portConstraints2"></a><p class="title"><b>Figure 15. Desired port constraint options</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="360"><tr><td align="center" valign="middle"><img src="figures/portConstraints2.png" align="middle" width="360" alt="Desired port constraint options"></td></tr></table></div></div></div><br class="figure-break"><p>
It is important to note that due to a bug in yFiles format
it is not possible to save port constraints in <code class="code">.graphml</code> files. Thus,
we will need to reset the port constraints every time a file is reopened.
</p><p>
Now we are ready to run an automatic layout algorithm. The
generated GraphML-yFiles graph is prepared to be displayed
from left to right. The hierarchical layout
(<span class="emphasis"><em>Layout -> Hierarchical -> Classic</em></span>)
seems to give the best results for system diagrams. It is
important to set the Orientation to <span class="emphasis"><em>Left to
Right</em></span> and allow <span class="emphasis"><em>Backloop Routing</em></span>.
</p><div class="figure"><a name="layout"></a><p class="title"><b>Figure 16. hierarchical layout</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="360"><tr><td align="center" valign="middle"><img src="figures/layout.png" align="middle" width="360" alt="hierarchical layout"></td></tr></table></div></div></div><br class="figure-break">
After clicking on <span class="emphasis"><em>OK</em></span>, the system diagram should look like this:
<div class="figure"><a name="sourceSY_counterProc2"></a><p class="title"><b>Figure 17. Final yEd representation</b></p><div class="figure-contents"><div class="mediaobject" align="center"><table border="0" summary="manufactured viewport for HTML img" cellspacing="0" cellpadding="0" width="450"><tr><td align="center" valign="middle"><object data="figures/sourceSY_counterProc2.svg" type="image/svg+xml" width="450" align="middle"></object></td></tr></table></div></div></div><br class="figure-break"></div><div class="section" lang="en"><div class="titlepage"><div><div><h4 class="title"><a name="id1255153"></a>5.5.2. GraphML limitations</h4></div></div></div><p>
Unfortunately, GraphML nor yFiles-GraphML + yEd suit all ForSyDe needs:
</p><div class="itemizedlist"><ul type="disc"><li><p>
yFiles does not respect GraphML ports (source signal
sharing). We provide a workaround based on precalculate
the location of edge ends plus yEd routing port constraints
(which unfortunately cannot be saved).
</p></li><li><p>
yEd wipes out external <code class="code"><data></code> tags
(external GraphML attributes). That includes ForSyDe's
metainformation, which will be lost after editing the
graph with yEd.
</p></li><li><p>
GraphML nor yFiles-GraphML explicitly support subgraphs
but not subgraph sharing (components). Our solution is
to use external <data> tags indicating parent
systems in instance nodes. However, yEd is obviously
unaware of that trick, not being able to offer
hierarchical browsing.
</p></li></ul></div></div></div></div><div class="section" lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a name="SE"></a>6. Shallow-embedded signals</h2></div></div></div><p>
As it was previously mentioned, ForSyDe offers a flavour of
signals called shallow-embedded signals, modelled as
streams of data:
</p><pre class="programlisting">
data Signal a = NullS | a :- Signal a
</pre><p>
This representation offers some advantages:
</p><div class="itemizedlist"><ul type="disc"><li><p>
Rapid prototyping of systems.
</p></li><li><p>
It is easy to include new MoCs.
</p></li><li><p>
It supports all the MoCs covered by ForSyDe (Synchronous, Untimed and Continuous).
</p></li></ul></div><p>
Shallow-embedded signals also present some disadvantages:
</p><div class="itemizedlist"><ul type="disc"><li><p>
Systems built with them can only be
simulated. Shallow-embedded signals don't contain any
structural information. Thus, the models resulting from them
cannot be analyzed or compiled to other target languages.
</p></li><li><p>
No support for components. However, they are not really needed, components are not
useful for simulation and reusability can be achieved by function refactoring.
</p></li></ul></div><p>
Here is the implementation of <span class="emphasis"><em>plus1</em></span> using shallow-embedded signals.
</p><pre class="programlisting">
module Plus1Shallow where
import ForSyDe.Shallow
import Data.Int(Int32)
plus1 :: Signal Int32 -> Signal Int32
plus1 = mapSY (+1)
</pre><p>
The system can be simulated directly simply by calling <span class="emphasis"><em>plus1</em></span>.
</p><pre class="screen">
$ ghci Plus1Shallow.hs
*Plus1Shallow> :t signal
signal :: [a] -> Signal a
*Plus1Shallow> plus1 (signal [1..10])
{2,3,4,5,6,7,8,9,10,11}
</pre><p>
We can also integrate deep-embedded models into shallow-embedded
ones by using <code class="code">simulate</code>, <code class="code">signal</code> and
<code class="code">fromSignal</code> (the inverse of <code class="code">signal</code>).
In the example below, we use the deep-embedded
<code class="code">addFour</code> system and the shallow-embedded
<code class="code">plus1</code> to build <span class="emphasis"><em>plus5</em></span>
</p><pre class="programlisting">
module Plus5 where
import Plus1Shallow
import AddFour
import ForSyDe (simulate)
import ForSyDe.Shallow
import Data.Int (Int32)
plus5 :: Signal Int32 -> Signal Int32
plus5 = plus1 . signal . simulate addFourSysDef . fromSignal
</pre><pre class="screen">
$ ghci Plus5.hs
*Plus5> plus5 (signal [1..10])
{6,7,8,9,10,11,12,13,14,15}
</pre></div><div class="appendix" lang="en"><h2 class="title" style="clear: both"><a name="FSVec"></a>A. <code class="literal">FSVec</code>s: Vectors parameterized in size</h2><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="id1255404"></a>1. Goal</h3></div></div></div><p>
We would like to numerically parameterize vectors using their
length in order to implement fixed-sized vectors
(<code class="code">FSVec</code>). Ideally, we would like to be able to
implement something similar to this:
</p><pre class="programlisting">
v :: FSVec 23 Int -- Not Haskell
</pre><p>
<code class="code">v</code> would be a a vector containing 23 <code class="code">Int</code>s. Note it
is not possible to directly do this in Haskell.
</p><p>
The vector concatenation function would be something along the lines of:
</p><pre class="programlisting">
(++) :: FSVec s1 a -> FSVec s2 a -> FSVec (s1+s2) a -- Again, not valid Haskell
</pre><p>
We would also like to establish static security constraints on
functions. Those constrains would be checked at compile time
guaranteeing a correct behaviour during runtime. For instance.
</p><pre class="programlisting">
head :: FSVec (s > 0) a -> FSVec (s - 1) a -- Not Haskell
</pre><p>
However, Haskell does not support dependent types (a numerically
parameterized-vector is in practice a dependent type) nor type-level
lambdas directly. Yet, it is still possible to implement our <code class="code">FSVec</code>
type using Haskell plus a few GHC extensions.
</p></div><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="id1255478"></a>2. How?</h3></div></div></div><p>
Before diving into the details, let me spoil the final result:
</p><pre class="programlisting">
v :: FSVec D23 Int
(++) :: (Nat s1, Nat s2, Add s1 s2 s3) => FSVec s1 a -> FSVec s2 a -> FSVec s3 a
head :: Pos s => FSVec s a -> a
</pre><p>
The code is a bit more verbose that the pseudo-Haskell code of
previous section, but note that <span class="strong"><strong>it
is</strong></span> Haskell code (using the Multiparameter class
extension).
</p><p>
The trick is to emulate the parameters using type-level decimal
numerals. But, What is that?
</p></div><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="id1255502"></a>3. Type-level decimal numerals</h3></div></div></div><p>
We already mentioned that the trick is to use types to represent the size of
the vector. So, we want a type parameter to represent a number, but, How?
</p><pre class="programlisting">
-- Numerical digits
data D0 -- empty type (supported by a EmptyDataDecls GHC extension,
-- we could have included a phony constructor otherwise)
data D1
data D2
..
data D9
data a :* b -- connective to build multidigit numerals (empty again)
-- note that the type constructor is infix (GHC TypeOperators extension)
</pre><p>
Using the definitions above we can represent arbitrarily-sized natural
numbers. Some examples:
</p><div class="segmentedlist"><table border="0"><thead><tr class="segtitle"><th>Number</th><th>Type-level representation</th></tr></thead><tbody><tr class="seglistitem"><td class="seg">0</td><td class="seg"><code class="code">D0</code></td></tr><tr class="seglistitem"><td class="seg">13</td><td class="seg"><code class="code">D1 :* D3</code></td></tr><tr class="seglistitem"><td class="seg">1024</td><td class="seg"><code class="code">D1 :* D0 :* D2 :* D4</code></td></tr></tbody></table></div><p>
It seems sensible, but very verbose. It would certainly be nicer to be
able to express 0 as <code class="code">D0</code>, 13 as <code class="code">D13</code> and so on.
</p><p>
We solved the problem by using Template Haskell to generate
type synonyms (aliases) up to <code class="code">D5000</code>. The same
trick was used to emulate binaries (up to
<code class="code">B10000000000</code>), octals (up to <code class="code">O10000</code>)
and hexadecimals (up to <code class="code">H1000</code>):
</p><pre class="screen">
$ ghci -XTypeOperators -XFlexibleContexts # Extensions used in different parts of this appendix
Prelude> :m +Data.TypeLevel
Prelude Data.TypeLevel> :i D124
type D124 = (D1 :* D2) :* D4
-- Defined in Data.TypeLevel.Num.Aliases
Prelude Data.TypeLevel> :i HFF
type HFF = (D2 :* D5) :* D5
-- Defined in Data.TypeLevel.Num.Aliases
Prelude Data.TypeLevel> :i B101
type B101 = D5 -- Defined in Data.TypeLevel.Num.Aliases
</pre><p>
Of course, if you want to use a numeral which is out of the
aliases range, the only option is to use the verbose decimal
representation (it shouldn't be the normal case though)
</p><p>
Similarly to <code class="code">D13</code>, <code class="code">D124</code> ...
undercase value-level aliases (<code class="code">d12</code>,
<code class="code">d123</code>, .. declared as <code class="code">undefined</code>)
are generated in order to create type-level values.
</p><pre class="screen">
Prelude Data.TypeLevel> :i d123
d123 :: (D1 :* D2) :* D3 -- Defined in Data.TypeLevel.Num.Aliases
</pre><p>
Fair enough. However, you might already have guessed that
<code class="code">:*</code> can be used to construct ambiguous or
not-normalized numerals, for instance:
</p><pre class="programlisting">
D0 :* D0 :* D1 -- numeral with trailing zeros
(D1 :* D0) :* (D2 :* D2) -- malformed numeral
</pre><p>
Now is when the natural (<code class="code">Nat</code>) and positive
(<code class="code">Pos</code>) type-classes get in the game. We are
going to omit the instances but, trust us, they guarantee
that numerals are well-formed:
</p><pre class="programlisting">
class Nat n where
toNum :: Num a => n -> a
class Nat n => Pos n
</pre><p>
<code class="code">toNum</code> allows to pass the type-level numeral to value-level.
</p><pre class="screen">
Prelude Data.TypeLevel> toNum d123
123
-- a non-normalized numeral
Prelude Data.TypeLevel> toNum (undefined :: D0 :* D1)
<interactive>:1:0:
No instance for (Data.TypeLevel.Num.Sets.PosI D0)
arising from a use of `toNum' at <interactive>:1:0-28
Possible fix:
add an instance declaration for (Data.TypeLevel.Num.Sets.PosI D0)
In the expression: toNum (undefined :: D0 :* D1)
In the definition of `it': it = toNum (undefined :: D0 :* D1)
</pre><p>
Based on the numerical representation we created, and using
multiparameter type-classes, we can define type-level
operations. The operations supported right now are:
</p><div class="itemizedlist"><ul type="disc"><li><p>
Arithmetic: Successor, Predecesor, Addition,
Subtraction, Multiplication, Division, Modulus, Greatest
Common Divisor, Exponentiation and Logarithm.
</p></li><li><p>
Comparison: trichotomy classification, (<), (>) (<=),
(>=), (==), Minimum and Maximum.
</p></li></ul></div><p>
Some examples:
</p><pre class="screen">
Prelude Data.TypeLevel> :i Data.TypeLevel.divMod
Data.TypeLevel.divMod :: (DivMod x y q r) => x -> y -> (q, r)
-- Defined in Data.TypeLevel.Num.Ops
Prelude Data.TypeLevel> d23 `Data.TypeLevel.divMod` d2
(11,1)
</pre><p>
Note that the resulting type is calculated at compile time:
</p><pre class="screen">
Prelude Data.TypeLevel> :t d23 `Data.TypeLevel.divMod` d2
d23 `Data.TypeLevel.divMod` d2 :: (D1 :* D1, D1)
d23 `Data.TypeLevel.divMod` d2 :: (D1 :* D1, D1)
</pre><p>
Note as well that the operations are consistent, we cannot, for
instance, calculate the predecessor of zero:
</p><pre class="screen">
Prelude Data.TypeLevel> Data.TypeLevel.pred d0
<interactive>:1:0:
No instances for (Data.TypeLevel.Num.Ops.Failure
(Data.TypeLevel.Num.Ops.PredecessorOfZeroError x),
[..]
</pre><p>
We can even add constraints to our own functions. For instance, we
want to guarantee (at compilation time) that a type-level
numeral number is lower than 6 and greater than 3.
</p><pre class="screen">
Prelude Data.TypeLevel> let check :: (Nat x, x :<: D6, x :;>: D3, Num a) => x -> a; check n = toNum n
</pre><p>
For example, 2 does not meet the constraints.
</p><pre class="screen">
Prelude Data.TypeLevel> check d2
<interactive>:1:0:
Couldn't match expected type `CGT' against inferred type `CLT'
[..]
</pre><p>
Whereas 4 does
</p><pre class="screen">
Prelude Data.TypeLevel> check d4
4
</pre></div><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="id1255520"></a>4. Fixed Sized Vectors themselves</h3></div></div></div><p>
Getting back to fixed-sized vectors themselves, FSVec offers
a <a class="ulink" href="http://hackage.haskell.org/packages/archive/parameterized-data/0.1.2/doc/html/Data-Param-FSVec.html" target="_top">reasonably
rich vector API</a> based on type-level numerals.
</p><p>
For example, we can safely access the elements of a vector
without the risk of getting
<span class="emphasis"><em>out-of-bounds</em></span> errors.
</p><pre class="programlisting">
(!) :: (Pos s, Nat i, i :<: s) => FSVec s a -> i -> a
</pre><p>
The best part of it is that the bound checks are performed
on the type level at compilation time, not adding any
overhead to the execution of our code.
</p><pre class="screen">
Prelude Data.TypeLevel> :m +Data.Param.FSVec
Prelude Data.TypeLevel Data.Param.FSVec> $(vectorTH [1::Int,2,3]) ! d0
1
Prelude Data.TypeLevel Data.Param.FSVec> $(vectorTH [1::Int,2,3]) ! d7
<interactive>:1:0:
Couldn't match expected type `LT' against inferred type `GT'
When using functional dependencies to combine
Trich D7 D3 GT,
[..]
</pre><p>
<code class="code">vectorTH</code> is a Template Haskell function to
create vectors out of lists, we will get back to why TH is
needed later. <code class="code">d0</code> and <code class="code">d7</code> are
declared as <code class="code">undefined</code> (bottom) and force the
inference of the <code class="code">D0</code> and <code class="code">D7</code>
type-level values. Note that the explicit type signatures
are needed due to Haskell's monomorphism restriction, in the
general non-interactive code does not need this kind of type
annotations.
</p><div class="warning" style="margin-left: 0.5in; margin-right: 0.5in;"><h3 class="title">Warning</h3>
Using numerical literals instead of the
<code class="code">undefined</code> values (e.g. 0 and 7 instead of
<code class="code">d0</code> and <code class="code">d7</code>) is a very common error.
</div><p>
Here are two further examples using <code class="code">head</code>.
</p><pre class="screen">
Prelude Data.TypeLevel Data.Param.FSVec> Data.Param.FSVec.head $(vectorTH [1::Int,2,3])
1
Prelude Data.TypeLevel Data.Param.FSVec> Data.Param.FSVec.head empty
<interactive>:1:0:
No instance for (Data.TypeLevel.Num.Sets.PosI D0)
arising from a use of `Data.Param.FSVec.head'
</pre><p>
Again, attempting to obtain the head of an empty vector triggers a compile-time error.
</p><p>
Even if FSVec offers many nice features, it also has a few problems.
</p></div><div class="section" lang="en"><div class="titlepage"><div><div><h3 class="title"><a name="id1255822"></a>5. <code class="code">FSVec</code> issues</h3></div></div></div><div class="orderedlist"><ol type="1"><li><p>
Some functions such as <code class="code">filter</code> cannot be
implemented. One can think about something along the
lines of:
</p><pre class="programlisting">
filter :: (a -> Bool) -> FSVec s a -> FSVec s2 a
</pre><p>
However, the size of the output vector (<code class="code">s2</code>) cannot be precalculated
statically.
</p></li><li><p>
Since <code class="code">FSVec</code> is an abstract data type,
pattern matching is lost, but that is the general case
in vector implementations
<sup>[<a name="id1255999" href="#ftn.id1255999" class="footnote">9</a>]</sup>.
</p></li><li><p>
It is difficult to build a vector from a list. Again, the first thing one would
think of would be
</p><pre class="programlisting">
vector :: Nat s => [a] -> FSVec s a
</pre><p>
However, since <code class="code">s</code> would be a different type
depending on the length of <code class="code">[a]</code>, this is not
a valid Haskell function. <code class="code">s</code> is
existentially quantified, a feature not supported
directly by Haskell98.
</p><p>
In addition, since the list-length is a run-time
condition, it is impossible to guess at compile
time.
</p><p>
However, there are a few workarounds which are already
included in the library:
</p><div class="orderedlist"><ol type="a"><li><p>
As suggested in Eaton's <a class="ulink" href="http://ofb.net/~frederik/vectro/draft-r2.pdf" target="_top">Statically
Typed Linear Algebra in Haskell</a>, emulate an
existential through <a class="ulink" href="http://en.wikibooks.org/wiki/Haskell/Continuation_passing_style" target="_top">CPS</a>
(Continuation passing style). CPS is a style of
programming where functions never return values, but
instead take an extra parameter which they give
their result to.
</p><pre class="programlisting">
vectorCPS :: Nat s => vectorCPS :: [a] -> (forall s. Nat s => FSVec s a -> w) -> w
</pre><p>
Note that the <code class="code">forall</code> keyword is due to using Rank2 types
to emulate the existential. You don't
really need to understand how they work but just know to use
vectorCPS. Here is an example:
</p><pre class="screen">
$ ghci
Prelude> :m +Data.Param
Prelude Data.Param> (vectorCPS [1,2,3,4]) Data.Param.length
4
</pre><p>
Note that length is passed to the result of <code class="code">vectorCPS</code> and not the
other way around.
</p></li><li><p>
Unsafely provide the length of the resulting vector:
</p><pre class="programlisting">
unsafeVector :: Nat s => s -> [a] -> FSVec s a
</pre><p>
<code class="code">unsafeVector</code> does not suffer the
"existential type" problem of <code class="code">vectorCPS</code>,
however it can happen that the dynamic length of the
list does not match the provided length (that is why the
function name has an "unsafe" prefix). Furthermore if
that is the case, we will only be able to know at
runtime.
</p><pre class="programlisting">
Prelude Data.Param> :m +Data.TypeLevel
Prelude Data.Param Data.TypeLevel> unsafeVector d8 [1,2]
*** Exception: unsafeVector: dynamic/static length mismatch
Prelude Data.Param Data.TypeLevel> unsafeVector d2 [1,2]
<1,2>
</pre></li><li><p>
Template Haskell.
</p><p>
This is the preferred solution. The only problem is that, of course,
the TH extension is required (but we already had that dependency in ForSyDe) and you
can only use it with lists which are available at compile time (which,
for the general case of ForSyDe designs should not be a problem).
</p><pre class="screen">
$ ghci -XTemplateHaskell
Prelude> :m +Data.Param
Prelude Data.Param> $(vectorTH [1 :: Int,2,3,4])
Prelude Data.Param> :t $(vectorTH [1 :: Int,2,3,4])
$(vectorTH [1 :: Int,2,3,4]) :: (Num t) => FSVec Data.TypeLevel.Num.Reps.D4 t
</pre></li></ol></div></li></ol></div></div></div><div class="footnotes"><br><hr width="100" align="left"><div class="footnote"><p><sup>[<a name="ftn.id1251533" href="#id1251533" class="para">1</a>] </sup>ForSyDe has been tested to run
successfully on Linux, OSX-Leopard-x86 and Windows when compiled
under GHC version 6.8.2. Due to the massive number of instances
automatically generated in ForSyDe, it is not recommended to use
a higher version of GHC until <a class="ulink" href="http://hackage.haskell.org/trac/ghc/ticket/2328" target="_top">bug
#2328</a> is fixed.</p></div><div class="footnote"><p><sup>[<a name="ftn.id1251950" href="#id1251950" class="para">2</a>] </sup>The term combinational comes from
Digital Circuit Theory. In the context of ForSyDe, a
synchronous process is combinational, as opposed to
sequential, if its outputs don't depend on the history of the
input signals. That is, the process is stateless, all output
values can only depend on the input values consumed in the
same clock cycle.</p></div><div class="footnote"><p><sup>[<a name="ftn.id1252412" href="#id1252412" class="para">3</a>] </sup>In the sense of
belonging to any particular MoC</p></div><div class="footnote"><p><sup>[<a name="ftn.id1252502" href="#id1252502" class="para">4</a>] </sup>Current implementation is based on
<a class="ulink" href="http://www.cs.chalmers.se/~koen/Lava/" target="_top">Lava</a>'s
<a class="ulink" href="http://www.cs.chalmers.se/~koen/pubs/entry-asian99-lava.html" target="_top">Observable
Sharing</a>.</p></div><div class="footnote"><p><sup>[<a name="ftn.id1253225" href="#id1253225" class="para">5</a>] </sup>More formally, a datatype with
data constructors whose arity is zero in all
cases.</p></div><div class="footnote"><p><sup>[<a name="ftn.id1253310" href="#id1253310" class="para">6</a>] </sup>Based
on the <a class="ulink" href="http://hackage.haskell.org/cgi-bin/hackage-scripts/package/th-lift" target="_top"><code class="code">th-lift</code></a>
package</p></div><div class="footnote"><p><sup>[<a name="ftn.id1254317" href="#id1254317" class="para">7</a>] </sup>Again,
consider an enumerated type to be an algebraic type
whose data constructors all have arity
zero.</p></div><div class="footnote"><p><sup>[<a name="ftn.id1254337" href="#id1254337" class="para">8</a>] </sup>In practice, the upper limit is
Haskell-compiler dependent. In the case of GHC,
current limit is 62.</p></div><div class="footnote"><p><sup>[<a name="ftn.id1255999" href="#id1255999" class="para">9</a>] </sup>
We tried to implement pattern matching using the
<a class="ulink" href="http://www.haskell.org/ghc/dist/current/docs/users_guide/template-haskell.html#th-quasiquotation" target="_top">new
Quasiquoting mechanism in GHC</a> <a class="ulink" href="http://www.haskell.org/pipermail/template-haskell/2008-February/000655.html" target="_top">
without success</a>.
</p></div></div></div></body></html>