module Data.SBV.BitVectors.Rounding (RoundingFloat(..)) where
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.Model ()
class (SymWord a, Floating a) => RoundingFloat a where
fpAdd :: SRoundingMode -> SBV a -> SBV a -> SBV a
fpSub :: SRoundingMode -> SBV a -> SBV a -> SBV a
fpMul :: SRoundingMode -> SBV a -> SBV a -> SBV a
fpDiv :: SRoundingMode -> SBV a -> SBV a -> SBV a
fpFMA :: SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a
fpSqrt :: SRoundingMode -> SBV a -> SBV a
fpAdd = lift2Rm "fp.add"
fpSub = lift2Rm "fp.sub"
fpMul = lift2Rm "fp.mul"
fpDiv = lift2Rm "fp.div"
fpFMA = lift3Rm "fp.fma"
fpSqrt = lift1Rm "fp.sqrt"
lift1Rm :: (SymWord a, Floating a) => String -> SRoundingMode -> SBV a -> SBV a
lift1Rm w m a = SBV k $ Right $ cache r
where k = kindOf a
r st = do swm <- sbvToSW st m
swa <- sbvToSW st a
newExpr st k (SBVApp (FPRound w) [swm, swa])
lift2Rm :: (SymWord a, Floating a) => String -> SRoundingMode -> SBV a -> SBV a -> SBV a
lift2Rm w m a b = SBV k $ Right $ cache r
where k = kindOf a
r st = do swm <- sbvToSW st m
swa <- sbvToSW st a
swb <- sbvToSW st b
newExpr st k (SBVApp (FPRound w) [swm, swa, swb])
lift3Rm :: (SymWord a, Floating a) => String -> SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a
lift3Rm w m a b c = SBV k $ Right $ cache r
where k = kindOf a
r st = do swm <- sbvToSW st m
swa <- sbvToSW st a
swb <- sbvToSW st b
swc <- sbvToSW st c
newExpr st k (SBVApp (FPRound w) [swm, swa, swb, swc])
instance RoundingFloat Float
instance RoundingFloat Double