Cryptol.Backend.FloatHelpers

Documentation

data BF

Constructors

BF

Fields

• bfExpWidth :: Integer
• bfPrecWidth :: Integer
• bfValue :: BigFloat

fpOpts :: Integer -> Integer -> RoundMode -> BFOpts

Make LibBF options for the given precision and rounding mode.

fpRound :: Integer -> Either EvalError RoundMode

Mapping from the rounding modes defined in the cry to the rounding modes of LibBF.

fpCheckStatus :: (BigFloat, Status) -> BigFloat

Check that we didn't get an unexpected status.

fpPP :: PPOpts -> BF -> Doc

Pretty print a float

fpLit

Arguments

:: Integer

Exponent width

-> Integer

Precision width

-> Rational

-> BF

Make a literal

floatFromRational :: Integer -> Integer -> RoundMode -> Rational -> BF

Make a floating point number from a rational, using the given rounding mode

floatToRational :: String -> BF -> Either EvalError Rational

Convert a floating point number to a rational, if possible.

floatToInteger :: String -> RoundMode -> BF -> Either EvalError Integer

Convert a floating point number to an integer, if possible.

floatFromBits

Arguments

:: Integer

Exponent width

-> Integer

Precision widht

-> Integer

Raw bits

-> BF

floatFromBits'

Arguments

:: Integer

Exponent width

-> Integer

Precision widht

-> Integer

Raw bits

-> BigFloat

Make a float using "raw" bits.

floatToBits :: Integer -> Integer -> BigFloat -> Integer

Turn a float into raw bits. NaN is represented as a positive "quiet" NaN (most significant bit in the significand is set, the rest of it is 0)