module Data.SBV.BitVectors.SignCast (SignCast(..)) where
import Data.Word (Word8, Word16, Word32, Word64)
import Data.Int (Int8, Int16, Int32, Int64)
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.Model()
class SignCast a b | a -> b, b -> a where
signCast :: a -> b
unsignCast :: b -> a
instance SignCast Word64 Int64 where
signCast = fromIntegral
unsignCast = fromIntegral
instance SignCast Word32 Int32 where
signCast = fromIntegral
unsignCast = fromIntegral
instance SignCast Word16 Int16 where
signCast = fromIntegral
unsignCast = fromIntegral
instance SignCast Word8 Int8 where
signCast = fromIntegral
unsignCast = fromIntegral
genericSign :: (Integral a, SymWord a, Num b, SymWord b) => SBV a -> SBV b
genericSign x
| Just c <- unliteral x = literal $ fromIntegral c
| True = SBV k (Right (cache y))
where k = case kindOf x of
KBounded False n -> KBounded True n
KBounded True _ -> error "Data.SBV.SignCast.genericSign: Called on signed value"
KUnbounded -> error "Data.SBV.SignCast.genericSign: Called on unbounded value"
KReal -> error "Data.SBV.SignCast.genericSign: Called on real value"
KUninterpreted s -> error $ "Data.SBV.SignCast.genericSign: Called on unintepreted sort " ++ s
y st = do xsw <- sbvToSW st x
newExpr st k (SBVApp (Extract (intSizeOf x1) 0) [xsw])
genericUnsign :: (Integral a, SymWord a, Num b, SymWord b) => SBV a -> SBV b
genericUnsign x
| Just c <- unliteral x = literal $ fromIntegral c
| True = SBV k (Right (cache y))
where k = case kindOf x of
KBounded True n -> KBounded False n
KBounded False _ -> error "Data.SBV.SignCast.genericUnSign: Called on unsigned value"
KUnbounded -> error "Data.SBV.SignCast.genericUnSign: Called on unbounded value"
KReal -> error "Data.SBV.SignCast.genericUnSign: Called on real value"
KUninterpreted s -> error $ "Data.SBV.SignCast.genericUnSign: Called on unintepreted sort " ++ s
y st = do xsw <- sbvToSW st x
newExpr st k (SBVApp (Extract (intSizeOf x1) 0) [xsw])
instance SignCast SWord8 SInt8 where
signCast = genericSign
unsignCast = genericUnsign
instance SignCast SWord16 SInt16 where
signCast = genericSign
unsignCast = genericUnsign
instance SignCast SWord32 SInt32 where
signCast = genericSign
unsignCast = genericUnsign
instance SignCast SWord64 SInt64 where
signCast = genericSign
unsignCast = genericUnsign