copilot 3.8 → 3.9
raw patch · 16 files changed
+32/−65 lines, 16 filesdep ~copilot-c99dep ~copilot-coredep ~copilot-languagePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-theorem
API changes (from Hackage documentation)
Files
- CHANGELOG +5/−0
- copilot.cabal +6/−6
- examples/AddMult.hs +0/−2
- examples/Array.hs +1/−3
- examples/Cast.hs +0/−2
- examples/Clock.hs +0/−2
- examples/Counter.hs +3/−4
- examples/Engine.hs +5/−8
- examples/Heater.hs +0/−2
- examples/Structs.hs +0/−2
- examples/Voting.hs +0/−2
- examples/WCV.hs +1/−17
- examples/what4/Arithmetic.hs +0/−1
- examples/what4/Propositional.hs +0/−1
- examples/what4/Structs.hs +0/−2
- src/Language/Copilot/Main.hs +11/−11
CHANGELOG view
@@ -1,3 +1,8 @@+2022-05-06+ * Version bump (3.9). (#320)+ * Compliance with style guide (partial). (#316)+ * Add support for GHC 9.0. (#294)+ 2022-03-07 * Version bump (3.8). (#298) * Mark package as uncurated to avoid modification. (#288)
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 3.8+version: 3.9 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE@@ -52,11 +52,11 @@ , directory >= 1.3 && < 1.4 , filepath >= 1.4 && < 1.5 - , copilot-core >= 3.8 && < 3.9- , copilot-theorem >= 3.8 && < 3.9- , copilot-language >= 3.8 && < 3.9- , copilot-libraries >= 3.8 && < 3.9- , copilot-c99 >= 3.8 && < 3.9+ , copilot-core >= 3.9 && < 3.10+ , copilot-theorem >= 3.9 && < 3.10+ , copilot-language >= 3.9 && < 3.10+ , copilot-libraries >= 3.9 && < 3.10+ , copilot-c99 >= 3.9 && < 3.10 exposed-modules: Language.Copilot, Language.Copilot.Main
examples/AddMult.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Another small example that calculates a constant value using a recursive -- function.
examples/Array.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | 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.@@ -8,8 +6,8 @@ -- | Enable compiler extension for type-level data, necesary for the array -- length. -{-# LANGUAGE RebindableSyntax #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE RebindableSyntax #-} module Main where
examples/Cast.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Examples of casting types.
examples/Clock.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Example showing usage of clocks to generate periodically recurring truth -- values.
examples/Counter.hs view
@@ -1,6 +1,4 @@-------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Example showing an implementation of a resettable counter. @@ -22,8 +20,9 @@ -- Counter that resets when it reaches 256 bytecounter :: Stream Int32-bytecounter = counter true reset where- reset = counter true false `mod` 256 == 0+bytecounter = counter true reset+ where+ reset = counter true false `mod` 256 == 0 spec :: Spec spec = trigger "counter" true [arg $ bytecounter]
examples/Engine.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Example implementing an engine cooling control system. @@ -11,11 +9,10 @@ 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.--}+-- 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@@ -28,7 +25,7 @@ exceed = map (> 250) vals maj = majority exceed checkMaj = aMajority exceed maj- ok = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler) + ok = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler) two51 = Just $ [251, 251] P.++ repeat (250 :: Word8) zero = Just $ repeat (0 :: Word8)
examples/Heater.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- This is a simple example with basic usage. It implements a simple home -- heating system: It heats when temp gets too low, and stops when it is high
examples/Structs.hs view
@@ -11,7 +11,6 @@ import Language.Copilot import Copilot.Compile.C99 - -- | Definition for `Volts`. data Volts = Volts { numVolts :: Field "numVolts" Word16@@ -65,7 +64,6 @@ trigger "equalityDifferentIndices" ((((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)) [arg battery]- main :: IO () main = do
examples/Voting.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Fault-tolerant voting examples.
examples/WCV.hs view
@@ -3,7 +3,7 @@ -- Well-Clear Bounday Models for the Integration of UAS in the NAS', -- https://ntrs.nasa.gov/citations/20140010078. -{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE RebindableSyntax #-} module Main where@@ -14,7 +14,6 @@ import Data.Foldable (forM_) import qualified Control.Monad as Monad - -- | `dthr` is the horizontal distance threshold. dthr :: Stream Double dthr = extern "dthr" Nothing@@ -33,10 +32,7 @@ type Vect2 = (Stream Double, Stream Double) ---------------------------------- -- External streams for relative position and velocity.--------------------------------- -- | The relative x velocity between ownship and the intruder. vx :: Stream Double@@ -54,7 +50,6 @@ v :: (Stream Double, Stream Double) v = (vx, vy) - -- | The relative x position between ownship and the intruder. sx :: Stream Double sx = extern "relative_position_x" Nothing@@ -71,10 +66,7 @@ s :: (Stream Double, Stream Double) s = (sx, sy) -------------------- -- The following section contains basic libraries for working with vectors.------------------- -- | Multiply two Vectors. (|*|) :: Vect2 -> Vect2 -> Stream Double@@ -101,11 +93,8 @@ neg :: Vect2 -> Vect2 neg (x, y) = (negate x, negate y) ---------------------- -- From here on the algorithm, as described by the paper mentioned on the top -- of this file, is implemented. Please refer to the paper for details.--------------------- tau :: Vect2 -> Vect2 -> Stream Double tau s v = if s |*| v < 0@@ -134,7 +123,6 @@ theta :: Vect2 -> Vect2 -> Stream Double -> Stream Double -> Stream Double theta s v d e = (-(s |*| v) + e * (sqrt $ delta s v d)) / (sq v) - tcoa :: Stream Double -> Stream Double -> Stream Double tcoa sz vz = if (sz * vz) < 0 then (-sz) / vz@@ -143,10 +131,7 @@ dcpa :: Vect2 -> Vect2 -> Stream Double dcpa s@(sx, sy) v@(vx, vy) = norm (sx + (tcpa s v) * vx, sy + (tcpa s v) * vy) ---------------------------- -- Well clear Violation ----------------------------- -- | Determines if the well clear property is violated or not. wcv :: (Vect2 -> Vect2 -> Stream Double) ->@@ -168,7 +153,6 @@ spec = do Monad.void $ prop "1a" (forall $ (tau s v) ~= (tau (neg s) (neg v))) -- Monad.void $ prop "3d" (forall $ (wcv tep s sz v vz) == (wcv tep (neg s) (-sz) (neg v) (-vz)))- main :: IO () main = do
examples/what4/Arithmetic.hs view
@@ -38,7 +38,6 @@ -- Another example with floats. This fails, because it isn't true. void $ prop "Example 6" (forall ((efloat + 1) /= efloat)) - main :: IO () main = do spec' <- reify spec
examples/what4/Propositional.hs view
@@ -46,7 +46,6 @@ let a = extern "a" Nothing void $ prop "Example 7" (forall (a || not a)) - main :: IO () main = do spec' <- reify spec
examples/what4/Structs.hs view
@@ -12,7 +12,6 @@ import Language.Copilot import Copilot.Theorem.What4 - -- | Definition for `Volts`. data Volts = Volts { numVolts :: Field "numVolts" Word16@@ -64,7 +63,6 @@ -- false). void $ prop "Example 2" $ forall $ (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)- main :: IO () main = do
src/Language/Copilot/Main.hs view
@@ -44,7 +44,6 @@ <> metavar "INT" <> showDefault <> help "Interpret specification and write result to output") - -- | Create a main to either compile or interpret a copilot specification. -- -- This function must be provided an auxiliary function capable of compiling@@ -63,18 +62,19 @@ -- * @--interpret/-i NUM@: interpret the specification for a given number -- of steps. copilotMain :: Interpreter -> Printer -> Compiler -> Spec -> IO ()-copilotMain interp pretty comp spec = main =<< execParser opts where- opts = info (cmdargs <**> helper) fullDesc+copilotMain interp pretty comp spec = main =<< execParser opts+ where+ opts = info (cmdargs <**> helper) fullDesc - main :: CmdArgs -> IO ()- main args = do- let iters = ainterpret args- when (apretty args) $ pretty spec- when (iters Prelude.> 0) $ interp (fromIntegral iters) spec+ main :: CmdArgs -> IO ()+ main args = do+ let iters = ainterpret args+ when (apretty args) $ pretty spec+ when (iters Prelude.> 0) $ interp (fromIntegral iters) spec - when (not $ acompile args) $ do- spec' <- reify spec- comp (aoutput args) spec'+ when (not $ acompile args) $ do+ spec' <- reify spec+ comp (aoutput args) spec' -- | Create a main function with a default interpreter and pretty printer. --