    {-# 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
      }

    -- | 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] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Integer -> [Char]
    forall a. Show a => a -> [Char]
    show Integer
    e
                                       , [Char]
    "precision: " [Char] -> [Char] -> [Char]
    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 :: * -> *) 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  -> [Char] -> [[Char]] -> BigFloat
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "checkStatus" [ [Char]
    "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 -> [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 ShowFmt -> ShowFmt -> ShowFmt
    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 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 :: [Char]
    hacStr
        | Int
    base Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    10   = [Char]
    trimZeros
        | Char -> [Char] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    elem Char
    '.' [Char]
    str = [Char]
    str
        | Bool
    otherwise = case (Char -> Bool) -> [Char] -> ([Char], [Char])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    'p') [Char]
    str of
                        ([Char]
    xs,[Char]
    ys) -> [Char]
    xs [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ".0" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ys

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

      processFraction :: [Char] -> [Char]
    processFraction [Char]
    frac =
        case (Char -> Bool) -> [Char] -> [Char]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '0') ([Char] -> [Char]
    forall a. [a] -> [a]
    reverse [Char]
    frac) of
          [] -> [Char]
    "0"
          [Char]
    zs -> [Char] -> [Char]
    forall a. [a] -> [a]
    reverse [Char]
    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 { 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 :: [Char] -> BF -> Either EvalError Rational
    floatToRational [Char]
    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 ([Char] -> EvalError
    BadValue [Char]
    fun)
        BFRep Sign
    s BFNum
    num ->
          case BFNum
    num of
            BFNum
    Inf  -> EvalError -> Either EvalError Rational
    forall a b. a -> Either a b
    Left ([Char] -> EvalError
    BadValue [Char]
    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 :: [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
         Integer -> Either EvalError Integer
    forall a. a -> Either EvalError a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure case RoundMode
    r of
                RoundMode
    NearEven -> Rational -> Integer
    forall b. Integral b => Rational -> b
    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 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
                RoundMode
    ToPosInf -> Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    ceiling Rational
    rat
                RoundMode
    ToNegInf -> Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    floor Rational
    rat
                RoundMode
    ToZero   -> Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    truncate Rational
    rat
                RoundMode
    _        -> [Char] -> [[Char]] -> Integer
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "fpCvtToInteger"
                                  [[Char]
    "Unexpected rounding mode", RoundMode -> [Char]
    forall a. Show a => a -> [Char]
    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 { 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

    -- | Create a 64-bit IEEE-754 float.
    floatFromDouble :: Double -> BF
    floatFromDouble :: Double -> BF
    floatFromDouble = (Integer -> Integer -> BigFloat -> BF)
    -> (Integer, Integer) -> BigFloat -> BF
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Integer -> Integer -> BigFloat -> BF
    BF (Integer, Integer)
    float64ExpPrec (BigFloat -> BF) -> (Double -> BigFloat) -> Double -> BF
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Double -> BigFloat
    bfFromDouble