-----------------------------------------------------------------------------
-- |
-- 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 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 = 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
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 = 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 (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 (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 :: 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, Show a) => Int -> a -> String
mkB Int
eb Integer
fpExponent, Int -> Integer -> String
forall a. (Integral a, Show 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, Show 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 (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 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)