sbv-9.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.SBV.Float

Description

A collection of arbitrary float operations.

Synopsis

Type-sized floats

data FP Source #

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 

Instances

Instances details
Floating FP Source #

Floating instance for big-floats

Instance details

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 Source #

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

Instance details

Defined in Data.SBV.Core.SizedFloats

Num FP Source #

Num instance for big-floats

Instance details

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 Source #

Fractional instance for big-floats

Instance details

Defined in Data.SBV.Core.SizedFloats

Methods

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

recip :: FP -> FP #

fromRational :: Rational -> FP #

Real FP Source #

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

Instance details

Defined in Data.SBV.Core.SizedFloats

Methods

toRational :: FP -> Rational #

RealFrac FP Source #

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

Instance details

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 Source # 
Instance details

Defined in Data.SBV.Core.SizedFloats

Methods

showsPrec :: Int -> FP -> ShowS #

show :: FP -> String #

showList :: [FP] -> ShowS #

Eq FP Source # 
Instance details

Defined in Data.SBV.Core.SizedFloats

Methods

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

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

Ord FP Source # 
Instance details

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 Source #

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 Source #

Construct a float, by appropriately rounding

fpNaN :: Int -> Int -> FP Source #

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

fpInf :: Bool -> Int -> Int -> FP Source #

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

fpZero :: Bool -> Int -> Int -> FP Source #

Make a signed zero.

Operations

fpFromInteger :: Int -> Int -> Integer -> FP Source #

Make from an integer value.

fpFromRational :: Int -> Int -> Rational -> FP Source #

Make a generalized floating-point value from a Rational.

fpFromFloat :: Int -> Int -> Float -> FP Source #

Convert from a IEEE float.

fpFromDouble :: Int -> Int -> Double -> FP Source #

Convert from a IEEE double.

fpEncodeFloat :: Int -> Int -> Integer -> Int -> FP Source #

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