Merge branch 'master' into genKDInduction

CHANGES.md

@@ -19,6 +19,11 @@
   * [BACKWARDS COMPATIBILITY] Removed rarely used functions mapi, foldli, foldri from Data.SBV.List. These
     can now be defined by the user as we have proper support for fold and map using lambdas.
 
+  * [BACKWARDS COMPATIBILITY] Removed "Data/SBV/Tools/BoundedFix.hs", and "Data/SBV/Tools/BoundedList.hs", which
+    were relatively unused and are more or less obsolete with SBV's new support for sequences and recursive
+    functions. If you were using these functions you could easily recreate them. Please get in touch if you
+    need this old functionality.
+
 ### Version 11.0, 2024-11-06
 
   * [BACKWARDS COMPATIBILITY] SBV now handles arrays in a much more uniform way, unifying

Data/SBV/List.hs

@@ -41,11 +41,12 @@ module Data.SBV.List (
         -- * Filtering
         , filter
         -- * Other list functions
-        , all, any
+        , all, any, and, or
         ) where
 
 import Prelude hiding (head, tail, init, length, take, drop, concat, null, elem,
-                       notElem, reverse, (++), (!!), map, foldl, foldr, zip, zipWith, filter, all, any)
+                       notElem, reverse, (++), (!!), map, foldl, foldr, zip, zipWith, filter,
+                       all, any, and, or)
 import qualified Prelude as P
 
 import Data.SBV.Core.Kind
@@ -529,7 +530,7 @@ zipWith f xs ys
 
        r st = do svxs <- sbvToSV st xs
                  svys <- sbvToSV st ys
-                 lam <- lambdaStr st False kb f
+                 lam <- lambdaStr st False kc f
                  let op = SeqOp (SBVZipWith ka kb kc lam)
                  registerSpecialFunction st op
                  newExpr st kr (SBVApp op [svxs, svys])
@@ -579,6 +580,14 @@ any f l
                  registerSpecialFunction st op
                  newExpr st KBool (SBVApp op [sva])
 
+-- | Conjunction of all the elements.
+and :: SList Bool -> SBool
+and = all id
+
+-- | Disjunction of all the elements.
+or :: SList Bool -> SBool
+or = any id
+
 -- | @filter f xs@ filters the list with the given predicate.
 --
 -- >>> filter (\x -> x `sMod` 2 .== 0) [1 .. 10 :: Integer]

Data/SBV/String.hs

@@ -119,8 +119,7 @@ init s
  | True
  = subStr s 0 (length s - 1)
 
--- | @`singleton` c@ is the string of length 1 that contains the only character
--- whose value is the 8-bit value @c@.
+-- | @`singleton` c@ is the string of length 1 that contains the only character @c@.
 --
 -- >>> prove $ \c -> c .== literal 'A' .=> singleton c .== "A"
 -- Q.E.D.
@@ -141,7 +140,7 @@ singleton = lift1 StrUnit (Just wrap)
 strToStrAt :: SString -> SInteger -> SString
 strToStrAt s offset = subStr s offset 1
 
--- | @`strToCharAt` s i@ is the 8-bit value stored at location @i@. Unspecified if
+-- | @`strToCharAt` s i@ is the character stored at location @i@. Unspecified if
 -- index is out of bounds.
 --
 -- >>> prove $ \i -> i .>= 0 .&& i .<= 4 .=> "AAAAA" `strToCharAt` i .== literal 'A'

Documentation/SBV/Examples/Lists/BoundedMutex.hs

@@ -6,8 +6,7 @@
 -- Maintainer: [email protected]
 -- Stability : experimental
 --
--- Demonstrates use of bounded list utilities, proving a simple
--- mutex algorithm correct up to given bounds.
+-- Proves a simple mutex algorithm correct up to a given bound.
 -----------------------------------------------------------------------------
 
 {-# LANGUAGE DeriveAnyClass      #-}
@@ -27,8 +26,7 @@ import Data.SBV.Control
 
 import Prelude hiding ((!!))
 import Data.SBV.List ((!!))
-import qualified Data.SBV.List              as L
-import qualified Data.SBV.Tools.BoundedList as L
+import qualified Data.SBV.List as L
 
 -- | Each agent can be in one of the three states
 data State = Idle     -- ^ Regular work
@@ -38,10 +36,10 @@ data State = Idle     -- ^ Regular work
 -- | Make 'State' a symbolic enumeration
 mkSymbolicEnumeration ''State
 
--- | A bounded mutex property holds for two sequences of state transitions, if they are not in
--- their critical section at the same time up to that given bound.
-mutex :: Int -> SList State -> SList State -> SBool
-mutex i p1s p2s = L.band i $ L.bzipWith i (\p1 p2 -> p1 ./= sCritical .|| p2 ./= sCritical) p1s p2s
+-- | The mutex property holds for two sequences of state transitions, if they are not in
+-- their critical section at the same time.
+mutex :: SList State -> SList State -> SBool
+mutex p1s p2s = L.and $ L.zipWith (\p1 p2 -> p1 ./= sCritical .|| p2 ./= sCritical) p1s p2s
 
 -- | A sequence is valid upto a bound if it starts at 'Idle', and follows the mutex rules. That is:
 --
@@ -100,7 +98,7 @@ checkMutex b = runSMT $ do
 
                   -- Try to assert that mutex does not hold. If we get a
                   -- counter example, we would've found a violation!
-                  constrain $ sNot $ mutex b p1 p2
+                  constrain $ sNot $ mutex p1 p2
 
                   query $ do cs <- checkSat
                              case cs of
@@ -121,11 +119,11 @@ checkMutex b = runSMT $ do
 -- trying to show a bounded trace of length 10, such that the second process is ready but
 -- never transitions to critical. We have:
 --
--- > ghci> notFair 10
--- > Fairness is violated at bound: 10
--- > P1: [Idle,Idle,Ready,Critical,Idle,Idle,Ready,Critical,Idle,Idle]
--- > P2: [Idle,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready]
--- > Ts: [1,2,1,1,1,1,1,1,1,1]
+-- >>> notFair 10
+-- Fairness is violated at bound: 10
+-- P1: [Idle,Ready,Critical,Critical,Critical,Critical,Critical,Idle,Idle,Idle]
+-- P2: [Idle,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready]
+-- Ts: [1,1,1,1,1,1,1,1,1,1]
 --
 -- As expected, P2 gets ready but never goes critical since the arbiter keeps picking
 -- P1 unfairly. (You might get a different trace depending on what z3 happens to produce!)
@@ -148,7 +146,7 @@ notFair b = runSMT $ do p1    :: SList State   <- sList "p1"
 
                         -- Find a trace where p2 never goes critical
                         -- counter example, we would've found a violation!
-                        constrain $ sNot $ L.belem b sCritical p2
+                        constrain $ sNot $ sCritical `L.elem` p2
 
                         query $ do cs <- checkSat
                                    case cs of