{-# 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 Data.Hashable (Hashable (hashWithSalt))
import Data.Proxy (Proxy (Proxy))
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.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,
  )
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, Typeable t, Hashable t, Eq t, Show 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
. Symbol -> Term (FP eb sb)
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm
  conView :: SymFP eb sb -> Maybe (FP eb sb)
conView (SymFP (ConTerm Int
_ 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. SupportedPrim 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, Typeable t, Hashable t, Eq t, Show 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
. Symbol -> Term FPRoundingMode
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm
  conView :: SymFPRoundingMode -> Maybe FPRoundingMode
conView (SymFPRoundingMode (ConTerm Int
_ 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. SupportedPrim 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),
 SupportedPrim FPRoundingMode) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm FPRoundingBinaryOp
FPAdd Term FPRoundingMode
mode Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE 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),
 SupportedPrim FPRoundingMode) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm FPRoundingBinaryOp
FPSub Term FPRoundingMode
mode Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE 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),
 SupportedPrim FPRoundingMode) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm FPRoundingBinaryOp
FPMul Term FPRoundingMode
mode Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE 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),
 SupportedPrim FPRoundingMode) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm FPRoundingBinaryOp
FPDiv Term FPRoundingMode
mode Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE 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),
 SupportedPrim FPRoundingMode) =>
Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPFMATerm Term FPRoundingMode
mode Term (FP eb sb)
l Term (FP eb sb)
m Term (FP eb sb)
r
  {-# INLINE 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),
 SupportedPrim FPRoundingMode) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPRoundingUnaryTerm FPRoundingUnaryOp
FPSqrt Term FPRoundingMode
mode Term (FP eb sb)
v
  {-# INLINE 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),
 SupportedPrim FPRoundingMode) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPRoundingUnaryTerm FPRoundingUnaryOp
FPRoundToIntegral Term FPRoundingMode
mode Term (FP eb sb)
v
  {-# INLINE 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