IEEEFP.hs

{-# 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 = isNaN
{-# INLINE fpIsNaN #-}

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

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

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

-- | Check if a floating-point number is negative infinite.
fpIsNegativeInfinite :: (RealFloat a) => a -> Bool
fpIsNegativeInfinite x = isInfinite x && x < 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 x = not (fpIsNaN x) && (x > 0 || fpIsPositiveZero 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 x = not (fpIsNaN x) && (x < 0 || isNegativeZero x)
{-# INLINE fpIsNegative #-}

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

-- | Check if a floating-point number is zero.
fpIsZero :: (RealFloat a) => a -> Bool
fpIsZero x = fpIsPositiveZero x || fpIsNegativeZero 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 x =
  not (fpIsZero x)
    && not (fpIsSubnormal x)
    && not (fpIsInfinite x)
    && not (fpIsNaN 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 = isDenormalized
{-# INLINE fpIsSubnormal #-}

-- | Check if a floating-point number is a point, i.e., not inf, not nan.
fpIsPoint :: (RealFloat a) => a -> Bool
fpIsPoint x = not (fpIsInfinite x) && not (fpIsNaN 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 d = fromFPOr d rna