{-# Language BlockArguments, OverloadedStrings #-}
{-# Language BangPatterns #-}
module Cryptol.Backend.FloatHelpers where
import Data.Ratio(numerator,denominator)
import Data.Int(Int64)
import Data.Bits(testBit,setBit,shiftL,shiftR,(.&.),(.|.))
import LibBF
import Cryptol.Utils.PP
import Cryptol.Utils.Panic(panic)
import Cryptol.Backend.Monad( EvalError(..)
, PPOpts(..), PPFloatFormat(..), PPFloatExp(..)
)
data BF = BF
{ BF -> Integer
bfExpWidth :: Integer
, BF -> Integer
bfPrecWidth :: Integer
, BF -> BigFloat
bfValue :: BigFloat
}
fpOpts :: Integer -> Integer -> RoundMode -> BFOpts
fpOpts :: Integer -> Integer -> RoundMode -> BFOpts
fpOpts Integer
e Integer
p RoundMode
r =
case Maybe BFOpts
ok of
Just BFOpts
opts -> BFOpts
opts
Maybe BFOpts
Nothing -> String -> [String] -> BFOpts
forall a. HasCallStack => String -> [String] -> a
panic String
"floatOpts" [ String
"Invalid Float size"
, String
"exponent: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
e
, String
"precision: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
p
]
where
ok :: Maybe BFOpts
ok = do BFOpts
eb <- (Int -> BFOpts) -> Int -> Int -> Integer -> Maybe BFOpts
forall a a t a.
(Integral a, Integral a, Num t) =>
(t -> a) -> a -> a -> Integer -> Maybe a
rng Int -> BFOpts
expBits Int
expBitsMin Int
expBitsMax Integer
e
BFOpts
pb <- (Int -> BFOpts) -> Int -> Int -> Integer -> Maybe BFOpts
forall a a t a.
(Integral a, Integral a, Num t) =>
(t -> a) -> a -> a -> Integer -> Maybe a
rng Int -> BFOpts
precBits Int
precBitsMin Int
precBitsMax Integer
p
BFOpts -> Maybe BFOpts
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BFOpts
eb BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> BFOpts
pb BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> BFOpts
allowSubnormal BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> RoundMode -> BFOpts
rnd RoundMode
r)
rng :: (t -> a) -> a -> a -> Integer -> Maybe a
rng t -> a
f a
a a
b Integer
x = if a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
x Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= a -> Integer
forall a. Integral a => a -> Integer
toInteger a
b
then a -> Maybe a
forall a. a -> Maybe a
Just (t -> a
f (Integer -> t
forall a. Num a => Integer -> a
fromInteger Integer
x))
else Maybe a
forall a. Maybe a
Nothing
fpRound :: Integer -> Either EvalError RoundMode
fpRound :: Integer -> Either EvalError RoundMode
fpRound Integer
n =
case Integer
n of
Integer
0 -> RoundMode -> Either EvalError RoundMode
forall a b. b -> Either a b
Right RoundMode
NearEven
Integer
1 -> RoundMode -> Either EvalError RoundMode
forall a b. b -> Either a b
Right RoundMode
NearAway
Integer
2 -> RoundMode -> Either EvalError RoundMode
forall a b. b -> Either a b
Right RoundMode
ToPosInf
Integer
3 -> RoundMode -> Either EvalError RoundMode
forall a b. b -> Either a b
Right RoundMode
ToNegInf
Integer
4 -> RoundMode -> Either EvalError RoundMode
forall a b. b -> Either a b
Right RoundMode
ToZero
Integer
_ -> EvalError -> Either EvalError RoundMode
forall a b. a -> Either a b
Left (Integer -> EvalError
BadRoundingMode Integer
n)
fpCheckStatus :: (BigFloat,Status) -> BigFloat
fpCheckStatus :: (BigFloat, Status) -> BigFloat
fpCheckStatus (BigFloat
r,Status
s) =
case Status
s of
Status
MemError -> String -> [String] -> BigFloat
forall a. HasCallStack => String -> [String] -> a
panic String
"checkStatus" [ String
"libBF: Memory error" ]
Status
_ -> BigFloat
r
fpPP :: PPOpts -> BF -> Doc
fpPP :: PPOpts -> BF -> Doc
fpPP PPOpts
opts BF
bf =
case BigFloat -> Maybe Sign
bfSign BigFloat
num of
Maybe Sign
Nothing -> Doc
"fpNaN"
Just Sign
s
| BigFloat -> Bool
bfIsFinite BigFloat
num -> String -> Doc
text String
hacStr
| Bool
otherwise ->
case Sign
s of
Sign
Pos -> Doc
"fpPosInf"
Sign
Neg -> Doc
"fpNegInf"
where
num :: BigFloat
num = BF -> BigFloat
bfValue BF
bf
precW :: Integer
precW = BF -> Integer
bfPrecWidth BF
bf
base :: Int
base = PPOpts -> Int
useFPBase PPOpts
opts
withExp :: PPFloatExp -> ShowFmt -> ShowFmt
withExp :: PPFloatExp -> ShowFmt -> ShowFmt
withExp PPFloatExp
e ShowFmt
f = case PPFloatExp
e of
PPFloatExp
AutoExponent -> ShowFmt
f
PPFloatExp
ForceExponent -> ShowFmt
f ShowFmt -> ShowFmt -> ShowFmt
forall a. Semigroup a => a -> a -> a
<> ShowFmt
forceExp
str :: String
str = Int -> ShowFmt -> BigFloat -> String
bfToString Int
base ShowFmt
fmt BigFloat
num
fmt :: ShowFmt
fmt = ShowFmt
addPrefix ShowFmt -> ShowFmt -> ShowFmt
forall a. Semigroup a => a -> a -> a
<> RoundMode -> ShowFmt
showRnd RoundMode
NearEven ShowFmt -> ShowFmt -> ShowFmt
forall a. Semigroup a => a -> a -> a
<>
case PPOpts -> PPFloatFormat
useFPFormat PPOpts
opts of
FloatFree PPFloatExp
e -> PPFloatExp -> ShowFmt -> ShowFmt
withExp PPFloatExp
e (ShowFmt -> ShowFmt) -> ShowFmt -> ShowFmt
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> ShowFmt
showFreeMin
(Maybe Word64 -> ShowFmt) -> Maybe Word64 -> ShowFmt
forall a b. (a -> b) -> a -> b
$ Word64 -> Maybe Word64
forall a. a -> Maybe a
Just (Word64 -> Maybe Word64) -> Word64 -> Maybe Word64
forall a b. (a -> b) -> a -> b
$ Integer -> Word64
forall a. Num a => Integer -> a
fromInteger Integer
precW
FloatFixed Int
n PPFloatExp
e -> PPFloatExp -> ShowFmt -> ShowFmt
withExp PPFloatExp
e (ShowFmt -> ShowFmt) -> ShowFmt -> ShowFmt
forall a b. (a -> b) -> a -> b
$ Word64 -> ShowFmt
showFixed (Word64 -> ShowFmt) -> Word64 -> ShowFmt
forall a b. (a -> b) -> a -> b
$ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n
FloatFrac Int
n -> Word64 -> ShowFmt
showFrac (Word64 -> ShowFmt) -> Word64 -> ShowFmt
forall a b. (a -> b) -> a -> b
$ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n
hacStr :: String
hacStr
| Int
base Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
10 Bool -> Bool -> Bool
|| Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
'.' String
str = String
str
| Bool
otherwise = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'p') String
str of
(String
xs,String
ys) -> String
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".0" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ys
fpLit ::
Integer ->
Integer ->
Rational ->
BF
fpLit :: Integer -> Integer -> Rational -> BF
fpLit Integer
e Integer
p Rational
rat = Integer -> Integer -> RoundMode -> Rational -> BF
floatFromRational Integer
e Integer
p RoundMode
NearEven Rational
rat
floatFromRational :: Integer -> Integer -> RoundMode -> Rational -> BF
floatFromRational :: Integer -> Integer -> RoundMode -> Rational -> BF
floatFromRational Integer
e Integer
p RoundMode
r Rational
rat =
BF :: Integer -> Integer -> BigFloat -> BF
BF { bfExpWidth :: Integer
bfExpWidth = Integer
e
, bfPrecWidth :: Integer
bfPrecWidth = Integer
p
, bfValue :: BigFloat
bfValue = (BigFloat, Status) -> BigFloat
fpCheckStatus
if Integer
den Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 then BFOpts -> BigFloat -> (BigFloat, Status)
bfRoundFloat BFOpts
opts BigFloat
num
else BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
bfDiv BFOpts
opts BigFloat
num (Integer -> BigFloat
bfFromInteger Integer
den)
}
where
opts :: BFOpts
opts = Integer -> Integer -> RoundMode -> BFOpts
fpOpts Integer
e Integer
p RoundMode
r
num :: BigFloat
num = Integer -> BigFloat
bfFromInteger (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
rat)
den :: Integer
den = Rational -> Integer
forall a. Ratio a -> a
denominator Rational
rat
floatToRational :: String -> BF -> Either EvalError Rational
floatToRational :: String -> BF -> Either EvalError Rational
floatToRational String
fun BF
bf =
case BigFloat -> BFRep
bfToRep (BF -> BigFloat
bfValue BF
bf) of
BFRep
BFNaN -> EvalError -> Either EvalError Rational
forall a b. a -> Either a b
Left (String -> EvalError
BadValue String
fun)
BFRep Sign
s BFNum
num ->
case BFNum
num of
BFNum
Inf -> EvalError -> Either EvalError Rational
forall a b. a -> Either a b
Left (String -> EvalError
BadValue String
fun)
BFNum
Zero -> Rational -> Either EvalError Rational
forall a b. b -> Either a b
Right Rational
0
Num Integer
i Int64
ev -> Rational -> Either EvalError Rational
forall a b. b -> Either a b
Right case Sign
s of
Sign
Pos -> Rational
ab
Sign
Neg -> Rational -> Rational
forall a. Num a => a -> a
negate Rational
ab
where ab :: Rational
ab = Integer -> Rational
forall a. Num a => Integer -> a
fromInteger Integer
i Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* (Rational
2 Rational -> Int64 -> Rational
forall a b. (Fractional a, Integral b) => a -> b -> a
^^ Int64
ev)
floatToInteger :: String -> RoundMode -> BF -> Either EvalError Integer
floatToInteger :: String -> RoundMode -> BF -> Either EvalError Integer
floatToInteger String
fun RoundMode
r BF
fp =
do Rational
rat <- String -> BF -> Either EvalError Rational
floatToRational String
fun BF
fp
Integer -> Either EvalError Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure case RoundMode
r of
RoundMode
NearEven -> Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
round Rational
rat
RoundMode
NearAway -> if Rational
rat Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0 then Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
rat else Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
rat
RoundMode
ToPosInf -> Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
rat
RoundMode
ToNegInf -> Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
rat
RoundMode
ToZero -> Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
truncate Rational
rat
RoundMode
_ -> String -> [String] -> Integer
forall a. HasCallStack => String -> [String] -> a
panic String
"fpCvtToInteger"
[String
"Unexpected rounding mode", RoundMode -> String
forall a. Show a => a -> String
show RoundMode
r]
floatFromBits ::
Integer ->
Integer ->
Integer ->
BF
floatFromBits :: Integer -> Integer -> Integer -> BF
floatFromBits Integer
e Integer
p Integer
bv = BF :: Integer -> Integer -> BigFloat -> BF
BF { bfValue :: BigFloat
bfValue = Integer -> Integer -> Integer -> BigFloat
floatFromBits' Integer
e Integer
p Integer
bv
, bfExpWidth :: Integer
bfExpWidth = Integer
e, bfPrecWidth :: Integer
bfPrecWidth = Integer
p }
floatFromBits' ::
Integer ->
Integer ->
Integer ->
BigFloat
floatFromBits' :: Integer -> Integer -> Integer -> BigFloat
floatFromBits' Integer
e Integer
p Integer
bits
| Int64
expoBiased Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
== Int64
0 Bool -> Bool -> Bool
&& Integer
mant Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 =
if Bool
isNeg then BigFloat
bfNegZero else BigFloat
bfPosZero
| Int64
expoBiased Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
== Int64
eMask Bool -> Bool -> Bool
&& Integer
mant Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 =
if Bool
isNeg then BigFloat
bfNegInf else BigFloat
bfPosInf
| Int64
expoBiased Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
== Int64
eMask = BigFloat
bfNaN
| Int64
expoBiased Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
== Int64
0 =
case BFOpts -> BigFloat -> Int64 -> (BigFloat, Status)
bfMul2Exp BFOpts
opts (Integer -> BigFloat
bfFromInteger Integer
mant) (Int64
expoVal Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int64
1) of
(BigFloat
num,Status
Ok) -> if Bool
isNeg then BigFloat -> BigFloat
bfNeg BigFloat
num else BigFloat
num
(BigFloat
_,Status
s) -> String -> [String] -> BigFloat
forall a. HasCallStack => String -> [String] -> a
panic String
"floatFromBits" [ String
"Unexpected status: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Status -> String
forall a. Show a => a -> String
show Status
s ]
| Bool
otherwise =
case BFOpts -> BigFloat -> Int64 -> (BigFloat, Status)
bfMul2Exp BFOpts
opts (Integer -> BigFloat
bfFromInteger Integer
mantVal) Int64
expoVal of
(BigFloat
num,Status
Ok) -> if Bool
isNeg then BigFloat -> BigFloat
bfNeg BigFloat
num else BigFloat
num
(BigFloat
_,Status
s) -> String -> [String] -> BigFloat
forall a. HasCallStack => String -> [String] -> a
panic String
"floatFromBits" [ String
"Unexpected status: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Status -> String
forall a. Show a => a -> String
show Status
s ]
where
opts :: BFOpts
opts = Int -> BFOpts
expBits Int
e' BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> Int -> BFOpts
precBits (Int
p' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> BFOpts
allowSubnormal
e' :: Int
e' = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
e :: Int
p' :: Int
p' = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
p Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 :: Int
eMask :: Int64
eMask = (Int64
1 Int64 -> Int -> Int64
forall a. Bits a => a -> Int -> a
`shiftL` Int
e') Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
- Int64
1 :: Int64
pMask :: Integer
pMask = (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
p') Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 :: Integer
isNeg :: Bool
isNeg = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
bits (Int
e' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
p')
mant :: Integer
mant = Integer
pMask Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bits :: Integer
mantVal :: Integer
mantVal = Integer
mant Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`setBit` Int
p' :: Integer
expoBiased :: Int64
expoBiased = Int64
eMask Int64 -> Int64 -> Int64
forall a. Bits a => a -> a -> a
.&. Integer -> Int64
forall a. Num a => Integer -> a
fromInteger (Integer
bits Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
p') :: Int64
bias :: Int64
bias = Int64
eMask Int64 -> Int -> Int64
forall a. Bits a => a -> Int -> a
`shiftR` Int
1 :: Int64
expoVal :: Int64
expoVal = Int64
expoBiased Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
- Int64
bias Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
- Int -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
p' :: Int64
floatToBits :: Integer -> Integer -> BigFloat -> Integer
floatToBits :: Integer -> Integer -> BigFloat -> Integer
floatToBits Integer
e Integer
p BigFloat
bf = (Integer
isNeg Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
e' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
p'))
Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. (Integer
expBiased Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
p')
Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. (Integer
mant Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
0)
where
e' :: Int
e' = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
e :: Int
p' :: Int
p' = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
p Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 :: Int
eMask :: Integer
eMask = (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
e') Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 :: Integer
pMask :: Integer
pMask = (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
p') Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 :: Integer
(Integer
isNeg, Integer
expBiased, Integer
mant) =
case BigFloat -> BFRep
bfToRep BigFloat
bf of
BFRep
BFNaN -> (Integer
0, Integer
eMask, Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
p' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
BFRep Sign
s BFNum
num -> (Integer
sign, Integer
be, Integer
ma)
where
sign :: Integer
sign = case Sign
s of
Sign
Neg -> Integer
1
Sign
Pos -> Integer
0
(Integer
be,Integer
ma) =
case BFNum
num of
BFNum
Zero -> (Integer
0,Integer
0)
Num Integer
i Int64
ev
| Integer
ex Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> (Integer
0, Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
p' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))
| Bool
otherwise -> (Integer
ex, (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
p' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m)) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
pMask)
where
m :: Int
m = Int -> Integer -> Int
forall t t. (Num t, Num t, Bits t) => t -> t -> t
msb Int
0 Integer
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
bias :: Integer
bias = Integer
eMask Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
1
ex :: Integer
ex = Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger Int64
ev Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
bias Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
m
BFNum
Inf -> (Integer
eMask,Integer
0)
msb :: t -> t -> t
msb !t
n t
j = if t
j t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 then t
n else t -> t -> t
msb (t
nt -> t -> t
forall a. Num a => a -> a -> a
+t
1) (t
j t -> Int -> t
forall a. Bits a => a -> Int -> a
`shiftR` Int
1)