{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# 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,
    SymIEEEFPTraits (..),
    IEEEConstants (..),
    IEEEFPRoundingMode (..),
    IEEEFPOp (..),
    IEEEFPRoundingOp (..),
  )
where

import Data.SBV (infinity, nan)
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.SymPrim.FP (FP (FP), FPRoundingMode (RNA, RNE, RTN, RTP, RTZ), ValidFP)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP
  ( pevalFPBinaryTerm,
    pevalFPFMATerm,
    pevalFPRoundingBinaryTerm,
    pevalFPRoundingUnaryTerm,
    pevalFPTraitTerm,
    pevalFPUnaryTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( FPBinaryOp (FPMax, FPMin, FPRem),
    FPRoundingBinaryOp (FPAdd, FPDiv, FPMul, FPSub),
    FPRoundingUnaryOp (FPRoundToIntegral, FPSqrt),
    FPTrait
      ( FPIsInfinite,
        FPIsNaN,
        FPIsNegative,
        FPIsNegativeInfinite,
        FPIsNegativeZero,
        FPIsNormal,
        FPIsPoint,
        FPIsPositive,
        FPIsPositiveInfinite,
        FPIsPositiveZero,
        FPIsSubnormal,
        FPIsZero
      ),
    FPUnaryOp (FPAbs, FPNeg),
  )
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
import Grisette.Internal.SymPrim.SymFP (SymFP (SymFP), SymFPRoundingMode (SymFPRoundingMode))

-- | 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 -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero
{-# 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 #-}

-- | 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 f -> SymBool
symFpIsNaN (ConcreteFloat f
x) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ f -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN f
x
  {-# INLINE symFpIsNaN #-}

  symFpIsPositive :: ConcreteFloat f -> SymBool
symFpIsPositive (ConcreteFloat f
x) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ f -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositive f
x
  {-# INLINE symFpIsPositive #-}

  symFpIsNegative :: ConcreteFloat f -> SymBool
symFpIsNegative (ConcreteFloat f
x) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ f -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegative f
x
  {-# INLINE symFpIsNegative #-}

  symFpIsInfinite :: ConcreteFloat f -> SymBool
symFpIsInfinite (ConcreteFloat f
x) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ f -> Bool
forall a. RealFloat a => a -> Bool
fpIsInfinite f
x
  {-# INLINE symFpIsInfinite #-}

  symFpIsPositiveInfinite :: ConcreteFloat f -> SymBool
symFpIsPositiveInfinite (ConcreteFloat f
x) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ f -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveInfinite f
x
  {-# INLINE symFpIsPositiveInfinite #-}

  symFpIsNegativeInfinite :: ConcreteFloat f -> SymBool
symFpIsNegativeInfinite (ConcreteFloat f
x) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ f -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeInfinite f
x
  {-# INLINE symFpIsNegativeInfinite #-}

  symFpIsPositiveZero :: ConcreteFloat f -> SymBool
symFpIsPositiveZero (ConcreteFloat f
x) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ f -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveZero f
x
  {-# INLINE symFpIsPositiveZero #-}

  symFpIsNegativeZero :: ConcreteFloat f -> SymBool
symFpIsNegativeZero (ConcreteFloat f
x) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ f -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeZero f
x
  {-# INLINE symFpIsNegativeZero #-}

  symFpIsZero :: ConcreteFloat f -> SymBool
symFpIsZero (ConcreteFloat f
x) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ f -> Bool
forall a. RealFloat a => a -> Bool
fpIsZero f
x
  {-# INLINE symFpIsZero #-}

  symFpIsNormal :: ConcreteFloat f -> SymBool
symFpIsNormal (ConcreteFloat f
x) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ f -> Bool
forall a. RealFloat a => a -> Bool
fpIsNormal f
x
  {-# INLINE symFpIsNormal #-}

  symFpIsSubnormal :: ConcreteFloat f -> SymBool
symFpIsSubnormal (ConcreteFloat f
x) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ f -> Bool
forall a. RealFloat a => a -> Bool
fpIsSubnormal f
x
  {-# INLINE symFpIsSubnormal #-}

  symFpIsPoint :: ConcreteFloat f -> SymBool
symFpIsPoint (ConcreteFloat f
x) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ f -> Bool
forall a. RealFloat a => a -> Bool
fpIsPoint f
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 (ValidFP eb sb) => SymIEEEFPTraits (SymFP eb sb) where
  symFpIsNaN :: SymFP eb sb -> SymBool
symFpIsNaN (SymFP Term (FP eb sb)
x) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
FPIsNaN Term (FP eb sb)
x
  {-# INLINE symFpIsNaN #-}
  symFpIsPositive :: SymFP eb sb -> SymBool
symFpIsPositive (SymFP Term (FP eb sb)
x) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
FPIsPositive Term (FP eb sb)
x
  {-# INLINE symFpIsPositive #-}
  symFpIsNegative :: SymFP eb sb -> SymBool
symFpIsNegative (SymFP Term (FP eb sb)
x) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
FPIsNegative Term (FP eb sb)
x
  {-# INLINE symFpIsNegative #-}
  symFpIsInfinite :: SymFP eb sb -> SymBool
symFpIsInfinite (SymFP Term (FP eb sb)
x) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
FPIsInfinite Term (FP eb sb)
x
  {-# INLINE symFpIsInfinite #-}
  symFpIsPositiveInfinite :: SymFP eb sb -> SymBool
symFpIsPositiveInfinite (SymFP Term (FP eb sb)
x) =
    Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
FPIsPositiveInfinite Term (FP eb sb)
x
  {-# INLINE symFpIsPositiveInfinite #-}
  symFpIsNegativeInfinite :: SymFP eb sb -> SymBool
symFpIsNegativeInfinite (SymFP Term (FP eb sb)
x) =
    Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
FPIsNegativeInfinite Term (FP eb sb)
x
  {-# INLINE symFpIsNegativeInfinite #-}
  symFpIsPositiveZero :: SymFP eb sb -> SymBool
symFpIsPositiveZero (SymFP Term (FP eb sb)
x) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
FPIsPositiveZero Term (FP eb sb)
x
  {-# INLINE symFpIsPositiveZero #-}
  symFpIsNegativeZero :: SymFP eb sb -> SymBool
symFpIsNegativeZero (SymFP Term (FP eb sb)
x) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
FPIsNegativeZero Term (FP eb sb)
x
  {-# INLINE symFpIsNegativeZero #-}
  symFpIsZero :: SymFP eb sb -> SymBool
symFpIsZero (SymFP Term (FP eb sb)
x) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
FPIsZero Term (FP eb sb)
x
  {-# INLINE symFpIsZero #-}
  symFpIsNormal :: SymFP eb sb -> SymBool
symFpIsNormal (SymFP Term (FP eb sb)
x) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
FPIsNormal Term (FP eb sb)
x
  {-# INLINE symFpIsNormal #-}
  symFpIsSubnormal :: SymFP eb sb -> SymBool
symFpIsSubnormal (SymFP Term (FP eb sb)
x) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
FPIsSubnormal Term (FP eb sb)
x
  {-# INLINE symFpIsSubnormal #-}
  symFpIsPoint :: SymFP eb sb -> SymBool
symFpIsPoint (SymFP Term (FP eb sb)
x) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
FPIsPoint Term (FP eb sb)
x
  {-# INLINE symFpIsPoint #-}

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

  -- | Negative infinity.
  fpNegativeInfinite :: a

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

  -- | Negative zero.
  fpNegativeZero :: a

  -- | Positive zero.
  fpPositiveZero :: a

instance (ValidFP eb sb) => IEEEConstants (FP eb sb) where
  fpPositiveInfinite :: FP eb sb
fpPositiveInfinite = FloatingPoint eb sb -> FP eb sb
forall (eb :: Nat) (sb :: Nat). FloatingPoint eb sb -> FP eb sb
FP FloatingPoint eb sb
forall a. Floating a => a
infinity
  {-# INLINE fpPositiveInfinite #-}
  fpNegativeInfinite :: FP eb sb
fpNegativeInfinite = FloatingPoint eb sb -> FP eb sb
forall (eb :: Nat) (sb :: Nat). FloatingPoint eb sb -> FP eb sb
FP (FloatingPoint eb sb -> FP eb sb)
-> FloatingPoint eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ -FloatingPoint eb sb
forall a. Floating a => a
infinity
  {-# INLINE fpNegativeInfinite #-}
  fpNaN :: FP eb sb
fpNaN = FloatingPoint eb sb -> FP eb sb
forall (eb :: Nat) (sb :: Nat). FloatingPoint eb sb -> FP eb sb
FP FloatingPoint eb sb
forall a. Floating a => a
nan
  {-# INLINE fpNaN #-}
  fpNegativeZero :: FP eb sb
fpNegativeZero = FloatingPoint eb sb -> FP eb sb
forall (eb :: Nat) (sb :: Nat). FloatingPoint eb sb -> FP eb sb
FP (FloatingPoint eb sb -> FP eb sb)
-> FloatingPoint eb sb -> FP eb sb
forall a b. (a -> b) -> a -> b
$ -FloatingPoint eb sb
0
  {-# INLINE fpNegativeZero #-}
  fpPositiveZero :: FP eb sb
fpPositiveZero = FloatingPoint eb sb -> FP eb sb
forall (eb :: Nat) (sb :: Nat). FloatingPoint eb sb -> FP eb sb
FP FloatingPoint eb sb
0
  {-# INLINE fpPositiveZero #-}

instance (ValidFP eb sb) => IEEEConstants (SymFP eb sb) where
  fpPositiveInfinite :: SymFP eb sb
fpPositiveInfinite = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con FP eb sb
forall a. IEEEConstants a => a
fpPositiveInfinite
  {-# INLINE fpPositiveInfinite #-}
  fpNegativeInfinite :: SymFP eb sb
fpNegativeInfinite = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con FP eb sb
forall a. IEEEConstants a => a
fpNegativeInfinite
  {-# INLINE fpNegativeInfinite #-}
  fpNaN :: SymFP eb sb
fpNaN = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con FP eb sb
forall a. IEEEConstants a => a
fpNaN
  {-# INLINE fpNaN #-}
  fpNegativeZero :: SymFP eb sb
fpNegativeZero = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con FP eb sb
forall a. IEEEConstants a => a
fpNegativeZero
  {-# INLINE fpNegativeZero #-}
  fpPositiveZero :: SymFP eb sb
fpPositiveZero = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con FP eb sb
forall a. IEEEConstants a => a
fpPositiveZero
  {-# INLINE fpPositiveZero #-}

-- | Operations on IEEE floating-point numbers, without rounding mode.
class IEEEFPOp a where
  symFpAbs :: a -> a
  symFpNeg :: a -> a
  symFpRem :: a -> a -> a
  symFpMin :: a -> a -> a
  symFpMax :: a -> a -> a

instance (ValidFP eb sb) => IEEEFPOp (SymFP eb sb) where
  symFpAbs :: SymFP eb sb -> SymFP eb sb
symFpAbs (SymFP Term (FP eb sb)
l) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPUnaryTerm FPUnaryOp
FPAbs Term (FP eb sb)
l
  {-# INLINE symFpAbs #-}
  symFpNeg :: SymFP eb sb -> SymFP eb sb
symFpNeg (SymFP Term (FP eb sb)
l) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPUnaryTerm FPUnaryOp
FPNeg Term (FP eb sb)
l
  {-# INLINE symFpNeg #-}
  symFpRem :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
symFpRem (SymFP Term (FP eb sb)
l) (SymFP Term (FP eb sb)
r) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPBinaryTerm FPBinaryOp
FPRem Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE symFpRem #-}
  symFpMin :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
symFpMin (SymFP Term (FP eb sb)
l) (SymFP Term (FP eb sb)
r) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPBinaryTerm FPBinaryOp
FPMin Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE symFpMin #-}
  symFpMax :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
symFpMax (SymFP Term (FP eb sb)
l) (SymFP Term (FP eb sb)
r) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPBinaryTerm FPBinaryOp
FPMax Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE symFpMax #-}

-- | 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

instance IEEEFPRoundingMode FPRoundingMode where
  rne :: FPRoundingMode
rne = FPRoundingMode
RNE
  {-# INLINE rne #-}
  rna :: FPRoundingMode
rna = FPRoundingMode
RNA
  {-# INLINE rna #-}
  rtp :: FPRoundingMode
rtp = FPRoundingMode
RTP
  {-# INLINE rtp #-}
  rtn :: FPRoundingMode
rtn = FPRoundingMode
RTN
  {-# INLINE rtn #-}
  rtz :: FPRoundingMode
rtz = FPRoundingMode
RTZ
  {-# INLINE rtz #-}

instance IEEEFPRoundingMode SymFPRoundingMode where
  rne :: SymFPRoundingMode
rne = FPRoundingMode -> SymFPRoundingMode
forall c t. Solvable c t => c -> t
con FPRoundingMode
RNE
  {-# INLINE rne #-}
  rna :: SymFPRoundingMode
rna = FPRoundingMode -> SymFPRoundingMode
forall c t. Solvable c t => c -> t
con FPRoundingMode
RNA
  {-# INLINE rna #-}
  rtp :: SymFPRoundingMode
rtp = FPRoundingMode -> SymFPRoundingMode
forall c t. Solvable c t => c -> t
con FPRoundingMode
RTP
  {-# INLINE rtp #-}
  rtn :: SymFPRoundingMode
rtn = FPRoundingMode -> SymFPRoundingMode
forall c t. Solvable c t => c -> t
con FPRoundingMode
RTN
  {-# INLINE rtn #-}
  rtz :: SymFPRoundingMode
rtz = FPRoundingMode -> SymFPRoundingMode
forall c t. Solvable c t => c -> t
con FPRoundingMode
RTZ
  {-# INLINE rtz #-}

-- | Operations on IEEE floating-point numbers, with rounding mode.
class (IEEEFPRoundingMode mode) => IEEEFPRoundingOp a mode | a -> mode where
  symFpAdd :: mode -> a -> a -> a
  symFpSub :: mode -> a -> a -> a
  symFpMul :: mode -> a -> a -> a
  symFpDiv :: mode -> a -> a -> a
  symFpFMA :: mode -> a -> a -> a -> a
  symFpSqrt :: mode -> a -> a
  symFpRoundToIntegral :: mode -> a -> a

instance (ValidFP eb sb) => IEEEFPRoundingOp (SymFP eb sb) SymFPRoundingMode where
  symFpAdd :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
symFpAdd (SymFPRoundingMode Term FPRoundingMode
mode) (SymFP Term (FP eb sb)
l) (SymFP Term (FP eb sb)
r) =
    Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb),
 SupportedPrim FPRoundingMode) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm FPRoundingBinaryOp
FPAdd Term FPRoundingMode
mode Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE symFpAdd #-}
  symFpSub :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
symFpSub (SymFPRoundingMode Term FPRoundingMode
mode) (SymFP Term (FP eb sb)
l) (SymFP Term (FP eb sb)
r) =
    Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb),
 SupportedPrim FPRoundingMode) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm FPRoundingBinaryOp
FPSub Term FPRoundingMode
mode Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE symFpSub #-}
  symFpMul :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
symFpMul (SymFPRoundingMode Term FPRoundingMode
mode) (SymFP Term (FP eb sb)
l) (SymFP Term (FP eb sb)
r) =
    Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb),
 SupportedPrim FPRoundingMode) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm FPRoundingBinaryOp
FPMul Term FPRoundingMode
mode Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE symFpMul #-}
  symFpDiv :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
symFpDiv (SymFPRoundingMode Term FPRoundingMode
mode) (SymFP Term (FP eb sb)
l) (SymFP Term (FP eb sb)
r) =
    Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb),
 SupportedPrim FPRoundingMode) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm FPRoundingBinaryOp
FPDiv Term FPRoundingMode
mode Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE symFpDiv #-}
  symFpFMA :: SymFPRoundingMode
-> SymFP eb sb -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
symFpFMA (SymFPRoundingMode Term FPRoundingMode
mode) (SymFP Term (FP eb sb)
l) (SymFP Term (FP eb sb)
m) (SymFP Term (FP eb sb)
r) =
    Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb),
 SupportedPrim FPRoundingMode) =>
Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPFMATerm Term FPRoundingMode
mode Term (FP eb sb)
l Term (FP eb sb)
m Term (FP eb sb)
r
  {-# INLINE symFpFMA #-}
  symFpSqrt :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb
symFpSqrt (SymFPRoundingMode Term FPRoundingMode
mode) (SymFP Term (FP eb sb)
v) =
    Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb),
 SupportedPrim FPRoundingMode) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPRoundingUnaryTerm FPRoundingUnaryOp
FPSqrt Term FPRoundingMode
mode Term (FP eb sb)
v
  {-# INLINE symFpSqrt #-}
  symFpRoundToIntegral :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb
symFpRoundToIntegral (SymFPRoundingMode Term FPRoundingMode
mode) (SymFP Term (FP eb sb)
v) =
    Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb),
 SupportedPrim FPRoundingMode) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPRoundingUnaryTerm FPRoundingUnaryOp
FPRoundToIntegral Term FPRoundingMode
mode Term (FP eb sb)
v
  {-# INLINE symFpRoundToIntegral #-}