cryptol-3.0.0: Cryptol: The Language of Cryptography

Safe Haskell | Safe-Inferred
Language | Haskell2010

Cryptol.Backend.FloatHelpers

Synopsis

- data BF = BF {
  - bfExpWidth :: !Integer
  - bfPrecWidth :: !Integer
  - bfValue :: !BigFloat
  }
- fpOpts :: Integer -> Integer -> RoundMode -> BFOpts
- fpRound :: Integer -> Either EvalError RoundMode
- fpCheckStatus :: (BigFloat, Status) -> BigFloat
- fpPP :: PPOpts -> BF -> Doc
- fpLit :: Integer -> Integer -> Rational -> BF
- floatFromRational :: Integer -> Integer -> RoundMode -> Rational -> BF
- floatToRational :: String -> BF -> Either EvalError Rational
- floatToInteger :: String -> RoundMode -> BF -> Either EvalError Integer
- floatFromBits :: Integer -> Integer -> Integer -> BF
- floatToBits :: Integer -> Integer -> BigFloat -> Integer
- floatFromDouble :: Double -> BF

# Documentation

data BF Source #

Constructors

BF |

Fields

- bfExpWidth :: !Integer
- bfPrecWidth :: !Integer
- bfValue :: !BigFloat

fpOpts :: Integer -> Integer -> RoundMode -> BFOpts Source #

Make LibBF options for the given precision and rounding mode.

fpRound :: Integer -> Either EvalError RoundMode Source #

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

fpCheckStatus :: (BigFloat, Status) -> BigFloat Source #

Check that we didn't get an unexpected status.

fpPP :: PPOpts -> BF -> Doc Source #

Pretty print a float

fpLit Source #

Arguments

:: Integer | Exponent width
-> Integer | Precision width
-> Rational |
-> BF |

Make a literal

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

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

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

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

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

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

floatFromBits Source #

Arguments

:: Integer | Exponent width
-> Integer | Precision widht
-> Integer | Raw bits
-> BF |

floatToBits :: Integer -> Integer -> BigFloat -> Integer Source #

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)

floatFromDouble :: Double -> BF Source #

Create a 64-bit IEEE-754 float.