{-# 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
( 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)
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)
type SymFP16 = SymFP 5 11
type SymFP32 = SymFP 8 24
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"
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