content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveAnyClass #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE DeriveLift #-}
  {-# LANGUAGE DerivingStrategies #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE PatternSynonyms #-}
  {-# 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,
      SymFPKey,
      SymFP16Key,
      SymFP32Key,
      SymFP64Key,
      SymFPRoundingMode (SymFPRoundingMode),
      SymFPRoundingModeKey,
    )
  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.AsKey
    ( AsKey,
      KeyEq (keyEq),
      KeyHashable (keyHashWithSalt),
      shouldUseAsKeyError,
      shouldUseAsKeyHasSymbolicVersionError,
    )
  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 ()
  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),
      PEvalFPTerm
        ( pevalFPBinaryTerm,
          pevalFPFMATerm,
          pevalFPRoundingBinaryTerm,
          pevalFPRoundingUnaryTerm,
          pevalFPTraitTerm,
          pevalFPUnaryTerm
        ),
      PEvalFloatingTerm (pevalFloatingUnaryTerm),
      PEvalFractionalTerm (pevalFdivTerm, pevalRecipTerm),
      PEvalIEEEFPConvertibleTerm (pevalFromFPOrTerm, pevalToFPTerm),
      PEvalNumTerm
        ( pevalAbsNumTerm,
          pevalAddNumTerm,
          pevalMulNumTerm,
          pevalNegNumTerm,
          pevalSignumNumTerm
        ),
      SymRep (SymType),
      Term,
      conTerm,
      pevalSubNumTerm,
      pformatTerm,
      symTerm,
      typedConstantSymbol,
      pattern ConTerm,
    )
  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 {underlyingFPTerm :: Term (FP eb sb)}
    deriving (Lift, Generic)
    deriving anyclass (NFData)
  
  -- | t'SymFP' type with identity equality.
  type SymFPKey eb sb = AsKey (SymFP eb sb)
  
  -- | 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
  
  -- | @t'SymFP' 16@ type with identity equality.
  type SymFP16Key = SymFPKey 5 11
  
  -- | @t'SymFP' 32@ type with identity equality.
  type SymFP32Key = SymFPKey 8 24
  
  -- | @t'SymFP' 64@ type with identity equality.
  type SymFP64Key = SymFPKey 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 a) = a
    wrapTerm = SymFP
  
  instance (ValidFP eb sb) => Apply (SymFP eb sb) where
    type FunType (SymFP eb sb) = SymFP eb sb
    apply = id
  
  -- | This will crash the program.
  --
  -- 'SymFP' cannot be compared concretely.
  --
  -- If you want to use the type as keys in hash maps based on term equality, say
  -- memo table, you should use @'AsKey' 'SymFP'@ instead.
  --
  -- If you want symbolic version of the equality operator, use
  -- t'Grisette.Core.SymEq' instead.
  instance (ValidFP eb sb) => Eq (SymFP eb sb) where
    (==) = shouldUseAsKeyHasSymbolicVersionError "SymFP" "(==)" "(.==)"
  
  instance (ValidFP eb sb) => KeyEq (SymFP eb sb) where
    keyEq (SymFP l) (SymFP r) = l == r
  
  -- | This will crash the program.
  --
  -- 'SymFP' cannot be hashed concretely.
  --
  -- If you want to use the type as keys in hash maps based on term equality, say
  -- memo table, you should use @'AsKey' 'SymFP'@ instead.
  instance (ValidFP eb sb) => Hashable (SymFP eb sb) where
    hashWithSalt = shouldUseAsKeyError "SymFP" "hashWithSalt"
  
  instance (ValidFP eb sb) => KeyHashable (SymFP eb sb) where
    keyHashWithSalt s (SymFP a) = hashWithSalt s a
  
  instance (ValidFP eb sb) => IsString (SymFP eb sb) where
    fromString = ssym . fromString
  
  instance (ValidFP eb sb) => Solvable (FP eb sb) (SymFP eb sb) where
    con = SymFP . conTerm
    sym = SymFP . symTerm . typedConstantSymbol
    conView (SymFP (ConTerm t)) = Just t
    conView _ = Nothing
  
  instance (ValidFP eb sb) => Show (SymFP eb sb) where
    show (SymFP a) = pformatTerm a
  
  instance (ValidFP eb sb) => AllSyms (SymFP eb sb) where
    allSymsS v = (SomeSym v :)
  
  instance (ValidFP eb sb) => Num (SymFP eb sb) where
    (SymFP l) + (SymFP r) = SymFP $ pevalAddNumTerm l r
    (SymFP l) - (SymFP r) = SymFP $ pevalSubNumTerm l r
    (SymFP l) * (SymFP r) = SymFP $ pevalMulNumTerm l r
    negate (SymFP v) = SymFP $ pevalNegNumTerm v
    abs (SymFP v) = SymFP $ pevalAbsNumTerm v
    signum (SymFP v) = SymFP $ pevalSignumNumTerm v
    fromInteger = con . fromInteger
  
  instance (ValidFP eb sb) => Fractional (SymFP eb sb) where
    (SymFP l) / (SymFP r) = SymFP $ pevalFdivTerm l r
    recip (SymFP v) = SymFP $ pevalRecipTerm v
    fromRational = con . fromRational
  
  instance (ValidFP eb sb) => Floating (SymFP eb sb) where
    pi = error "pi isn't supported by the underlying sbv library"
    exp = error "exp isn't supported by the underlying sbv library"
    log = error "log isn't supported by the underlying sbv library"
    sqrt (SymFP v) = SymFP $ pevalFloatingUnaryTerm FloatingSqrt v
    (**) = error "(**) isn't supported by the underlying sbv library"
    logBase = error "logBase isn't supported by the underlying sbv library"
    sin = error "sin isn't supported by the underlying sbv library"
    cos = error "cos isn't supported by the underlying sbv library"
    asin = error "asin isn't supported by the underlying sbv library"
    acos = error "acos isn't supported by the underlying sbv library"
    atan = error "atan isn't supported by the underlying sbv library"
    sinh = error "sinh isn't supported by the underlying sbv library"
    cosh = error "cosh isn't supported by the underlying sbv library"
    asinh = error "asinh isn't supported by the underlying sbv library"
    acosh = error "acosh isn't supported by the underlying sbv library"
    atanh = error "atanh isn't supported by the underlying sbv library"
  
  -- | Symbolic floating-point rounding mode.
  newtype SymFPRoundingMode = SymFPRoundingMode (Term FPRoundingMode)
    deriving (Lift, Generic)
    deriving anyclass (NFData)
  
  -- | t'SymFPRoundingMode' type with identity equality.
  type SymFPRoundingModeKey = AsKey SymFPRoundingMode
  
  instance ConRep SymFPRoundingMode where
    type ConType SymFPRoundingMode = FPRoundingMode
  
  instance SymRep FPRoundingMode where
    type SymType FPRoundingMode = SymFPRoundingMode
  
  instance LinkedRep FPRoundingMode SymFPRoundingMode where
    underlyingTerm (SymFPRoundingMode a) = a
    wrapTerm = SymFPRoundingMode
  
  instance Apply SymFPRoundingMode where
    type FunType SymFPRoundingMode = SymFPRoundingMode
    apply = id
  
  -- | This will crash the program.
  --
  -- 'SymFPRoundingMode' cannot be compared concretely.
  --
  -- If you want to use the type as keys in hash maps based on term equality, say
  -- memo table, you should use @'AsKey' 'SymFPRoundingMode'@ instead.
  instance Eq SymFPRoundingMode where
    (==) =
      shouldUseAsKeyHasSymbolicVersionError "SymFPRoundingMode" "(==)" "(.==)"
  
  instance KeyEq SymFPRoundingMode where
    keyEq (SymFPRoundingMode l) (SymFPRoundingMode r) = l == r
  
  instance KeyHashable SymFPRoundingMode where
    keyHashWithSalt s (SymFPRoundingMode a) = hashWithSalt s a
  
  instance IsString SymFPRoundingMode where
    fromString = ssym . fromString
  
  instance Solvable FPRoundingMode SymFPRoundingMode where
    con = SymFPRoundingMode . conTerm
    sym = SymFPRoundingMode . symTerm . typedConstantSymbol
    conView (SymFPRoundingMode (ConTerm t)) = Just t
    conView _ = Nothing
  
  instance Show SymFPRoundingMode where
    show (SymFPRoundingMode a) = pformatTerm a
  
  instance AllSyms SymFPRoundingMode where
    allSymsS v = (SomeSym v :)
  
  instance
    (ValidFP eb sb, r ~ (eb + sb)) =>
    BitCastCanonical (SymFP eb sb) (SymWordN r)
    where
    bitCastCanonicalValue _ =
      withValidFPProofs @eb @sb $
        con (bitCastCanonicalValue (Proxy @(FP eb sb)) :: WordN r)
  
  instance
    (ValidFP eb sb, r ~ (eb + sb)) =>
    BitCastCanonical (SymFP eb sb) (SymIntN r)
    where
    bitCastCanonicalValue _ =
      withValidFPProofs @eb @sb $
        con (bitCastCanonicalValue (Proxy @(FP eb sb)) :: IntN r)
  
  instance
    (ValidFP eb sb, r ~ (eb + sb)) =>
    BitCastOr (SymFP eb sb) (SymWordN r)
    where
    bitCastOr (SymWordN d) (SymFP a) =
      withValidFPProofs @eb @sb $ SymWordN (pevalBitCastOrTerm d a)
  
  instance
    (ValidFP eb sb, r ~ (eb + sb)) =>
    BitCastOr (SymFP eb sb) (SymIntN r)
    where
    bitCastOr (SymIntN d) (SymFP a) =
      withValidFPProofs @eb @sb $ SymIntN (pevalBitCastOrTerm d 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 a) =
      withValidFPProofs @eb @sb $ SymFP $ pevalBitCastTerm a
  
  instance
    (ValidFP eb sb, r ~ (eb + sb)) =>
    BitCast (SymWordN r) (SymFP eb sb)
    where
    bitCast (SymWordN a) =
      withValidFPProofs @eb @sb $ SymFP $ pevalBitCastTerm a
  
  instance (ValidFP eb sb) => IEEEFPConstants (SymFP eb sb) where
    fpPositiveInfinite = con fpPositiveInfinite
    {-# INLINE fpPositiveInfinite #-}
    fpNegativeInfinite = con fpNegativeInfinite
    {-# INLINE fpNegativeInfinite #-}
    fpNaN = con fpNaN
    {-# INLINE fpNaN #-}
    fpNegativeZero = con fpNegativeZero
    {-# INLINE fpNegativeZero #-}
    fpPositiveZero = con fpPositiveZero
    {-# INLINE fpPositiveZero #-}
    fpMinNormalized = con fpMinNormalized
    {-# INLINE fpMinNormalized #-}
    fpMinSubnormal = con fpMinSubnormal
    {-# INLINE fpMinSubnormal #-}
    fpMaxNormalized = con fpMaxNormalized
    {-# INLINE fpMaxNormalized #-}
    fpMaxSubnormal = con fpMaxSubnormal
    {-# INLINE fpMaxSubnormal #-}
  
  instance (ValidFP eb sb) => SymIEEEFPTraits (SymFP eb sb) where
    symFpIsNaN (SymFP x) = SymBool $ pevalFPTraitTerm FPIsNaN x
    {-# INLINE symFpIsNaN #-}
    symFpIsPositive (SymFP x) = SymBool $ pevalFPTraitTerm FPIsPositive x
    {-# INLINE symFpIsPositive #-}
    symFpIsNegative (SymFP x) = SymBool $ pevalFPTraitTerm FPIsNegative x
    {-# INLINE symFpIsNegative #-}
    symFpIsInfinite (SymFP x) = SymBool $ pevalFPTraitTerm FPIsInfinite x
    {-# INLINE symFpIsInfinite #-}
    symFpIsPositiveInfinite (SymFP x) =
      SymBool $ pevalFPTraitTerm FPIsPositiveInfinite x
    {-# INLINE symFpIsPositiveInfinite #-}
    symFpIsNegativeInfinite (SymFP x) =
      SymBool $ pevalFPTraitTerm FPIsNegativeInfinite x
    {-# INLINE symFpIsNegativeInfinite #-}
    symFpIsPositiveZero (SymFP x) = SymBool $ pevalFPTraitTerm FPIsPositiveZero x
    {-# INLINE symFpIsPositiveZero #-}
    symFpIsNegativeZero (SymFP x) = SymBool $ pevalFPTraitTerm FPIsNegativeZero x
    {-# INLINE symFpIsNegativeZero #-}
    symFpIsZero (SymFP x) = SymBool $ pevalFPTraitTerm FPIsZero x
    {-# INLINE symFpIsZero #-}
    symFpIsNormal (SymFP x) = SymBool $ pevalFPTraitTerm FPIsNormal x
    {-# INLINE symFpIsNormal #-}
    symFpIsSubnormal (SymFP x) = SymBool $ pevalFPTraitTerm FPIsSubnormal x
    {-# INLINE symFpIsSubnormal #-}
    symFpIsPoint (SymFP x) = SymBool $ pevalFPTraitTerm FPIsPoint x
    {-# INLINE symFpIsPoint #-}
  
  instance (ValidFP eb sb) => IEEEFPOp (SymFP eb sb) where
    fpAbs (SymFP l) = SymFP $ pevalFPUnaryTerm FPAbs l
    {-# INLINE fpAbs #-}
    fpNeg (SymFP l) = SymFP $ pevalFPUnaryTerm FPNeg l
    {-# INLINE fpNeg #-}
    fpRem (SymFP l) (SymFP r) = SymFP $ pevalFPBinaryTerm FPRem l r
    {-# INLINE fpRem #-}
    fpMinimum (SymFP l) (SymFP r) = SymFP $ pevalFPBinaryTerm FPMinimum l r
    {-# INLINE fpMinimum #-}
    fpMinimumNumber (SymFP l) (SymFP r) =
      SymFP $ pevalFPBinaryTerm FPMinimumNumber l r
    {-# INLINE fpMinimumNumber #-}
    fpMaximum (SymFP l) (SymFP r) = SymFP $ pevalFPBinaryTerm FPMaximum l r
    {-# INLINE fpMaximum #-}
    fpMaximumNumber (SymFP l) (SymFP r) =
      SymFP $ pevalFPBinaryTerm FPMaximumNumber l r
    {-# INLINE fpMaximumNumber #-}
  
  instance IEEEFPRoundingMode SymFPRoundingMode where
    rne = con RNE
    {-# INLINE rne #-}
    rna = con RNA
    {-# INLINE rna #-}
    rtp = con RTP
    {-# INLINE rtp #-}
    rtn = con RTN
    {-# INLINE rtn #-}
    rtz = con RTZ
    {-# INLINE rtz #-}
  
  instance (ValidFP eb sb) => IEEEFPRoundingOp (SymFP eb sb) SymFPRoundingMode where
    fpAdd (SymFPRoundingMode mode) (SymFP l) (SymFP r) =
      SymFP $ pevalFPRoundingBinaryTerm FPAdd mode l r
    {-# INLINE fpAdd #-}
    fpSub (SymFPRoundingMode mode) (SymFP l) (SymFP r) =
      SymFP $ pevalFPRoundingBinaryTerm FPSub mode l r
    {-# INLINE fpSub #-}
    fpMul (SymFPRoundingMode mode) (SymFP l) (SymFP r) =
      SymFP $ pevalFPRoundingBinaryTerm FPMul mode l r
    {-# INLINE fpMul #-}
    fpDiv (SymFPRoundingMode mode) (SymFP l) (SymFP r) =
      SymFP $ pevalFPRoundingBinaryTerm FPDiv mode l r
    {-# INLINE fpDiv #-}
    fpFMA (SymFPRoundingMode mode) (SymFP l) (SymFP m) (SymFP r) =
      SymFP $ pevalFPFMATerm mode l m r
    {-# INLINE fpFMA #-}
    fpSqrt (SymFPRoundingMode mode) (SymFP v) =
      SymFP $ pevalFPRoundingUnaryTerm FPSqrt mode v
    {-# INLINE fpSqrt #-}
    fpRoundToIntegral (SymFPRoundingMode mode) (SymFP v) =
      SymFP $ pevalFPRoundingUnaryTerm FPRoundToIntegral mode v
    {-# INLINE fpRoundToIntegral #-}
  
  instance
    (ValidFP eb sb) =>
    IEEEFPConvertible SymInteger (SymFP eb sb) SymFPRoundingMode
    where
    fromFPOr (SymInteger d) (SymFPRoundingMode mode) (SymFP fp) =
      SymInteger $ pevalFromFPOrTerm d mode fp
    toFP (SymFPRoundingMode mode) (SymInteger v) = SymFP $ pevalToFPTerm mode v
  
  instance
    (ValidFP eb sb) =>
    IEEEFPConvertible SymAlgReal (SymFP eb sb) SymFPRoundingMode
    where
    fromFPOr (SymAlgReal d) (SymFPRoundingMode mode) (SymFP fp) =
      SymAlgReal $ pevalFromFPOrTerm d mode fp
    toFP (SymFPRoundingMode mode) (SymAlgReal v) = SymFP $ pevalToFPTerm mode 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 d) (SymFPRoundingMode mode) (SymFP fp) =
      SymWordN $ pevalFromFPOrTerm d mode fp
    toFP (SymFPRoundingMode mode) (SymWordN v) = SymFP $ pevalToFPTerm mode v
  
  instance
    (ValidFP eb sb, KnownNat n, 1 <= n) =>
    IEEEFPConvertible (SymIntN n) (SymFP eb sb) SymFPRoundingMode
    where
    fromFPOr (SymIntN d) (SymFPRoundingMode mode) (SymFP fp) =
      SymIntN $ pevalFromFPOrTerm d mode fp
    toFP (SymFPRoundingMode mode) (SymIntN v) = SymFP $ pevalToFPTerm mode v
  
  instance
    (ValidFP eb sb, ValidFP eb' sb') =>
    IEEEFPConvertible (SymFP eb' sb') (SymFP eb sb) SymFPRoundingMode
    where
    fromFPOr (SymFP d) (SymFPRoundingMode mode) (SymFP fp) =
      SymFP $ pevalFromFPOrTerm d mode fp
    toFP (SymFPRoundingMode mode) (SymFP v) = SymFP $ pevalToFPTerm mode v
  
  instance (ValidFP eb sb) => Serial (SymFP eb sb) where
    serialize = serialize . underlyingFPTerm
    deserialize = SymFP <$> deserialize
  
  instance (ValidFP eb sb) => Cereal.Serialize (SymFP eb sb) where
    put = serialize
    get = deserialize
  
  instance (ValidFP eb sb) => Binary.Binary (SymFP eb sb) where
    put = serialize
    get = deserialize
  