copilot-libraries 3.16 → 3.16.1

raw patch · 4 files changed

+22/−8 lines, 4 filesdep ~copilot-languagePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot-language

API changes (from Hackage documentation)

Files

CHANGELOG +6/−0
copilot-libraries.cabal +2/−2
src/Copilot/Library/PTLTL.hs +3/−5
src/Copilot/Library/Voting.hs +11/−1

CHANGELOG view

@@ -1,3 +1,9 @@+2023-09-07+        * Version bump (3.16.1). (#455)+        * Fix semantics of since in Copilot.Library.PTLTL. (#443)+        * Prevent the majority function from generating unused local variables.+          (#408)+ 2023-07-07         * Version bump (3.16). (#448)

copilot-libraries.cabal view

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-libraries-version:             3.16+version:             3.16.1 synopsis:            Libraries for the Copilot language. description:   Libraries for the Copilot language.@@ -41,7 +41,7 @@                , containers       >= 0.4 && < 0.7                , mtl              >= 2.0 && < 2.4                , parsec           >= 2.0 && < 3.2-               , copilot-language >= 3.16 && < 3.17+               , copilot-language >= 3.16.1 && < 3.17    exposed-modules:       Copilot.Library.Libraries

src/Copilot/Library/PTLTL.hs view

@@ -39,8 +39,6 @@   where     tmp = [ False ] ++ s || tmp --- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold?-since ::  Stream Bool -> Stream Bool -> Stream Bool-since s1 s2 = alwaysBeen ( tmp ==> s1 )-    where-      tmp = eventuallyPrev $ [ False ] ++ s2+-- | Is there a time when @s2@ holds and after which @s1@ continuously holds?+since :: Stream Bool -> Stream Bool -> Stream Bool+since s1 s2 = eventuallyPrev (s2 ==> (alwaysBeen s1))

src/Copilot/Library/Voting.hs view

@@ -56,7 +56,17 @@   where   inZero zero    = local (if zero then x else can) inCan     where-    inCan can'   = local (if zero || x == can then cnt+1 else cnt-1) inCnt+    inCan can' =+        -- We include a special case for when `xs` is empty that immediately+        -- returns `can'`. We could omit this special case without changing the+        -- final result, but this has the downside that `local` would bind a+        -- local variable that would go unused in `inCnt`. (Note that `inCnt`+        -- recursively invokes `majority'`, which doesn't use its last argument+        -- if the list of vote streams is empty.) These unused local variables+        -- would result in C code that triggers compiler warnings.+        case xs of+          [] -> can'+          _  -> local (if zero || x == can then cnt+1 else cnt-1) inCnt       where       inCnt cnt' = majority' xs can' cnt'