Fix expected printout after printing changes

Data/SBV.hs

@@ -19,7 +19,7 @@
 --
 -- >>> prove $ \x -> x `shiftL` 2 .== 2 * (x :: SWord8)
 -- Falsifiable. Counter-example:
---   s0 = 32 :: SWord8
+--   s0 = 32 :: Word8
 --
 -- The function 'prove' has the following type:
 --
@@ -609,15 +609,15 @@ If we try to prove a theorem regarding sub, we'll get an exception:
 
 >>> prove $ \x y -> sub x y .>= (0 :: SInt16)
 *** Exception: Assertion failure: "sub: x >= y must hold!"
-  s0 = -32768 :: SInt16
-  s1 = -32767 :: SInt16
+  s0 = -32768 :: Int16
+  s1 = -32767 :: Int16
 
 Of course, we can use, 'safe' to statically see if such a violation is possible before we attempt a proof:
 
 >>> safe (sub :: SInt8 -> SInt8 -> SInt8)
 Assertion failure: "sub: x >= y must hold!"
-  s0 = -128 :: SInt8
-  s1 = -127 :: SInt8
+  s0 = -128 :: Int8
+  s1 = -127 :: Int8
 
 What happens if we make sure to arrange for this invariant? Consider this version:
 

Data/SBV/Examples/BitPrecise/PrefixSum.hs

@@ -100,14 +100,14 @@ thm2 = prove $ flIsCorrect 16 (0, smax)
 --
 -- >>> thm3
 -- Falsifiable. Counter-example:
---   s0 = 0 :: SWord32
---   s1 = 0 :: SWord32
---   s2 = 0 :: SWord32
---   s3 = 0 :: SWord32
---   s4 = 1073741824 :: SWord32
---   s5 = 0 :: SWord32
---   s6 = 0 :: SWord32
---   s7 = 0 :: SWord32
+--   s0 = 0 :: Word32
+--   s1 = 0 :: Word32
+--   s2 = 0 :: Word32
+--   s3 = 0 :: Word32
+--   s4 = 1073741824 :: Word32
+--   s5 = 0 :: Word32
+--   s6 = 0 :: Word32
+--   s7 = 0 :: Word32
 --   -- uninterpreted: u
 --        u  = 0
 --   -- uninterpreted: flOp

Data/SBV/Examples/Misc/Floating.hs

@@ -28,9 +28,9 @@ import Data.SBV
 --
 -- >>> prove assocPlus
 -- Falsifiable. Counter-example:
---   s0 = -9.62965e-35 :: SFloat
---   s1 = Infinity :: SFloat
---   s2 = -Infinity :: SFloat
+--   s0 = -9.62965e-35 :: Float
+--   s1 = Infinity :: Float
+--   s2 = -Infinity :: Float
 --
 -- Indeed:
 --
@@ -56,9 +56,9 @@ assocPlus x y z = x + (y + z) .== (x + y) + z
 --
 -- >>> assocPlusRegular
 -- Falsifiable. Counter-example:
---   x = -1.0491915e7 :: SFloat
---   y = 1967115.5 :: SFloat
---   z = 982003.94 :: SFloat
+--   x = -1.0491915e7 :: Float
+--   y = 1967115.5 :: Float
+--   z = 982003.94 :: Float
 --
 -- Indeed, we have:
 --
@@ -87,8 +87,8 @@ assocPlusRegular = prove $ do [x, y, z] <- sFloats ["x", "y", "z"]
 --
 -- >>> nonZeroAddition
 -- Falsifiable. Counter-example:
---   a = -2.0 :: SFloat
---   b = -3.0e-45 :: SFloat
+--   a = -2.0 :: Float
+--   b = -3.0e-45 :: Float
 --
 -- Indeed, we have:
 --
@@ -118,7 +118,7 @@ nonZeroAddition = prove $ do [a, b] <- sFloats ["a", "b"]
 --
 -- >>> multInverse
 -- Falsifiable. Counter-example:
---   a = -2.0445642768532407e154 :: SDouble
+--   a = -2.0445642768532407e154 :: Double
 --
 -- Indeed, we have:
 --
@@ -146,8 +146,8 @@ multInverse = prove $ do a <- sDouble "a"
 -- >>> roundingAdd
 -- Satisfiable. Model:
 --   rm = RoundTowardPositive :: RoundingMode
---   x = 246080.08 :: SFloat
---   y = 16255.999 :: SFloat
+--   x = 246080.08 :: Float
+--   y = 16255.999 :: Float
 --
 -- Unfortunately we can't directly validate this result at the Haskell level, as Haskell only supports
 -- 'RoundNearestTiesToEven'. We have:

Data/SBV/Examples/Puzzles/Coins.hs

@@ -81,12 +81,12 @@ c6 xs = sum (map val xs) ./= 95
 --
 -- >>> puzzle
 -- Satisfiable. Model:
---   c1 = 50 :: SWord16
---   c2 = 25 :: SWord16
---   c3 = 10 :: SWord16
---   c4 = 10 :: SWord16
---   c5 = 10 :: SWord16
---   c6 = 10 :: SWord16
+--   c1 = 50 :: Word16
+--   c2 = 25 :: Word16
+--   c3 = 10 :: Word16
+--   c4 = 10 :: Word16
+--   c5 = 10 :: Word16
+--   c6 = 10 :: Word16
 --
 -- i.e., your friend has 4 dimes, a quarter, and a half dollar.
 puzzle :: IO SatResult

Data/SBV/Examples/Puzzles/DogCatMouse.hs

@@ -21,9 +21,9 @@ import Data.SBV
 --
 -- >>> puzzle
 -- Solution #1:
---   dog = 3 :: SInteger
---   cat = 41 :: SInteger
---   mouse = 56 :: SInteger
+--   dog = 3 :: Integer
+--   cat = 41 :: Integer
+--   mouse = 56 :: Integer
 -- This is the only solution.
 puzzle :: IO AllSatResult
 puzzle = allSat $ do

Data/SBV/Examples/Uninterpreted/Function.hs

@@ -33,8 +33,8 @@ thmGood x y z = x .== y+2 ==> f x z .== f (y + 2) z
 --
 -- >>> proveWith yicesSMT09 $ forAll ["x", "y"] thmBad
 -- Falsifiable. Counter-example:
---   x = 0 :: SWord8
---   y = 128 :: SWord8
+--   x = 0 :: Word8
+--   y = 128 :: Word8
 --   -- uninterpreted: f
 --        f 128 0 = 32768
 --        f _   _ = 0

SBVUnitTest/SBVUnitTestBuildTime.hs

@@ -2,4 +2,4 @@
 module SBVUnitTestBuildTime (buildTime) where
 
 buildTime :: String
-buildTime = "Sat Apr 11 13:07:54 PDT 2015"
+buildTime = "Sat Apr 11 13:14:43 PDT 2015"