Agda.Utils.Float

Logically consistent comparison of floating point numbers.

Documentation

asFinite :: Double -> Maybe Double

Return Just x if it's a finite number, otherwise return Nothing.

isPosInf :: Double -> Bool

isNegInf :: Double -> Bool

isPosZero :: Double -> Bool

isNegZero :: Double -> Bool

isSafeInteger :: Double -> Bool

Checks whether or not the Double is within a safe range of operation.

doubleEq :: Double -> Double -> Bool

doubleLe :: Double -> Double -> Bool

doubleLt :: Double -> Double -> Bool

intToDouble :: Integral a => a -> Double

doublePlus :: Double -> Double -> Double

doubleMinus :: Double -> Double -> Double

doubleTimes :: Double -> Double -> Double

doubleNegate :: Double -> Double

doubleDiv :: Double -> Double -> Double

doublePow :: Double -> Double -> Double

doubleSqrt :: Double -> Double

doubleExp :: Double -> Double

doubleLog :: Double -> Double

doubleSin :: Double -> Double

doubleCos :: Double -> Double

doubleTan :: Double -> Double

doubleASin :: Double -> Double

doubleACos :: Double -> Double

doubleATan :: Double -> Double

doubleATan2 :: Double -> Double -> Double

doubleSinh :: Double -> Double

doubleCosh :: Double -> Double

doubleTanh :: Double -> Double

doubleASinh :: Double -> Double

doubleACosh :: Double -> Double

doubleATanh :: Double -> Double

doubleRound :: Double -> Maybe Integer

doubleFloor :: Double -> Maybe Integer

doubleCeiling :: Double -> Maybe Integer

doubleDenotEq :: Double -> Double -> Bool

Denotational equality for floating point numbers, checks bitwise equality.

NOTE: Denotational equality distinguishes NaNs, so its results may vary depending on the architecture and compilation flags. Unfortunately, this is a problem with floating-point numbers in general.

doubleDenotOrd :: Double -> Double -> Ordering

I guess "denotational orderings" are now a thing? The point is that we need an Ord instance which provides a total ordering, and is consistent with the denotational equality.

NOTE: The ordering induced via doubleToWord64 is total, and is consistent with doubleDenotEq. However, it is *deeply* unintuitive. For one, it considers all negative numbers to be larger than positive numbers.

doubleToWord64 :: Double -> Word64

doubleToRatio :: Double -> (Integer, Integer)

Decode a Double to an integer ratio.

ratioToDouble :: Integer -> Integer -> Double

Encode an integer ratio as a double.

doubleDecode :: Double -> Maybe (Integer, Integer)

Decode a Double to its mantissa and its exponent, normalised such that the mantissa is the smallest possible number without loss of accuracy.

doubleEncode :: Integer -> Integer -> Maybe Double

Encode a mantissa and an exponent as a Double.

toStringWithoutDotZero :: Double -> String

Remove suffix .0 from printed floating point number.