Data.SBV.Float

A collection of arbitrary float operations.

Type-sized floats

data FP

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.

Constructors

FP

Fields

• fpExponentSize :: Int
• fpSignificandSize :: Int
• fpValue :: BigFloat

Instances

Floating FP

Floating instance for big-floats

Defined in Data.SBV.Core.SizedFloats

Methods

pi :: FP

exp :: FP -> FP

log :: FP -> FP

sqrt :: FP -> FP

(**) :: FP -> FP -> FP

logBase :: FP -> FP -> FP

sin :: FP -> FP

cos :: FP -> FP

tan :: FP -> FP

asin :: FP -> FP

acos :: FP -> FP

atan :: FP -> FP

sinh :: FP -> FP

cosh :: FP -> FP

tanh :: FP -> FP

asinh :: FP -> FP

acosh :: FP -> FP

atanh :: FP -> FP

log1p :: FP -> FP

expm1 :: FP -> FP

log1pexp :: FP -> FP

log1mexp :: FP -> FP

RealFloat FP

Real-float instance for big-floats. Beware! Some of these aren't really all that well tested.

Defined in Data.SBV.Core.SizedFloats

Methods

floatRadix :: FP -> Integer

floatDigits :: FP -> Int

floatRange :: FP -> (Int, Int)

decodeFloat :: FP -> (Integer, Int)

encodeFloat :: Integer -> Int -> FP

exponent :: FP -> Int

significand :: FP -> FP

scaleFloat :: Int -> FP -> FP

isNaN :: FP -> Bool

isInfinite :: FP -> Bool

isDenormalized :: FP -> Bool

isNegativeZero :: FP -> Bool

isIEEE :: FP -> Bool

atan2 :: FP -> FP -> FP

Num FP

Num instance for big-floats

Defined in Data.SBV.Core.SizedFloats

Methods

(+) :: FP -> FP -> FP

(-) :: FP -> FP -> FP

(*) :: FP -> FP -> FP

negate :: FP -> FP

abs :: FP -> FP

signum :: FP -> FP

fromInteger :: Integer -> FP

Fractional FP

Fractional instance for big-floats

Defined in Data.SBV.Core.SizedFloats

Methods

(/) :: FP -> FP -> FP

recip :: FP -> FP

fromRational :: Rational -> FP

Real FP

Real instance for big-floats. Beware, not that well tested!

Defined in Data.SBV.Core.SizedFloats

Methods

toRational :: FP -> Rational

RealFrac FP

Real-frac instance for big-floats. Beware, not that well tested!

Defined in Data.SBV.Core.SizedFloats

Methods

properFraction :: Integral b => FP -> (b, FP)

truncate :: Integral b => FP -> b

round :: Integral b => FP -> b

ceiling :: Integral b => FP -> b

floor :: Integral b => FP -> b

Show FP

Defined in Data.SBV.Core.SizedFloats

Methods

showsPrec :: Int -> FP -> ShowS

show :: FP -> String

showList :: [FP] -> ShowS

Eq FP

Defined in Data.SBV.Core.SizedFloats

Methods

(==) :: FP -> FP -> Bool

(/=) :: FP -> FP -> Bool

Ord FP

Defined in Data.SBV.Core.SizedFloats

Methods

compare :: FP -> FP -> Ordering

(<) :: FP -> FP -> Bool

(<=) :: FP -> FP -> Bool

(>) :: FP -> FP -> Bool

(>=) :: FP -> FP -> Bool

max :: FP -> FP -> FP

min :: FP -> FP -> FP

Constructing values

fpFromRawRep :: Bool -> (Integer, Int) -> (Integer, Int) -> FP

Convert from an signexponentmantissa 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.

fpFromBigFloat :: Int -> Int -> BigFloat -> FP

Construct a float, by appropriately rounding

fpNaN :: Int -> Int -> FP

Make NaN. Exponent is all 1s. Significand is non-zero. The sign is irrelevant.

fpInf :: Bool -> Int -> Int -> FP

Make Infinity. Exponent is all 1s. Significand is 0.

fpZero :: Bool -> Int -> Int -> FP

Make a signed zero.

Operations

fpFromInteger :: Int -> Int -> Integer -> FP

Make from an integer value.

fpFromRational :: Int -> Int -> Rational -> FP

Make a generalized floating-point value from a Rational.

fpFromFloat :: Int -> Int -> Float -> FP

Convert from a IEEE float.

fpFromDouble :: Int -> Int -> Double -> FP

Convert from a IEEE double.

fpEncodeFloat :: Int -> Int -> Integer -> Int -> FP

Encode from exponent/mantissa form to a float representation. Corresponds to encodeFloat in Haskell.