Revert "Remove Eq SBV instance. Fixes half of #241."

This reverts commit 5958276.

Author: LeventErkok

Data/SBV/Control/Query.hs

@@ -640,7 +640,7 @@ infix 1 |->
 (|->) :: SymWord a => SBV a -> a -> Assignment
 SBV a |-> v = case literal v of
                 SBV (SVal _ (Left cw)) -> Assign a cw
-                _                      -> error "Data.SBV: Impossible happened in |->: Cannot construct a CW with a symbolic value!"
+                r                      -> error $ "Data.SBV: Impossible happened in |->: Cannot construct a CW with literal: " ++ show r
 
 -- | Produce the query result from an assignment.
 mkSMTResult :: [Assignment] -> Query SMTResult

Data/SBV/Core/Data.hs

@@ -208,12 +208,9 @@ sRTN = sRoundTowardNegative
 sRTZ :: SRoundingMode
 sRTZ = sRoundTowardZero
 
--- | Show a symbolic value. Not particularly "desirable," since we can't
--- really show symbolic values, but will do if needed for test purposes.
--- Note that we don't make this a show instance on purpose to make sure we
--- keep it under control and not let it be visible to the end users
-showSBV :: SBV a -> String
-showSBV (SBV sv) = show sv
+-- Not particularly "desirable", but will do if needed
+instance Show (SBV a) where
+  show (SBV sv) = show sv
 
 -- Equality constraint on SBV values. Not desirable since we can't really compare two
 -- symbolic values, but will do.
@@ -458,8 +455,8 @@ declNewSArray mkNm = do
 -- | Declare a new functional symbolic array. Note that a read from an uninitialized cell will result in an error.
 declNewSFunArray :: forall a b. (HasKind a, HasKind b) => Maybe String -> Symbolic (SFunArray a b)
 declNewSFunArray mbNm = return $ SFunArray $ error . msg mbNm
-  where msg Nothing   i = "Reading from an uninitialized array entry, index: " ++ showSBV i
-        msg (Just nm) i = "Array " ++ show nm ++ ": Reading from an uninitialized array entry, index: " ++ showSBV i
+  where msg Nothing   i = "Reading from an uninitialized array entry, index: " ++ show i
+        msg (Just nm) i = "Array " ++ show nm ++ ": Reading from an uninitialized array entry, index: " ++ show i
 
 -- | Arrays implemented internally as functions
 --

Data/SBV/Core/Model.hs

@@ -49,7 +49,7 @@ import GHC.Stack
 import Data.Array      (Array, Ix, listArray, elems, bounds, rangeSize)
 import Data.Bits       (Bits(..))
 import Data.Int        (Int8, Int16, Int32, Int64)
-import Data.List       (genericLength, genericIndex, genericTake, unzip4, unzip5, unzip6, unzip7)
+import Data.List       (genericLength, genericIndex, genericTake, unzip4, unzip5, unzip6, unzip7, intercalate)
 import Data.Maybe      (fromMaybe)
 import Data.Word       (Word8, Word16, Word32, Word64)
 
@@ -630,7 +630,7 @@ pbToInteger :: String -> Int -> SBool -> Integer
 pbToInteger w c b
  | c < 0                 = error $ "SBV." ++ w ++ ": Non-negative coefficient required, received: " ++ show c
  | Just v <- unliteral b = if v then fromIntegral c else 0
- | True                  = error $ "SBV.pbToInteger: Received a symbolic boolean at coefficient " ++ show c
+ | True                  = error $ "SBV.pbToInteger: Received a symbolic boolean: " ++ show (c, b)
 
 -- | Predicate for optimizing word operations like (+) and (*).
 isConcreteZero :: SBV a -> Bool
@@ -761,13 +761,13 @@ instance (Num a, Bits a, SymWord a) => Bits (SBV a) where
     | SBV (SVal _ (Left (CW _ (CWInteger n)))) <- x
     = testBit n i
     | True
-    = error "SBV.testBit: Called on symbolic value! Use sTestBit instead."
+    = error $ "SBV.testBit: Called on symbolic value: " ++ show x ++ ". Use sTestBit instead."
   -- NB. popCount is *not* implementable on non-concrete symbolic words
   popCount x
     | SBV (SVal _ (Left (CW (KBounded _ w) (CWInteger n)))) <- x
     = popCount (n .&. (bit w - 1))
     | True
-    = error "SBV.popCount: Called on symbolic value! Use sPopCount instead."
+    = error $ "SBV.popCount: Called on symbolic value: " ++ show x ++ ". Use sPopCount instead."
 
 -- | Replacement for 'testBit'. Since 'testBit' requires a 'Bool' to be returned,
 -- we cannot implement it for symbolic words. Index 0 is the least-significant bit.
@@ -1000,7 +1000,7 @@ instance (Show a, Bounded a, Integral a, Num a, SymWord a) => Enum (SBV a) where
 -- | Helper function for use in enum operations
 enumCvt :: (SymWord a, Integral a, Num b) => String -> SBV a -> b
 enumCvt w x = case unliteral x of
-                Nothing -> error $ "Enum." ++ w ++ "{" ++ showType x ++ "}: Called on symbolic value!"
+                Nothing -> error $ "Enum." ++ w ++ "{" ++ showType x ++ "}: Called on symbolic value " ++ show x
                 Just v  -> fromIntegral v
 
 -- | The 'SDivisible' class captures the essence of division.
@@ -1757,7 +1757,7 @@ instance Metric SReal    where minimize nm o = addSValOptGoal (unSBV `fmap` Mini
 -- Quickcheck interface on symbolic-booleans..
 instance Testable SBool where
   property (SBV (SVal _ (Left b))) = property (cwToBool b)
-  property _                       = error "Cannot quick-check in the presence of uninterpreted constants!"
+  property s                       = error $ "Cannot quick-check in the presence of uninterpreted constants! (" ++ show s ++ ")"
 
 instance Testable (Symbolic SBool) where
    property prop = QC.monadicIO $ do (cond, r, tvals) <- QC.run test
@@ -1771,13 +1771,13 @@ instance Testable (Symbolic SBool) where
 
                      case map fst unints of
                        [] -> case unliteral r of
-                               Nothing -> noQC
+                               Nothing -> noQC [show r]
                                Just b  -> return (cond, b, tvals)
-                       _  -> noQC
+                       us -> noQC us
 
            complain qcInfo = showModel defaultSMTCfg (SMTModel [] qcInfo)
 
-           noQC = error "Cannot quick-check in the presence of uninterpreted constants!"
+           noQC us         = error $ "Cannot quick-check in the presence of uninterpreted constants: " ++ intercalate ", " us
 
 -- | Quick check an SBV property. Note that a regular 'quickCheck' call will work just as
 -- well. Use this variant if you want to receive the boolean result.

Data/SBV/Core/Symbolic.hs

@@ -596,8 +596,7 @@ instance Show SVal where
   show (SVal k     (Right _)) =         "<symbolic> :: " ++ show k
 
 -- | Equality constraint on SBV values. Not desirable since we can't really compare two
--- symbolic values, but will do. The only reason we have this is because we want
--- Bits instance for SBV, which has an Eq super-class.
+-- symbolic values, but will do.
 instance Eq SVal where
   SVal _ (Left a) == SVal _ (Left b) = a == b
   a == b = error $ "Comparing symbolic bit-vectors; Use (.==) instead. Received: " ++ show (a, b)

Data/SBV/Examples/Crypto/AES.hs

@@ -112,14 +112,14 @@ toBytes x = [x1, x2, x3, x4]
 -- Q.E.D.
 fromBytes :: [GF28] -> SWord32
 fromBytes [x1, x2, x3, x4] = (x1 # x2) # (x3 # x4)
-fromBytes xs               = error $ "fromBytes: Unexpected (/= 4) input length: " ++ show (length xs)
+fromBytes xs               = error $ "fromBytes: Unexpected input: " ++ show xs
 
 -- | Rotating a state row by a fixed amount to the right.
 rotR :: [GF28] -> Int -> [GF28]
 rotR [a, b, c, d] 1 = [d, a, b, c]
 rotR [a, b, c, d] 2 = [c, d, a, b]
 rotR [a, b, c, d] 3 = [b, c, d, a]
-rotR xs           i = error $ "rotR: Unexpected input: " ++ show (length xs, i)
+rotR xs           i = error $ "rotR: Unexpected input: " ++ show (xs, i)
 
 -----------------------------------------------------------------------------
 -- ** The key schedule

Data/SBV/Examples/Puzzles/MagicSquare.hs

@@ -66,11 +66,7 @@ magic n
           | True
           = do putStrLn $ "Solution #" ++ show i
                mapM_ printRow board
-               let good = case unliteral (isMagic sboard) of
-                            Just False -> "False"
-                            Just True  -> "True"
-                            Nothing    -> "Symbolic!"
-               putStrLn $ "Valid Check: " ++ good
+               putStrLn $ "Valid Check: " ++ show (isMagic sboard)
                putStrLn "Done."
           where lmod  = length model
                 board = chunk n model

Data/SBV/Examples/Puzzles/NQueens.hs

@@ -42,11 +42,5 @@ nQueens n
          dispSolution model
            | lmod /= n = error $ "Impossible! Backend solver returned " ++ show lmod ++ " values, was expecting: " ++ show n
            | True      = do putStr $ show model
-                            let v = isValid n (map literal model)
-                            case unliteral v of
-                              Just True  -> putStrLn " (Valid: True)"
-                              Just False -> do putStrLn " (Valid: False)"
-                                               error $ "Failed to solve!"
-                              Nothing    -> do putStrLn " (Valid: Symbolic!)"
-                                               error $ "Failed to solve!"
+                            putStrLn $ " (Valid: " ++ show (isValid n (map literal model)) ++ ")"
            where lmod  = length model

Data/SBV/Examples/Puzzles/Sudoku.hs

@@ -64,11 +64,7 @@ dispSolution (i, f) (_, fs)
   | lmod /= i = error $ "Impossible! Backend solver returned " ++ show lmod ++ " values, was expecting: " ++ show i
   | True      = do putStrLn "Final board:"
                    mapM_ printRow final
-                   let res = case unliteral (valid final) of
-                                Nothing    -> "Symbolic!"
-                                Just False -> "Failed!"
-                                Just True  -> "True"
-                   putStrLn $ "Valid Check: " ++ res
+                   putStrLn $ "Valid Check: " ++ show (valid final)
                    putStrLn "Done."
   where lmod = length fs
         final = f (map literal fs)

Data/SBV/Tools/Polynomial.hs

@@ -95,7 +95,7 @@ liftC f x y = let (a, b) = f (literal x) (literal y) in (fromJust (unliteral a),
 liftS :: SymWord a => (a -> String) -> SBV a -> String
 liftS f s
   | Just x <- unliteral s = f x
-  | True                  = "<symbolic>"
+  | True                  = show s
 
 -- | Pretty print as a polynomial
 sp :: Bits a => Bool -> a -> String
@@ -137,9 +137,9 @@ ites s xs ys
 polyMult :: (Num a, Bits a, SymWord a, FromBits (SBV a)) => (SBV a, SBV a, [Int]) -> SBV a
 polyMult (x, y, red)
   | isReal x
-  = error $ "SBV.polyMult: Received a real value: " ++ show (unSBV x)
+  = error $ "SBV.polyMult: Received a real value: " ++ show x
   | not (isBounded x)
-  = error $ "SBV.polyMult: Received infinite precision value: " ++ show (unSBV x)
+  = error $ "SBV.polyMult: Received infinite precision value: " ++ show x
   | True
   = fromBitsLE $ genericTake sz $ r ++ repeat false
   where (_, r) = mdp ms rs
@@ -152,9 +152,9 @@ polyMult (x, y, red)
 polyDivMod :: (Num a, Bits a, SymWord a, FromBits (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
 polyDivMod x y
    | isReal x
-   = error $ "SBV.polyDivMod: Received a real value: " ++ show (unSBV x)
+   = error $ "SBV.polyDivMod: Received a real value: " ++ show x
    | not (isBounded x)
-   = error $ "SBV.polyDivMod: Received infinite precision value: " ++ show (unSBV x)
+   = error $ "SBV.polyDivMod: Received infinite precision value: " ++ show x
    | True
    = ite (y .== 0) (0, x) (adjust d, adjust r)
    where adjust xs = fromBitsLE $ genericTake sz $ xs ++ repeat false
@@ -243,9 +243,9 @@ crcBV n m p = take n $ go (replicate n false) (m ++ replicate n false)
 crc :: (FromBits (SBV a), FromBits (SBV b), Num a, Num b, Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b
 crc n m p
   | isReal m || isReal p
-  = error $ "SBV.crc: Received a real value: " ++ show (unSBV m, unSBV p)
+  = error $ "SBV.crc: Received a real value: " ++ show (m, p)
   | not (isBounded m) || not (isBounded p)
-  = error $ "SBV.crc: Received an infinite precision value: " ++ show (unSBV m, unSBV p)
+  = error $ "SBV.crc: Received an infinite precision value: " ++ show (m, p)
   | True
   = fromBitsBE $ replicate (sz - n) false ++ crcBV n (blastBE m) (blastBE p)
   where sz = intSizeOf p

Data/SBV/Tools/STree.hs

@@ -47,15 +47,15 @@ readSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV
 readSTree s i = walk (blastBE i) s
   where walk []     (SLeaf v)  = v
         walk (b:bs) (SBin l r) = ite b (walk bs r) (walk bs l)
-        walk bs     _          = error $ "SBV.STree.readSTree: Impossible happened! Length: " ++ show (length bs)
+        walk _      _          = error $ "SBV.STree.readSTree: Impossible happened while reading: " ++ show i
 
 -- | Writing a value, similar to how reads are done. The important thing is that the tree
 -- representation keeps updates to a minimum.
 writeSTree :: (Mergeable (SBV e), Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e
 writeSTree s i j = walk (blastBE i) s
   where walk []     _          = SLeaf j
         walk (b:bs) (SBin l r) = SBin (ite b l (walk bs l)) (ite b (walk bs r) r)
-        walk bs     _          = error $ "SBV.STree.writeSTree: Impossible happened! Length: " ++ show (length bs)
+        walk _      _          = error $ "SBV.STree.writeSTree: Impossible happened while reading: " ++ show i
 
 -- | Construct the fully balanced initial tree using the given values.
 mkSTree :: forall i e. HasKind i => [SBV e] -> STree i e

Data/SBV/Utils/PrettyNum.hs

@@ -100,10 +100,10 @@ instance PrettyNum CW where
          | True               = let CWInteger w = cwVal cw in sbin  False False (hasSign cw, intSizeOf cw) w
 
 instance (SymWord a, PrettyNum a) => PrettyNum (SBV a) where
-  hexS s = maybe "<symbolic>" (hexS :: a -> String) $ unliteral s
-  binS s = maybe "<symbolic>" (binS :: a -> String) $ unliteral s
-  hex  s = maybe "<symbolic>" (hex  :: a -> String) $ unliteral s
-  bin  s = maybe "<symbolic>" (bin  :: a -> String) $ unliteral s
+  hexS s = maybe (show s) (hexS :: a -> String) $ unliteral s
+  binS s = maybe (show s) (binS :: a -> String) $ unliteral s
+  hex  s = maybe (show s) (hex  :: a -> String) $ unliteral s
+  bin  s = maybe (show s) (bin  :: a -> String) $ unliteral s
 
 -- | Show as a hexadecimal value. First bool controls whether type info is printed
 -- while the second boolean controls wether 0x prefix is printed. The tuple is