cryptol-3.2.0: Cryptol: The Language of Cryptography
Safe HaskellSafe-Inferred
LanguageHaskell2010

Cryptol.Backend.FloatHelpers

Synopsis

Documentation

data BF Source #

Constructors

BF 

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.