copilot-language 3.17 → 3.18

raw patch · 5 files changed

+23/−7 lines, 5 filesdep ~copilot-coredep ~copilot-interpreterdep ~copilot-theorem

Dependency ranges changed: copilot-core, copilot-interpreter, copilot-theorem

Files

• CHANGELOG +5/−0
• copilot-language.cabal +4/−4
• src/Copilot/Language.hs +1/−0
• src/Copilot/Language/Spec.hs +7/−1
• tests/Test/Copilot/Language/Reify.hs +6/−2

@@ -1,3 +1,8 @@+2024-01-07+        * Version bump (3.18). (#487)+        * Add type annotation to help type inference engine. (#469)+        * Rename forall to forAll. (#470)+ 2023-11-07         * Version bump (3.17). (#466) 

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-language-version:             3.17+version:             3.18 synopsis:            A Haskell-embedded DSL for monitoring hard real-time                      distributed systems. description:@@ -42,9 +42,9 @@                , data-reify            >= 0.6 && < 0.7                , mtl                   >= 2.0 && < 3 -               , copilot-core          >= 3.17 && < 3.18-               , copilot-interpreter   >= 3.17 && < 3.18-               , copilot-theorem       >= 3.17 && < 3.18+               , copilot-core          >= 3.18 && < 3.19+               , copilot-interpreter   >= 3.18 && < 3.19+               , copilot-theorem       >= 3.18 && < 3.19    exposed-modules: Copilot.Language                  , Copilot.Language.Operators.BitWise

@@ -37,6 +37,7 @@   , arg   , prop   , theorem+  , forAll   , forall, exists   ) where 

@@ -27,6 +27,7 @@   , Prop (..)   , prop, properties   , theorem, theorems+  , forAll   , forall, exists   , extractProp   , Universal, Existential@@ -161,8 +162,13 @@   Exists :: Stream Bool -> Prop Existential  -- | Universal quantification of boolean streams over time.+forAll :: Stream Bool -> Prop Universal+forAll = Forall++{-# DEPRECATED forall "Use forAll instead." #-}+-- | Universal quantification of boolean streams over time. forall :: Stream Bool -> Prop Universal-forall = Forall+forall = forAll  -- | Existential quantification of boolean streams over time. exists :: Stream Bool -> Prop Existential

@@ -31,7 +31,7 @@ import qualified Copilot.Language.Operators.Mux      as Copilot import qualified Copilot.Language.Operators.Ord      as Copilot import           Copilot.Language.Reify              (reify)-import           Copilot.Language.Spec               (observer)+import           Copilot.Language.Spec               (Spec, observer) import           Copilot.Language.Stream             (Stream) import qualified Copilot.Language.Stream             as Copilot @@ -732,7 +732,11 @@ checkSemanticsP :: Int -> [a] -> SemanticsP -> IO Bool checkSemanticsP steps _streams (SemanticsP (expr, exprList)) = do     -- Spec with just one observer of one expression.-    let spec = observer testObserverName expr+    --+    -- Because SemanticsP is an existential type, we need to help GHC figure+    -- out the type of spec.+    let spec :: Spec+        spec = observer testObserverName expr      -- Reified stream (low-level)     llSpec <- reify spec