content: {-# LANGUAGE DerivingVia #-}
  {-# LANGUAGE StandaloneDeriving #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  -- |
  -- Module      :   Grisette.Internal.Core.Data.Class.SymIEEEFP
  -- 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.SymIEEEFP
    ( SymIEEEFPTraits (..),
    )
  where
  
  import Grisette.Internal.Core.Data.Class.AsKey (AsKey (AsKey))
  import Grisette.Internal.Core.Data.Class.IEEEFP
    ( fpIsInfinite,
      fpIsNaN,
      fpIsNegative,
      fpIsNegativeInfinite,
      fpIsNegativeZero,
      fpIsNormal,
      fpIsPoint,
      fpIsPositive,
      fpIsPositiveInfinite,
      fpIsPositiveZero,
      fpIsSubnormal,
      fpIsZero,
    )
  import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
  import Grisette.Internal.SymPrim.FP (FP, ValidFP)
  import Grisette.Internal.SymPrim.SymBool (SymBool)
  
  -- | A class for symbolic traits of IEEE floating-point numbers.
  class SymIEEEFPTraits a where
    -- | Check if a symbolic floating-point number is not-a-number.
    symFpIsNaN :: a -> SymBool
  
    -- | Check if a symbolic floating-point number is positive.
    -- +0, +inf are considered positive. nan, -0, -inf are not positive.
    symFpIsPositive :: a -> SymBool
  
    -- | Check if a symbolic floating-point number is negative.
    -- -0, -inf are considered negative. nan, +0, +inf are not negative.
    symFpIsNegative :: a -> SymBool
  
    -- | Check if a symbolic floating-point number is positive infinite.
    symFpIsPositiveInfinite :: a -> SymBool
  
    -- | Check if a symbolic floating-point number is negative infinite.
    symFpIsNegativeInfinite :: a -> SymBool
  
    -- | Check if a symbolic floating-point number is infinite.
    symFpIsInfinite :: a -> SymBool
  
    -- | Check if a symbolic floating-point number is positive zero.
    symFpIsPositiveZero :: a -> SymBool
  
    -- | Check if a symbolic floating-point number is negative zero.
    symFpIsNegativeZero :: a -> SymBool
  
    -- | Check if a symbolic floating-point number is zero.
    symFpIsZero :: a -> SymBool
  
    -- | Check if a symbolic floating-point number is normal, i.e., not 0, not
    -- inf, not nan, and not denormalized.
    symFpIsNormal :: a -> SymBool
  
    -- | Check if a symbolic floating-point number is subnormal, i.e.,
    -- denormalized. 0, inf, or nan are not subnormal.
    symFpIsSubnormal :: a -> SymBool
  
    -- | Check if a symbolic floating-point number is a point, i.e., not inf, not
    -- nan.
    symFpIsPoint :: a -> SymBool
  
  newtype ConcreteFloat f = ConcreteFloat f
  
  instance (RealFloat f) => SymIEEEFPTraits (ConcreteFloat f) where
    symFpIsNaN (ConcreteFloat x) = con $ fpIsNaN x
    {-# INLINE symFpIsNaN #-}
  
    symFpIsPositive (ConcreteFloat x) = con $ fpIsPositive x
    {-# INLINE symFpIsPositive #-}
  
    symFpIsNegative (ConcreteFloat x) = con $ fpIsNegative x
    {-# INLINE symFpIsNegative #-}
  
    symFpIsInfinite (ConcreteFloat x) = con $ fpIsInfinite x
    {-# INLINE symFpIsInfinite #-}
  
    symFpIsPositiveInfinite (ConcreteFloat x) = con $ fpIsPositiveInfinite x
    {-# INLINE symFpIsPositiveInfinite #-}
  
    symFpIsNegativeInfinite (ConcreteFloat x) = con $ fpIsNegativeInfinite x
    {-# INLINE symFpIsNegativeInfinite #-}
  
    symFpIsPositiveZero (ConcreteFloat x) = con $ fpIsPositiveZero x
    {-# INLINE symFpIsPositiveZero #-}
  
    symFpIsNegativeZero (ConcreteFloat x) = con $ fpIsNegativeZero x
    {-# INLINE symFpIsNegativeZero #-}
  
    symFpIsZero (ConcreteFloat x) = con $ fpIsZero x
    {-# INLINE symFpIsZero #-}
  
    symFpIsNormal (ConcreteFloat x) = con $ fpIsNormal x
    {-# INLINE symFpIsNormal #-}
  
    symFpIsSubnormal (ConcreteFloat x) = con $ fpIsSubnormal x
    {-# INLINE symFpIsSubnormal #-}
  
    symFpIsPoint (ConcreteFloat x) = con $ fpIsPoint x
    {-# INLINE symFpIsPoint #-}
  
  deriving via (ConcreteFloat Float) instance SymIEEEFPTraits Float
  
  deriving via (ConcreteFloat Double) instance SymIEEEFPTraits Double
  
  deriving via
    (ConcreteFloat (FP eb sb))
    instance
      (ValidFP eb sb) => SymIEEEFPTraits (FP eb sb)
  
  instance (SymIEEEFPTraits a) => SymIEEEFPTraits (AsKey a) where
    symFpIsNaN (AsKey a) = symFpIsNaN a
    {-# INLINE symFpIsNaN #-}
  
    symFpIsPositive (AsKey a) = symFpIsPositive a
    {-# INLINE symFpIsPositive #-}
  
    symFpIsNegative (AsKey a) = symFpIsNegative a
    {-# INLINE symFpIsNegative #-}
  
    symFpIsInfinite (AsKey a) = symFpIsInfinite a
    {-# INLINE symFpIsInfinite #-}
  
    symFpIsPositiveZero (AsKey a) = symFpIsPositiveZero a
    {-# INLINE symFpIsPositiveZero #-}
  
    symFpIsNegativeZero (AsKey a) = symFpIsNegativeZero a
    {-# INLINE symFpIsNegativeZero #-}
  
    symFpIsZero (AsKey a) = symFpIsZero a
    {-# INLINE symFpIsZero #-}
  
    symFpIsNormal (AsKey a) = symFpIsNormal a
    {-# INLINE symFpIsNormal #-}
  
    symFpIsSubnormal (AsKey a) = symFpIsSubnormal a
    {-# INLINE symFpIsSubnormal #-}
  
    symFpIsPoint (AsKey a) = symFpIsPoint a
    {-# INLINE symFpIsPoint #-}
  
    symFpIsPositiveInfinite (AsKey a) = symFpIsPositiveInfinite a
    {-# INLINE symFpIsPositiveInfinite #-}
  
    symFpIsNegativeInfinite (AsKey a) = symFpIsNegativeInfinite a
    {-# INLINE symFpIsNegativeInfinite #-}
  