diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,4 @@ +2019-11-22 Ivan Perez + * Version bump (3.1). + * Update multiple examples (#41). + * Update instructions to match new repositry name (#45). diff --git a/Examples/AddMult.hs b/Examples/AddMult.hs new file mode 100644 --- /dev/null +++ b/Examples/AddMult.hs @@ -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 diff --git a/Examples/Array.hs b/Examples/Array.hs --- a/Examples/Array.hs +++ b/Examples/Array.hs @@ -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 diff --git a/Examples/Cast.hs b/Examples/Cast.hs new file mode 100644 --- /dev/null +++ b/Examples/Cast.hs @@ -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 diff --git a/Examples/Clock.hs b/Examples/Clock.hs new file mode 100644 --- /dev/null +++ b/Examples/Clock.hs @@ -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 diff --git a/Examples/Counter.hs b/Examples/Counter.hs --- a/Examples/Counter.hs +++ b/Examples/Counter.hs @@ -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 diff --git a/Examples/Engine.hs b/Examples/Engine.hs new file mode 100644 --- /dev/null +++ b/Examples/Engine.hs @@ -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 diff --git a/Examples/Heater.hs b/Examples/Heater.hs --- a/Examples/Heater.hs +++ b/Examples/Heater.hs @@ -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 diff --git a/Examples/Struct.hs b/Examples/Struct.hs deleted file mode 100644 --- a/Examples/Struct.hs +++ /dev/null @@ -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" diff --git a/Examples/Voting.hs b/Examples/Voting.hs new file mode 100644 --- /dev/null +++ b/Examples/Voting.hs @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/copilot.cabal b/copilot.cabal --- a/copilot.cabal +++ b/copilot.cabal @@ -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 . -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