{-# LANGUAGE CPP #-}
module Agda.Utils.Float
( normaliseNaN
, doubleToWord64
, floatEq
, floatLt
, toStringWithoutDotZero
) where
import Data.Maybe ( fromMaybe )
import Data.Word
import Numeric.IEEE ( IEEE(identicalIEEE, nan) )
#if __GLASGOW_HASKELL__ >= 804
import GHC.Float ( castDoubleToWord64 )
#else
import System.IO.Unsafe ( unsafePerformIO )
import qualified Foreign as F
#endif
import Agda.Utils.List ( stripSuffix )
#if __GLASGOW_HASKELL__ < 804
castDoubleToWord64 :: Double -> Word64
castDoubleToWord64 float = unsafePerformIO $ F.alloca $ \buf -> do
F.poke (F.castPtr buf) float
F.peek buf
#endif
normaliseNaN :: Double -> Double
normaliseNaN x
| isNaN x = nan
| otherwise = x
doubleToWord64 :: Double -> Word64
doubleToWord64 = castDoubleToWord64 . normaliseNaN
floatEq :: Double -> Double -> Bool
floatEq x y = identicalIEEE x y || (isNaN x && isNaN y)
floatLt :: Double -> Double -> Bool
floatLt x y =
case compareFloat x y of
LT -> True
_ -> False
where
compareFloat :: Double -> Double -> Ordering
compareFloat x y
| identicalIEEE x y = EQ
| isNegInf x = LT
| isNegInf y = GT
| isNaN x && isNaN y = EQ
| isNaN x = LT
| isNaN y = GT
| otherwise = compare (x, isNegZero y) (y, isNegZero x)
isNegInf z = z < 0 && isInfinite z
isNegZero z = identicalIEEE z (-0.0)
toStringWithoutDotZero :: Double -> String
toStringWithoutDotZero d = fromMaybe s $ stripSuffix ".0" s
where s = show d