Copilot: A (Haskell DSL) stream language for generating hard real-time C code.
Can you write a list in Haskell? Then you can write embedded C code using
Copilot. Here's a Copilot program that computes the Fibonacci sequence (over
Word 64s) and tests for even numbers:
fib :: Streams
fib = do
let f = varW64 "f"
let t = varB "t"
f .= [0,1] ++ f + (drop 1 f)
t .= even f
where even :: Spec Word64 -> Spec Bool
even w' = w' `mod` 2 == 0
Copilot contains an interpreter, a compiler, and uses a model-checker to check
the correctness of your program. The compiler generates constant time and
constant space C code via Tom Hawkin's Atom (thanks Tom!). Copilot was
originally developed to write embedded monitors for more complex embedded
systems, but it can be used to develop a variety of functional-style embedded
code.
*******************************************************************************
Please visit <http://leepike.github.com/Copilot/> for more information about
installing and using Copilot.
Also available as index.html in the gh-pages branch of the Copilot repo. In
your local repo,
> git checkout gh-pages
and you should see index.html.
*******************************************************************************
Release notes
* Copilot-0.26
* Variables are now specs, not strings. This gives stream expressions a type,
so no need for constant functions, monomorphic cast functions, or var
annotations in expressions. Examples updated to reflect the change.
* Copilot-0.25
* Added true, false Specs (Spec Bool)
* Removed generic const -- unneeded, since Spec instantiates Num.
* Change casting to only allow casts that (1) are guaranteed not to change the
sign and (2) are to a larger type.
* Removed libs from Copilot.hs. You must import these explicitly.
* Fixed buts with LTL and ptLTL libraries and examples and added documentation.
* Copilot-0.24
* Fixed a bug in external array analysis for computing the minimum period
size.
* Added the ability to specify a HW clock for Atom.
* Copilot-0.23
* All -Wall warnings removed (from importing Copilot.hs).
* Added support for sampling external array values. (See Examples.hs).
* Fixed a bug in calling CBMC to ensure it unrolls it's loop. Updated
documentation in Help.hs.
* Other minor stylistic changes and fixes.
* Copilot-0.22: initial release