Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.Float

Description

Logically consistent comparison of floating point numbers.

Synopsis

- asFinite :: Double -> Maybe Double
- isPosInf :: Double -> Bool
- isNegInf :: Double -> Bool
- isPosZero :: Double -> Bool
- isNegZero :: Double -> Bool
- isSafeInteger :: Double -> Bool
- 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
- doubleDenotOrd :: Double -> Double -> Ordering
- doubleToWord64 :: Double -> Word64
- doubleToRatio :: Double -> (Integer, Integer)
- ratioToDouble :: Integer -> Integer -> Double
- doubleDecode :: Double -> Maybe (Integer, Integer)
- doubleEncode :: Integer -> Integer -> Maybe Double
- toStringWithoutDotZero :: Double -> String

# Documentation

asFinite :: Double -> Maybe Double Source #

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

isPosInf :: Double -> Bool Source #

isNegInf :: Double -> Bool Source #

isPosZero :: Double -> Bool Source #

isNegZero :: Double -> Bool Source #

isSafeInteger :: Double -> Bool Source #

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

doubleEq :: Double -> Double -> Bool Source #

doubleLe :: Double -> Double -> Bool Source #

doubleLt :: Double -> Double -> Bool Source #

intToDouble :: Integral a => a -> Double Source #

doublePlus :: Double -> Double -> Double Source #

doubleMinus :: Double -> Double -> Double Source #

doubleTimes :: Double -> Double -> Double Source #

doubleNegate :: Double -> Double Source #

doubleDiv :: Double -> Double -> Double Source #

doublePow :: Double -> Double -> Double Source #

doubleSqrt :: Double -> Double Source #

doubleExp :: Double -> Double Source #

doubleLog :: Double -> Double Source #

doubleSin :: Double -> Double Source #

doubleCos :: Double -> Double Source #

doubleTan :: Double -> Double Source #

doubleASin :: Double -> Double Source #

doubleACos :: Double -> Double Source #

doubleATan :: Double -> Double Source #

doubleATan2 :: Double -> Double -> Double Source #

doubleSinh :: Double -> Double Source #

doubleCosh :: Double -> Double Source #

doubleTanh :: Double -> Double Source #

doubleASinh :: Double -> Double Source #

doubleACosh :: Double -> Double Source #

doubleATanh :: Double -> Double Source #

doubleRound :: Double -> Maybe Integer Source #

doubleFloor :: Double -> Maybe Integer Source #

doubleCeiling :: Double -> Maybe Integer Source #

doubleDenotEq :: Double -> Double -> Bool Source #

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 Source #

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 Source #

doubleToRatio :: Double -> (Integer, Integer) Source #

Decode a Double to an integer ratio.

ratioToDouble :: Integer -> Integer -> Double Source #

Encode an integer ratio as a double.

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

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 Source #

Encode a mantissa and an exponent as a Double.

toStringWithoutDotZero :: Double -> String Source #

Remove suffix `.0` from printed floating point number.