Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Data.SBV.Float

Contents

Type-sized floats
Constructing values
Operations

Description

A collection of arbitrary float operations.

Synopsis

data FP = FP {
- fpExponentSize :: Int
- fpSignificandSize :: Int
- fpValue :: BigFloat
}
fpFromRawRep :: Bool -> (Integer, Int) -> (Integer, Int) -> FP
fpFromBigFloat :: Int -> Int -> BigFloat -> FP
fpNaN :: Int -> Int -> FP
fpInf :: Bool -> Int -> Int -> FP
fpZero :: Bool -> Int -> Int -> FP
fpFromInteger :: Int -> Int -> Integer -> FP
fpFromRational :: Int -> Int -> Rational -> FP
fpFromFloat :: Int -> Int -> Float -> FP
fpFromDouble :: Int -> Int -> Double -> FP
fpEncodeFloat :: Int -> Int -> Integer -> Int -> FP

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
Fields fpExponentSize :: Int fpSignificandSize :: Int fpValue :: BigFloat

Instances

Instances details

Data FP Source #
Instance details Defined in Data.SBV.Core.SizedFloats Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FP -> c FP # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FP # toConstr :: FP -> Constr # dataTypeOf :: FP -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FP) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FP) # gmapT :: (forall b. Data b => b -> b) -> FP -> FP # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FP -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FP -> r # gmapQ :: (forall d. Data d => d -> u) -> FP -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FP -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FP -> m FP # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FP -> m FP # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FP -> m FP #
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 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 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.