{-# LANGUAGE CPP #-}

-- | Logically consistent comparison of floating point numbers.
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 :: Double -> Double
normaliseNaN Double
x
  | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
x   = Double
forall a. IEEE a => a
nan
  | Bool
otherwise = Double
x

doubleToWord64 :: Double -> Word64
doubleToWord64 :: Double -> Word64
doubleToWord64 = Double -> Word64
castDoubleToWord64 (Double -> Word64) -> (Double -> Double) -> Double -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
normaliseNaN

floatEq :: Double -> Double -> Bool
floatEq :: Double -> Double -> Bool
floatEq Double
x Double
y = Double -> Double -> Bool
forall a. IEEE a => a -> a -> Bool
identicalIEEE Double
x Double
y  Bool -> Bool -> Bool
|| (Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
x Bool -> Bool -> Bool
&& Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
y)

floatLt :: Double -> Double -> Bool
floatLt :: Double -> Double -> Bool
floatLt Double
x Double
y =
  case Double -> Double -> Ordering
compareFloat Double
x Double
y of
    Ordering
LT -> Bool
True
    Ordering
_  -> Bool
False
  where
    -- Also implemented in the GHC backend
    compareFloat :: Double -> Double -> Ordering
    compareFloat :: Double -> Double -> Ordering
compareFloat Double
x Double
y
      | Double -> Double -> Bool
forall a. IEEE a => a -> a -> Bool
identicalIEEE Double
x Double
y          = Ordering
EQ
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isNegInf Double
x                 = Ordering
LT
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isNegInf Double
y                 = Ordering
GT
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
x Bool -> Bool -> Bool
&& Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
y         = Ordering
EQ
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
x                    = Ordering
LT
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
y                    = Ordering
GT
      | Bool
otherwise                  = (Double, Bool) -> (Double, Bool) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Double
x, Double -> Bool
forall a. IEEE a => a -> Bool
isNegZero Double
y) (Double
y, Double -> Bool
forall a. IEEE a => a -> Bool
isNegZero Double
x)
    isNegInf :: a -> Bool
isNegInf  a
z = a
z a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 Bool -> Bool -> Bool
&& a -> Bool
forall a. RealFloat a => a -> Bool
isInfinite a
z
    isNegZero :: a -> Bool
isNegZero a
z = a -> a -> Bool
forall a. IEEE a => a -> a -> Bool
identicalIEEE a
z (-a
0.0)

-- | Remove suffix @.0@ from printed floating point number.
toStringWithoutDotZero :: Double -> String
toStringWithoutDotZero :: Double -> String
toStringWithoutDotZero Double
d = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
s (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> Maybe String
forall a. Eq a => Suffix a -> Suffix a -> Maybe (Suffix a)
stripSuffix String
".0" String
s
  where s :: String
s = Double -> String
forall a. Show a => a -> String
show Double
d