{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.IEEEFP
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.Class.IEEEFP
  ( fpIsNaN,
    fpIsPositiveZero,
    fpIsNegativeZero,
    fpIsPositiveInfinite,
    fpIsNegativeInfinite,
    fpIsPositive,
    fpIsNegative,
    fpIsInfinite,
    fpIsZero,
    fpIsNormal,
    fpIsSubnormal,
    fpIsPoint,
    IEEEFPConstants (..),
    IEEEFPRoundingMode (..),
    IEEEFPOp (..),
    IEEEFPRoundingOp (..),
    IEEEFPConvertible (..),
    IEEEFPToAlgReal (..),
  )
where

-- | Check if a floating-point number is not-a-number.
fpIsNaN :: (RealFloat a) => a -> Bool
fpIsNaN :: forall a. RealFloat a => a -> Bool
fpIsNaN = a -> Bool
forall a. RealFloat a => a -> Bool
isNaN
{-# INLINE fpIsNaN #-}

-- | Check if a floating-point number is positive zero.
fpIsPositiveZero :: (RealFloat a) => a -> Bool
fpIsPositiveZero :: forall a. RealFloat a => a -> Bool
fpIsPositiveZero a
x = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (a -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeZero a
x)
{-# INLINE fpIsPositiveZero #-}

-- | Check if a floating-point number is negative zero.
fpIsNegativeZero :: (RealFloat a) => a -> Bool
fpIsNegativeZero :: forall a. RealFloat a => a -> Bool
fpIsNegativeZero = a -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero
{-# INLINE fpIsNegativeZero #-}

-- | Check if a floating-point number is positive infinite.
fpIsPositiveInfinite :: (RealFloat a) => a -> Bool
fpIsPositiveInfinite :: forall a. RealFloat a => a -> Bool
fpIsPositiveInfinite a
x = a -> Bool
forall a. RealFloat a => a -> Bool
isInfinite a
x Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0
{-# INLINE fpIsPositiveInfinite #-}

-- | Check if a floating-point number is negative infinite.
fpIsNegativeInfinite :: (RealFloat a) => a -> Bool
fpIsNegativeInfinite :: forall a. RealFloat a => a -> Bool
fpIsNegativeInfinite a
x = a -> Bool
forall a. RealFloat a => a -> Bool
isInfinite a
x Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0
{-# INLINE fpIsNegativeInfinite #-}

-- | Check if a floating-point number is positive.
-- +0, +inf are considered positive. nan, -0, -inf are not positive.
fpIsPositive :: (RealFloat a) => a -> Bool
fpIsPositive :: forall a. RealFloat a => a -> Bool
fpIsPositive a
x = Bool -> Bool
not (a -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN a
x) Bool -> Bool -> Bool
&& (a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 Bool -> Bool -> Bool
|| a -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveZero a
x)
{-# INLINE fpIsPositive #-}

-- | Check if a floating-point number is negative.
-- -0, -inf are considered negative. nan, +0, +inf are not negative.
fpIsNegative :: (RealFloat a) => a -> Bool
fpIsNegative :: forall a. RealFloat a => a -> Bool
fpIsNegative a
x = Bool -> Bool
not (a -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN a
x) Bool -> Bool -> Bool
&& (a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 Bool -> Bool -> Bool
|| a -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero a
x)
{-# INLINE fpIsNegative #-}

-- | Check if a floating-point number is infinite.
fpIsInfinite :: (RealFloat a) => a -> Bool
fpIsInfinite :: forall a. RealFloat a => a -> Bool
fpIsInfinite a
x = a -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveInfinite a
x Bool -> Bool -> Bool
|| a -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeInfinite a
x
{-# INLINE fpIsInfinite #-}

-- | Check if a floating-point number is zero.
fpIsZero :: (RealFloat a) => a -> Bool
fpIsZero :: forall a. RealFloat a => a -> Bool
fpIsZero a
x = a -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveZero a
x Bool -> Bool -> Bool
|| a -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeZero a
x
{-# INLINE fpIsZero #-}

-- | Check if a floating-point number is normal, i.e., not 0, not inf, not
-- nan, and not denormalized.
fpIsNormal :: (RealFloat a) => a -> Bool
fpIsNormal :: forall a. RealFloat a => a -> Bool
fpIsNormal a
x =
  Bool -> Bool
not (a -> Bool
forall a. RealFloat a => a -> Bool
fpIsZero a
x)
    Bool -> Bool -> Bool
&& Bool -> Bool
not (a -> Bool
forall a. RealFloat a => a -> Bool
fpIsSubnormal a
x)
    Bool -> Bool -> Bool
&& Bool -> Bool
not (a -> Bool
forall a. RealFloat a => a -> Bool
fpIsInfinite a
x)
    Bool -> Bool -> Bool
&& Bool -> Bool
not (a -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN a
x)
{-# INLINE fpIsNormal #-}

-- | Check if a floating-point number is subnormal, i.e., denormalized. 0,
-- inf, or nan are not subnormal.
fpIsSubnormal :: (RealFloat a) => a -> Bool
fpIsSubnormal :: forall a. RealFloat a => a -> Bool
fpIsSubnormal = a -> Bool
forall a. RealFloat a => a -> Bool
isDenormalized
{-# INLINE fpIsSubnormal #-}

-- | Check if a floating-point number is a point, i.e., not inf, not nan.
fpIsPoint :: (RealFloat a) => a -> Bool
fpIsPoint :: forall a. RealFloat a => a -> Bool
fpIsPoint a
x = Bool -> Bool
not (a -> Bool
forall a. RealFloat a => a -> Bool
fpIsInfinite a
x) Bool -> Bool -> Bool
&& Bool -> Bool
not (a -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN a
x)
{-# INLINE fpIsPoint #-}

-- | Constants for IEEE floating-point numbers.
class IEEEFPConstants a where
  -- | Positive infinity.
  fpPositiveInfinite :: a

  -- | Negative infinity.
  fpNegativeInfinite :: a

  -- | Not-a-number.
  fpNaN :: a

  -- | Negative zero.
  fpNegativeZero :: a

  -- | Positive zero.
  fpPositiveZero :: a

  -- | Smallest positive normalized number.
  fpMinNormalized :: a

  -- | Smallest positive subnormal number.
  fpMinSubnormal :: a

  -- | Largest positive normalized number.
  fpMaxNormalized :: a

  -- | Largest positive subnormal number.
  fpMaxSubnormal :: a

-- | Operations on IEEE floating-point numbers, without rounding mode.
class IEEEFPOp a where
  -- | IEEE754-2019 abs operation.
  fpAbs :: a -> a

  -- | IEEE754-2019 negate operation.
  fpNeg :: a -> a

  -- | IEEE754-2019 remainder operation.
  fpRem :: a -> a -> a

  -- | IEEE754-2019 minimum operation.
  --
  -- * The comparison for zeros follows -0 < 0
  -- * Returns NaN if one operand is NaN.
  fpMinimum :: a -> a -> a

  -- | IEEE754-2019 minimumNumber operation.
  --
  -- * The comparison for zeros follows -0 < 0
  -- * Returns the other operand if one operand is NaN.
  fpMinimumNumber :: a -> a -> a

  -- | IEEE754-2019 maximum operation.
  --
  -- * The comparison for zeros follows -0 < 0
  -- * Returns NaN if one operand is NaN.
  fpMaximum :: a -> a -> a

  -- | IEEE754-2019 maximumNumber operation.
  --
  -- * The comparison for zeros follows -0 < 0
  -- * Returns the other operand if one operand is NaN.
  fpMaximumNumber :: a -> a -> a

-- | Rounding modes for floating-point operations.
class IEEEFPRoundingMode mode where
  -- | Round to nearest, ties to even.
  rne :: mode

  -- | Round to nearest, ties to away from zero.
  rna :: mode

  -- | Round towards positive infinity.
  rtp :: mode

  -- | Round towards negative infinity.
  rtn :: mode

  -- | Round towards zero.
  rtz :: mode

-- | Operations on IEEE floating-point numbers, with rounding mode.
class (IEEEFPRoundingMode mode) => IEEEFPRoundingOp a mode | a -> mode where
  fpAdd :: mode -> a -> a -> a
  fpSub :: mode -> a -> a -> a
  fpMul :: mode -> a -> a -> a
  fpDiv :: mode -> a -> a -> a
  fpFMA :: mode -> a -> a -> a -> a
  fpSqrt :: mode -> a -> a
  fpRoundToIntegral :: mode -> a -> a

-- | Conversion from and to FPs.
class IEEEFPConvertible a fp mode | fp -> mode where
  fromFPOr ::
    -- | Default value when converting non-representable FPs. For example, when
    -- converting to non-FP types, the NaN and infinities are not representable.
    -- Additionally, when converting to bit-vectors, out-of-bound FPs are not
    -- representable.
    --
    -- Note that out-of-bound means that the /value after conversion/ is out of
    -- bound, not the /value before conversion/, meaning that converting from
    -- 3.5 to 2-bit unsigned bit-vector is out-of-bound when rounding to
    -- positive, but not when rounding to negative.
    a ->
    -- | Rounding mode. Ignored when converting to 'Grisette.AlgReal' because
    -- every representable FP value is converted to an exact 'Grisette.AlgReal'.
    mode ->
    -- | FP value.
    fp ->
    a
  toFP :: mode -> a -> fp

-- | Converting FP to real numbers.
class
  (IEEEFPConvertible a fp mode, IEEEFPRoundingMode mode) =>
  IEEEFPToAlgReal a fp mode
    | fp -> mode
  where
  -- | Similar to 'fromFPOr' for 'Grisette.AlgReal', but dropped the ignored
  -- rounding mode.
  fpToAlgReal :: a -> fp -> a
  fpToAlgReal a
d = a -> mode -> fp -> a
forall a fp mode.
IEEEFPConvertible a fp mode =>
a -> mode -> fp -> a
fromFPOr a
d mode
forall mode. IEEEFPRoundingMode mode => mode
rna