-----------------------------------------------------------------------------
-- |
-- 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, FPSingle, FPDouble, FPQuad

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

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

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

import Data.Char (intToDigit)
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 a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
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
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 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
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
min :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
$cmin :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
max :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
$cmax :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
>= :: 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
$c< :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
compare :: FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering
$ccompare :: forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering
$cp1Ord :: forall (eb :: Nat) (sb :: Nat). Eq (FloatingPoint eb sb)
Ord)

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

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

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

-- | Abbreviation for IEEE quadruble precision float, bit width 128.
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
min :: FP -> FP -> FP
$cmin :: FP -> FP -> FP
max :: FP -> FP -> FP
$cmax :: FP -> FP -> FP
>= :: FP -> FP -> Bool
$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
compare :: FP -> FP -> Ordering
$ccompare :: FP -> FP -> Ordering
$cp1Ord :: Eq FP
Ord, FP -> FP -> Bool
(FP -> FP -> Bool) -> (FP -> FP -> Bool) -> Eq FP
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FP -> FP -> Bool
$c/= :: FP -> FP -> Bool
== :: FP -> FP -> Bool
$c== :: FP -> FP -> Bool
Eq)

instance Show FP where
  show :: FP -> String
show = Int -> Bool -> FP -> String
bfToString Int
10 Bool
False

-- | 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 -> FP -> String
bfToString :: Int -> Bool -> FP -> String
bfToString Int
b Bool
withPrefix (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
withP 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))
        withP :: ShowFmt
withP
          | Bool
withPrefix = ShowFmt
BF.addPrefix ShowFmt -> ShowFmt -> ShowFmt
forall a. Semigroup a => a -> a -> a
<> ShowFmt
opts
          | Bool
True       = ShowFmt
opts

        trimZeros :: ShowS
trimZeros String
s
          | Char
'.' Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
s = 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
s of
                                       res :: String
res@(Char
'.':String
_) -> Char
'0' Char -> ShowS
forall a. a -> [a] -> [a]
: String
res
                                       String
res         -> String
res
          | Bool
True         = String
s

-- | Default options for BF options.
mkBFOpts :: Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts :: 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)

-- | normFP the float to make sure it's within the required range
mkFP :: Int -> Int -> BigFloat -> FP
mkFP :: Int -> Int -> BigFloat -> FP
mkFP 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
mkFP 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
mkFP 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
mkFP 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
mkFP 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
mkB Int
eb Integer
fpExponent, Int -> Integer -> 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 -> Integer -> String
mkB Int
sz Integer
val = String
"#b" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
pad Int
sz (Integer -> ShowS
showBin Integer
val String
"")
       showBin :: Integer -> ShowS
showBin = Integer -> (Int -> Char) -> Integer -> ShowS
forall a. (Integral a, Show a) => a -> (Int -> Char) -> a -> ShowS
showIntAtBase Integer
2 Int -> Char
intToDigit
       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 (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 :: 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 (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)) (Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
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 (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)) (Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
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 :: 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 mkFP 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
mkFP 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 mkFP, 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
54 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)