{-# LANGUAGE FlexibleContexts #-}

module Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP
  ( pevalFPTraitTerm,
    sbvFPTraitTerm,
    pevalFPUnaryTerm,
    sbvFPUnaryTerm,
    pevalFPBinaryTerm,
    sbvFPBinaryTerm,
    pevalFPRoundingUnaryTerm,
    sbvFPRoundingUnaryTerm,
    pevalFPRoundingBinaryTerm,
    sbvFPRoundingBinaryTerm,
    pevalFPFMATerm,
    sbvFPFMATerm,
  )
where

import qualified Data.SBV as SBV
import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP)
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),
    SupportedPrim,
    Term (ConTerm),
    conTerm,
    fpBinaryTerm,
    fpFMATerm,
    fpRoundingBinaryTerm,
    fpRoundingUnaryTerm,
    fpTraitTerm,
    fpUnaryTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (unaryUnfoldOnce)

pevalFPTraitTerm ::
  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
  FPTrait ->
  Term (FP eb sb) ->
  Term Bool
pevalFPTraitTerm :: forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
trait = PartialRuleUnary (FP eb sb) Bool
-> TotalRuleUnary (FP eb sb) Bool -> TotalRuleUnary (FP eb sb) Bool
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary (FP eb sb) Bool
forall {t}. RealFloat t => Term t -> Maybe (Term Bool)
doPevalFPTraitTerm (FPTrait -> TotalRuleUnary (FP eb sb) Bool
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
fpTraitTerm FPTrait
trait)
  where
    doPevalFPTraitTerm :: Term t -> Maybe (Term Bool)
doPevalFPTraitTerm (ConTerm Id
_ t
a) = case FPTrait
trait of
      FPTrait
FPIsNaN -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. RealFloat a => a -> Bool
isNaN t
a
      FPTrait
FPIsPositive ->
        Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$
          Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$
            Bool -> Bool
not (t -> Bool
forall a. RealFloat a => a -> Bool
isNaN t
a) Bool -> Bool -> Bool
&& t
a t -> t -> Bool
forall a. Ord a => a -> a -> Bool
>= t
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (t -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero t
a)
      FPTrait
FPIsNegative ->
        Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (t -> Bool
forall a. RealFloat a => a -> Bool
isNaN t
a) Bool -> Bool -> Bool
&& (t
a t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
0 Bool -> Bool -> Bool
|| t -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero t
a)
      FPTrait
FPIsInfinite -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. RealFloat a => a -> Bool
isInfinite t
a
      FPTrait
FPIsPositiveInfinite -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. RealFloat a => a -> Bool
isInfinite t
a Bool -> Bool -> Bool
&& t
a t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0
      FPTrait
FPIsNegativeInfinite -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. RealFloat a => a -> Bool
isInfinite t
a Bool -> Bool -> Bool
&& t
a t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
0
      FPTrait
FPIsPositiveZero ->
        Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (t -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero t
a)
      FPTrait
FPIsNegativeZero -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero t
a
      FPTrait
FPIsZero -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0
      FPTrait
FPIsNormal ->
        Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$
          Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$
            Bool -> Bool
not (t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 Bool -> Bool -> Bool
|| t -> Bool
forall a. RealFloat a => a -> Bool
isNaN t
a Bool -> Bool -> Bool
|| t -> Bool
forall a. RealFloat a => a -> Bool
isInfinite t
a Bool -> Bool -> Bool
|| t -> Bool
forall a. RealFloat a => a -> Bool
isDenormalized t
a)
      FPTrait
FPIsSubnormal -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. RealFloat a => a -> Bool
isDenormalized t
a
      FPTrait
FPIsPoint -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (t -> Bool
forall a. RealFloat a => a -> Bool
isNaN t
a Bool -> Bool -> Bool
|| t -> Bool
forall a. RealFloat a => a -> Bool
isInfinite t
a)
    doPevalFPTraitTerm Term t
_ = Maybe (Term Bool)
forall a. Maybe a
Nothing

-- Workaround for https://github.com/GaloisInc/libBF-hs/pull/32, which affects
-- the correctness of the Ord instance for 'Data.SBV.FloatingPoint'.
goodFpIsPositive ::
  (ValidFP eb sb) =>
  SBV.SFloatingPoint eb sb ->
  SBV.SBool
goodFpIsPositive :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsPositive SFloatingPoint eb sb
x =
  SBool -> SBool
SBV.sNot (SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SFloatingPoint eb sb
x) SBool -> SBool -> SBool
SBV..&& SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsPositive SFloatingPoint eb sb
x
{-# INLINE goodFpIsPositive #-}

goodFpIsNegative ::
  (ValidFP eb sb) =>
  SBV.SFloatingPoint eb sb ->
  SBV.SBool
goodFpIsNegative :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsNegative SFloatingPoint eb sb
x = SBool -> SBool
SBV.sNot (SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SFloatingPoint eb sb
x) SBool -> SBool -> SBool
SBV..&& SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNegative SFloatingPoint eb sb
x
{-# INLINE goodFpIsNegative #-}

sbvFPTraitTerm ::
  (ValidFP eb sb) =>
  FPTrait ->
  SBV.SFloatingPoint eb sb ->
  SBV.SBool
sbvFPTraitTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPTrait -> SFloatingPoint eb sb -> SBool
sbvFPTraitTerm FPTrait
FPIsNaN = SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN
sbvFPTraitTerm FPTrait
FPIsPositive = SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsPositive
sbvFPTraitTerm FPTrait
FPIsNegative = SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsNegative
sbvFPTraitTerm FPTrait
FPIsInfinite = SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsInfinite
sbvFPTraitTerm FPTrait
FPIsPositiveInfinite = \SBV (FloatingPoint eb sb)
f ->
  SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsInfinite SBV (FloatingPoint eb sb)
f SBool -> SBool -> SBool
SBV..&& SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsPositive SBV (FloatingPoint eb sb)
f
sbvFPTraitTerm FPTrait
FPIsNegativeInfinite = \SBV (FloatingPoint eb sb)
f ->
  SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsInfinite SBV (FloatingPoint eb sb)
f SBool -> SBool -> SBool
SBV..&& SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsNegative SBV (FloatingPoint eb sb)
f
sbvFPTraitTerm FPTrait
FPIsPositiveZero =
  \SBV (FloatingPoint eb sb)
f -> SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsZero SBV (FloatingPoint eb sb)
f SBool -> SBool -> SBool
SBV..&& SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsPositive SBV (FloatingPoint eb sb)
f
sbvFPTraitTerm FPTrait
FPIsNegativeZero =
  \SBV (FloatingPoint eb sb)
f -> SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsZero SBV (FloatingPoint eb sb)
f SBool -> SBool -> SBool
SBV..&& SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsNegative SBV (FloatingPoint eb sb)
f
sbvFPTraitTerm FPTrait
FPIsZero = SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsZero
sbvFPTraitTerm FPTrait
FPIsNormal = SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNormal
sbvFPTraitTerm FPTrait
FPIsSubnormal = SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsSubnormal
sbvFPTraitTerm FPTrait
FPIsPoint = SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsPoint

pevalFPUnaryTerm ::
  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
  FPUnaryOp ->
  Term (FP eb sb) ->
  Term (FP eb sb)
pevalFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPUnaryTerm = 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)
fpUnaryTerm
{-# INLINE pevalFPUnaryTerm #-}

sbvFPUnaryTerm ::
  (ValidFP eb sb) =>
  FPUnaryOp ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb
sbvFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPUnaryOp -> SFloatingPoint eb sb -> SFloatingPoint eb sb
sbvFPUnaryTerm FPUnaryOp
FPAbs = SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. IEEEFloating a => SBV a -> SBV a
SBV.fpAbs
sbvFPUnaryTerm FPUnaryOp
FPNeg = SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. IEEEFloating a => SBV a -> SBV a
SBV.fpNeg
{-# INLINE sbvFPUnaryTerm #-}

pevalFPBinaryTerm ::
  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
  FPBinaryOp ->
  Term (FP eb sb) ->
  Term (FP eb sb) ->
  Term (FP eb sb)
pevalFPBinaryTerm :: 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 -> 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)
fpBinaryTerm
{-# INLINE pevalFPBinaryTerm #-}

sbvFPBinaryTerm ::
  (ValidFP eb sb) =>
  FPBinaryOp ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb
sbvFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPBinaryOp
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
sbvFPBinaryTerm FPBinaryOp
FPRem = SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. IEEEFloating a => SBV a -> SBV a -> SBV a
SBV.fpRem
sbvFPBinaryTerm FPBinaryOp
FPMin = SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. IEEEFloating a => SBV a -> SBV a -> SBV a
SBV.fpMin
sbvFPBinaryTerm FPBinaryOp
FPMax = SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. IEEEFloating a => SBV a -> SBV a -> SBV a
SBV.fpMax
{-# INLINE sbvFPBinaryTerm #-}

pevalFPRoundingUnaryTerm ::
  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
  FPRoundingUnaryOp ->
  Term FPRoundingMode ->
  Term (FP eb sb) ->
  Term (FP eb sb)
pevalFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPRoundingUnaryTerm = FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
fpRoundingUnaryTerm
{-# INLINE pevalFPRoundingUnaryTerm #-}

sbvFPRoundingUnaryTerm ::
  (ValidFP eb sb) =>
  FPRoundingUnaryOp ->
  SBV.SRoundingMode ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb
sbvFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPRoundingUnaryOp
-> SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb
sbvFPRoundingUnaryTerm FPRoundingUnaryOp
FPSqrt = SRoundingMode
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. IEEEFloating a => SRoundingMode -> SBV a -> SBV a
SBV.fpSqrt
sbvFPRoundingUnaryTerm FPRoundingUnaryOp
FPRoundToIntegral = SRoundingMode
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. IEEEFloating a => SRoundingMode -> SBV a -> SBV a
SBV.fpRoundToIntegral
{-# INLINE sbvFPRoundingUnaryTerm #-}

pevalFPRoundingBinaryTerm ::
  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
  FPRoundingBinaryOp ->
  Term FPRoundingMode ->
  Term (FP eb sb) ->
  Term (FP eb sb) ->
  Term (FP eb sb)
pevalFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm = 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)) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
fpRoundingBinaryTerm
{-# INLINE pevalFPRoundingBinaryTerm #-}

sbvFPRoundingBinaryTerm ::
  (ValidFP eb sb) =>
  FPRoundingBinaryOp ->
  SBV.SRoundingMode ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb
sbvFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPRoundingBinaryOp
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
sbvFPRoundingBinaryTerm FPRoundingBinaryOp
FPAdd = SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a
SBV.fpAdd
sbvFPRoundingBinaryTerm FPRoundingBinaryOp
FPSub = SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a
SBV.fpSub
sbvFPRoundingBinaryTerm FPRoundingBinaryOp
FPMul = SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a
SBV.fpMul
sbvFPRoundingBinaryTerm FPRoundingBinaryOp
FPDiv = SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a
SBV.fpDiv
{-# INLINE sbvFPRoundingBinaryTerm #-}

pevalFPFMATerm ::
  (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 :: 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
-> 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)
fpFMATerm
{-# INLINE pevalFPFMATerm #-}

sbvFPFMATerm ::
  (ValidFP eb sb) =>
  SBV.SRoundingMode ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb
sbvFPFMATerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
sbvFPFMATerm = SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a
SBV.fpFMA
{-# INLINE sbvFPFMATerm #-}