GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-10-06 00:22:49 +03:00
Code Issues Projects Releases Wiki Activity

Remove data-binary-ieee754 dependency in favor of GHC.Float

Browse Source 
The `data-binary-ieee754` library, which `what4` depends on, is deprecated.
Fortunately, `what4` only uses this library for converting `Float`s and
`Double`s to `Word`s, which is functionality that the `base` library has
provided since GHC 8.2. As a result, removing the `data-binary-ieee754`
dependency is straightforward.
This commit is contained in:
Ryan Scott 2022-06-21 11:23:27 -04:00 committed by Ryan Scott
parent 835238d875
commit 200b6c9ce6
3 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
what4/CHANGES.md
View File

@ -1,3 +1,7 @@
# next (TBA)
* Remove a dependency on `data-binary-ieee754`, which has been deprecated.
# 1.3 (April 2022)
* Allow building with GHC 9.2.

10
what4/src/What4/Expr/Builder.hs
View File

@ -187,7 +187,6 @@ import Control.Monad.Trans.Writer.Strict (writer, runWriter)
import qualified Data.BitVector.Sized as BV
import Data.Bimap (Bimap)
import qualified Data.Bimap as Bimap
import qualified Data.Binary.IEEE754 as IEEE754
import Data.Hashable
import Data.IORef
@ -208,6 +207,7 @@ import Data.Parameterized.TraversableFC
import Data.Ratio (numerator, denominator)
import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Float (castFloatToWord32, castDoubleToWord64)
import qualified LibBF as BF
import What4.BaseTypes
@ -3668,10 +3668,10 @@ instance IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatUninterpret
iFloatLitRational sym fi x = iRealToFloat sym fi RNE =<< realLit sym x
iFloatLitSingle sym x =
iFloatFromBinary sym SingleFloatRepr
=<< (bvLit sym knownNat $ BV.word32 $ IEEE754.floatToWord x)
=<< (bvLit sym knownNat $ BV.word32 $ castFloatToWord32 x)
iFloatLitDouble sym x =
iFloatFromBinary sym DoubleFloatRepr
=<< (bvLit sym knownNat $ BV.word64 $ IEEE754.doubleToWord x)
=<< (bvLit sym knownNat $ BV.word64 $ castDoubleToWord64 x)
iFloatLitLongDouble sym x =
iFloatFromBinary sym X86_80FloatRepr
=<< (bvLit sym knownNat $ BV.mkBV knownNat $ fp80ToBits x)
@ -3853,10 +3853,10 @@ instance IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatIEEE)) wher
iFloatLitRational sym = floatLitRational sym . floatInfoToPrecisionRepr
iFloatLitSingle sym x =
floatFromBinary sym knownRepr
=<< (bvLit sym knownNat $ BV.word32 $ IEEE754.floatToWord x)
=<< (bvLit sym knownNat $ BV.word32 $ castFloatToWord32 x)
iFloatLitDouble sym x =
floatFromBinary sym knownRepr
=<< (bvLit sym knownNat $ BV.word64 $ IEEE754.doubleToWord x)
=<< (bvLit sym knownNat $ BV.word64 $ castDoubleToWord64 x)
iFloatLitLongDouble sym (X86_80Val e s) = do
el <- bvLit sym (knownNat @16) $ BV.word16 e
sl <- bvLit sym (knownNat @64) $ BV.word64 s

6
what4/what4.cabal
View File

@ -91,7 +91,7 @@ common testdefs-hunit
library
import: bldflags
build-depends:
base >= 4.8 && < 5,
base >= 4.10 && < 5,
async,
attoparsec >= 0.13,
bimap >= 0.2,
@ -102,7 +102,6 @@ library
concurrent-extra >= 0.7 && < 0.8,
config-value >= 0.8 && < 0.9,
containers >= 0.5.0.0,
data-binary-ieee754,
deepseq >= 1.3,
directory >= 1.2.2,
exceptions >= 0.10,
@ -257,7 +256,6 @@ test-suite adapter-test
bv-sized,
bytestring,
containers,
data-binary-ieee754,
lens,
mtl >= 2.2.1,
process,
@ -296,7 +294,6 @@ test-suite online-solver-test
bytestring,
clock,
containers,
data-binary-ieee754,
exceptions,
lens,
prettyprinter,
@ -320,7 +317,6 @@ test-suite expr-builder-smtlib2
bv-sized,
bytestring,
containers,
data-binary-ieee754,
libBF,
prettyprinter,
process,