{-# Language BlockArguments, OverloadedStrings #-}
{-# Language BangPatterns #-}
module Cryptol.Backend.FloatHelpers where
import Data.Char (isDigit)
import Data.Ratio(numerator,denominator)
import LibBF
import Cryptol.Utils.PP
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Types
import Cryptol.Backend.Monad( EvalError(..) )
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 -> forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"floatOpts" [ [Char]
"Invalid Float size"
, [Char]
"exponent: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Integer
e
, [Char]
"precision: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Integer
p
]
where
ok :: Maybe BFOpts
ok = do BFOpts
eb <- 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 <- forall {a} {a} {t} {a}.
(Integral a, Integral a, Num t) =>
(t -> a) -> a -> a -> Integer -> Maybe a
rng Word -> BFOpts
precBits Int
precBitsMin Int
precBitsMax Integer
p
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BFOpts
eb forall a. Semigroup a => a -> a -> a
<> BFOpts
pb forall a. Semigroup a => a -> a -> a
<> BFOpts
allowSubnormal 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 forall a. Integral a => a -> Integer
toInteger a
a forall a. Ord a => a -> a -> Bool
<= Integer
x Bool -> Bool -> Bool
&& Integer
x forall a. Ord a => a -> a -> Bool
<= forall a. Integral a => a -> Integer
toInteger a
b
then forall a. a -> Maybe a
Just (t -> a
f (forall a. Num a => Integer -> a
fromInteger Integer
x))
else forall a. Maybe a
Nothing
fpRound :: Integer -> Either EvalError RoundMode
fpRound :: Integer -> Either EvalError RoundMode
fpRound Integer
n =
case Integer
n of
Integer
0 -> forall a b. b -> Either a b
Right RoundMode
NearEven
Integer
1 -> forall a b. b -> Either a b
Right RoundMode
NearAway
Integer
2 -> forall a b. b -> Either a b
Right RoundMode
ToPosInf
Integer
3 -> forall a b. b -> Either a b
Right RoundMode
ToNegInf
Integer
4 -> forall a b. b -> Either a b
Right RoundMode
ToZero
Integer
_ -> 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 -> forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"checkStatus" [ [Char]
"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 -> [Char] -> Doc
text [Char]
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 forall a. Semigroup a => a -> a -> a
<> ShowFmt
forceExp
str :: [Char]
str = Int -> ShowFmt -> BigFloat -> [Char]
bfToString Int
base ShowFmt
fmt BigFloat
num
fmt :: ShowFmt
fmt = ShowFmt
addPrefix forall a. Semigroup a => a -> a -> a
<> RoundMode -> ShowFmt
showRnd RoundMode
NearEven forall a. Semigroup a => a -> a -> a
<>
case PPOpts -> PPFloatFormat
useFPFormat PPOpts
opts of
FloatFree PPFloatExp
e -> PPFloatExp -> ShowFmt -> ShowFmt
withExp PPFloatExp
e forall a b. (a -> b) -> a -> b
$ Maybe Word -> ShowFmt
showFree
forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
precW
FloatFixed Int
n PPFloatExp
e -> PPFloatExp -> ShowFmt -> ShowFmt
withExp PPFloatExp
e forall a b. (a -> b) -> a -> b
$ Word -> ShowFmt
showFixed forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n
FloatFrac Int
n -> Word -> ShowFmt
showFrac forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n
hacStr :: [Char]
hacStr
| Int
base forall a. Eq a => a -> a -> Bool
== Int
10 = [Char]
trimZeros
| forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
'.' [Char]
str = [Char]
str
| Bool
otherwise = case forall a. (a -> Bool) -> [a] -> ([a], [a])
break (forall a. Eq a => a -> a -> Bool
== Char
'p') [Char]
str of
([Char]
xs,[Char]
ys) -> [Char]
xs forall a. [a] -> [a] -> [a]
++ [Char]
".0" forall a. [a] -> [a] -> [a]
++ [Char]
ys
trimZeros :: [Char]
trimZeros =
case forall a. (a -> Bool) -> [a] -> ([a], [a])
break (forall a. Eq a => a -> a -> Bool
== Char
'.') [Char]
str of
([Char]
xs,Char
'.':[Char]
ys) ->
case forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isDigit) [Char]
ys of
([Char]
frac, [Char]
suffix) -> [Char]
xs forall a. [a] -> [a] -> [a]
++ Char
'.' forall a. a -> [a] -> [a]
: [Char] -> [Char]
processFraction [Char]
frac forall a. [a] -> [a] -> [a]
++ [Char]
suffix
([Char], [Char])
_ -> [Char]
str
processFraction :: [Char] -> [Char]
processFraction [Char]
frac =
case forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Eq a => a -> a -> Bool
== Char
'0') (forall a. [a] -> [a]
reverse [Char]
frac) of
[] -> [Char]
"0"
[Char]
zs -> forall a. [a] -> [a]
reverse [Char]
zs
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 { bfExpWidth :: Integer
bfExpWidth = Integer
e
, bfPrecWidth :: Integer
bfPrecWidth = Integer
p
, bfValue :: BigFloat
bfValue = (BigFloat, Status) -> BigFloat
fpCheckStatus
if Integer
den 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 (forall a. Ratio a -> a
numerator Rational
rat)
den :: Integer
den = forall a. Ratio a -> a
denominator Rational
rat
floatToRational :: String -> BF -> Either EvalError Rational
floatToRational :: [Char] -> BF -> Either EvalError Rational
floatToRational [Char]
fun BF
bf =
case BigFloat -> BFRep
bfToRep (BF -> BigFloat
bfValue BF
bf) of
BFRep
BFNaN -> forall a b. a -> Either a b
Left ([Char] -> EvalError
BadValue [Char]
fun)
BFRep Sign
s BFNum
num ->
case BFNum
num of
BFNum
Inf -> forall a b. a -> Either a b
Left ([Char] -> EvalError
BadValue [Char]
fun)
BFNum
Zero -> forall a b. b -> Either a b
Right Rational
0
Num Integer
i Int64
ev -> forall a b. b -> Either a b
Right case Sign
s of
Sign
Pos -> Rational
ab
Sign
Neg -> forall a. Num a => a -> a
negate Rational
ab
where ab :: Rational
ab = forall a. Num a => Integer -> a
fromInteger Integer
i forall a. Num a => a -> a -> a
* (Rational
2 forall a b. (Fractional a, Integral b) => a -> b -> a
^^ Int64
ev)
floatToInteger :: String -> RoundMode -> BF -> Either EvalError Integer
floatToInteger :: [Char] -> RoundMode -> BF -> Either EvalError Integer
floatToInteger [Char]
fun RoundMode
r BF
fp =
do Rational
rat <- [Char] -> BF -> Either EvalError Rational
floatToRational [Char]
fun BF
fp
forall (f :: * -> *) a. Applicative f => a -> f a
pure case RoundMode
r of
RoundMode
NearEven -> forall a b. (RealFrac a, Integral b) => a -> b
round Rational
rat
RoundMode
NearAway -> if Rational
rat forall a. Ord a => a -> a -> Bool
> Rational
0 then forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
rat else forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
rat
RoundMode
ToPosInf -> forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
rat
RoundMode
ToNegInf -> forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
rat
RoundMode
ToZero -> forall a b. (RealFrac a, Integral b) => a -> b
truncate Rational
rat
RoundMode
_ -> forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"fpCvtToInteger"
[[Char]
"Unexpected rounding mode", forall a. Show a => a -> [Char]
show RoundMode
r]
floatFromBits ::
Integer ->
Integer ->
Integer ->
BF
floatFromBits :: Integer -> Integer -> Integer -> BF
floatFromBits Integer
e Integer
p Integer
bv = BF { bfValue :: BigFloat
bfValue = BFOpts -> Integer -> BigFloat
bfFromBits (Integer -> Integer -> RoundMode -> BFOpts
fpOpts Integer
e Integer
p RoundMode
NearEven) Integer
bv
, bfExpWidth :: Integer
bfExpWidth = Integer
e, bfPrecWidth :: Integer
bfPrecWidth = Integer
p }
floatToBits :: Integer -> Integer -> BigFloat -> Integer
floatToBits :: Integer -> Integer -> BigFloat -> Integer
floatToBits Integer
e Integer
p BigFloat
bf = BFOpts -> BigFloat -> Integer
bfToBits (Integer -> Integer -> RoundMode -> BFOpts
fpOpts Integer
e Integer
p RoundMode
NearEven) BigFloat
bf
floatFromDouble :: Double -> BF
floatFromDouble :: Double -> BF
floatFromDouble = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Integer -> Integer -> BigFloat -> BF
BF (Integer, Integer)
float64ExpPrec forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> BigFloat
bfFromDouble