copilot 3.0.1 → 3.1
raw patch · 12 files changed
+314/−91 lines, 12 filesdep +copilotdep ~copilot-c99dep ~copilot-coredep ~copilot-languagenew-component:exe:addmultnew-component:exe:arraynew-component:exe:castnew-component:exe:clocknew-component:exe:counternew-component:exe:enginenew-component:exe:heaternew-component:exe:votingnew-uploaderPVP ok
version bump matches the API change (PVP)
Dependencies added: copilot
Dependency ranges changed: copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-theorem
API changes (from Hackage documentation)
Files
- CHANGELOG +4/−0
- Examples/AddMult.hs +20/−0
- Examples/Array.hs +12/−14
- Examples/Cast.hs +29/−0
- Examples/Clock.hs +30/−0
- Examples/Counter.hs +8/−5
- Examples/Engine.hs +38/−0
- Examples/Heater.hs +1/−1
- Examples/Struct.hs +0/−45
- Examples/Voting.hs +57/−0
- README.md +48/−18
- copilot.cabal +67/−8
+ CHANGELOG view
@@ -0,0 +1,4 @@+2019-11-22 Ivan Perez <ivan.perez@nianet.org>+ * Version bump (3.1).+ * Update multiple examples (#41).+ * Update instructions to match new repositry name (#45).
+ Examples/AddMult.hs view
@@ -0,0 +1,20 @@+--------------------------------------------------------------------------------+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Another small example that calculates a constant value using a recursive+-- function.++module Main where++import Language.Copilot++spec :: Spec+spec = trigger "f" true [ arg $ mult 5 ]+ where+ mult :: Word64 -> Stream Word64+ mult 0 = 1+ mult i = constant i * mult (i-1)++main :: IO ()+main = interpret 100 spec
Examples/Array.hs view
@@ -2,18 +2,18 @@ -- Copyright © 2019 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- This is a simple example for arrays. As a program, it does not make much+-- | This is a simple example for arrays. As a program, it does not make much -- sense, however it shows of the features of arrays nicely. --- Enable compiler extension for type-level data, necesary for the array length.-{-# LANGUAGE DataKinds #-}+-- | Enable compiler extension for type-level data, necesary for the array+-- length. -module Array where+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE DataKinds #-} -import Language.Copilot-import Copilot.Compile.C99+module Main where -import Prelude hiding ((++), (>))+import Language.Copilot -- Lets define an array of length 2. -- Make the buffer of the streams 3 elements long.@@ -22,16 +22,14 @@ , array [True, True] , array [False, False]] ++ arr --- Refer to an external array.-exarr :: Stream (Array 3 Int8)-exarr = extern "exarr" Nothing-+spec :: Spec spec = do -- A trigger that fires 'func' when the first element of 'arr' is True.- -- It passes the current value of exarr as an argument.+ -- It passes the current value of arr as an argument. -- The prototype of 'func' would be: -- void func (int8_t arg[3]);- trigger "func" (arr .!! 0) [arg exarr]+ trigger "func" (arr .!! 0) [arg arr] -- Compile the spec-main = reify spec >>= compile "array"+main :: IO ()+main = interpret 30 spec
+ Examples/Cast.hs view
@@ -0,0 +1,29 @@+--------------------------------------------------------------------------------+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Examples of casting types.++{-# LANGUAGE RebindableSyntax #-}++module Main where++import Language.Copilot++b :: Stream Bool+b = [True] ++ not b++i :: Stream Int8+i = cast b++x :: Stream Word16+x = [0] ++ x + 1++y :: Stream Int32+y = 1 + cast x++spec :: Spec+spec = trigger "trigger" true [arg y, arg i]++main :: IO ()+main = interpret 30 spec
+ Examples/Clock.hs view
@@ -0,0 +1,30 @@+--------------------------------------------------------------------------------+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Example showing usage of clocks to generate periodically recurring truth+-- values.++module Main where++import Language.Copilot+import Copilot.Library.Clocks++-- | We need to force a type for the argument of `period`.+p :: Word8+p = 5++-- | Both have the same period, but a different phase.+clkStream :: Stream Bool+clkStream = clk (period p) (phase 0)++clkStream' :: Stream Bool+clkStream' = clk (period p) (phase 2)++spec :: Spec+spec = do+ observer "clk" clkStream+ observer "clk'" clkStream'++main :: IO ()+main = interpret 30 spec
Examples/Counter.hs view
@@ -1,12 +1,15 @@+--------------------------------------------------------------------------------+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Example showing an implementation of a resettable counter.+ {-# LANGUAGE RebindableSyntax #-} -module Latch where+module Main where import Language.Copilot-import Copilot.Compile.C99 -import Prelude hiding ((++), (==), mod)- -- A resettable counter counter :: Stream Bool -> Stream Bool -> Stream Int32 counter inc reset = cnt@@ -25,4 +28,4 @@ spec = trigger "counter" true [arg $ bytecounter] main :: IO ()-main = reify spec >>= compile "latch"+main = interpret 270 spec
+ Examples/Engine.hs view
@@ -0,0 +1,38 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Example implementing an engine cooling control system.++{-# LANGUAGE RebindableSyntax #-}++module Main where++import Language.Copilot+import qualified Prelude as P++{- If the majority of the engine temperature probes exeeds 250 degrees, then+ - the cooler is engaged and remains engaged until the majority of the engine+ - temperature probes drop to 250 or below. Otherwise, trigger an immediate+ - shutdown of the engine.+-}++engineMonitor :: Spec+engineMonitor = do+ trigger "shutoff" (not ok) [arg maj]++ where+ vals = [ externW8 "tmp_probe_0" two51+ , externW8 "tmp_probe_1" two51+ , externW8 "tmp_probe_2" zero]+ exceed = map (> 250) vals+ maj = majority exceed+ checkMaj = aMajority exceed maj+ ok = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler) ++ two51 = Just $ [251, 251] P.++ repeat (250 :: Word8)+ zero = Just $ repeat (0 :: Word8)+ cooler = Just $ [True, True] P.++ repeat False++main :: IO ()+main = interpret 10 engineMonitor
Examples/Heater.hs view
@@ -7,7 +7,7 @@ -- enough. It read temperature as a byte (range -50C to 100C) and translates -- this to Celcius. -module Heater where+module Main where import Language.Copilot import Copilot.Compile.C99
− Examples/Struct.hs
@@ -1,45 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2019 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- Example showing the use of structs with a vector datatype.--{-# LANGUAGE DataKinds #-}--module Struct where--import Language.Copilot-import Copilot.Compile.C99--import Prelude hiding ((>), (<), div, (++))---data Vec = Vec- { x :: Field "x" Float- , y :: Field "y" Float- }--instance Struct Vec where- typename _ = "vec" -- Name of the type in C-- -- Function to translate Vec to list of Value's, order should match struct.- toValues v = [ Value Float (x v)- , Value Float (y v)- ]---- We need to provide an instance to Typed with a bogus Vec-instance Typed Vec where- typeOf = Struct (Vec (Field 0) (Field 0))---vecs :: Stream Vec-vecs = [ Vec (Field 1) (Field 2)- , Vec (Field 12) (Field 8)- ] ++ vecs---spec = do- -- Trigger that always executes, splits the vec into seperate args.- trigger "split" true [arg $ vecs # x, arg $ vecs # y]--main = reify spec >>= compile "struct"
+ Examples/Voting.hs view
@@ -0,0 +1,57 @@+--------------------------------------------------------------------------------+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Fault-tolerant voting examples.++{-# LANGUAGE RebindableSyntax #-}++module Main where++import Language.Copilot++vote :: Spec+vote = do+ -- majority selects element with the biggest occurance.+ trigger "maj" true [arg maj]++ -- aMajority checks if the selected element has a majority.+ trigger "aMaj" true [arg $ aMajority inputs maj]++ where+ maj = majority inputs++ -- 26 input streams to vote on+ inputs :: [Stream Word32]+ inputs = [ a, b, c, d, e, f, g, h, i, j, k, l, m+ , n, o, p, q, r, s, t, u, v, w, x, y, z+ ]+ a = [0] ++ a + 1+ b = [0] ++ b + 1+ c = [0] ++ c + 1+ d = [0] ++ d + 1+ e = [1] ++ e + 1+ f = [1] ++ f + 1+ g = [1] ++ g + 1+ h = [1] ++ h + 1+ i = [1] ++ i + 1+ j = [1] ++ j + 1+ k = [1] ++ k + 1+ l = [1] ++ l + 1+ m = [1] ++ m + 1+ n = [1] ++ n + 1+ o = [1] ++ o + 1+ p = [1] ++ p + 1+ q = [1] ++ q + 1+ r = [1] ++ r + 1+ s = [1] ++ s + 1+ t = [1] ++ t + 1+ u = [1] ++ u + 1+ v = [1] ++ v + 1+ w = [1] ++ w + 1+ x = [1] ++ x + 1+ y = [1] ++ y + 1+ z = [1] ++ z + 1++main :: IO ()+main = interpret 30 vote
README.md view
@@ -13,30 +13,61 @@ realtime requirements. -## Installation-There are two ways to install Copilot:+## Using Copilot+Assuming you have GHC and cabal already installed (see [Haskell+Platform](http://hackage.haskell.org/platform/) or+[ghcup](https://www.haskell.org/ghcup/)), there are several ways to use+Copilot: -* From Hackage (recommended):+* Adding Copilot to your project - The Copilot library is cabalized. Assuming you have cabal, the GHC- compiler installed (the- [Haskell Platform](http://hackage.haskell.org/platform/) is the easiest way- to obtain these), and an Internet connection, it should merely be a matter of-running:+ Copilot is available from+ [Hackage](https://hackage.haskell.org/package/copilot). Adding `copilot`+ to your project's cabal file should be enough to get going. - ```bash- cabal install copilot- ```+* Adding Copilot to the default GHC environment -* Building from source from the GitHub repositories (typically, one would only- go this route to develop Copilot): ```bash- git clone https://github.com/Copilot-Language/Copilot.git- cd Copilot- git submodule update --init --remote- make+ cabal v2-install --lib copilot ``` + After which Copilot will be available from ghci.++* Launching a repl with Copilot++ Another quick solution is to cabal to launch a repl with Copilot+ available.++ ```bash+ cabal v2-repl --build-depends copilot+ ```++ Cabal will download and build Copilot only to make it available in the+ launched repl. The global GHC environment will not be affected.++* Building from source (typically done for development):++ ```bash+ git clone https://github.com/Copilot-Language/copilot.git+ cd copilot+ git submodule update --init --remote+ ```++ Compiling can either be done in a Nix-style build, or a traditional one:++ _Nix-Style build (Cabal >= 2.x)_++ ```bash+ cabal build # For Cabal 3.x+ cabal v2-build # For Cabal 2.x+ ```++ _Traditional build (Cabal 1.x)_+ ```bash+ cabal install --dependencies-only+ cabal build+ ```+ Note there is a TravisCI build (linked to at the top of this README) if you have trouble building/installing. @@ -137,7 +168,6 @@ * Lee Pike * Alwyn Goodloe (maintainer) * Robin Morisset-* Levent Erkők * Sebastian Niller * Nis Wegmann * Chris Hathhorn
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 3.0.1+version: 3.1 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE@@ -21,12 +21,12 @@ . Examples are available at <https://github.com/Copilot-Language/Copilot/tree/master/Examples>. -extra-source-files: +extra-source-files: README.md Examples/Heater.hs Examples/Array.hs- Examples/Struct.hs Examples/Counter.hs+ CHANGELOG source-repository head type: git@@ -45,11 +45,70 @@ , directory >= 1.3 && < 1.4 , filepath >= 1.4 && < 1.5 - , copilot-core >= 3.0.1 && < 3.1- , copilot-theorem >= 3.0 && < 3.1- , copilot-language >= 3.0.1 && < 3.1- , copilot-libraries >= 3.0 && < 3.1- , copilot-c99 >= 3.0.1 && < 3.1+ , copilot-core >= 3.1 && < 3.2+ , copilot-theorem >= 3.1 && < 3.2+ , copilot-language >= 3.1 && < 3.2+ , copilot-libraries >= 3.1 && < 3.2+ , copilot-c99 >= 3.1 && < 3.2 exposed-modules: Language.Copilot, Language.Copilot.Main+++executable addmult+ main-is: AddMult.hs+ hs-source-dirs: Examples+ build-depends: base >= 4.9 && < 5+ , copilot >= 3.1 && < 3.2+ default-language: Haskell2010++executable array+ main-is: Array.hs+ hs-source-dirs: Examples+ build-depends: base >= 4.9 && < 5+ , copilot >= 3.1 && < 3.2+ default-language: Haskell2010++executable cast+ main-is: Cast.hs+ hs-source-dirs: Examples+ build-depends: base >= 4.9 && < 5+ , copilot >= 3.1 && < 3.2+ default-language: Haskell2010++executable clock+ main-is: Clock.hs+ hs-source-dirs: Examples+ build-depends: base >= 4.9 && < 5+ , copilot >= 3.1 && < 3.2+ , copilot-libraries >= 3.1 && < 3.2+ default-language: Haskell2010++executable counter+ main-is: Counter.hs+ hs-source-dirs: Examples+ build-depends: base >= 4.9 && < 5+ , copilot >= 3.1 && < 3.2+ default-language: Haskell2010++executable engine+ main-is: Engine.hs+ hs-source-dirs: Examples+ build-depends: base >= 4.9 && < 5+ , copilot >= 3.1 && < 3.2+ default-language: Haskell2010++executable heater+ main-is: Heater.hs+ hs-source-dirs: Examples+ build-depends: base >= 4.9 && < 5+ , copilot >= 3.1 && < 3.2+ , copilot-c99 >= 3.1 && < 3.2+ default-language: Haskell2010++executable voting+ main-is: Voting.hs+ hs-source-dirs: Examples+ build-depends: base >= 4.9 && < 5+ , copilot >= 3.1 && < 3.2+ default-language: Haskell2010