{-# 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.Backend.Monad( EvalError(..) )


data BF = BF
  { BF -> Integer
bfExpWidth  :: !Integer
  , BF -> Integer
bfPrecWidth :: !Integer
  , BF -> BigFloat
bfValue     :: !BigFloat
  }


-- | Make LibBF options for the given precision and rounding mode.
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 <- (Word -> 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 Word -> 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



-- | Mapping from the rounding modes defined in the `Float.cry` to
-- the rounding modes of `LibBF`.
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)

-- | Check that we didn't get an unexpected status.
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


-- | Pretty print a float
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 Word -> ShowFmt
showFree
                                   (Maybe Word -> ShowFmt) -> Maybe Word -> ShowFmt
forall a b. (a -> b) -> a -> b
$ Word -> Maybe Word
forall a. a -> Maybe a
Just (Word -> Maybe Word) -> Word -> Maybe Word
forall a b. (a -> b) -> a -> b
$ Integer -> Word
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
$ Word -> ShowFmt
showFixed (Word -> ShowFmt) -> Word -> ShowFmt
forall a b. (a -> b) -> a -> b
$ Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n
          FloatFrac Int
n    -> Word -> ShowFmt
showFrac (Word -> ShowFmt) -> Word -> ShowFmt
forall a b. (a -> b) -> a -> b
$ Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n

  -- non-base 10 literals are not overloaded so we add an explicit
  -- .0 if one is not present.  Moreover, we trim any extra zeros
  -- that appear in a decimal representation.
  hacStr :: String
hacStr
    | Int
base Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
10   = String
trimZeros
    | 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

  trimZeros :: String
trimZeros =
    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
'.') String
str of
      (String
xs,Char
'.':String
ys) ->
        case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isDigit) String
ys of
          (String
frac, String
suffix) -> String
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char
'.' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
processFraction String
frac String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
suffix
      (String, String)
_ -> String
str

  processFraction :: String -> String
processFraction String
frac =
    case (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'0') (String -> String
forall a. [a] -> [a]
reverse String
frac) of
      [] -> String
"0"
      String
zs -> String -> String
forall a. [a] -> [a]
reverse String
zs

-- | Make a literal
fpLit ::
  Integer     {- ^ Exponent width -} ->
  Integer     {- ^ Precision width -} ->
  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

-- | Make a floating point number from a rational, using the given rounding mode
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


-- | Convert a floating point number to a rational, if possible.
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)


-- | Convert a floating point number to an integer, if possible.
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 {- ^ Exponent width -} ->
  Integer {- ^ Precision widht -} ->
  Integer {- ^ Raw bits -} ->
  BF
floatFromBits :: Integer -> Integer -> Integer -> BF
floatFromBits Integer
e Integer
p Integer
bv = BF :: Integer -> Integer -> BigFloat -> BF
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 }


-- | Turn a float into raw bits.
-- @NaN@ is represented as a positive "quiet" @NaN@
-- (most significant bit in the significand is set, the rest of it is 0)
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