Hackage :: [Package]

copilot: A stream DSL for writing embedded C monitors.

[ bsd3, embedded, language, library ] [ Propose Tags ] [ Report a vulnerability ]

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 "fib"
 let t = varB "t"
 f .= [0,1] ++ f + (drop 1 f)
 t .= even f
   where even :: Spaec 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.

[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.21, 0.22, 0.23, 0.25, 0.26, 0.27, 0.28, 1.0, 1.0.1, 1.0.2, 2.0, 2.0.1, 2.0.2, 2.0.3, 2.0.4, 2.0.5, 2.0.6, 2.0.7, 2.0.8, 2.0.9, 2.1.0, 2.1.1, 2.1.2, 2.2.0, 2.2.1, 3.0, 3.0.1, 3.1, 3.2, 3.2.1, 3.3, 3.4, 3.5, 3.6, 3.7, 3.8, 3.9, 3.10, 3.11, 3.12, 3.13, 3.14, 3.15, 3.16, 3.16.1, 3.17, 3.18, 3.18.1, 3.19, 3.19.1, 3.20, 4.0, 4.1, 4.2, 4.3, 4.4, 4.5, 4.5.1, 4.6
Dependencies atom (>=1.0.7), base (>4 && <6), containers (>=0.2.0.1), directory (>=1.0.0.0), filepath (>=1.0.0.0), mtl (>=1.0.0.0), process (>=1.0.0.0), random (>=1.0.0.0) [details]
License BSD-3-Clause
Author Lee Pike, Robin Morisset, Alwyn Goodloe, Sebastian Niller
Maintainer Lee Pike <leepike@galois.com>
Category Language
Home page http://leepike.github.com/Copilot/
Uploaded by LeePike at 2010-11-13T00:20:02Z
Distributions Fedora:4.1, LTSHaskell:4.5.1, NixOS:4.1
Reverse Dependencies 7 direct, 0 indirect [details]
Downloads 29199 total (145 in the last 30 days)
Rating 2.25 (votes: 2) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]

Readme for copilot-0.26

[back to package description] 
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