diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,12 @@ * Hackage: * GitHub: -* 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 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -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) diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs --- a/Data/SBV/BitVectors/Model.hs +++ b/Data/SBV/BitVectors/Model.hs @@ -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(..)) diff --git a/Data/SBV/BitVectors/Symbolic.hs b/Data/SBV/BitVectors/Symbolic.hs --- a/Data/SBV/BitVectors/Symbolic.hs +++ b/Data/SBV/BitVectors/Symbolic.hs @@ -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) diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -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 diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -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) diff --git a/GHC/SrcLoc/Compat.hs b/GHC/SrcLoc/Compat.hs new file mode 100644 --- /dev/null +++ b/GHC/SrcLoc/Compat.hs @@ -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 diff --git a/GHC/Stack/Compat.hs b/GHC/Stack/Compat.hs new file mode 100644 --- /dev/null +++ b/GHC/Stack/Compat.hs @@ -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 diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs --- a/SBVUnitTest/SBVUnitTestBuildTime.hs +++ b/SBVUnitTest/SBVUnitTestBuildTime.hs @@ -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" diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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