copilot-language 4.0 → 4.1

raw patch · 3 files changed

+34/−16 lines, 3 filesdep ~copilot-coredep ~copilot-interpreterdep ~copilot-theoremPVP ok

version bump matches the API change (PVP)

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

API changes (from Hackage documentation)

Files

• CHANGELOG +13/−8
• copilot-language.cabal +4/−4
• src/Copilot/Language/Analyze.hs +17/−4

@@ -1,3 +1,8 @@+2024-11-07+        * Version bump (4.1). (#561)+        * Reject duplicate externs in properties and theorems. (#536)+        * Standardize changelog format. (#550)+ 2024-09-07         * Version bump (4.0). (#532)         * Add support for array updates. (#36)@@ -108,12 +113,12 @@         * Completed the documentation. (#112)  2020-05-07-        * Version bump (3.2).-        * Fixed the reverse order of triggers (#114).-        * Update description, bug-reports, changelog fields in cabal file-          (#116).-        * Bump ghc-prim version bounds (#122).+        * Version bump (3.2). (#65)+        * Fixed the reverse order of triggers. (#114)+        * Update description, bug-reports, changelog fields in cabal file.+          (#116)+        * Bump ghc-prim version bounds. (#122) -2019-11-22 Ivan Perez <ivan.perez@nianet.org>-        * Version bump (3.1).-        * Remove ExternFun (#118).+2019-11-22+        * Version bump (3.1). (#46)+        * Remove ExternFun. (#118)

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-language-version:             4.0+version:             4.1 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          >= 4.0 && < 4.1-               , copilot-interpreter   >= 4.0 && < 4.1-               , copilot-theorem       >= 4.0 && < 4.1+               , copilot-core          >= 4.1 && < 4.2+               , copilot-interpreter   >= 4.1 && < 4.2+               , copilot-theorem       >= 4.1 && < 4.2    exposed-modules: Copilot.Language                  , Copilot.Language.Operators.BitWise

@@ -17,6 +17,7 @@ import Copilot.Language.Stream (Stream (..)) import Copilot.Language.Spec import Copilot.Language.Error (badUsage)+import Copilot.Theorem.Prove (UProof)  import Data.List (groupBy) import Data.IORef@@ -268,10 +269,16 @@ -- | Obtain all the externs in a specification. specExts :: IORef Env -> Spec' a -> IO ExternEnv specExts refStreams spec = do-  env <- foldM triggerExts-           (ExternEnv [] [] [] [])-           (triggers $ runSpec spec)-  foldM observerExts env (observers $ runSpec spec)+  env0 <- foldM triggerExts+            (ExternEnv [] [] [] [])+            (triggers $ runSpec spec)+  env1 <- foldM observerExts+            env0+            (observers $ runSpec spec)+  env2 <- foldM propertyExts+            env1+            (properties $ runSpec spec)+  foldM theoremExts env2 (theorems $ runSpec spec)    where   observerExts :: ExternEnv -> Observer -> IO ExternEnv@@ -282,6 +289,12 @@     env' <- collectExts refStreams guard env     foldM (\env'' (Arg arg_) -> collectExts refStreams arg_ env'')           env' args++  propertyExts :: ExternEnv -> Property -> IO ExternEnv+  propertyExts env (Property _ stream) = collectExts refStreams stream env++  theoremExts :: ExternEnv -> (Property, UProof) -> IO ExternEnv+  theoremExts env (p, _) = propertyExts env p  -- | Obtain all the externs in a stream. collectExts :: C.Typed a => IORef Env -> Stream a -> ExternEnv -> IO ExternEnv