    {-# Language BlockArguments, OverloadedStrings #-}
    {-# Language BangPatterns #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# Language GADTs #-}
    module What4.Utils.FloatHelpers where

    import qualified Control.Exception as Ex
    import Data.Ratio(numerator,denominator)
    import Data.Hashable
    import GHC.Generics (Generic)
    import GHC.Stack

    import LibBF

    import What4.BaseTypes
    import What4.Panic (panic)

    -- | Rounding modes for IEEE-754 floating point operations.
    data RoundingMode
      = RNE -- ^ Round to nearest even.
      | RNA -- ^ Round to nearest away.
      | RTP -- ^ Round toward plus Infinity.
      | RTN -- ^ Round toward minus Infinity.
      | RTZ -- ^ Round toward zero.
      deriving (RoundingMode -> RoundingMode -> Bool
    (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> Bool) -> Eq RoundingMode
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: RoundingMode -> RoundingMode -> Bool
    == :: RoundingMode -> RoundingMode -> Bool
    $c/= :: RoundingMode -> RoundingMode -> Bool
    /= :: RoundingMode -> RoundingMode -> Bool
    Eq, (forall x. RoundingMode -> Rep RoundingMode x)
    -> (forall x. Rep RoundingMode x -> RoundingMode)
    -> Generic RoundingMode
    forall x. Rep RoundingMode x -> RoundingMode
    forall x. RoundingMode -> Rep RoundingMode x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. RoundingMode -> Rep RoundingMode x
    from :: forall x. RoundingMode -> Rep RoundingMode x
    $cto :: forall x. Rep RoundingMode x -> RoundingMode
    to :: forall x. Rep RoundingMode x -> RoundingMode
    Generic, Eq RoundingMode
    Eq RoundingMode
    -> (RoundingMode -> RoundingMode -> Ordering)
    -> (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> RoundingMode)
    -> (RoundingMode -> RoundingMode -> RoundingMode)
    -> Ord RoundingMode
    RoundingMode -> RoundingMode -> Bool
    RoundingMode -> RoundingMode -> Ordering
    RoundingMode -> RoundingMode -> RoundingMode
    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
    $ccompare :: RoundingMode -> RoundingMode -> Ordering
    compare :: RoundingMode -> RoundingMode -> Ordering
    $c< :: RoundingMode -> RoundingMode -> Bool
    < :: RoundingMode -> RoundingMode -> Bool
    $c<= :: RoundingMode -> RoundingMode -> Bool
    <= :: RoundingMode -> RoundingMode -> Bool
    $c> :: RoundingMode -> RoundingMode -> Bool
    > :: RoundingMode -> RoundingMode -> Bool
    $c>= :: RoundingMode -> RoundingMode -> Bool
    >= :: RoundingMode -> RoundingMode -> Bool
    $cmax :: RoundingMode -> RoundingMode -> RoundingMode
    max :: RoundingMode -> RoundingMode -> RoundingMode
    $cmin :: RoundingMode -> RoundingMode -> RoundingMode
    min :: RoundingMode -> RoundingMode -> RoundingMode
    Ord, Int -> RoundingMode -> ShowS
    [RoundingMode] -> ShowS
    RoundingMode -> [Char]
    (Int -> RoundingMode -> ShowS)
    -> (RoundingMode -> [Char])
    -> ([RoundingMode] -> ShowS)
    -> Show RoundingMode
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> RoundingMode -> ShowS
    showsPrec :: Int -> RoundingMode -> ShowS
    $cshow :: RoundingMode -> [Char]
    show :: RoundingMode -> [Char]
    $cshowList :: [RoundingMode] -> ShowS
    showList :: [RoundingMode] -> ShowS
    Show, Int -> RoundingMode
    RoundingMode -> Int
    RoundingMode -> [RoundingMode]
    RoundingMode -> RoundingMode
    RoundingMode -> RoundingMode -> [RoundingMode]
    RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
    (RoundingMode -> RoundingMode)
    -> (RoundingMode -> RoundingMode)
    -> (Int -> RoundingMode)
    -> (RoundingMode -> Int)
    -> (RoundingMode -> [RoundingMode])
    -> (RoundingMode -> RoundingMode -> [RoundingMode])
    -> (RoundingMode -> RoundingMode -> [RoundingMode])
    -> (RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode])
    -> Enum RoundingMode
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: RoundingMode -> RoundingMode
    succ :: RoundingMode -> RoundingMode
    $cpred :: RoundingMode -> RoundingMode
    pred :: RoundingMode -> RoundingMode
    $ctoEnum :: Int -> RoundingMode
    toEnum :: Int -> RoundingMode
    $cfromEnum :: RoundingMode -> Int
    fromEnum :: RoundingMode -> Int
    $cenumFrom :: RoundingMode -> [RoundingMode]
    enumFrom :: RoundingMode -> [RoundingMode]
    $cenumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]
    enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]
    $cenumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]
    enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]
    $cenumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
    enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
    Enum)

    instance Hashable RoundingMode

    bfStatus :: HasCallStack => (a, Status) -> a
    bfStatus :: forall a. HasCallStack => (a, Status) -> a
    bfStatus (a
    _, Status
    MemError)     = AsyncException -> a
    forall a e. Exception e => e -> a
    Ex.throw AsyncException
    Ex.HeapOverflow
    bfStatus (a
    x,Status
    _)             = a
    x

    fppOpts :: FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
    fppOpts :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
    fppOpts (FloatingPointPrecisionRepr NatRepr eb
    eb NatRepr sb
    sb) RoundingMode
    r =
      Integer -> Integer -> RoundMode -> BFOpts
    fpOpts (NatRepr eb -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr eb
    eb) (NatRepr sb -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr sb
    sb) (RoundingMode -> RoundMode
    toRoundMode RoundingMode
    r)

    toRoundMode :: RoundingMode -> RoundMode
    toRoundMode :: RoundingMode -> RoundMode
    toRoundMode RoundingMode
    RNE = RoundMode
    NearEven
    toRoundMode RoundingMode
    RNA = RoundMode
    NearAway
    toRoundMode RoundingMode
    RTP = RoundMode
    ToPosInf
    toRoundMode RoundingMode
    RTN = RoundMode
    ToNegInf
    toRoundMode RoundingMode
    RTZ = RoundMode
    ToZero

    -- | 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   -> [Char] -> [[Char]] -> BFOpts
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "floatOpts" [ [Char]
    "Invalid Float size"
                                       , [Char]
    "exponent: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> [Char]
    forall a. Show a => a -> [Char]
    show Integer
    e
                                       , [Char]
    "precision: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> [Char]
    forall a. Show a => a -> [Char]
    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 a. a -> Maybe a
    forall (f :: Type -> Type) 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

    -- | Make a floating point number from an integer, using the given rounding mode
    floatFromInteger :: BFOpts -> Integer -> BigFloat
    floatFromInteger :: BFOpts -> Integer -> BigFloat
    floatFromInteger BFOpts
    opts Integer
    i = (BigFloat, Status) -> BigFloat
    forall a. HasCallStack => (a, Status) -> a
    bfStatus (BFOpts -> BigFloat -> (BigFloat, Status)
    bfRoundFloat BFOpts
    opts (Integer -> BigFloat
    bfFromInteger Integer
    i))

    -- | Make a floating point number from a rational, using the given rounding mode
    floatFromRational :: BFOpts -> Rational -> BigFloat
    floatFromRational :: BFOpts -> Rational -> BigFloat
    floatFromRational BFOpts
    opts Rational
    rat = (BigFloat, Status) -> BigFloat
    forall a. HasCallStack => (a, Status) -> a
    bfStatus
        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

      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 :: BigFloat -> Maybe Rational
    floatToRational :: BigFloat -> Maybe Rational
    floatToRational BigFloat
    bf =
      case BigFloat -> BFRep
    bfToRep BigFloat
    bf of
        BFRep
    BFNaN -> Maybe Rational
    forall a. Maybe a
    Nothing
        BFRep Sign
    s BFNum
    num ->
          case BFNum
    num of
            BFNum
    Inf  -> Maybe Rational
    forall a. Maybe a
    Nothing
            BFNum
    Zero -> Rational -> Maybe Rational
    forall a. a -> Maybe a
    Just Rational
    0
            Num Integer
    i Int64
    ev -> Rational -> Maybe Rational
    forall a. a -> Maybe a
    Just 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 :: RoundingMode -> BigFloat -> Maybe Integer
    floatToInteger :: RoundingMode -> BigFloat -> Maybe Integer
    floatToInteger RoundingMode
    r BigFloat
    fp =
      do Rational
    rat <- BigFloat -> Maybe Rational
    floatToRational BigFloat
    fp
         Integer -> Maybe Integer
    forall a. a -> Maybe a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure case RoundingMode
    r of
                RoundingMode
    RNE -> Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    round Rational
    rat
                RoundingMode
    RNA -> if Rational
    rat Rational -> Rational -> Bool
    forall a. Ord a => a -> a -> Bool
    > Rational
    0 then Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    ceiling Rational
    rat else Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    floor Rational
    rat
                RoundingMode
    RTP -> Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    ceiling Rational
    rat
                RoundingMode
    RTN -> Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    floor Rational
    rat
                RoundingMode
    RTZ -> Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    truncate Rational
    rat

    floatRoundToInt :: HasCallStack =>
      FloatPrecisionRepr fpp -> RoundingMode -> BigFloat -> BigFloat
    floatRoundToInt :: forall (fpp :: FloatPrecision).
    HasCallStack =>
    FloatPrecisionRepr fpp -> RoundingMode -> BigFloat -> BigFloat
    floatRoundToInt FloatPrecisionRepr fpp
    fpp RoundingMode
    r BigFloat
    bf =
      (BigFloat, Status) -> BigFloat
    forall a. HasCallStack => (a, Status) -> a
    bfStatus (BFOpts -> BigFloat -> (BigFloat, Status)
    bfRoundFloat (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
    forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
    fppOpts FloatPrecisionRepr fpp
    fpp RoundingMode
    r) ((BigFloat, Status) -> BigFloat
    forall a. HasCallStack => (a, Status) -> a
    bfStatus (RoundMode -> BigFloat -> (BigFloat, Status)
    bfRoundInt (RoundingMode -> RoundMode
    toRoundMode RoundingMode
    r) BigFloat
    bf)))