{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.SymFP
-- 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.SymPrim.SymFP
  ( SymFP (SymFP),
    SymFP16,
    SymFP32,
    SymFP64,
    SymFPRoundingMode (SymFPRoundingMode),
  )
where

import Control.DeepSeq (NFData)
import qualified Data.Binary as Binary
import Data.Bytes.Serial (Serial (deserialize, serialize))
import Data.Hashable (Hashable (hashWithSalt))
import Data.Proxy (Proxy (Proxy))
import qualified Data.Serialize as Cereal
import Data.String (IsString (fromString))
import GHC.Generics (Generic)
import GHC.TypeLits (KnownNat, type (+), type (<=))
import Grisette.Internal.Core.Data.Class.BitCast
  ( BitCast (bitCast),
    BitCastCanonical (bitCastCanonicalValue),
    BitCastOr (bitCastOr),
  )
import Grisette.Internal.Core.Data.Class.Function (Apply (FunType, apply))
import Grisette.Internal.Core.Data.Class.IEEEFP
  ( IEEEFPConstants
      ( fpMaxNormalized,
        fpMaxSubnormal,
        fpMinNormalized,
        fpMinSubnormal,
        fpNaN,
        fpNegativeInfinite,
        fpNegativeZero,
        fpPositiveInfinite,
        fpPositiveZero
      ),
    IEEEFPConvertible (fromFPOr, toFP),
    IEEEFPOp
      ( fpAbs,
        fpMaximum,
        fpMaximumNumber,
        fpMinimum,
        fpMinimumNumber,
        fpNeg,
        fpRem
      ),
    IEEEFPRoundingMode (rna, rne, rtn, rtp, rtz),
    IEEEFPRoundingOp
      ( fpAdd,
        fpDiv,
        fpFMA,
        fpMul,
        fpRoundToIntegral,
        fpSqrt,
        fpSub
      ),
    IEEEFPToAlgReal,
  )
import Grisette.Internal.Core.Data.Class.Solvable
  ( Solvable (con, conView, ssym, sym),
  )
import Grisette.Internal.Core.Data.Class.SymIEEEFP
  ( SymIEEEFPTraits
      ( symFpIsInfinite,
        symFpIsNaN,
        symFpIsNegative,
        symFpIsNegativeInfinite,
        symFpIsNegativeZero,
        symFpIsNormal,
        symFpIsPoint,
        symFpIsPositive,
        symFpIsPositiveInfinite,
        symFpIsPositiveZero,
        symFpIsSubnormal,
        symFpIsZero
      ),
  )
import Grisette.Internal.Internal.Decl.SymPrim.AllSyms
  ( AllSyms (allSymsS),
    SomeSym (SomeSym),
  )
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP
  ( FP,
    FPRoundingMode (RNA, RNE, RTN, RTP, RTZ),
    ValidFP,
    withValidFPProofs,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP
  ( pevalFPBinaryTerm,
    pevalFPFMATerm,
    pevalFPRoundingBinaryTerm,
    pevalFPRoundingUnaryTerm,
    pevalFPTraitTerm,
    pevalFPUnaryTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( ConRep (ConType),
    FPBinaryOp (FPMaximum, FPMaximumNumber, FPMinimum, FPMinimumNumber, 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),
    FloatingUnaryOp (FloatingSqrt),
    LinkedRep (underlyingTerm, wrapTerm),
    PEvalBitCastOrTerm (pevalBitCastOrTerm),
    PEvalBitCastTerm (pevalBitCastTerm),
    PEvalFloatingTerm (pevalFloatingUnaryTerm),
    PEvalFractionalTerm (pevalFdivTerm, pevalRecipTerm),
    PEvalIEEEFPConvertibleTerm (pevalFromFPOrTerm, pevalToFPTerm),
    PEvalNumTerm
      ( pevalAbsNumTerm,
        pevalAddNumTerm,
        pevalMulNumTerm,
        pevalNegNumTerm,
        pevalSignumNumTerm
      ),
    SymRep (SymType),
    Term (ConTerm),
    conTerm,
    pevalSubNumTerm,
    pformatTerm,
    symTerm,
    typedConstantSymbol,
  )
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))
import Grisette.Internal.SymPrim.SymBV (SymIntN (SymIntN), SymWordN (SymWordN))
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))
import Language.Haskell.TH.Syntax (Lift)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Grisette.Backend
-- >>> import Data.Proxy

-- | Symbolic IEEE 754 floating-point number with @eb@ exponent bits and @sb@
-- significand bits.
--
-- >>> "a" + 2.0 :: SymFP 11 53
-- (+ a 2.0)
-- >>> fpAdd rne "a" 2.0 :: SymFP 11 53
-- (fp.add rne a 2.0)
--
-- More operations are available. Please refer to "Grisette.Core#g:symops" for
-- more information.
newtype SymFP eb sb = SymFP {forall (eb :: Nat) (sb :: Nat). SymFP eb sb -> Term (FP eb sb)
underlyingFPTerm :: Term (FP eb sb)}
  deriving ((forall (m :: * -> *). Quote m => SymFP eb sb -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    SymFP eb sb -> Code m (SymFP eb sb))
-> Lift (SymFP eb sb)
forall (eb :: Nat) (sb :: Nat) (m :: * -> *).
Quote m =>
SymFP eb sb -> m Exp
forall (eb :: Nat) (sb :: Nat) (m :: * -> *).
Quote m =>
SymFP eb sb -> Code m (SymFP eb sb)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymFP eb sb -> m Exp
forall (m :: * -> *).
Quote m =>
SymFP eb sb -> Code m (SymFP eb sb)
$clift :: forall (eb :: Nat) (sb :: Nat) (m :: * -> *).
Quote m =>
SymFP eb sb -> m Exp
lift :: forall (m :: * -> *). Quote m => SymFP eb sb -> m Exp
$cliftTyped :: forall (eb :: Nat) (sb :: Nat) (m :: * -> *).
Quote m =>
SymFP eb sb -> Code m (SymFP eb sb)
liftTyped :: forall (m :: * -> *).
Quote m =>
SymFP eb sb -> Code m (SymFP eb sb)
Lift, (forall x. SymFP eb sb -> Rep (SymFP eb sb) x)
-> (forall x. Rep (SymFP eb sb) x -> SymFP eb sb)
-> Generic (SymFP eb sb)
forall (eb :: Nat) (sb :: Nat) x.
Rep (SymFP eb sb) x -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat) x.
SymFP eb sb -> Rep (SymFP eb sb) x
forall x. Rep (SymFP eb sb) x -> SymFP eb sb
forall x. SymFP eb sb -> Rep (SymFP eb sb) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (eb :: Nat) (sb :: Nat) x.
SymFP eb sb -> Rep (SymFP eb sb) x
from :: forall x. SymFP eb sb -> Rep (SymFP eb sb) x
$cto :: forall (eb :: Nat) (sb :: Nat) x.
Rep (SymFP eb sb) x -> SymFP eb sb
to :: forall x. Rep (SymFP eb sb) x -> SymFP eb sb
Generic)
  deriving anyclass (SymFP eb sb -> ()
(SymFP eb sb -> ()) -> NFData (SymFP eb sb)
forall (eb :: Nat) (sb :: Nat). SymFP eb sb -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (eb :: Nat) (sb :: Nat). SymFP eb sb -> ()
rnf :: SymFP eb sb -> ()
NFData)

-- | Symbolic IEEE 754 half-precision floating-point number.
type SymFP16 = SymFP 5 11

-- | Symbolic IEEE 754 single-precision floating-point number.
type SymFP32 = SymFP 8 24

-- | Symbolic IEEE 754 double-precision floating-point number.
type SymFP64 = SymFP 11 53

instance ConRep (SymFP eb sb) where
  type ConType (SymFP eb sb) = FP eb sb

instance (ValidFP eb sb) => SymRep (FP eb sb) where
  type SymType (FP eb sb) = SymFP eb sb

instance (ValidFP eb sb) => LinkedRep (FP eb sb) (SymFP eb sb) where
  underlyingTerm :: SymFP eb sb -> Term (FP eb sb)
underlyingTerm (SymFP Term (FP eb sb)
a) = Term (FP eb sb)
a
  wrapTerm :: Term (FP eb sb) -> SymFP eb sb
wrapTerm = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP

instance (ValidFP eb sb) => Apply (SymFP eb sb) where
  type FunType (SymFP eb sb) = SymFP eb sb
  apply :: SymFP eb sb -> FunType (SymFP eb sb)
apply = SymFP eb sb -> FunType (SymFP eb sb)
SymFP eb sb -> SymFP eb sb
forall a. a -> a
id

instance (ValidFP eb sb) => Eq (SymFP eb sb) where
  SymFP Term (FP eb sb)
a == :: SymFP eb sb -> SymFP eb sb -> Bool
== SymFP Term (FP eb sb)
b = Term (FP eb sb)
a Term (FP eb sb) -> Term (FP eb sb) -> Bool
forall a. Eq a => a -> a -> Bool
== Term (FP eb sb)
b

instance (ValidFP eb sb) => Hashable (SymFP eb sb) where
  hashWithSalt :: Int -> SymFP eb sb -> Int
hashWithSalt Int
s (SymFP Term (FP eb sb)
a) = Int -> Term (FP eb sb) -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Term (FP eb sb)
a

instance (ValidFP eb sb) => IsString (SymFP eb sb) where
  fromString :: String -> SymFP eb sb
fromString = Identifier -> SymFP eb sb
forall c t. Solvable c t => Identifier -> t
ssym (Identifier -> SymFP eb sb)
-> (String -> Identifier) -> String -> SymFP eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Identifier
forall a. IsString a => String -> a
fromString

instance (ValidFP eb sb) => Solvable (FP eb sb) (SymFP eb sb) where
  con :: FP eb sb -> SymFP eb sb
con = 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)
-> (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> SymFP eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm
  sym :: Symbol -> SymFP eb sb
sym = 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)
-> (Symbol -> Term (FP eb sb)) -> Symbol -> SymFP eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol 'ConstantKind (FP eb sb) -> Term (FP eb sb)
forall (knd :: SymbolKind) t. TypedSymbol knd t -> Term t
symTerm (TypedSymbol 'ConstantKind (FP eb sb) -> Term (FP eb sb))
-> (Symbol -> TypedSymbol 'ConstantKind (FP eb sb))
-> Symbol
-> Term (FP eb sb)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> TypedSymbol 'ConstantKind (FP eb sb)
forall t.
SupportedNonFuncPrim t =>
Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol
  conView :: SymFP eb sb -> Maybe (FP eb sb)
conView (SymFP (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FP eb sb
t)) = FP eb sb -> Maybe (FP eb sb)
forall a. a -> Maybe a
Just FP eb sb
t
  conView SymFP eb sb
_ = Maybe (FP eb sb)
forall a. Maybe a
Nothing

instance (ValidFP eb sb) => Show (SymFP eb sb) where
  show :: SymFP eb sb -> String
show (SymFP Term (FP eb sb)
a) = Term (FP eb sb) -> String
forall t. Term t -> String
pformatTerm Term (FP eb sb)
a

instance (ValidFP eb sb) => AllSyms (SymFP eb sb) where
  allSymsS :: SymFP eb sb -> [SomeSym] -> [SomeSym]
allSymsS SymFP eb sb
v = (SymFP eb sb -> SomeSym
forall con sym. LinkedRep con sym => sym -> SomeSym
SomeSym SymFP eb sb
v SomeSym -> [SomeSym] -> [SomeSym]
forall a. a -> [a] -> [a]
:)

instance (ValidFP eb sb) => Num (SymFP eb sb) where
  (SymFP Term (FP eb sb)
l) + :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
+ (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 (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalAddNumTerm Term (FP eb sb)
l Term (FP eb sb)
r
  (SymFP Term (FP eb sb)
l) - :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
- (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 (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalSubNumTerm Term (FP eb sb)
l Term (FP eb sb)
r
  (SymFP Term (FP eb sb)
l) * :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
* (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 (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalMulNumTerm Term (FP eb sb)
l Term (FP eb sb)
r
  negate :: SymFP eb sb -> SymFP eb sb
negate (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
$ Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term (FP eb sb)
v
  abs :: SymFP eb sb -> SymFP eb sb
abs (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
$ Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalNumTerm t => Term t -> Term t
pevalAbsNumTerm Term (FP eb sb)
v
  signum :: SymFP eb sb -> SymFP eb sb
signum (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
$ Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalNumTerm t => Term t -> Term t
pevalSignumNumTerm Term (FP eb sb)
v
  fromInteger :: Integer -> SymFP eb sb
fromInteger = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb)
-> (Integer -> FP eb sb) -> Integer -> SymFP eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> FP eb sb
forall a. Num a => Integer -> a
fromInteger

instance (ValidFP eb sb) => Fractional (SymFP eb sb) where
  (SymFP Term (FP eb sb)
l) / :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
/ (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 (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalFractionalTerm t => Term t -> Term t -> Term t
pevalFdivTerm Term (FP eb sb)
l Term (FP eb sb)
r
  recip :: SymFP eb sb -> SymFP eb sb
recip (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
$ Term (FP eb sb) -> Term (FP eb sb)
forall t. PEvalFractionalTerm t => Term t -> Term t
pevalRecipTerm Term (FP eb sb)
v
  fromRational :: Rational -> SymFP eb sb
fromRational = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb)
-> (Rational -> FP eb sb) -> Rational -> SymFP eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> FP eb sb
forall a. Fractional a => Rational -> a
fromRational

instance (ValidFP eb sb) => Floating (SymFP eb sb) where
  pi :: SymFP eb sb
pi = String -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"pi isn't supported by the underlying sbv library"
  exp :: SymFP eb sb -> SymFP eb sb
exp = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"exp isn't supported by the underlying sbv library"
  log :: SymFP eb sb -> SymFP eb sb
log = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"log isn't supported by the underlying sbv library"
  sqrt :: SymFP eb sb -> SymFP eb sb
sqrt (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
$ FloatingUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
FloatingSqrt Term (FP eb sb)
v
  ** :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
(**) = String -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"(**) isn't supported by the underlying sbv library"
  logBase :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
logBase = String -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"logBase isn't supported by the underlying sbv library"
  sin :: SymFP eb sb -> SymFP eb sb
sin = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"sin isn't supported by the underlying sbv library"
  cos :: SymFP eb sb -> SymFP eb sb
cos = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"cos isn't supported by the underlying sbv library"
  asin :: SymFP eb sb -> SymFP eb sb
asin = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"asin isn't supported by the underlying sbv library"
  acos :: SymFP eb sb -> SymFP eb sb
acos = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"acos isn't supported by the underlying sbv library"
  atan :: SymFP eb sb -> SymFP eb sb
atan = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"atan isn't supported by the underlying sbv library"
  sinh :: SymFP eb sb -> SymFP eb sb
sinh = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"sinh isn't supported by the underlying sbv library"
  cosh :: SymFP eb sb -> SymFP eb sb
cosh = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"cosh isn't supported by the underlying sbv library"
  asinh :: SymFP eb sb -> SymFP eb sb
asinh = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"asinh isn't supported by the underlying sbv library"
  acosh :: SymFP eb sb -> SymFP eb sb
acosh = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"acosh isn't supported by the underlying sbv library"
  atanh :: SymFP eb sb -> SymFP eb sb
atanh = String -> SymFP eb sb -> SymFP eb sb
forall a. HasCallStack => String -> a
error String
"atanh isn't supported by the underlying sbv library"

-- | Symbolic floating-point rounding mode.
newtype SymFPRoundingMode = SymFPRoundingMode (Term FPRoundingMode)
  deriving ((forall (m :: * -> *). Quote m => SymFPRoundingMode -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    SymFPRoundingMode -> Code m SymFPRoundingMode)
-> Lift SymFPRoundingMode
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymFPRoundingMode -> m Exp
forall (m :: * -> *).
Quote m =>
SymFPRoundingMode -> Code m SymFPRoundingMode
$clift :: forall (m :: * -> *). Quote m => SymFPRoundingMode -> m Exp
lift :: forall (m :: * -> *). Quote m => SymFPRoundingMode -> m Exp
$cliftTyped :: forall (m :: * -> *).
Quote m =>
SymFPRoundingMode -> Code m SymFPRoundingMode
liftTyped :: forall (m :: * -> *).
Quote m =>
SymFPRoundingMode -> Code m SymFPRoundingMode
Lift, (forall x. SymFPRoundingMode -> Rep SymFPRoundingMode x)
-> (forall x. Rep SymFPRoundingMode x -> SymFPRoundingMode)
-> Generic SymFPRoundingMode
forall x. Rep SymFPRoundingMode x -> SymFPRoundingMode
forall x. SymFPRoundingMode -> Rep SymFPRoundingMode x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SymFPRoundingMode -> Rep SymFPRoundingMode x
from :: forall x. SymFPRoundingMode -> Rep SymFPRoundingMode x
$cto :: forall x. Rep SymFPRoundingMode x -> SymFPRoundingMode
to :: forall x. Rep SymFPRoundingMode x -> SymFPRoundingMode
Generic)
  deriving anyclass (SymFPRoundingMode -> ()
(SymFPRoundingMode -> ()) -> NFData SymFPRoundingMode
forall a. (a -> ()) -> NFData a
$crnf :: SymFPRoundingMode -> ()
rnf :: SymFPRoundingMode -> ()
NFData)

instance ConRep SymFPRoundingMode where
  type ConType SymFPRoundingMode = FPRoundingMode

instance SymRep FPRoundingMode where
  type SymType FPRoundingMode = SymFPRoundingMode

instance LinkedRep FPRoundingMode SymFPRoundingMode where
  underlyingTerm :: SymFPRoundingMode -> Term FPRoundingMode
underlyingTerm (SymFPRoundingMode Term FPRoundingMode
a) = Term FPRoundingMode
a
  wrapTerm :: Term FPRoundingMode -> SymFPRoundingMode
wrapTerm = Term FPRoundingMode -> SymFPRoundingMode
SymFPRoundingMode

instance Apply SymFPRoundingMode where
  type FunType SymFPRoundingMode = SymFPRoundingMode
  apply :: SymFPRoundingMode -> FunType SymFPRoundingMode
apply = SymFPRoundingMode -> FunType SymFPRoundingMode
SymFPRoundingMode -> SymFPRoundingMode
forall a. a -> a
id

instance Eq SymFPRoundingMode where
  SymFPRoundingMode Term FPRoundingMode
a == :: SymFPRoundingMode -> SymFPRoundingMode -> Bool
== SymFPRoundingMode Term FPRoundingMode
b = Term FPRoundingMode
a Term FPRoundingMode -> Term FPRoundingMode -> Bool
forall a. Eq a => a -> a -> Bool
== Term FPRoundingMode
b

instance Hashable SymFPRoundingMode where
  hashWithSalt :: Int -> SymFPRoundingMode -> Int
hashWithSalt Int
s (SymFPRoundingMode Term FPRoundingMode
a) = Int -> Term FPRoundingMode -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Term FPRoundingMode
a

instance IsString SymFPRoundingMode where
  fromString :: String -> SymFPRoundingMode
fromString = Identifier -> SymFPRoundingMode
forall c t. Solvable c t => Identifier -> t
ssym (Identifier -> SymFPRoundingMode)
-> (String -> Identifier) -> String -> SymFPRoundingMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Identifier
forall a. IsString a => String -> a
fromString

instance Solvable FPRoundingMode SymFPRoundingMode where
  con :: FPRoundingMode -> SymFPRoundingMode
con = Term FPRoundingMode -> SymFPRoundingMode
SymFPRoundingMode (Term FPRoundingMode -> SymFPRoundingMode)
-> (FPRoundingMode -> Term FPRoundingMode)
-> FPRoundingMode
-> SymFPRoundingMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FPRoundingMode -> Term FPRoundingMode
forall t. SupportedPrim t => t -> Term t
conTerm
  sym :: Symbol -> SymFPRoundingMode
sym = Term FPRoundingMode -> SymFPRoundingMode
SymFPRoundingMode (Term FPRoundingMode -> SymFPRoundingMode)
-> (Symbol -> Term FPRoundingMode) -> Symbol -> SymFPRoundingMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol 'ConstantKind FPRoundingMode -> Term FPRoundingMode
forall (knd :: SymbolKind) t. TypedSymbol knd t -> Term t
symTerm (TypedSymbol 'ConstantKind FPRoundingMode -> Term FPRoundingMode)
-> (Symbol -> TypedSymbol 'ConstantKind FPRoundingMode)
-> Symbol
-> Term FPRoundingMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> TypedSymbol 'ConstantKind FPRoundingMode
forall t.
SupportedNonFuncPrim t =>
Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol
  conView :: SymFPRoundingMode -> Maybe FPRoundingMode
conView (SymFPRoundingMode (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FPRoundingMode
t)) = FPRoundingMode -> Maybe FPRoundingMode
forall a. a -> Maybe a
Just FPRoundingMode
t
  conView SymFPRoundingMode
_ = Maybe FPRoundingMode
forall a. Maybe a
Nothing

instance Show SymFPRoundingMode where
  show :: SymFPRoundingMode -> String
show (SymFPRoundingMode Term FPRoundingMode
a) = Term FPRoundingMode -> String
forall t. Term t -> String
pformatTerm Term FPRoundingMode
a

instance AllSyms SymFPRoundingMode where
  allSymsS :: SymFPRoundingMode -> [SomeSym] -> [SomeSym]
allSymsS SymFPRoundingMode
v = (SymFPRoundingMode -> SomeSym
forall con sym. LinkedRep con sym => sym -> SomeSym
SomeSym SymFPRoundingMode
v SomeSym -> [SomeSym] -> [SomeSym]
forall a. a -> [a] -> [a]
:)

instance
  (ValidFP eb sb, r ~ (eb + sb)) =>
  BitCastCanonical (SymFP eb sb) (SymWordN r)
  where
  bitCastCanonicalValue :: forall (proxy :: * -> *). proxy (SymFP eb sb) -> SymWordN r
bitCastCanonicalValue proxy (SymFP eb sb)
_ =
    forall (eb :: Nat) (sb :: Nat) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  SymWordN r)
 -> SymWordN r)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    SymWordN r)
-> SymWordN r
forall a b. (a -> b) -> a -> b
$
      WordN r -> SymWordN r
forall c t. Solvable c t => c -> t
con (Proxy (FP eb sb) -> WordN r
forall from to (proxy :: * -> *).
BitCastCanonical from to =>
proxy from -> to
forall (proxy :: * -> *). proxy (FP eb sb) -> WordN r
bitCastCanonicalValue (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(FP eb sb)) :: WordN r)

instance
  (ValidFP eb sb, r ~ (eb + sb)) =>
  BitCastCanonical (SymFP eb sb) (SymIntN r)
  where
  bitCastCanonicalValue :: forall (proxy :: * -> *). proxy (SymFP eb sb) -> SymIntN r
bitCastCanonicalValue proxy (SymFP eb sb)
_ =
    forall (eb :: Nat) (sb :: Nat) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  SymIntN r)
 -> SymIntN r)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    SymIntN r)
-> SymIntN r
forall a b. (a -> b) -> a -> b
$
      IntN r -> SymIntN r
forall c t. Solvable c t => c -> t
con (Proxy (FP eb sb) -> IntN r
forall from to (proxy :: * -> *).
BitCastCanonical from to =>
proxy from -> to
forall (proxy :: * -> *). proxy (FP eb sb) -> IntN r
bitCastCanonicalValue (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(FP eb sb)) :: IntN r)

instance
  (ValidFP eb sb, r ~ (eb + sb)) =>
  BitCastOr (SymFP eb sb) (SymWordN r)
  where
  bitCastOr :: SymWordN r -> SymFP eb sb -> SymWordN r
bitCastOr (SymWordN Term (WordN r)
d) (SymFP Term (FP eb sb)
a) =
    forall (eb :: Nat) (sb :: Nat) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  SymWordN r)
 -> SymWordN r)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    SymWordN r)
-> SymWordN r
forall a b. (a -> b) -> a -> b
$ Term (WordN r) -> SymWordN r
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN r) -> Term (FP eb sb) -> Term (WordN r)
forall a b. PEvalBitCastOrTerm a b => Term b -> Term a -> Term b
pevalBitCastOrTerm Term (WordN r)
d Term (FP eb sb)
a)

instance
  (ValidFP eb sb, r ~ (eb + sb)) =>
  BitCastOr (SymFP eb sb) (SymIntN r)
  where
  bitCastOr :: SymIntN r -> SymFP eb sb -> SymIntN r
bitCastOr (SymIntN Term (IntN r)
d) (SymFP Term (FP eb sb)
a) =
    forall (eb :: Nat) (sb :: Nat) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  SymIntN r)
 -> SymIntN r)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    SymIntN r)
-> SymIntN r
forall a b. (a -> b) -> a -> b
$ Term (IntN r) -> SymIntN r
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN r) -> Term (FP eb sb) -> Term (IntN r)
forall a b. PEvalBitCastOrTerm a b => Term b -> Term a -> Term b
pevalBitCastOrTerm Term (IntN r)
d Term (FP eb sb)
a)

#define BIT_CAST_CANONICAL_VIA_INTERMEDIATE(from, to, intermediate) \
  instance BitCastCanonical (from) (to) where \
    bitCastCanonicalValue x = bitCast (bitCastCanonicalValue x :: intermediate)

instance
  (ValidFP eb sb, r ~ (eb + sb)) =>
  BitCast (SymIntN r) (SymFP eb sb)
  where
  bitCast :: SymIntN r -> SymFP eb sb
bitCast (SymIntN Term (IntN r)
a) =
    forall (eb :: Nat) (sb :: Nat) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  SymFP eb sb)
 -> SymFP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    SymFP eb sb)
-> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ 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 (IntN r) -> Term (FP eb sb)
forall a b. PEvalBitCastTerm a b => Term a -> Term b
pevalBitCastTerm Term (IntN r)
a

instance
  (ValidFP eb sb, r ~ (eb + sb)) =>
  BitCast (SymWordN r) (SymFP eb sb)
  where
  bitCast :: SymWordN r -> SymFP eb sb
bitCast (SymWordN Term (WordN r)
a) =
    forall (eb :: Nat) (sb :: Nat) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
  1 <= eb, 1 <= sb) =>
 r)
-> r
withValidFPProofs @eb @sb (((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
   1 <= eb, 1 <= sb) =>
  SymFP eb sb)
 -> SymFP eb sb)
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
     1 <= eb, 1 <= sb) =>
    SymFP eb sb)
-> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ 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 (WordN r) -> Term (FP eb sb)
forall a b. PEvalBitCastTerm a b => Term a -> Term b
pevalBitCastTerm Term (WordN r)
a

instance (ValidFP eb sb) => IEEEFPConstants (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. IEEEFPConstants 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. IEEEFPConstants 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. IEEEFPConstants 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. IEEEFPConstants 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. IEEEFPConstants a => a
fpPositiveZero
  {-# INLINE fpPositiveZero #-}
  fpMinNormalized :: SymFP eb sb
fpMinNormalized = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con FP eb sb
forall a. IEEEFPConstants a => a
fpMinNormalized
  {-# INLINE fpMinNormalized #-}
  fpMinSubnormal :: SymFP eb sb
fpMinSubnormal = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con FP eb sb
forall a. IEEEFPConstants a => a
fpMinSubnormal
  {-# INLINE fpMinSubnormal #-}
  fpMaxNormalized :: SymFP eb sb
fpMaxNormalized = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con FP eb sb
forall a. IEEEFPConstants a => a
fpMaxNormalized
  {-# INLINE fpMaxNormalized #-}
  fpMaxSubnormal :: SymFP eb sb
fpMaxSubnormal = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con FP eb sb
forall a. IEEEFPConstants a => a
fpMaxSubnormal
  {-# INLINE fpMaxSubnormal #-}

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

instance (ValidFP eb sb) => IEEEFPOp (SymFP eb sb) where
  fpAbs :: SymFP eb sb -> SymFP eb sb
fpAbs (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 fpAbs #-}
  fpNeg :: SymFP eb sb -> SymFP eb sb
fpNeg (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 fpNeg #-}
  fpRem :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
fpRem (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 fpRem #-}
  fpMinimum :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
fpMinimum (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
FPMinimum Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE fpMinimum #-}
  fpMinimumNumber :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
fpMinimumNumber (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
FPMinimumNumber Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE fpMinimumNumber #-}
  fpMaximum :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
fpMaximum (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
FPMaximum Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE fpMaximum #-}
  fpMaximumNumber :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb
fpMaximumNumber (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
FPMaximumNumber Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE fpMaximumNumber #-}

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

instance (ValidFP eb sb) => IEEEFPRoundingOp (SymFP eb sb) SymFPRoundingMode where
  fpAdd :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
fpAdd (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)) =>
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 fpAdd #-}
  fpSub :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
fpSub (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)) =>
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 fpSub #-}
  fpMul :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
fpMul (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)) =>
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 fpMul #-}
  fpDiv :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
fpDiv (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)) =>
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 fpDiv #-}
  fpFMA :: SymFPRoundingMode
-> SymFP eb sb -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
fpFMA (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)) =>
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 fpFMA #-}
  fpSqrt :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb
fpSqrt (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)) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPRoundingUnaryTerm FPRoundingUnaryOp
FPSqrt Term FPRoundingMode
mode Term (FP eb sb)
v
  {-# INLINE fpSqrt #-}
  fpRoundToIntegral :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb
fpRoundToIntegral (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)) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPRoundingUnaryTerm FPRoundingUnaryOp
FPRoundToIntegral Term FPRoundingMode
mode Term (FP eb sb)
v
  {-# INLINE fpRoundToIntegral #-}

instance
  (ValidFP eb sb) =>
  IEEEFPConvertible SymInteger (SymFP eb sb) SymFPRoundingMode
  where
  fromFPOr :: SymInteger -> SymFPRoundingMode -> SymFP eb sb -> SymInteger
fromFPOr (SymInteger Term Integer
d) (SymFPRoundingMode Term FPRoundingMode
mode) (SymFP Term (FP eb sb)
fp) =
    Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer
-> Term FPRoundingMode -> Term (FP eb sb) -> Term Integer
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term Integer
-> Term FPRoundingMode -> Term (FP eb sb) -> Term Integer
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
pevalFromFPOrTerm Term Integer
d Term FPRoundingMode
mode Term (FP eb sb)
fp
  toFP :: SymFPRoundingMode -> SymInteger -> SymFP eb sb
toFP (SymFPRoundingMode Term FPRoundingMode
mode) (SymInteger Term Integer
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
$ Term FPRoundingMode -> Term Integer -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term FPRoundingMode -> Term Integer -> Term (FP eb sb)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
pevalToFPTerm Term FPRoundingMode
mode Term Integer
v

instance
  (ValidFP eb sb) =>
  IEEEFPConvertible SymAlgReal (SymFP eb sb) SymFPRoundingMode
  where
  fromFPOr :: SymAlgReal -> SymFPRoundingMode -> SymFP eb sb -> SymAlgReal
fromFPOr (SymAlgReal Term AlgReal
d) (SymFPRoundingMode Term FPRoundingMode
mode) (SymFP Term (FP eb sb)
fp) =
    Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term AlgReal
-> Term FPRoundingMode -> Term (FP eb sb) -> Term AlgReal
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term AlgReal
-> Term FPRoundingMode -> Term (FP eb sb) -> Term AlgReal
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
pevalFromFPOrTerm Term AlgReal
d Term FPRoundingMode
mode Term (FP eb sb)
fp
  toFP :: SymFPRoundingMode -> SymAlgReal -> SymFP eb sb
toFP (SymFPRoundingMode Term FPRoundingMode
mode) (SymAlgReal Term AlgReal
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
$ Term FPRoundingMode -> Term AlgReal -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term FPRoundingMode -> Term AlgReal -> Term (FP eb sb)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
pevalToFPTerm Term FPRoundingMode
mode Term AlgReal
v

instance
  (ValidFP eb sb) =>
  IEEEFPToAlgReal SymAlgReal (SymFP eb sb) SymFPRoundingMode

instance
  (ValidFP eb sb, KnownNat n, 1 <= n) =>
  IEEEFPConvertible (SymWordN n) (SymFP eb sb) SymFPRoundingMode
  where
  fromFPOr :: SymWordN n -> SymFPRoundingMode -> SymFP eb sb -> SymWordN n
fromFPOr (SymWordN Term (WordN n)
d) (SymFPRoundingMode Term FPRoundingMode
mode) (SymFP Term (FP eb sb)
fp) =
    Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> SymWordN n) -> Term (WordN n) -> SymWordN n
forall a b. (a -> b) -> a -> b
$ Term (WordN n)
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (WordN n)
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term (WordN n)
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (WordN n)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
pevalFromFPOrTerm Term (WordN n)
d Term FPRoundingMode
mode Term (FP eb sb)
fp
  toFP :: SymFPRoundingMode -> SymWordN n -> SymFP eb sb
toFP (SymFPRoundingMode Term FPRoundingMode
mode) (SymWordN Term (WordN n)
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
$ Term FPRoundingMode -> Term (WordN n) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term FPRoundingMode -> Term (WordN n) -> Term (FP eb sb)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
pevalToFPTerm Term FPRoundingMode
mode Term (WordN n)
v

instance
  (ValidFP eb sb, KnownNat n, 1 <= n) =>
  IEEEFPConvertible (SymIntN n) (SymFP eb sb) SymFPRoundingMode
  where
  fromFPOr :: SymIntN n -> SymFPRoundingMode -> SymFP eb sb -> SymIntN n
fromFPOr (SymIntN Term (IntN n)
d) (SymFPRoundingMode Term FPRoundingMode
mode) (SymFP Term (FP eb sb)
fp) =
    Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$ Term (IntN n)
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (IntN n)
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term (IntN n)
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (IntN n)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
pevalFromFPOrTerm Term (IntN n)
d Term FPRoundingMode
mode Term (FP eb sb)
fp
  toFP :: SymFPRoundingMode -> SymIntN n -> SymFP eb sb
toFP (SymFPRoundingMode Term FPRoundingMode
mode) (SymIntN Term (IntN n)
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
$ Term FPRoundingMode -> Term (IntN n) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term FPRoundingMode -> Term (IntN n) -> Term (FP eb sb)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
pevalToFPTerm Term FPRoundingMode
mode Term (IntN n)
v

instance
  (ValidFP eb sb, ValidFP eb' sb') =>
  IEEEFPConvertible (SymFP eb' sb') (SymFP eb sb) SymFPRoundingMode
  where
  fromFPOr :: SymFP eb' sb' -> SymFPRoundingMode -> SymFP eb sb -> SymFP eb' sb'
fromFPOr (SymFP Term (FP eb' sb')
d) (SymFPRoundingMode Term FPRoundingMode
mode) (SymFP Term (FP eb sb)
fp) =
    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 (FP eb' sb')
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb' sb')
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term (FP eb' sb')
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb' sb')
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
pevalFromFPOrTerm Term (FP eb' sb')
d Term FPRoundingMode
mode Term (FP eb sb)
fp
  toFP :: SymFPRoundingMode -> SymFP eb' sb' -> SymFP eb sb
toFP (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
$ Term FPRoundingMode -> Term (FP eb' sb') -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term FPRoundingMode -> Term (FP eb' sb') -> Term (FP eb sb)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
pevalToFPTerm Term FPRoundingMode
mode Term (FP eb' sb')
v

instance (ValidFP eb sb) => Serial (SymFP eb sb) where
  serialize :: forall (m :: * -> *). MonadPut m => SymFP eb sb -> m ()
serialize = Term (FP eb sb) -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => Term (FP eb sb) -> m ()
serialize (Term (FP eb sb) -> m ())
-> (SymFP eb sb -> Term (FP eb sb)) -> SymFP eb sb -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymFP eb sb -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat). SymFP eb sb -> Term (FP eb sb)
underlyingFPTerm
  deserialize :: forall (m :: * -> *). MonadGet m => m (SymFP eb sb)
deserialize = 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)
-> m (Term (FP eb sb)) -> m (SymFP eb sb)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Term (FP eb sb))
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (Term (FP eb sb))
deserialize

instance (ValidFP eb sb) => Cereal.Serialize (SymFP eb sb) where
  put :: Putter (SymFP eb sb)
put = Putter (SymFP eb sb)
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => SymFP eb sb -> m ()
serialize
  get :: Get (SymFP eb sb)
get = Get (SymFP eb sb)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (SymFP eb sb)
deserialize

instance (ValidFP eb sb) => Binary.Binary (SymFP eb sb) where
  put :: SymFP eb sb -> Put
put = SymFP eb sb -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => SymFP eb sb -> m ()
serialize
  get :: Get (SymFP eb sb)
get = Get (SymFP eb sb)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (SymFP eb sb)
deserialize