sbv 5.4 → 5.5

raw patch · 10 files changed

+70/−12 lines, 10 files

Files

• CHANGES.md +6/−1
• Data/SBV.hs +3/−3
• Data/SBV/BitVectors/Model.hs +1/−1
• Data/SBV/BitVectors/Symbolic.hs +1/−1
• Data/SBV/Compilers/C.hs +2/−2
• Data/SBV/Provers/Prover.hs +2/−2
• GHC/SrcLoc/Compat.hs +26/−0
• GHC/Stack/Compat.hs +25/−0
• SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
• sbv.cabal +3/−1

@@ -1,7 +1,12 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 5.4, 2015-11-09+* Latest Hackage released version: 5.5, 2015-11-10++### Version 5.5, 2015-11-10++  * This is essentially the same release as 5.4 below, except to allow SBV compile+    with GHC 7.8 series. Thanks to Adam Foltzer for the patch.  ### Version 5.4, 2015-11-09 

@@ -492,9 +492,9 @@  {- $safeIntro -The 'sAssert' function allow users to introduce invariants through-out their code to make sure+The 'sAssert' function allows users to introduce invariants to make sure certain properties hold at all times. This is another mechanism to provide further documentation/contract info-into SBV code. The functions 'safe' and 'safeWith' can then be used to statically discharge these proof assumptions.+into SBV code. The functions 'safe' and 'safeWith' can be used to statically discharge these proof assumptions. If a violation is found, SBV will print a model showing which inputs lead to the invariant being violated.  Here's a simple example. Let's assume we have a function that does subtraction, and requires its@@ -502,7 +502,7 @@  >>> let sub x y = sAssert Nothing "sub: x >= y must hold!" (x .>= y) (x - y) -Clearly, this function is not safe, as there's nothing that ensures us to pass a larger second argument.+Clearly, this function is not safe, as there's nothing that stops us from passing it a larger second argument. We can use 'safe' to statically see if such a violation is possible before we use this function elsewhere.  >>> safe (sub :: SInt8 -> SInt8 -> SInt8)

@@ -40,7 +40,7 @@ import Control.Monad.Reader (ask) import Control.Monad.Trans  (liftIO) -import GHC.Stack+import GHC.Stack.Compat  import Data.Array      (Array, Ix, listArray, elems, bounds, rangeSize) import Data.Bits       (Bits(..))

@@ -61,7 +61,7 @@ import Data.List            (intercalate, sortBy) import Data.Maybe           (isJust, fromJust, fromMaybe) -import GHC.Stack+import GHC.Stack.Compat  import qualified Data.Generics as G    (Data(..)) import qualified Data.Typeable as T    (Typeable)

@@ -27,8 +27,8 @@ import Data.SBV.BitVectors.PrettyNum (shex, showCFloat, showCDouble) import Data.SBV.Compilers.CodeGen -import GHC.Stack-import GHC.SrcLoc+import GHC.Stack.Compat+import GHC.SrcLoc.Compat  --------------------------------------------------------------------------- -- * API

@@ -37,8 +37,8 @@ import System.Time      (getClockTime) import System.IO.Unsafe (unsafeInterleaveIO) -import GHC.Stack-import GHC.SrcLoc+import GHC.Stack.Compat+import GHC.SrcLoc.Compat  import qualified Data.Set as Set (Set, toList) 

@@ -0,0 +1,26 @@+{-# LANGUAGE CPP #-}++-- | Compatibility shim for GHC 7.8 support. Remove once 7.8 is no+-- longer supported.++#if MIN_VERSION_base(4,8,0)++module GHC.SrcLoc.Compat (module GHC.SrcLoc) where+import GHC.SrcLoc++#else++module GHC.SrcLoc.Compat {-# WARNING "This version of GHC does not support SrcLoc; using a stub interface for compatibility" #-} (module GHC.SrcLoc.Compat) where++data SrcLoc++srcLocFile :: SrcLoc -> String+srcLocFile _ = ""++srcLocStartLine :: SrcLoc -> Int+srcLocStartLine _ = 0++srcLocStartCol :: SrcLoc -> Int+srcLocStartCol _ = 0++#endif

@@ -0,0 +1,25 @@+{-# LANGUAGE CPP #-}++-- | Compatibility shim for GHC 7.8 support. Remove once 7.8 is no+-- longer supported.++#if MIN_VERSION_base(4,8,0)++module GHC.Stack.Compat (module GHC.Stack) where+import GHC.Stack++#else++module GHC.Stack.Compat {-# WARNING "This version of GHC does not support SrcLoc; using a stub interface for compatibility" #-} (module GHC.Stack.Compat) where++import GHC.SrcLoc.Compat++data CallStack++getCallStack :: CallStack -> [(String, SrcLoc)]+getCallStack _ = []++showCallStack :: CallStack -> String+showCallStack _ = "CallStack not supported in GHC older than 7.10"++#endif

@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where  buildTime :: String-buildTime = "Mon Nov  9 17:48:14 PST 2015"+buildTime = "Tue Nov 10 17:02:49 PST 2015"

@@ -1,5 +1,5 @@ Name:          sbv-Version:       5.4+Version:       5.5 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis:      SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description:   Express properties about Haskell programs and automatically prove them using SMT@@ -131,6 +131,8 @@                   , Data.SBV.Utils.Numeric                   , Data.SBV.Utils.TDiff                   , Data.SBV.Utils.Lib+                  , GHC.SrcLoc.Compat+                  , GHC.Stack.Compat  Executable SBVUnitTests   default-language: Haskell2010