-----------------------------------------------------------------------------
-- |
-- 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
forall (eb :: Nat) (sb :: Nat).
FloatingPoint eb sb -> FloatingPoint eb sb -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: 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, 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
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
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) = 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
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
Ord, FP -> FP -> Bool
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 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 forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` String
v = forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse 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 forall a. a -> [a] -> [a]
: String
s 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 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 forall a. Semigroup a => a -> a -> a
<> Maybe Word -> ShowFmt
BF.showFree (forall a. a -> Maybe a
Just (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  forall a. Semigroup a => a -> a -> a
<> ShowFmt
opts
                  (Bool
True,  Bool
False) -> ShowFmt
BF.addPrefix                 forall a. Semigroup a => a -> a -> a
<> ShowFmt
opts
                  (Bool
True,  Bool
True ) -> ShowFmt
BF.addPrefix forall a. Semigroup a => a -> a -> a
<> ShowFmt
BF.forceExp  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 forall a. Eq a => a -> a -> Bool
== Int
10 then Char
'e' else Char
'p'

        trimZeros :: ShowS
trimZeros String
s
          | Char
'.' forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
s = case forall a. (a -> Bool) -> [a] -> ([a], [a])
span (forall a. Eq a => a -> a -> Bool
/= Char
expChar) String
s of
                            (String
pre, String
post) -> let pre' :: String
pre' = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ case forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Eq a => a -> a -> Bool
== Char
'0') forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse String
pre of
                                                                  res :: String
res@(Char
'.':String
_) -> Char
'0' forall a. a -> [a] -> [a]
: String
res
                                                                  String
res         -> String
res
                                           in String
pre' 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 forall a. Semigroup a => a -> a -> a
<> RoundMode -> BFOpts
BF.rnd RoundMode
rm forall a. Semigroup a => a -> a -> a
<> Int -> BFOpts
BF.expBits (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
eb) forall a. Semigroup a => a -> a -> a
<> Word -> BFOpts
BF.precBits (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 forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> (BigFloat, Status)
BF.bfRoundFloat (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 forall a b. (a -> b) -> a -> b
$ BFOpts -> Integer -> BigFloat
BF.bfFromBits (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 forall a. Bits a => a -> Int -> a
`shiftL` (Int
sb forall a. Num a => a -> a -> a
- Int
1)) forall a. Bits a => a -> a -> a
.|. Integer
s
        val :: Integer
val | Bool
sign = (Integer
1 forall a. Bits a => a -> Int -> a
`shiftL` (Int
eb forall a. Num a => a -> a -> a
+ Int
sb forall a. Num a => a -> a -> a
- Int
1)) 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 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 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 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 forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfDiv (forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
eb Int
sb RoundMode
BF.NearEven) (Integer -> BigFloat
BF.bfFromInteger (forall a. Ratio a -> a
numerator Rational
r))
                                                                                (Integer -> BigFloat
BF.bfFromInteger (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 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 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 = forall a. Show a => a -> String
show Int
eb
       s :: String
s = forall a. Show a => a -> String
show Int
sb

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

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

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

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

       mkB :: Int -> a -> String
mkB Int
sz a
val = String
"#b" forall a. [a] -> [a] -> [a]
++ Int -> ShowS
pad Int
sz (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 = forall a. Int -> a -> [a]
replicate (Int
l forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length String
str) Char
'0' 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) 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 = 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 = 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 forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> (BigFloat, Status)
BF.bfSqrt (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 forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
BF.bfPow  (forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
eb Int
sb RoundMode
BF.NearEven) BigFloat
a BigFloat
b

  pi :: FP
pi    = forall a. String -> a
unsupported String
"Floating.FP.pi"
  exp :: FP -> FP
exp   = forall a. String -> a
unsupported String
"Floating.FP.exp"
  log :: FP -> FP
log   = forall a. String -> a
unsupported String
"Floating.FP.log"
  sin :: FP -> FP
sin   = forall a. String -> a
unsupported String
"Floating.FP.sin"
  cos :: FP -> FP
cos   = forall a. String -> a
unsupported String
"Floating.FP.cos"
  tan :: FP -> FP
tan   = forall a. String -> a
unsupported String
"Floating.FP.tan"
  asin :: FP -> FP
asin  = forall a. String -> a
unsupported String
"Floating.FP.asin"
  acos :: FP -> FP
acos  = forall a. String -> a
unsupported String
"Floating.FP.acos"
  atan :: FP -> FP
atan  = forall a. String -> a
unsupported String
"Floating.FP.atan"
  sinh :: FP -> FP
sinh  = forall a. String -> a
unsupported String
"Floating.FP.sinh"
  cosh :: FP -> FP
cosh  = forall a. String -> a
unsupported String
"Floating.FP.cosh"
  tanh :: FP -> FP
tanh  = forall a. String -> a
unsupported String
"Floating.FP.tanh"
  asinh :: FP -> FP
asinh = forall a. String -> a
unsupported String
"Floating.FP.asinh"
  acosh :: FP -> FP
acosh = forall a. String -> a
unsupported String
"Floating.FP.acosh"
  atanh :: FP -> FP
atanh = 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
_) = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (-Integer
vforall a. Num a => a -> a -> a
+Integer
3), forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
v)
     where v :: Integer
           v :: Integer
v = Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ ((forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
eb :: 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 (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     -> forall a. RealFloat a => a -> (Integer, Int)
decodeFloat (Double
0forall 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) = forall a. RealFloat a => a -> (Int, Int)
floatRange FP
i
                                                                  x :: Integer
x = (Integer
2 :: Integer) forall a b. (Num a, Integral b) => a -> b -> a
^ forall a. Integral a => a -> Integer
toInteger (Int
mforall a. Num a => a -> a -> a
+Int
1)
                                                              in (if Sign
s 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 forall a. Eq a => a -> a -> Bool
== Sign
BF.Neg then -Integer
x else Integer
x, forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
y)

  encodeFloat :: Integer -> Int -> FP
encodeFloat = 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 forall a. Ord a => a -> a -> Bool
< Int
0 = Int -> Int -> Rational -> FP
fpFromRational Int
eb Int
sb (Integer
m      forall a. Integral a => a -> a -> Ratio a
% Integer
n')
                        | Bool
True  = Int -> Int -> Rational -> FP
fpFromRational Int
eb Int
sb (Integer
m forall a. Num a => a -> a -> a
* Integer
n' forall a. Integral a => a -> a -> Ratio a
% Integer
1)
    where n' :: Integer
          n' :: Integer
n' = (Integer
2 :: Integer) forall a b. (Num a, Integral b) => a -> b -> a
^ forall a. Num a => a -> a
abs (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 forall a. Ord a => a -> a -> Bool
>= Int
0  = Integer
m forall a. Num a => a -> a -> a
* Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ Int
n forall a. Integral a => a -> a -> Ratio a
% Integer
1
     | Bool
True    = Integer
m forall a. Integral a => a -> a -> Ratio a
% Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ forall a. Num a => a -> a
abs Int
n
    where (Integer
m, Int
n) = 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 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 forall a. Num a => a -> a -> a
- Int -> Int -> BigFloat -> FP
FP Int
eb Int
sb BigFloat
r')
                                  (BigFloat, Status)
x -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"RealFrac.FP.properFraction: Failed to convert: " forall a. [a] -> [a] -> [a]
++ 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     -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.FloatingPoint.properFraction: Failed to convert: " forall a. [a] -> [a] -> [a]
++ 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     -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.FloatingPoint.properFraction: Failed to convert: " forall a. [a] -> [a] -> [a]
++ 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 forall a b. (Num a, Integral b) => a -> b -> a
^ (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
y :: Integer)
                                                             sgn :: Integer -> Integer
sgn = if Sign
s forall a. Eq a => a -> a -> Bool
== Sign
BF.Neg then ((-Integer
1) forall a. Num a => a -> a -> a
*) else forall a. a -> a
id
                                                         in if Int64
y forall a. Ord a => a -> a -> Bool
> Int64
0
                                                            then forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Integer -> Integer
sgn forall a b. (a -> b) -> a -> b
$ Integer
v forall a. Num a => a -> a -> a
* Integer
e
                                                            else forall a b. (Integral a, Num b) => a -> b
fromIntegral 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 = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint forall a b. (a -> b) -> a -> b
$ FP
a forall a. Num a => a -> a -> a
+ FP
b
  FloatingPoint FP
a * :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
* FloatingPoint FP
b = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint forall a b. (a -> b) -> a -> b
$ FP
a forall a. Num a => a -> a -> a
* FP
b

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

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

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

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

unsupported :: String -> a
unsupported :: forall a. String -> a
unsupported String
w = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.FloatingPoint: Unsupported operation: " forall a. [a] -> [a] -> [a]
++ String
w 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 = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint forall a. Floating a => a
pi

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

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

  log :: FloatingPoint eb sb -> FloatingPoint eb sb
log   (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (forall a. Floating a => a -> a
log   FP
i)
  sin :: FloatingPoint eb sb -> FloatingPoint eb sb
sin   (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (forall a. Floating a => a -> a
sin   FP
i)
  cos :: FloatingPoint eb sb -> FloatingPoint eb sb
cos   (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (forall a. Floating a => a -> a
cos   FP
i)
  tan :: FloatingPoint eb sb -> FloatingPoint eb sb
tan   (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (forall a. Floating a => a -> a
tan   FP
i)
  asin :: FloatingPoint eb sb -> FloatingPoint eb sb
asin  (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (forall a. Floating a => a -> a
asin  FP
i)
  acos :: FloatingPoint eb sb -> FloatingPoint eb sb
acos  (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (forall a. Floating a => a -> a
acos  FP
i)
  atan :: FloatingPoint eb sb -> FloatingPoint eb sb
atan  (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (forall a. Floating a => a -> a
atan  FP
i)
  sinh :: FloatingPoint eb sb -> FloatingPoint eb sb
sinh  (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (forall a. Floating a => a -> a
sinh  FP
i)
  cosh :: FloatingPoint eb sb -> FloatingPoint eb sb
cosh  (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (forall a. Floating a => a -> a
cosh  FP
i)
  tanh :: FloatingPoint eb sb -> FloatingPoint eb sb
tanh  (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (forall a. Floating a => a -> a
tanh  FP
i)
  asinh :: FloatingPoint eb sb -> FloatingPoint eb sb
asinh (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (forall a. Floating a => a -> a
asinh FP
i)
  acosh :: FloatingPoint eb sb -> FloatingPoint eb sb
acosh (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (forall a. Floating a => a -> a
acosh FP
i)
  atanh :: FloatingPoint eb sb -> FloatingPoint eb sb
atanh (FloatingPoint FP
i) = forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint (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 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 forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
f (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 forall a. Bits a => a -> Int -> Bool
`testBit` Int
31, forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32
fw forall a. Bits a => a -> Int -> a
`shiftR` Int
23) forall a. Bits a => a -> a -> a
.&. Integer
0xFF, forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
fw 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 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.fprFromFloat: Unexpected input: " forall a. [a] -> [a] -> [a]
++ 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 forall a b. (a -> b) -> a -> b
$ Double -> BigFloat
BF.bfFromDouble Double
d
fpFromDouble Int
eb Int
sb Double
d = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.fprFromDouble: Unexpected input: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Int
eb, Int
sb, Double
d)