{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Core.SizedFloats (
FloatingPoint(..), FP(..), FPHalf, FPSingle, FPDouble, FPQuad
, fpFromRawRep, fpNaN, fpInf, fpZero
, fpFromInteger, fpFromRational, fpFromFloat, fpFromDouble, fpEncodeFloat
, fprCompareObject, fprToSMTLib2, mkBFOpts, bfToString
) where
import Data.Char (intToDigit)
import Data.Proxy
import GHC.TypeLits
import Data.Bits
import Data.Ratio
import Numeric
import Data.SBV.Core.Kind
import Data.SBV.Utils.Numeric (floatToWord)
import LibBF (BigFloat, BFOpts, RoundMode, Status)
import qualified LibBF as BF
newtype FloatingPoint (eb :: Nat) (sb :: Nat) = FloatingPoint FP
deriving (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
(FloatingPoint eb sb -> FloatingPoint eb sb -> Bool)
-> (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool)
-> Eq (FloatingPoint eb sb)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
/= :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
$c/= :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
== :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
$c== :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
Eq, Eq (FloatingPoint eb sb)
Eq (FloatingPoint eb sb)
-> (FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering)
-> (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool)
-> (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool)
-> (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool)
-> (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool)
-> (FloatingPoint eb sb
-> FloatingPoint eb sb -> FloatingPoint eb sb)
-> (FloatingPoint eb sb
-> FloatingPoint eb sb -> FloatingPoint eb sb)
-> Ord (FloatingPoint eb sb)
FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering
FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (eb :: Nat) (sb :: Nat). Eq (FloatingPoint eb sb)
forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering
forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
min :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
$cmin :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
max :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
$cmax :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
>= :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
$c>= :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
> :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
$c> :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
<= :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
$c<= :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
< :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
$c< :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
compare :: FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering
$ccompare :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering
$cp1Ord :: forall (eb :: Nat) (sb :: Nat). Eq (FloatingPoint eb sb)
Ord)
type FPHalf = FloatingPoint 5 11
type FPSingle = FloatingPoint 8 24
type FPDouble = FloatingPoint 11 53
type FPQuad = FloatingPoint 15 113
instance Show (FloatingPoint eb sb) where
show :: FloatingPoint eb sb -> String
show (FloatingPoint FP
r) = FP -> String
forall a. Show a => a -> String
show FP
r
data FP = FP { FP -> Int
fpExponentSize :: Int
, FP -> Int
fpSignificandSize :: Int
, FP -> BigFloat
fpValue :: BigFloat
}
deriving (Eq FP
Eq FP
-> (FP -> FP -> Ordering)
-> (FP -> FP -> Bool)
-> (FP -> FP -> Bool)
-> (FP -> FP -> Bool)
-> (FP -> FP -> Bool)
-> (FP -> FP -> FP)
-> (FP -> FP -> FP)
-> Ord FP
FP -> FP -> Bool
FP -> FP -> Ordering
FP -> FP -> FP
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FP -> FP -> FP
$cmin :: FP -> FP -> FP
max :: FP -> FP -> FP
$cmax :: FP -> FP -> FP
>= :: FP -> FP -> Bool
$c>= :: FP -> FP -> Bool
> :: FP -> FP -> Bool
$c> :: FP -> FP -> Bool
<= :: FP -> FP -> Bool
$c<= :: FP -> FP -> Bool
< :: FP -> FP -> Bool
$c< :: FP -> FP -> Bool
compare :: FP -> FP -> Ordering
$ccompare :: FP -> FP -> Ordering
$cp1Ord :: Eq FP
Ord, FP -> FP -> Bool
(FP -> FP -> Bool) -> (FP -> FP -> Bool) -> Eq FP
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FP -> FP -> Bool
$c/= :: FP -> FP -> Bool
== :: FP -> FP -> Bool
$c== :: FP -> FP -> Bool
Eq)
instance Show FP where
show :: FP -> String
show = Int -> Bool -> FP -> String
bfToString Int
10 Bool
False
bfToString :: Int -> Bool -> FP -> String
bfToString :: Int -> Bool -> FP -> String
bfToString Int
b Bool
withPrefix (FP Int
_ Int
sb BigFloat
a)
| BigFloat -> Bool
BF.bfIsNaN BigFloat
a = String
"NaN"
| BigFloat -> Bool
BF.bfIsInf BigFloat
a = if BigFloat -> Bool
BF.bfIsPos BigFloat
a then String
"Infinity" else String
"-Infinity"
| BigFloat -> Bool
BF.bfIsZero BigFloat
a = if BigFloat -> Bool
BF.bfIsPos BigFloat
a then String
"0.0" else String
"-0.0"
| Bool
True = ShowS
trimZeros ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> ShowFmt -> BigFloat -> String
BF.bfToString Int
b ShowFmt
withP BigFloat
a
where opts :: ShowFmt
opts = RoundMode -> ShowFmt
BF.showRnd RoundMode
BF.NearEven ShowFmt -> ShowFmt -> ShowFmt
forall a. Semigroup a => a -> a -> a
<> Maybe Word -> ShowFmt
BF.showFree (Word -> Maybe Word
forall a. a -> Maybe a
Just (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
sb))
withP :: ShowFmt
withP
| Bool
withPrefix = ShowFmt
BF.addPrefix ShowFmt -> ShowFmt -> ShowFmt
forall a. Semigroup a => a -> a -> a
<> ShowFmt
opts
| Bool
True = ShowFmt
opts
trimZeros :: ShowS
trimZeros String
s
| Char
'.' Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
s = ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ case (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'0') ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. [a] -> [a]
reverse String
s of
res :: String
res@(Char
'.':String
_) -> Char
'0' Char -> ShowS
forall a. a -> [a] -> [a]
: String
res
String
res -> String
res
| Bool
True = String
s
mkBFOpts :: Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts :: a -> a -> RoundMode -> BFOpts
mkBFOpts a
eb a
sb RoundMode
rm = BFOpts
BF.allowSubnormal BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> RoundMode -> BFOpts
BF.rnd RoundMode
rm BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> Int -> BFOpts
BF.expBits (a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
eb) BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> Word -> BFOpts
BF.precBits (a -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
sb)
mkFP :: Int -> Int -> BigFloat -> FP
mkFP :: Int -> Int -> BigFloat -> FP
mkFP Int
eb Int
sb BigFloat
r = Int -> Int -> BigFloat -> FP
FP Int
eb Int
sb (BigFloat -> FP) -> BigFloat -> FP
forall a b. (a -> b) -> a -> b
$ (BigFloat, Status) -> BigFloat
forall a b. (a, b) -> a
fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> (BigFloat, Status)
BF.bfRoundFloat (Int -> Int -> RoundMode -> BFOpts
forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
eb Int
sb RoundMode
BF.NearEven) BigFloat
r
fpFromRawRep :: Bool -> (Integer, Int) -> (Integer, Int) -> FP
fpFromRawRep :: Bool -> (Integer, Int) -> (Integer, Int) -> FP
fpFromRawRep Bool
sign (Integer
e, Int
eb) (Integer
s, Int
sb) = Int -> Int -> BigFloat -> FP
FP Int
eb Int
sb (BigFloat -> FP) -> BigFloat -> FP
forall a b. (a -> b) -> a -> b
$ BFOpts -> Integer -> BigFloat
BF.bfFromBits (Int -> Int -> RoundMode -> BFOpts
forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
eb Int
sb RoundMode
BF.NearEven) Integer
val
where es, val :: Integer
es :: Integer
es = (Integer
e Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
sb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
s
val :: Integer
val | Bool
sign = (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
eb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
sb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
es
| Bool
True = Integer
es
fpNaN :: Int -> Int -> FP
fpNaN :: Int -> Int -> FP
fpNaN Int
eb Int
sb = Int -> Int -> BigFloat -> FP
mkFP Int
eb Int
sb BigFloat
BF.bfNaN
fpInf :: Bool -> Int -> Int -> FP
fpInf :: Bool -> Int -> Int -> FP
fpInf Bool
sign Int
eb Int
sb = Int -> Int -> BigFloat -> FP
mkFP Int
eb Int
sb (BigFloat -> FP) -> BigFloat -> FP
forall a b. (a -> b) -> a -> b
$ if Bool
sign then BigFloat
BF.bfNegInf else BigFloat
BF.bfPosInf
fpZero :: Bool -> Int -> Int -> FP
fpZero :: Bool -> Int -> Int -> FP
fpZero Bool
sign Int
eb Int
sb = Int -> Int -> BigFloat -> FP
mkFP Int
eb Int
sb (BigFloat -> FP) -> BigFloat -> FP
forall a b. (a -> b) -> a -> b
$ if Bool
sign then BigFloat
BF.bfNegZero else BigFloat
BF.bfPosZero
fpFromInteger :: Int -> Int -> Integer -> FP
fpFromInteger :: Int -> Int -> Integer -> FP
fpFromInteger Int
eb Int
sb Integer
iv = Int -> Int -> BigFloat -> FP
mkFP Int
eb Int
sb (BigFloat -> FP) -> BigFloat -> FP
forall a b. (a -> b) -> a -> b
$ Integer -> BigFloat
BF.bfFromInteger Integer
iv
fpFromRational :: Int -> Int -> Rational -> FP
fpFromRational :: Int -> Int -> Rational -> FP
fpFromRational Int
eb Int
sb Rational
r = Int -> Int -> BigFloat -> FP
FP Int
eb Int
sb (BigFloat -> FP) -> BigFloat -> FP
forall a b. (a -> b) -> a -> b
$ (BigFloat, Status) -> BigFloat
forall a b. (a, b) -> a
fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfDiv (Int -> Int -> RoundMode -> BFOpts
forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
eb Int
sb RoundMode
BF.NearEven) (Integer -> BigFloat
BF.bfFromInteger (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r))
(Integer -> BigFloat
BF.bfFromInteger (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r))
fprToSMTLib2 :: FP -> String
fprToSMTLib2 :: FP -> String
fprToSMTLib2 (FP Int
eb Int
sb BigFloat
r)
| BigFloat -> Bool
BF.bfIsNaN BigFloat
r = ShowS
as String
"NaN"
| BigFloat -> Bool
BF.bfIsInf BigFloat
r = ShowS
as ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ if BigFloat -> Bool
BF.bfIsPos BigFloat
r then String
"+oo" else String
"-oo"
| BigFloat -> Bool
BF.bfIsZero BigFloat
r = ShowS
as ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ if BigFloat -> Bool
BF.bfIsPos BigFloat
r then String
"+zero" else String
"-zero"
| Bool
True = String
generic
where e :: String
e = Int -> String
forall a. Show a => a -> String
show Int
eb
s :: String
s = Int -> String
forall a. Show a => a -> String
show Int
sb
bits :: Integer
bits = BFOpts -> BigFloat -> Integer
BF.bfToBits (Int -> Int -> RoundMode -> BFOpts
forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
eb Int
sb RoundMode
BF.NearEven) BigFloat
r
significandMask :: Integer
significandMask = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
sb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
exponentMask :: Integer
exponentMask = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
eb Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
fpSign :: Bool
fpSign = Integer
bits Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` (Int
eb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
sb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
fpExponent :: Integer
fpExponent = (Integer
bits Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` (Int
sb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
exponentMask
fpSignificand :: Integer
fpSignificand = Integer
bits Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
significandMask
generic :: String
generic = String
"(fp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [if Bool
fpSign then String
"#b1" else String
"#b0", Int -> Integer -> String
mkB Int
eb Integer
fpExponent, Int -> Integer -> String
mkB (Int
sb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Integer
fpSignificand] String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
as :: ShowS
as String
x = String
"(_ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
mkB :: Int -> Integer -> String
mkB Int
sz Integer
val = String
"#b" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
pad Int
sz (Integer -> ShowS
showBin Integer
val String
"")
showBin :: Integer -> ShowS
showBin = Integer -> (Int -> Char) -> Integer -> ShowS
forall a. (Integral a, Show a) => a -> (Int -> Char) -> a -> ShowS
showIntAtBase Integer
2 Int -> Char
intToDigit
pad :: Int -> ShowS
pad Int
l String
str = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
str) Char
'0' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str
fprCompareObject :: FP -> FP -> Ordering
fprCompareObject :: FP -> FP -> Ordering
fprCompareObject (FP Int
eb Int
sb BigFloat
a) (FP Int
eb' Int
sb' BigFloat
b) = case (Int
eb, Int
sb) (Int, Int) -> (Int, Int) -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` (Int
eb', Int
sb') of
Ordering
LT -> Ordering
LT
Ordering
GT -> Ordering
GT
Ordering
EQ -> BigFloat
a BigFloat -> BigFloat -> Ordering
`BF.bfCompare` BigFloat
b
bfSignum :: BigFloat -> BigFloat
bfSignum :: BigFloat -> BigFloat
bfSignum BigFloat
r | BigFloat -> Bool
BF.bfIsNaN BigFloat
r = BigFloat
r
| BigFloat -> Bool
BF.bfIsZero BigFloat
r = BigFloat
r
| BigFloat -> Bool
BF.bfIsPos BigFloat
r = Integer -> BigFloat
BF.bfFromInteger Integer
1
| Bool
True = Integer -> BigFloat
BF.bfFromInteger (-Integer
1)
instance Num FP where
+ :: FP -> FP -> FP
(+) = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FP -> FP -> FP
lift2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfAdd
(-) = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FP -> FP -> FP
lift2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfSub
* :: FP -> FP -> FP
(*) = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FP -> FP -> FP
lift2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfMul
abs :: FP -> FP
abs = (BigFloat -> BigFloat) -> FP -> FP
lift1 BigFloat -> BigFloat
BF.bfAbs
signum :: FP -> FP
signum = (BigFloat -> BigFloat) -> FP -> FP
lift1 BigFloat -> BigFloat
bfSignum
fromInteger :: Integer -> FP
fromInteger = String -> Integer -> FP
forall a. HasCallStack => String -> a
error String
"FP.fromInteger: Not supported for arbitrary floats. Use fpFromInteger instead, specifying the precision"
negate :: FP -> FP
negate = (BigFloat -> BigFloat) -> FP -> FP
lift1 BigFloat -> BigFloat
BF.bfNeg
instance Fractional FP where
fromRational :: Rational -> FP
fromRational = String -> Rational -> FP
forall a. HasCallStack => String -> a
error String
"FP.fromRational: Not supported for arbitrary floats. Use fpFromRational instead, specifying the precision"
/ :: FP -> FP -> FP
(/) = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FP -> FP -> FP
lift2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfDiv
instance Floating FP where
sqrt :: FP -> FP
sqrt (FP Int
eb Int
sb BigFloat
a) = Int -> Int -> BigFloat -> FP
FP Int
eb Int
sb (BigFloat -> FP) -> BigFloat -> FP
forall a b. (a -> b) -> a -> b
$ (BigFloat, Status) -> BigFloat
forall a b. (a, b) -> a
fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> (BigFloat, Status)
BF.bfSqrt (Int -> Int -> RoundMode -> BFOpts
forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
eb Int
sb RoundMode
BF.NearEven) BigFloat
a
FP Int
eb Int
sb BigFloat
a ** :: FP -> FP -> FP
** FP Int
_ Int
_ BigFloat
b = Int -> Int -> BigFloat -> FP
FP Int
eb Int
sb (BigFloat -> FP) -> BigFloat -> FP
forall a b. (a -> b) -> a -> b
$ (BigFloat, Status) -> BigFloat
forall a b. (a, b) -> a
fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfPow (Int -> Int -> RoundMode -> BFOpts
forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
eb Int
sb RoundMode
BF.NearEven) BigFloat
a BigFloat
b
pi :: FP
pi = String -> FP
forall a. String -> a
unsupported String
"Floating.FP.pi"
exp :: FP -> FP
exp = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.exp"
log :: FP -> FP
log = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.log"
sin :: FP -> FP
sin = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.sin"
cos :: FP -> FP
cos = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.cos"
tan :: FP -> FP
tan = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.tan"
asin :: FP -> FP
asin = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.asin"
acos :: FP -> FP
acos = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.acos"
atan :: FP -> FP
atan = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.atan"
sinh :: FP -> FP
sinh = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.sinh"
cosh :: FP -> FP
cosh = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.cosh"
tanh :: FP -> FP
tanh = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.tanh"
asinh :: FP -> FP
asinh = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.asinh"
acosh :: FP -> FP
acosh = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.acosh"
atanh :: FP -> FP
atanh = String -> FP -> FP
forall a. String -> a
unsupported String
"Floating.FP.atanh"
instance RealFloat FP where
floatRadix :: FP -> Integer
floatRadix FP
_ = Integer
2
floatDigits :: FP -> Int
floatDigits (FP Int
_ Int
sb BigFloat
_) = Int
sb
floatRange :: FP -> (Int, Int)
floatRange (FP Int
eb Int
_ BigFloat
_) = (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (-Integer
vInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
3), Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
v)
where v :: Integer
v :: Integer
v = Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ ((Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
eb :: Integer) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
isNaN :: FP -> Bool
isNaN (FP Int
_ Int
_ BigFloat
r) = BigFloat -> Bool
BF.bfIsNaN BigFloat
r
isInfinite :: FP -> Bool
isInfinite (FP Int
_ Int
_ BigFloat
r) = BigFloat -> Bool
BF.bfIsInf BigFloat
r
isDenormalized :: FP -> Bool
isDenormalized (FP Int
eb Int
sb BigFloat
r) = BFOpts -> BigFloat -> Bool
BF.bfIsSubnormal (Int -> Int -> RoundMode -> BFOpts
forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
eb Int
sb RoundMode
BF.NearEven) BigFloat
r
isNegativeZero :: FP -> Bool
isNegativeZero (FP Int
_ Int
_ BigFloat
r) = BigFloat -> Bool
BF.bfIsZero BigFloat
r Bool -> Bool -> Bool
&& BigFloat -> Bool
BF.bfIsNeg BigFloat
r
isIEEE :: FP -> Bool
isIEEE FP
_ = Bool
True
decodeFloat :: FP -> (Integer, Int)
decodeFloat i :: FP
i@(FP Int
_ Int
_ BigFloat
r) = case BigFloat -> BFRep
BF.bfToRep BigFloat
r of
BFRep
BF.BFNaN -> Double -> (Integer, Int)
forall a. RealFloat a => a -> (Integer, Int)
decodeFloat (Double
0Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/Double
0 :: Double)
BF.BFRep Sign
s BFNum
n -> case BFNum
n of
BFNum
BF.Zero -> (Integer
0, Int
0)
BFNum
BF.Inf -> let (Int
_, Int
m) = FP -> (Int, Int)
forall a. RealFloat a => a -> (Int, Int)
floatRange FP
i
x :: Integer
x = (Integer
2 :: Integer) Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
in (if Sign
s Sign -> Sign -> Bool
forall a. Eq a => a -> a -> Bool
== Sign
BF.Neg then -Integer
x else Integer
x, Int
0)
BF.Num Integer
x Int64
y ->
(if Sign
s Sign -> Sign -> Bool
forall a. Eq a => a -> a -> Bool
== Sign
BF.Neg then -Integer
x else Integer
x, Int64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
y)
encodeFloat :: Integer -> Int -> FP
encodeFloat = String -> Integer -> Int -> FP
forall a. HasCallStack => String -> a
error String
"FP.encodeFloat: Not supported for arbitrary floats. Use fpEncodeFloat instead, specifying the precision"
fpEncodeFloat :: Int -> Int -> Integer -> Int -> FP
fpEncodeFloat :: Int -> Int -> Integer -> Int -> FP
fpEncodeFloat Int
eb Int
sb Integer
m Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = Int -> Int -> Rational -> FP
fpFromRational Int
eb Int
sb (Integer
m Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
n')
| Bool
True = Int -> Int -> Rational -> FP
fpFromRational Int
eb Int
sb (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
n' Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1)
where n' :: Integer
n' :: Integer
n' = (Integer
2 :: Integer) Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer -> Integer
forall a. Num a => a -> a
abs (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n :: Integer)
instance Real FP where
toRational :: FP -> Rational
toRational FP
i
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1
| Bool
True = Integer
m Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int -> Int
forall a. Num a => a -> a
abs Int
n
where (Integer
m, Int
n) = FP -> (Integer, Int)
forall a. RealFloat a => a -> (Integer, Int)
decodeFloat FP
i
instance RealFrac FP where
properFraction :: FP -> (b, FP)
properFraction (FP Int
eb Int
sb BigFloat
r) = case RoundMode -> BigFloat -> (BigFloat, Status)
BF.bfRoundInt RoundMode
BF.ToNegInf BigFloat
r of
(BigFloat
r', Status
BF.Ok) | BigFloat -> Maybe Sign
BF.bfSign BigFloat
r Maybe Sign -> Maybe Sign -> Bool
forall a. Eq a => a -> a -> Bool
== BigFloat -> Maybe Sign
BF.bfSign BigFloat
r' -> (BigFloat -> b
getInt BigFloat
r', Int -> Int -> BigFloat -> FP
FP Int
eb Int
sb BigFloat
r FP -> FP -> FP
forall a. Num a => a -> a -> a
- Int -> Int -> BigFloat -> FP
FP Int
eb Int
sb BigFloat
r')
(BigFloat, Status)
x -> String -> (b, FP)
forall a. HasCallStack => String -> a
error (String -> (b, FP)) -> String -> (b, FP)
forall a b. (a -> b) -> a -> b
$ String
"RealFrac.FP.properFraction: Failed to convert: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (BigFloat, (BigFloat, Status)) -> String
forall a. Show a => a -> String
show (BigFloat
r, (BigFloat, Status)
x)
where getInt :: BigFloat -> b
getInt BigFloat
x = case BigFloat -> BFRep
BF.bfToRep BigFloat
x of
BFRep
BF.BFNaN -> String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.FloatingPoint.properFraction: Failed to convert: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (BigFloat, BigFloat) -> String
forall a. Show a => a -> String
show (BigFloat
r, BigFloat
x)
BF.BFRep Sign
s BFNum
n -> case BFNum
n of
BFNum
BF.Zero -> b
0
BFNum
BF.Inf -> String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.FloatingPoint.properFraction: Failed to convert: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (BigFloat, BigFloat) -> String
forall a. Show a => a -> String
show (BigFloat
r, BigFloat
x)
BF.Num Integer
v Int64
y ->
let e :: Integer
e :: Integer
e = Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
y :: Integer)
sgn :: Integer -> Integer
sgn = if Sign
s Sign -> Sign -> Bool
forall a. Eq a => a -> a -> Bool
== Sign
BF.Neg then ((-Integer
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*) else Integer -> Integer
forall a. a -> a
id
in if Int64
y Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
> Int64
0
then Integer -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> b) -> Integer -> b
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
sgn (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer
v Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
e
else Integer -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> b) -> Integer -> b
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
sgn Integer
v
instance ValidFloat eb sb => Num (FloatingPoint eb sb) where
FloatingPoint FP
a + :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
+ FloatingPoint FP
b = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FloatingPoint eb sb) -> FP -> FloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$ FP
a FP -> FP -> FP
forall a. Num a => a -> a -> a
+ FP
b
FloatingPoint FP
a * :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
* FloatingPoint FP
b = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FloatingPoint eb sb) -> FP -> FloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$ FP
a FP -> FP -> FP
forall a. Num a => a -> a -> a
* FP
b
abs :: FloatingPoint eb sb -> FloatingPoint eb sb
abs (FloatingPoint FP
fp) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Num a => a -> a
abs FP
fp)
signum :: FloatingPoint eb sb -> FloatingPoint eb sb
signum (FloatingPoint FP
fp) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Num a => a -> a
signum FP
fp)
negate :: FloatingPoint eb sb -> FloatingPoint eb sb
negate (FloatingPoint FP
fp) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Num a => a -> a
negate FP
fp)
fromInteger :: Integer -> FloatingPoint eb sb
fromInteger = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FloatingPoint eb sb)
-> (Integer -> FP) -> Integer -> FloatingPoint eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Integer -> FP
fpFromInteger (Proxy eb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)) (Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
forall k (t :: k). Proxy t
Proxy @sb))
instance ValidFloat eb sb => Fractional (FloatingPoint eb sb) where
fromRational :: Rational -> FloatingPoint eb sb
fromRational = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FloatingPoint eb sb)
-> (Rational -> FP) -> Rational -> FloatingPoint eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Rational -> FP
fpFromRational (Proxy eb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)) (Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
forall k (t :: k). Proxy t
Proxy @sb))
FloatingPoint FP
a / :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
/ FloatingPoint FP
b = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP
a FP -> FP -> FP
forall a. Fractional a => a -> a -> a
/ FP
b)
unsupported :: String -> a
unsupported :: String -> a
unsupported String
w = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.FloatingPoint: Unsupported operation: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
w String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
". Please request this as a feature!"
instance ValidFloat eb sb => Floating (FloatingPoint eb sb) where
pi :: FloatingPoint eb sb
pi = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint FP
forall a. Floating a => a
pi
exp :: FloatingPoint eb sb -> FloatingPoint eb sb
exp (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
exp FP
i)
sqrt :: FloatingPoint eb sb -> FloatingPoint eb sb
sqrt (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
sqrt FP
i)
FloatingPoint FP
a ** :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
** FloatingPoint FP
b = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FloatingPoint eb sb) -> FP -> FloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$ FP
a FP -> FP -> FP
forall a. Floating a => a -> a -> a
** FP
b
log :: FloatingPoint eb sb -> FloatingPoint eb sb
log (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
log FP
i)
sin :: FloatingPoint eb sb -> FloatingPoint eb sb
sin (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
sin FP
i)
cos :: FloatingPoint eb sb -> FloatingPoint eb sb
cos (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
cos FP
i)
tan :: FloatingPoint eb sb -> FloatingPoint eb sb
tan (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
tan FP
i)
asin :: FloatingPoint eb sb -> FloatingPoint eb sb
asin (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
asin FP
i)
acos :: FloatingPoint eb sb -> FloatingPoint eb sb
acos (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
acos FP
i)
atan :: FloatingPoint eb sb -> FloatingPoint eb sb
atan (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
atan FP
i)
sinh :: FloatingPoint eb sb -> FloatingPoint eb sb
sinh (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
sinh FP
i)
cosh :: FloatingPoint eb sb -> FloatingPoint eb sb
cosh (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
cosh FP
i)
tanh :: FloatingPoint eb sb -> FloatingPoint eb sb
tanh (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
tanh FP
i)
asinh :: FloatingPoint eb sb -> FloatingPoint eb sb
asinh (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
asinh FP
i)
acosh :: FloatingPoint eb sb -> FloatingPoint eb sb
acosh (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
acosh FP
i)
atanh :: FloatingPoint eb sb -> FloatingPoint eb sb
atanh (FloatingPoint FP
i) = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (FP -> FP
forall a. Floating a => a -> a
atanh FP
i)
lift1 :: (BigFloat -> BigFloat) -> FP -> FP
lift1 :: (BigFloat -> BigFloat) -> FP -> FP
lift1 BigFloat -> BigFloat
f (FP Int
eb Int
sb BigFloat
a) = Int -> Int -> BigFloat -> FP
mkFP Int
eb Int
sb (BigFloat -> FP) -> BigFloat -> FP
forall a b. (a -> b) -> a -> b
$ BigFloat -> BigFloat
f BigFloat
a
lift2 :: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) -> FP -> FP -> FP
lift2 :: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FP -> FP -> FP
lift2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
f (FP Int
eb Int
sb BigFloat
a) (FP Int
_ Int
_ BigFloat
b) = Int -> Int -> BigFloat -> FP
FP Int
eb Int
sb (BigFloat -> FP) -> BigFloat -> FP
forall a b. (a -> b) -> a -> b
$ (BigFloat, Status) -> BigFloat
forall a b. (a, b) -> a
fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
f (Int -> Int -> RoundMode -> BFOpts
forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
eb Int
sb RoundMode
BF.NearEven) BigFloat
a BigFloat
b
fpFromFloat :: Int -> Int -> Float -> FP
fpFromFloat :: Int -> Int -> Float -> FP
fpFromFloat Int
8 Int
24 Float
f = let fw :: Word32
fw = Float -> Word32
floatToWord Float
f
(Bool
sgn, Integer
e, Integer
s) = (Word32
fw Word32 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
31, Word32 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32
fw Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
`shiftR` Int
23) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
0xFF, Word32 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
fw Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
0x7FFFFF)
in Bool -> (Integer, Int) -> (Integer, Int) -> FP
fpFromRawRep Bool
sgn (Integer
e, Int
8) (Integer
s, Int
24)
fpFromFloat Int
eb Int
sb Float
f = String -> FP
forall a. HasCallStack => String -> a
error (String -> FP) -> String -> FP
forall a b. (a -> b) -> a -> b
$ String
"SBV.fprFromFloat: Unexpected input: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Int, Float) -> String
forall a. Show a => a -> String
show (Int
eb, Int
sb, Float
f)
fpFromDouble :: Int -> Int -> Double -> FP
fpFromDouble :: Int -> Int -> Double -> FP
fpFromDouble Int
11 Int
54 Double
d = Int -> Int -> BigFloat -> FP
FP Int
11 Int
54 (BigFloat -> FP) -> BigFloat -> FP
forall a b. (a -> b) -> a -> b
$ Double -> BigFloat
BF.bfFromDouble Double
d
fpFromDouble Int
eb Int
sb Double
d = String -> FP
forall a. HasCallStack => String -> a
error (String -> FP) -> String -> FP
forall a b. (a -> b) -> a -> b
$ String
"SBV.fprFromDouble: Unexpected input: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Int, Double) -> String
forall a. Show a => a -> String
show (Int
eb, Int
sb, Double
d)