diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,10 @@ * Hackage: * GitHub: +### Version 10.9, 2024-04-05 + + * Fix printing of floats to be more consistent, using lowercase letters + ### Version 10.8, 2024-04-05 * Increase the number of digits used in printing floats in decimal base, which leads to diff --git a/Data/SBV/Core/SizedFloats.hs b/Data/SBV/Core/SizedFloats.hs --- a/Data/SBV/Core/SizedFloats.hs +++ b/Data/SBV/Core/SizedFloats.hs @@ -33,7 +33,7 @@ , fprCompareObject, fprToSMTLib2, mkBFOpts, bfToString, bfRemoveRedundantExp ) where -import Data.Char (intToDigit, toUpper) +import Data.Char (intToDigit) import Data.List (isSuffixOf) import Data.Proxy import GHC.TypeLits @@ -113,7 +113,7 @@ | BF.bfIsInf a = if BF.bfIsPos a then "Infinity" else "-Infinity" | BF.bfIsZero a = if BF.bfIsPos a then "0.0" else "-0.0" | True - = cap $ trimZeros $ BF.bfToString b opts' a + = trimZeros $ BF.bfToString b opts' a where opts = BF.showRnd BF.NearEven <> BF.showFree (Just (fromIntegral prec)) -- For base 10, use a larger precision. It's really difficult to "pick" @@ -138,18 +138,6 @@ res -> res in pre' ++ post | True = s - - cap xs - | withPrefix = take 2 xs ++ capitalize (drop 2 xs) - | True = capitalize xs - - -- capitalize till we see the expChar - capitalize "" = "" - capitalize (x:xs) - | ux == ue = x:xs - | True = ux : capitalize xs - where ux = toUpper x - ue = toUpper expChar -- | Default options for BF options. mkBFOpts :: Integral a => a -> a -> RoundMode -> BFOpts diff --git a/Data/SBV/Utils/PrettyNum.hs b/Data/SBV/Utils/PrettyNum.hs --- a/Data/SBV/Utils/PrettyNum.hs +++ b/Data/SBV/Utils/PrettyNum.hs @@ -22,7 +22,7 @@ ) where import Data.Bits ((.&.), countTrailingZeros) -import Data.Char (intToDigit, ord, chr, toUpper) +import Data.Char (intToDigit, ord, chr) import Data.Int (Int8, Int16, Int32, Int64) import Data.List (isPrefixOf) import Data.Maybe (fromJust, fromMaybe, listToMaybe) @@ -552,10 +552,9 @@ | all (== 0) digits = "" | True = "." ++ concatMap toDigit digits - toDigit v = map toUpper d - where d | v <= 15 = [intToDigit v] - | v < 36 = [chr (ord 'a' + v - 10)] - | True = '<' : show v ++ ">" + toDigit v | v <= 15 = [intToDigit v] + | v < 36 = [chr (ord 'a' + v - 10)] + | True = '<' : show v ++ ">" -- | When we show a negative number in SMTLib, we must properly parenthesize. showNegativeNumber :: (Show a, Num a, Ord a) => a -> String diff --git a/SBVTestSuite/GoldFiles/allSat8.gold b/SBVTestSuite/GoldFiles/allSat8.gold --- a/SBVTestSuite/GoldFiles/allSat8.gold +++ b/SBVTestSuite/GoldFiles/allSat8.gold @@ -61,4 +61,4 @@ *** NB. If this is a use case you'd like SBV to support, please get in touch! CallStack (from HasCallStack): - error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.8-inplace:Data.SBV.Control.Utils + error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.9-inplace:Data.SBV.Control.Utils diff --git a/SBVTestSuite/GoldFiles/nested1.gold b/SBVTestSuite/GoldFiles/nested1.gold --- a/SBVTestSuite/GoldFiles/nested1.gold +++ b/SBVTestSuite/GoldFiles/nested1.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.8-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.9-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested2.gold b/SBVTestSuite/GoldFiles/nested2.gold --- a/SBVTestSuite/GoldFiles/nested2.gold +++ b/SBVTestSuite/GoldFiles/nested2.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.8-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.9-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested3.gold b/SBVTestSuite/GoldFiles/nested3.gold --- a/SBVTestSuite/GoldFiles/nested3.gold +++ b/SBVTestSuite/GoldFiles/nested3.gold @@ -37,4 +37,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.8-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.9-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested4.gold b/SBVTestSuite/GoldFiles/nested4.gold --- a/SBVTestSuite/GoldFiles/nested4.gold +++ b/SBVTestSuite/GoldFiles/nested4.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.8-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.9-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/optFloat1a.gold b/SBVTestSuite/GoldFiles/optFloat1a.gold --- a/SBVTestSuite/GoldFiles/optFloat1a.gold +++ b/SBVTestSuite/GoldFiles/optFloat1a.gold @@ -12,7 +12,7 @@ Binary: -0b1.11111111111111111111111p+127 Octal: -0o3.77777774p+126 Decimal: -3.4028235e38 - Hex: -0xF.FFFFFp+124 + Hex: -0xf.fffffp+124 min-x = 8388608 :: Word32 3 2 1 0 1098 7654 3210 9876 5432 1098 7654 3210 diff --git a/SBVTestSuite/GoldFiles/optFloat1c.gold b/SBVTestSuite/GoldFiles/optFloat1c.gold --- a/SBVTestSuite/GoldFiles/optFloat1c.gold +++ b/SBVTestSuite/GoldFiles/optFloat1c.gold @@ -12,7 +12,7 @@ Binary: 0b1.11111111111111111111111p+127 Octal: 0o3.77777774p+126 Decimal: 3.4028235e38 - Hex: 0xF.FFFFFp+124 + Hex: 0xf.fffffp+124 max-x = 4286578687 :: Word32 3 2 1 0 1098 7654 3210 9876 5432 1098 7654 3210 diff --git a/SBVTestSuite/GoldFiles/optFloat2a.gold b/SBVTestSuite/GoldFiles/optFloat2a.gold --- a/SBVTestSuite/GoldFiles/optFloat2a.gold +++ b/SBVTestSuite/GoldFiles/optFloat2a.gold @@ -12,7 +12,7 @@ Binary: -0b1.1111111111111111111111111111111111111111111111111111p+1023 Octal: -0o1.777777777777777774p+1023 Decimal: -1.7976931348623157e308 - Hex: -0xF.FFFFFFFFFFFF8p+1020 + Hex: -0xf.ffffffffffff8p+1020 min-x = 4503599627370496 :: Word64 6 5 4 3 2 1 0 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 diff --git a/SBVTestSuite/GoldFiles/optFloat2c.gold b/SBVTestSuite/GoldFiles/optFloat2c.gold --- a/SBVTestSuite/GoldFiles/optFloat2c.gold +++ b/SBVTestSuite/GoldFiles/optFloat2c.gold @@ -12,7 +12,7 @@ Binary: 0b1.1111111111111111111111111111111111111111111111111111p+1023 Octal: 0o1.777777777777777774p+1023 Decimal: 1.7976931348623157e308 - Hex: 0xF.FFFFFFFFFFFF8p+1020 + Hex: 0xf.ffffffffffff8p+1020 max-x = 18442240474082181119 :: Word64 6 5 4 3 2 1 0 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 diff --git a/SBVTestSuite/GoldFiles/optFloat3.gold b/SBVTestSuite/GoldFiles/optFloat3.gold --- a/SBVTestSuite/GoldFiles/optFloat3.gold +++ b/SBVTestSuite/GoldFiles/optFloat3.gold @@ -12,7 +12,7 @@ Binary: 0b1.11111111111111111111111p+127 Octal: 0o3.77777774p+126 Decimal: 3.4028235e38 - Hex: 0xF.FFFFFp+124 + Hex: 0xf.fffffp+124 x = 1.7014117e38 :: Float 3 2 1 0 1 09876543 21098765432109876543210 @@ -26,7 +26,7 @@ Binary: 0b1.11111111111111111111111p+126 Octal: 0o1.77777776p+126 Decimal: 1.7014117e38 - Hex: 0x7.FFFFF8p+124 + Hex: 0x7.fffff8p+124 y = 1.7014117e38 :: Float 3 2 1 0 1 09876543 21098765432109876543210 @@ -40,7 +40,7 @@ Binary: 0b1.11111111111111111111111p+126 Octal: 0o1.77777776p+126 Decimal: 1.7014117e38 - Hex: 0x7.FFFFF8p+124 + Hex: 0x7.fffff8p+124 metric-max-x+y = 4286578687 :: Word32 3 2 1 0 1098 7654 3210 9876 5432 1098 7654 3210 diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv -Version : 10.8 +Version : 10.9 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