    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Core.Sized
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Type-level sized floats.
    -----------------------------------------------------------------------------

    {-# LANGUAGE DataKinds            #-}
    {-# LANGUAGE FlexibleInstances    #-}
    {-# LANGUAGE ScopedTypeVariables  #-}
    {-# LANGUAGE TypeApplications     #-}
    {-# LANGUAGE TypeFamilies         #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Core.SizedFloats (
            -- * Type-sized floats
              FloatingPoint(..), FP(..), FPHalf, FPBFloat, FPSingle, FPDouble, FPQuad

            -- * Constructing values
            , fpFromRawRep, fpFromBigFloat, fpNaN, fpInf, fpZero

            -- * Operations
            , fpFromInteger, fpFromRational, fpFromFloat, fpFromDouble, fpEncodeFloat

            -- * Internal operations
           , fprCompareObject, fprToSMTLib2, mkBFOpts, bfToString, bfRemoveRedundantExp
           ) where

    import Data.Char (intToDigit)
    import Data.List (isSuffixOf)
    import Data.Proxy
    import GHC.TypeLits

    import Data.Bits
    import Data.Ratio
    import Numeric

    import Data.SBV.Core.Kind
    import Data.SBV.Utils.Numeric (floatToWord)

    import LibBF (BigFloat, BFOpts, RoundMode, Status)
    import qualified LibBF as BF

    -- | A floating point value, indexed by its exponent and significand sizes.
    --
    --   An IEEE SP is @FloatingPoint  8 24@
    --           DP is @FloatingPoint 11 53@
    -- etc.
    newtype FloatingPoint (eb :: Nat) (sb :: Nat) = FloatingPoint FP
                                                  deriving (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool)
    -> (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool)
    -> Eq (FloatingPoint eb sb)
    forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    == :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    $c/= :: forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    /= :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    Eq, Eq (FloatingPoint eb sb)
    Eq (FloatingPoint eb sb) =>
    (FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering)
    -> (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool)
    -> (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool)
    -> (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool)
    -> (FloatingPoint eb sb -> FloatingPoint eb sb -> Bool)
    -> (FloatingPoint eb sb
        -> FloatingPoint eb sb -> FloatingPoint eb sb)
    -> (FloatingPoint eb sb
        -> FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Ord (FloatingPoint eb sb)
    FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering
    FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). Eq (FloatingPoint eb sb)
    forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering
    forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    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 :: forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering
    compare :: FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering
    $c< :: forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    < :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    $c<= :: forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    <= :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    $c> :: forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    > :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    $c>= :: forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    >= :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
    $cmax :: forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    max :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    $cmin :: forall (eb :: Nat) (sb :: Nat).
    FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    min :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    Ord)

    -- | Abbreviation for IEEE half precision float, bit width 16 = 5 + 11.
    type FPHalf = FloatingPoint 5 11

    -- | Abbreviation for brain-float precision float, bit width 16 = 8 + 8.
    type FPBFloat = FloatingPoint 8 8

    -- | Abbreviation for IEEE single precision float, bit width 32 = 8 + 24.
    type FPSingle = FloatingPoint 8 24

    -- | Abbreviation for IEEE double precision float, bit width 64 = 11 + 53.
    type FPDouble = FloatingPoint 11 53

    -- | Abbreviation for IEEE quadruble precision float, bit width 128 = 15 + 113.
    type FPQuad = FloatingPoint 15 113

    -- | Show instance for Floats. By default we print in base 10, with standard scientific notation.
    instance Show (FloatingPoint eb sb) where
      show :: FloatingPoint eb sb -> String
    show (FloatingPoint FP
    r) = FP -> String
    forall a. Show a => a -> String
    show FP
    r

    -- | Internal representation of a parameterized float.
    --
    -- A note on cardinality: If we have eb exponent bits, and sb significand bits,
    -- then the total number of floats is 2^sb*(2^eb-1) + 3: All exponents except 11..11
    -- is allowed. So we get, 2^eb-1, different combinations, each with a sign, giving
    -- us 2^sb*(2^eb-1) totals. Then we have two infinities, and one NaN, adding 3 more.
    data FP = FP { FP -> Int
    fpExponentSize    :: Int
                 , FP -> Int
    fpSignificandSize :: Int
                 , FP -> BigFloat
    fpValue           :: BigFloat
                 }
                 deriving (Eq FP
    Eq FP =>
    (FP -> FP -> Ordering)
    -> (FP -> FP -> Bool)
    -> (FP -> FP -> Bool)
    -> (FP -> FP -> Bool)
    -> (FP -> FP -> Bool)
    -> (FP -> FP -> FP)
    -> (FP -> FP -> FP)
    -> Ord FP
    FP -> FP -> Bool
    FP -> FP -> Ordering
    FP -> FP -> FP
    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 :: FP -> FP -> Ordering
    compare :: FP -> FP -> Ordering
    $c< :: FP -> FP -> Bool
    < :: FP -> FP -> Bool
    $c<= :: FP -> FP -> Bool
    <= :: FP -> FP -> Bool
    $c> :: FP -> FP -> Bool
    > :: FP -> FP -> Bool
    $c>= :: FP -> FP -> Bool
    >= :: FP -> FP -> Bool
    $cmax :: FP -> FP -> FP
    max :: FP -> FP -> FP
    $cmin :: FP -> FP -> FP
    min :: FP -> FP -> FP
    Ord, FP -> FP -> Bool
    (FP -> FP -> Bool) -> (FP -> FP -> Bool) -> Eq FP
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: FP -> FP -> Bool
    == :: FP -> FP -> Bool
    $c/= :: FP -> FP -> Bool
    /= :: FP -> FP -> Bool
    Eq)

    instance Show FP where
      show :: FP -> String
    show = ShowS
    bfRemoveRedundantExp ShowS -> (FP -> String) -> FP -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Bool -> Bool -> FP -> String
    bfToString Int
    10 Bool
    False Bool
    False

    -- | Remove redundant p+0 etc.
    bfRemoveRedundantExp :: String -> String
    bfRemoveRedundantExp :: ShowS
    bfRemoveRedundantExp String
    v = [String] -> String
    walk [String]
    useless
      where walk :: [String] -> String
    walk []              = String
    v
            walk (String
    s:[String]
    ss)
             | String
    s String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isSuffixOf` String
    v = ShowS
    forall a. [a] -> [a]
    reverse ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> ShowS
    forall a. Int -> [a] -> [a]
    drop (String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    s) ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ShowS
    forall a. [a] -> [a]
    reverse ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ String
    v
             | Bool
    True             = [String] -> String
    walk [String]
    ss

            -- these suffixes are useless, drop them
            useless :: [String]
    useless = [Char
    c Char -> ShowS
    forall a. a -> [a] -> [a]
    : String
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "0" | Char
    c <- String
    "pe@", String
    s <- [String
    "+", String
    "-", String
    ""]]

    -- | Show a big float in the base given.
    -- NB. Do not be tempted to use BF.showFreeMin below; it produces arguably correct
    -- but very confusing results. See <https://github.com/GaloisInc/cryptol/issues/1089>
    -- for a discussion of the issues.
    bfToString :: Int -> Bool -> Bool -> FP -> String
    bfToString :: Int -> Bool -> Bool -> FP -> String
    bfToString Int
    b Bool
    withPrefix Bool
    forceExponent (FP Int
    _ Int
    sb BigFloat
    a)
      | BigFloat -> Bool
    BF.bfIsNaN  BigFloat
    a = String
    "NaN"
      | BigFloat -> Bool
    BF.bfIsInf  BigFloat
    a = if BigFloat -> Bool
    BF.bfIsPos BigFloat
    a then String
    "Infinity" else String
    "-Infinity"
      | BigFloat -> Bool
    BF.bfIsZero BigFloat
    a = if BigFloat -> Bool
    BF.bfIsPos BigFloat
    a then String
    "0.0"      else String
    "-0.0"
      | Bool
    True          = ShowS
    trimZeros ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ Int -> ShowFmt -> BigFloat -> String
    BF.bfToString Int
    b ShowFmt
    opts' BigFloat
    a
      where opts :: ShowFmt
    opts = RoundMode -> ShowFmt
    BF.showRnd RoundMode
    BF.NearEven ShowFmt -> ShowFmt -> ShowFmt
    forall a. Semigroup a => a -> a -> a
    <> Maybe Word -> ShowFmt
    BF.showFree (Word -> Maybe Word
    forall a. a -> Maybe a
    Just (Int -> Word
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    sb))
            opts' :: ShowFmt
    opts' = case (Bool
    withPrefix, Bool
    forceExponent) of
                      (Bool
    False, Bool
    False) ->                                 ShowFmt
    opts
                      (Bool
    False, Bool
    True ) ->                 ShowFmt
    BF.forceExp  ShowFmt -> ShowFmt -> ShowFmt
    forall a. Semigroup a => a -> a -> a
    <> ShowFmt
    opts
                      (Bool
    True,  Bool
    False) -> ShowFmt
    BF.addPrefix                 ShowFmt -> ShowFmt -> ShowFmt
    forall a. Semigroup a => a -> a -> a
    <> ShowFmt
    opts
                      (Bool
    True,  Bool
    True ) -> ShowFmt
    BF.addPrefix ShowFmt -> ShowFmt -> ShowFmt
    forall a. Semigroup a => a -> a -> a
    <> ShowFmt
    BF.forceExp  ShowFmt -> ShowFmt -> ShowFmt
    forall a. Semigroup a => a -> a -> a
    <> ShowFmt
    opts

            -- In base 10, exponent starts with 'e'. Otherwise (2, 8, 16) it starts with 'p'
            expChar :: Char
    expChar = if Int
    b Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    10 then Char
    'e' else Char
    'p'

            trimZeros :: ShowS
    trimZeros String
    s
              | Char
    '.' Char -> String -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` String
    s = case (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    expChar) String
    s of
                                (String
    pre, String
    post) -> let pre' :: String
    pre' = ShowS
    forall a. [a] -> [a]
    reverse ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ case (Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '0') ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ ShowS
    forall a. [a] -> [a]
    reverse String
    pre of
                                                                      res :: String
    res@(Char
    '.':String
    _) -> Char
    '0' Char -> ShowS
    forall a. a -> [a] -> [a]
    : String
    res
                                                                      String
    res         -> String
    res
                                               in String
    pre' String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    post
              | Bool
    True         = String
    s

    -- | Default options for BF options.
    mkBFOpts :: Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts :: forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts a
    eb a
    sb RoundMode
    rm = BFOpts
    BF.allowSubnormal BFOpts -> BFOpts -> BFOpts
    forall a. Semigroup a => a -> a -> a
    <> RoundMode -> BFOpts
    BF.rnd RoundMode
    rm BFOpts -> BFOpts -> BFOpts
    forall a. Semigroup a => a -> a -> a
    <> Int -> BFOpts
    BF.expBits (a -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    eb) BFOpts -> BFOpts -> BFOpts
    forall a. Semigroup a => a -> a -> a
    <> Word -> BFOpts
    BF.precBits (a -> Word
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    sb)

    -- | Construct a float, by appropriately rounding
    fpFromBigFloat :: Int -> Int -> BigFloat -> FP
    fpFromBigFloat :: Int -> Int -> BigFloat -> FP
    fpFromBigFloat Int
    eb Int
    sb BigFloat
    r = Int -> Int -> BigFloat -> FP
    FP Int
    eb Int
    sb (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ (BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
    forall a b. (a -> b) -> a -> b
    $ BFOpts -> BigFloat -> (BigFloat, Status)
    BF.bfRoundFloat (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    eb Int
    sb RoundMode
    BF.NearEven) BigFloat
    r

    -- | Convert from an sign/exponent/mantissa representation to a float. The values are the integers
    -- representing the bit-patterns of these values, i.e., the raw representation. We assume that these
    -- integers fit into the ranges given, i.e., no overflow checking is done here.
    fpFromRawRep :: Bool -> (Integer, Int) -> (Integer, Int) -> FP
    fpFromRawRep :: Bool -> (Integer, Int) -> (Integer, Int) -> FP
    fpFromRawRep Bool
    sign (Integer
    e, Int
    eb) (Integer
    s, Int
    sb) = Int -> Int -> BigFloat -> FP
    FP Int
    eb Int
    sb (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ BFOpts -> Integer -> BigFloat
    BF.bfFromBits (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    eb Int
    sb RoundMode
    BF.NearEven) Integer
    val
      where es, val :: Integer
            es :: Integer
    es = (Integer
    e Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftL` (Int
    sb Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)) Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Integer
    s
            val :: Integer
    val | Bool
    sign = (Integer
    1 Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftL` (Int
    eb Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    sb Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)) Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Integer
    es
                | Bool
    True =                                Integer
    es

    -- | Make NaN. Exponent is all 1s. Significand is non-zero. The sign is irrelevant.
    fpNaN :: Int -> Int -> FP
    fpNaN :: Int -> Int -> FP
    fpNaN Int
    eb Int
    sb = Int -> Int -> BigFloat -> FP
    fpFromBigFloat Int
    eb Int
    sb BigFloat
    BF.bfNaN

    -- | Make Infinity. Exponent is all 1s. Significand is 0.
    fpInf :: Bool -> Int -> Int -> FP
    fpInf :: Bool -> Int -> Int -> FP
    fpInf Bool
    sign Int
    eb Int
    sb = Int -> Int -> BigFloat -> FP
    fpFromBigFloat Int
    eb Int
    sb (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ if Bool
    sign then BigFloat
    BF.bfNegInf else BigFloat
    BF.bfPosInf

    -- | Make a signed zero.
    fpZero :: Bool -> Int -> Int -> FP
    fpZero :: Bool -> Int -> Int -> FP
    fpZero Bool
    sign Int
    eb Int
    sb = Int -> Int -> BigFloat -> FP
    fpFromBigFloat Int
    eb Int
    sb (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ if Bool
    sign then BigFloat
    BF.bfNegZero else BigFloat
    BF.bfPosZero

    -- | Make from an integer value.
    fpFromInteger :: Int -> Int -> Integer -> FP
    fpFromInteger :: Int -> Int -> Integer -> FP
    fpFromInteger Int
    eb Int
    sb Integer
    iv = Int -> Int -> BigFloat -> FP
    fpFromBigFloat Int
    eb Int
    sb (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ Integer -> BigFloat
    BF.bfFromInteger Integer
    iv

    -- | Make a generalized floating-point value from a 'Rational'.
    fpFromRational :: Int -> Int -> Rational -> FP
    fpFromRational :: Int -> Int -> Rational -> FP
    fpFromRational Int
    eb Int
    sb Rational
    r = Int -> Int -> BigFloat -> FP
    FP Int
    eb Int
    sb (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ (BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
    forall a b. (a -> b) -> a -> b
    $ BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    BF.bfDiv (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    eb Int
    sb RoundMode
    BF.NearEven) (Integer -> BigFloat
    BF.bfFromInteger (Rational -> Integer
    forall a. Ratio a -> a
    numerator Rational
    r))
                                                                                    (Integer -> BigFloat
    BF.bfFromInteger (Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    r))

    -- | Represent the FP in SMTLib2 format
    fprToSMTLib2 :: FP -> String
    fprToSMTLib2 :: FP -> String
    fprToSMTLib2 (FP Int
    eb Int
    sb BigFloat
    r)
      | BigFloat -> Bool
    BF.bfIsNaN  BigFloat
    r = ShowS
    as String
    "NaN"
      | BigFloat -> Bool
    BF.bfIsInf  BigFloat
    r = ShowS
    as ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ if BigFloat -> Bool
    BF.bfIsPos BigFloat
    r then String
    "+oo"   else String
    "-oo"
      | BigFloat -> Bool
    BF.bfIsZero BigFloat
    r = ShowS
    as ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ if BigFloat -> Bool
    BF.bfIsPos BigFloat
    r then String
    "+zero" else String
    "-zero"
      | Bool
    True          = String
    generic
     where e :: String
    e = Int -> String
    forall a. Show a => a -> String
    show Int
    eb
           s :: String
    s = Int -> String
    forall a. Show a => a -> String
    show Int
    sb

           bits :: Integer
    bits            = BFOpts -> BigFloat -> Integer
    BF.bfToBits (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    eb Int
    sb RoundMode
    BF.NearEven) BigFloat
    r
           significandMask :: Integer
    significandMask = (Integer
    1 :: Integer) Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftL` (Int
    sb Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1
           exponentMask :: Integer
    exponentMask    = (Integer
    1 :: Integer) Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    eb       Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1

           fpSign :: Bool
    fpSign          = Integer
    bits Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    `testBit` (Int
    eb Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    sb Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)
           fpExponent :: Integer
    fpExponent      = (Integer
    bits Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftR` (Int
    sb Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)) Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Integer
    exponentMask
           fpSignificand :: Integer
    fpSignificand   = Integer
    bits                     Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Integer
    significandMask

           generic :: String
    generic = String
    "(fp " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [if Bool
    fpSign then String
    "#b1" else String
    "#b0", Int -> Integer -> String
    forall {a}. Integral a => Int -> a -> String
    mkB Int
    eb Integer
    fpExponent, Int -> Integer -> String
    forall {a}. Integral a => Int -> a -> String
    mkB (Int
    sb Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Integer
    fpSignificand] String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

           as :: ShowS
    as String
    x = String
    "(_ " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    e String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

           mkB :: Int -> a -> String
    mkB Int
    sz a
    val = String
    "#b" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> ShowS
    pad Int
    sz (a -> (Int -> Char) -> a -> ShowS
    forall a. Integral a => a -> (Int -> Char) -> a -> ShowS
    showIntAtBase a
    2 Int -> Char
    intToDigit a
    val String
    "")
           pad :: Int -> ShowS
    pad Int
    l String
    str = Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (Int
    l Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    str) Char
    '0' String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    str

    -- | Structural comparison only, for internal map indexes
    fprCompareObject :: FP -> FP -> Ordering
    fprCompareObject :: FP -> FP -> Ordering
    fprCompareObject (FP Int
    eb Int
    sb BigFloat
    a) (FP Int
    eb' Int
    sb' BigFloat
    b) = case (Int
    eb, Int
    sb) (Int, Int) -> (Int, Int) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` (Int
    eb', Int
    sb') of
                                                     Ordering
    LT -> Ordering
    LT
                                                     Ordering
    GT -> Ordering
    GT
                                                     Ordering
    EQ -> BigFloat
    a BigFloat -> BigFloat -> Ordering
    `BF.bfCompare` BigFloat
    b

    -- | Compute the signum of a big float
    bfSignum :: BigFloat -> BigFloat
    bfSignum :: BigFloat -> BigFloat
    bfSignum BigFloat
    r | BigFloat -> Bool
    BF.bfIsNaN  BigFloat
    r = BigFloat
    r
               | BigFloat -> Bool
    BF.bfIsZero BigFloat
    r = BigFloat
    r
               | BigFloat -> Bool
    BF.bfIsPos  BigFloat
    r = Integer -> BigFloat
    BF.bfFromInteger Integer
    1
               | Bool
    True          = Integer -> BigFloat
    BF.bfFromInteger (-Integer
    1)

    -- | Num instance for big-floats
    instance Num FP where
      + :: FP -> FP -> FP
    (+)         = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> FP -> FP -> FP
    lift2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    BF.bfAdd
      (-)         = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> FP -> FP -> FP
    lift2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    BF.bfSub
      * :: FP -> FP -> FP
    (*)         = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> FP -> FP -> FP
    lift2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    BF.bfMul
      abs :: FP -> FP
    abs         = (BigFloat -> BigFloat) -> FP -> FP
    lift1 BigFloat -> BigFloat
    BF.bfAbs
      signum :: FP -> FP
    signum      = (BigFloat -> BigFloat) -> FP -> FP
    lift1 BigFloat -> BigFloat
    bfSignum
      fromInteger :: Integer -> FP
    fromInteger = String -> Integer -> FP
    forall a. HasCallStack => String -> a
    error String
    "FP.fromInteger: Not supported for arbitrary floats. Use fpFromInteger instead, specifying the precision"
      negate :: FP -> FP
    negate      = (BigFloat -> BigFloat) -> FP -> FP
    lift1 BigFloat -> BigFloat
    BF.bfNeg

    -- | Fractional instance for big-floats
    instance Fractional FP where
      fromRational :: Rational -> FP
    fromRational = String -> Rational -> FP
    forall a. HasCallStack => String -> a
    error String
    "FP.fromRational: Not supported for arbitrary floats. Use fpFromRational instead, specifying the precision"
      / :: FP -> FP -> FP
    (/)          = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> FP -> FP -> FP
    lift2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    BF.bfDiv

    -- | Floating instance for big-floats
    instance Floating FP where
      sqrt :: FP -> FP
    sqrt (FP Int
    eb Int
    sb BigFloat
    a)      = Int -> Int -> BigFloat -> FP
    FP Int
    eb Int
    sb (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ (BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
    forall a b. (a -> b) -> a -> b
    $ BFOpts -> BigFloat -> (BigFloat, Status)
    BF.bfSqrt (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    eb Int
    sb RoundMode
    BF.NearEven) BigFloat
    a
      FP Int
    eb Int
    sb BigFloat
    a ** :: FP -> FP -> FP
    ** FP Int
    _ Int
    _ BigFloat
    b = Int -> Int -> BigFloat -> FP
    FP Int
    eb Int
    sb (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ (BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
    forall a b. (a -> b) -> a -> b
    $ BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    BF.bfPow  (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    eb Int
    sb RoundMode
    BF.NearEven) BigFloat
    a BigFloat
    b

      pi :: FP
    pi    = String -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.pi"
      exp :: FP -> FP
    exp   = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.exp"
      log :: FP -> FP
    log   = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.log"
      sin :: FP -> FP
    sin   = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.sin"
      cos :: FP -> FP
    cos   = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.cos"
      tan :: FP -> FP
    tan   = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.tan"
      asin :: FP -> FP
    asin  = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.asin"
      acos :: FP -> FP
    acos  = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.acos"
      atan :: FP -> FP
    atan  = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.atan"
      sinh :: FP -> FP
    sinh  = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.sinh"
      cosh :: FP -> FP
    cosh  = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.cosh"
      tanh :: FP -> FP
    tanh  = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.tanh"
      asinh :: FP -> FP
    asinh = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.asinh"
      acosh :: FP -> FP
    acosh = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.acosh"
      atanh :: FP -> FP
    atanh = String -> FP -> FP
    forall a. String -> a
    unsupported String
    "Floating.FP.atanh"

    -- | Real-float instance for big-floats. Beware! Some of these aren't really all that well tested.
    instance RealFloat FP where
      floatRadix :: FP -> Integer
    floatRadix     FP
    _            = Integer
    2
      floatDigits :: FP -> Int
    floatDigits    (FP Int
    _  Int
    sb BigFloat
    _) = Int
    sb
      floatRange :: FP -> (Int, Int)
    floatRange     (FP Int
    eb Int
    _  BigFloat
    _) = (Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (-Integer
    vInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    3), Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Integer
    v)
         where v :: Integer
               v :: Integer
    v = Integer
    2 Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ ((Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    eb :: Integer) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1)

      isNaN :: FP -> Bool
    isNaN          (FP Int
    _ Int
    _   BigFloat
    r) = BigFloat -> Bool
    BF.bfIsNaN BigFloat
    r
      isInfinite :: FP -> Bool
    isInfinite     (FP Int
    _ Int
    _   BigFloat
    r) = BigFloat -> Bool
    BF.bfIsInf BigFloat
    r
      isDenormalized :: FP -> Bool
    isDenormalized (FP Int
    eb Int
    sb BigFloat
    r) = BFOpts -> BigFloat -> Bool
    BF.bfIsSubnormal (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    eb Int
    sb RoundMode
    BF.NearEven) BigFloat
    r
      isNegativeZero :: FP -> Bool
    isNegativeZero (FP Int
    _  Int
    _  BigFloat
    r) = BigFloat -> Bool
    BF.bfIsZero BigFloat
    r Bool -> Bool -> Bool
    && BigFloat -> Bool
    BF.bfIsNeg BigFloat
    r
      isIEEE :: FP -> Bool
    isIEEE         FP
    _            = Bool
    True

      decodeFloat :: FP -> (Integer, Int)
    decodeFloat i :: FP
    i@(FP Int
    _ Int
    _ BigFloat
    r) = case BigFloat -> BFRep
    BF.bfToRep BigFloat
    r of
                                   BFRep
    BF.BFNaN     -> Double -> (Integer, Int)
    forall a. RealFloat a => a -> (Integer, Int)
    decodeFloat (Double
    0Double -> Double -> Double
    forall a. Fractional a => a -> a -> a
    /Double
    0 :: Double)
                                   BF.BFRep Sign
    s BFNum
    n -> case BFNum
    n of
                                                    BFNum
    BF.Zero    -> (Integer
    0, Int
    0)
                                                    BFNum
    BF.Inf     -> let (Int
    _, Int
    m) = FP -> (Int, Int)
    forall a. RealFloat a => a -> (Int, Int)
    floatRange FP
    i
                                                                      x :: Integer
    x = (Integer
    2 :: Integer) Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int
    mInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1)
                                                                  in (if Sign
    s Sign -> Sign -> Bool
    forall a. Eq a => a -> a -> Bool
    == Sign
    BF.Neg then -Integer
    x else Integer
    x, Int
    0)
                                                    BF.Num Integer
    x Int64
    y -> -- The value here is x * 2^y
                                                                   (if Sign
    s Sign -> Sign -> Bool
    forall a. Eq a => a -> a -> Bool
    == Sign
    BF.Neg then -Integer
    x else Integer
    x, Int64 -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int64
    y)

      encodeFloat :: Integer -> Int -> FP
    encodeFloat = String -> Integer -> Int -> FP
    forall a. HasCallStack => String -> a
    error String
    "FP.encodeFloat: Not supported for arbitrary floats. Use fpEncodeFloat instead, specifying the precision"

    -- | Encode from exponent/mantissa form to a float representation. Corresponds to 'encodeFloat' in Haskell.
    fpEncodeFloat :: Int -> Int -> Integer -> Int -> FP
    fpEncodeFloat :: Int -> Int -> Integer -> Int -> FP
    fpEncodeFloat Int
    eb Int
    sb Integer
    m Int
    n | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    0 = Int -> Int -> Rational -> FP
    fpFromRational Int
    eb Int
    sb (Integer
    m      Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    n')
                            | Bool
    True  = Int -> Int -> Rational -> FP
    fpFromRational Int
    eb Int
    sb (Integer
    m Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    n' Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    1)
        where n' :: Integer
              n' :: Integer
    n' = (Integer
    2 :: Integer) Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Integer -> Integer
    forall a. Num a => a -> a
    abs (Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    n :: Integer)

    -- | Real instance for big-floats. Beware, not that well tested!
    instance Real FP where
      toRational :: FP -> Rational
    toRational FP
    i
         | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    0  = Integer
    m Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    2 Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int
    n Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    1
         | Bool
    True    = Integer
    m Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    2 Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int -> Int
    forall a. Num a => a -> a
    abs Int
    n
        where (Integer
    m, Int
    n) = FP -> (Integer, Int)
    forall a. RealFloat a => a -> (Integer, Int)
    decodeFloat FP
    i

    -- | Real-frac instance for big-floats. Beware, not that well tested!
    instance RealFrac FP where
      properFraction :: forall b. Integral b => FP -> (b, FP)
    properFraction (FP Int
    eb Int
    sb BigFloat
    r) = case RoundMode -> BigFloat -> (BigFloat, Status)
    BF.bfRoundInt RoundMode
    BF.ToNegInf BigFloat
    r of
                                      (BigFloat
    r', Status
    BF.Ok) | BigFloat -> Maybe Sign
    BF.bfSign BigFloat
    r Maybe Sign -> Maybe Sign -> Bool
    forall a. Eq a => a -> a -> Bool
    == BigFloat -> Maybe Sign
    BF.bfSign BigFloat
    r' -> (BigFloat -> b
    getInt BigFloat
    r', Int -> Int -> BigFloat -> FP
    FP Int
    eb Int
    sb BigFloat
    r FP -> FP -> FP
    forall a. Num a => a -> a -> a
    - Int -> Int -> BigFloat -> FP
    FP Int
    eb Int
    sb BigFloat
    r')
                                      (BigFloat, Status)
    x -> String -> (b, FP)
    forall a. HasCallStack => String -> a
    error (String -> (b, FP)) -> String -> (b, FP)
    forall a b. (a -> b) -> a -> b
    $ String
    "RealFrac.FP.properFraction: Failed to convert: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (BigFloat, (BigFloat, Status)) -> String
    forall a. Show a => a -> String
    show (BigFloat
    r, (BigFloat, Status)
    x)
           where getInt :: BigFloat -> b
    getInt BigFloat
    x = case BigFloat -> BFRep
    BF.bfToRep BigFloat
    x of
                              BFRep
    BF.BFNaN     -> String -> b
    forall a. HasCallStack => String -> a
    error (String -> b) -> String -> b
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.FloatingPoint.properFraction: Failed to convert: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (BigFloat, BigFloat) -> String
    forall a. Show a => a -> String
    show (BigFloat
    r, BigFloat
    x)
                              BF.BFRep Sign
    s BFNum
    n -> case BFNum
    n of
                                               BFNum
    BF.Zero    -> b
    0
                                               BFNum
    BF.Inf     -> String -> b
    forall a. HasCallStack => String -> a
    error (String -> b) -> String -> b
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.FloatingPoint.properFraction: Failed to convert: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (BigFloat, BigFloat) -> String
    forall a. Show a => a -> String
    show (BigFloat
    r, BigFloat
    x)
                                               BF.Num Integer
    v Int64
    y -> -- The value here is x * 2^y, and is integer if y >= 0
                                                             let e :: Integer
                                                                 e :: Integer
    e   = Integer
    2 Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ (Int64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int64
    y :: Integer)
                                                                 sgn :: Integer -> Integer
    sgn = if Sign
    s Sign -> Sign -> Bool
    forall a. Eq a => a -> a -> Bool
    == Sign
    BF.Neg then ((-Integer
    1) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *) else Integer -> Integer
    forall a. a -> a
    id
                                                             in if Int64
    y Int64 -> Int64 -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int64
    0
                                                                then Integer -> b
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> b) -> Integer -> b
    forall a b. (a -> b) -> a -> b
    $ Integer -> Integer
    sgn (Integer -> Integer) -> Integer -> Integer
    forall a b. (a -> b) -> a -> b
    $ Integer
    v Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    e
                                                                else Integer -> b
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> b) -> Integer -> b
    forall a b. (a -> b) -> a -> b
    $ Integer -> Integer
    sgn Integer
    v

    -- | Num instance for FloatingPoint
    instance ValidFloat eb sb => Num (FloatingPoint eb sb) where
      FloatingPoint FP
    a + :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    + FloatingPoint FP
    b = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FloatingPoint eb sb) -> FP -> FloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ FP
    a FP -> FP -> FP
    forall a. Num a => a -> a -> a
    + FP
    b
      FloatingPoint FP
    a * :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    * FloatingPoint FP
    b = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FloatingPoint eb sb) -> FP -> FloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ FP
    a FP -> FP -> FP
    forall a. Num a => a -> a -> a
    * FP
    b

      abs :: FloatingPoint eb sb -> FloatingPoint eb sb
    abs    (FloatingPoint FP
    fp) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Num a => a -> a
    abs    FP
    fp)
      signum :: FloatingPoint eb sb -> FloatingPoint eb sb
    signum (FloatingPoint FP
    fp) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Num a => a -> a
    signum FP
    fp)
      negate :: FloatingPoint eb sb -> FloatingPoint eb sb
    negate (FloatingPoint FP
    fp) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Num a => a -> a
    negate FP
    fp)

      fromInteger :: Integer -> FloatingPoint eb sb
    fromInteger = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FloatingPoint eb sb)
    -> (Integer -> FP) -> Integer -> FloatingPoint eb sb
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int -> Integer -> FP
    fpFromInteger (Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)) (Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb))

    instance ValidFloat eb sb => Fractional (FloatingPoint eb sb) where
      fromRational :: Rational -> FloatingPoint eb sb
    fromRational = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FloatingPoint eb sb)
    -> (Rational -> FP) -> Rational -> FloatingPoint eb sb
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int -> Rational -> FP
    fpFromRational (Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)) (Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb))

      FloatingPoint FP
    a / :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    / FloatingPoint FP
    b = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP
    a FP -> FP -> FP
    forall a. Fractional a => a -> a -> a
    / FP
    b)

    unsupported :: String -> a
    unsupported :: forall a. String -> a
    unsupported String
    w = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.FloatingPoint: Unsupported operation: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    w String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ". Please request this as a feature!"

    -- Float instance. Most methods are left unimplemented.
    instance ValidFloat eb sb => Floating (FloatingPoint eb sb) where
      pi :: FloatingPoint eb sb
    pi = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint FP
    forall a. Floating a => a
    pi

      exp :: FloatingPoint eb sb -> FloatingPoint eb sb
    exp  (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    exp FP
    i)
      sqrt :: FloatingPoint eb sb -> FloatingPoint eb sb
    sqrt (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    sqrt FP
    i)

      FloatingPoint FP
    a ** :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    ** FloatingPoint FP
    b = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FloatingPoint eb sb) -> FP -> FloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ FP
    a FP -> FP -> FP
    forall a. Floating a => a -> a -> a
    ** FP
    b

      log :: FloatingPoint eb sb -> FloatingPoint eb sb
    log   (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    log   FP
    i)
      sin :: FloatingPoint eb sb -> FloatingPoint eb sb
    sin   (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    sin   FP
    i)
      cos :: FloatingPoint eb sb -> FloatingPoint eb sb
    cos   (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    cos   FP
    i)
      tan :: FloatingPoint eb sb -> FloatingPoint eb sb
    tan   (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    tan   FP
    i)
      asin :: FloatingPoint eb sb -> FloatingPoint eb sb
    asin  (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    asin  FP
    i)
      acos :: FloatingPoint eb sb -> FloatingPoint eb sb
    acos  (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    acos  FP
    i)
      atan :: FloatingPoint eb sb -> FloatingPoint eb sb
    atan  (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    atan  FP
    i)
      sinh :: FloatingPoint eb sb -> FloatingPoint eb sb
    sinh  (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    sinh  FP
    i)
      cosh :: FloatingPoint eb sb -> FloatingPoint eb sb
    cosh  (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    cosh  FP
    i)
      tanh :: FloatingPoint eb sb -> FloatingPoint eb sb
    tanh  (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    tanh  FP
    i)
      asinh :: FloatingPoint eb sb -> FloatingPoint eb sb
    asinh (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    asinh FP
    i)
      acosh :: FloatingPoint eb sb -> FloatingPoint eb sb
    acosh (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    acosh FP
    i)
      atanh :: FloatingPoint eb sb -> FloatingPoint eb sb
    atanh (FloatingPoint FP
    i) = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FP
    forall a. Floating a => a -> a
    atanh FP
    i)

    -- | Lift a unary operation, simple case of function with no status. Here, we call fpFromBigFloat since the big-float isn't size aware.
    lift1 :: (BigFloat -> BigFloat) -> FP -> FP
    lift1 :: (BigFloat -> BigFloat) -> FP -> FP
    lift1 BigFloat -> BigFloat
    f (FP Int
    eb Int
    sb BigFloat
    a) = Int -> Int -> BigFloat -> FP
    fpFromBigFloat Int
    eb Int
    sb (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ BigFloat -> BigFloat
    f BigFloat
    a

    -- Lift a binary operation. Here we don't call fpFromBigFloat, because the result is correctly rounded.
    lift2 :: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) -> FP -> FP -> FP
    lift2 :: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> FP -> FP -> FP
    lift2 BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    f (FP Int
    eb Int
    sb BigFloat
    a) (FP Int
    _ Int
    _ BigFloat
    b) = Int -> Int -> BigFloat -> FP
    FP Int
    eb Int
    sb (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ (BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
    forall a b. (a -> b) -> a -> b
    $ BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    f (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    eb Int
    sb RoundMode
    BF.NearEven) BigFloat
    a BigFloat
    b

    -- | Convert from a IEEE float.
    fpFromFloat :: Int -> Int -> Float -> FP
    fpFromFloat :: Int -> Int -> Float -> FP
    fpFromFloat  Int
    8 Int
    24 Float
    f = let fw :: Word32
    fw          = Float -> Word32
    floatToWord Float
    f
                              (Bool
    sgn, Integer
    e, Integer
    s) = (Word32
    fw Word32 -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    `testBit` Int
    31, Word32 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Word32
    fw Word32 -> Int -> Word32
    forall a. Bits a => a -> Int -> a
    `shiftR` Int
    23) Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Integer
    0xFF, Word32 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word32
    fw Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Integer
    0x7FFFFF)
                          in Bool -> (Integer, Int) -> (Integer, Int) -> FP
    fpFromRawRep Bool
    sgn (Integer
    e, Int
    8) (Integer
    s, Int
    24)
    fpFromFloat Int
    eb Int
    sb Float
    f = String -> FP
    forall a. HasCallStack => String -> a
    error (String -> FP) -> String -> FP
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.fprFromFloat: Unexpected input: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int, Float) -> String
    forall a. Show a => a -> String
    show (Int
    eb, Int
    sb, Float
    f)

    -- | Convert from a IEEE double.
    fpFromDouble :: Int -> Int -> Double -> FP
    fpFromDouble :: Int -> Int -> Double -> FP
    fpFromDouble Int
    11 Int
    53 Double
    d = Int -> Int -> BigFloat -> FP
    FP Int
    11 Int
    54 (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ Double -> BigFloat
    BF.bfFromDouble Double
    d
    fpFromDouble Int
    eb Int
    sb Double
    d = String -> FP
    forall a. HasCallStack => String -> a
    error (String -> FP) -> String -> FP
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.fprFromDouble: Unexpected input: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int, Double) -> String
    forall a. Show a => a -> String
    show (Int
    eb, Int
    sb, Double
    d)