@hackage copilot0.26

A stream DSL for writing embedded C monitors.

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