module Copilot.Compile.SBV.Witness
( SymWordInst(..) , symWordInst
, NumInst(..) , numInst
, HasSignAndSizeInst(..), hasSignAndSizeInst
, EqInst(..) , eqInst
, CastInst(..) , castInst , sbvCast
, BVDivisibleInst(..) , divInst
, OrdInst(..) , ordInst
, MergeableInst(..) , mergeableInst
, BitsInst(..) , bitsInst
) where
import qualified Data.SBV as S
import qualified Data.SBV.Internals as S
import qualified Copilot.Core as C
import Data.Word (Word8, Word16, Word32, Word64)
import Data.Int (Int8, Int16, Int32, Int64)
import Data.Bits
badInst :: a
badInst = C.impossible "witnesses" "copilot-sbv"
data SymWordInst a = S.SymWord a => SymWordInst
symWordInst :: C.Type a -> SymWordInst a
symWordInst t =
case t of
C.Bool -> SymWordInst
C.Int8 -> SymWordInst ; C.Int16 -> SymWordInst
C.Int32 -> SymWordInst ; C.Int64 -> SymWordInst
C.Word8 -> SymWordInst ; C.Word16 -> SymWordInst
C.Word32 -> SymWordInst ; C.Word64 -> SymWordInst
C.Float -> badInst
C.Double -> badInst
data NumInst a = Num a => NumInst
numInst :: C.Type a -> NumInst a
numInst t =
case t of
C.Bool -> badInst
C.Int8 -> NumInst ; C.Int16 -> NumInst
C.Int32 -> NumInst ; C.Int64 -> NumInst
C.Word8 -> NumInst ; C.Word16 -> NumInst
C.Word32 -> NumInst ; C.Word64 -> NumInst
C.Float -> badInst
C.Double -> badInst
data HasSignAndSizeInst a = S.HasSignAndSize a => HasSignAndSizeInst
hasSignAndSizeInst :: C.Type a -> HasSignAndSizeInst a
hasSignAndSizeInst t =
case t of
C.Bool -> HasSignAndSizeInst
C.Int8 -> HasSignAndSizeInst
C.Int16 -> HasSignAndSizeInst
C.Int32 -> HasSignAndSizeInst
C.Int64 -> HasSignAndSizeInst
C.Word8 -> HasSignAndSizeInst
C.Word16 -> HasSignAndSizeInst
C.Word32 -> HasSignAndSizeInst
C.Word64 -> HasSignAndSizeInst
C.Float -> badInst
C.Double -> badInst
data EqInst a = S.EqSymbolic (S.SBV a) => EqInst
eqInst :: C.Type a -> EqInst a
eqInst t =
case t of
C.Bool -> EqInst
C.Int8 -> EqInst ; C.Int16 -> EqInst
C.Int32 -> EqInst ; C.Int64 -> EqInst
C.Word8 -> EqInst ; C.Word16 -> EqInst
C.Word32 -> EqInst ; C.Word64 -> EqInst
C.Float -> badInst
C.Double -> badInst
data BVDivisibleInst a = S.BVDivisible (S.SBV a) => BVDivisibleInst
divInst :: C.Type a -> BVDivisibleInst a
divInst t =
case t of
C.Bool -> badInst
C.Int8 -> badInst
C.Int16 -> badInst
C.Int32 -> badInst
C.Int64 -> badInst
C.Word8 -> BVDivisibleInst
C.Word16 -> BVDivisibleInst
C.Word32 -> BVDivisibleInst
C.Word64 -> BVDivisibleInst
C.Float -> badInst
C.Double -> badInst
data OrdInst a = S.OrdSymbolic (S.SBV a) => OrdInst
ordInst :: C.Type a -> OrdInst a
ordInst t =
case t of
C.Bool -> OrdInst
C.Int8 -> OrdInst ; C.Int16 -> OrdInst
C.Int32 -> OrdInst ; C.Int64 -> OrdInst
C.Word8 -> OrdInst ; C.Word16 -> OrdInst
C.Word32 -> OrdInst ; C.Word64 -> OrdInst
C.Float -> badInst
C.Double -> badInst
data MergeableInst a = S.Mergeable (S.SBV a) => MergeableInst
mergeableInst :: C.Type a -> MergeableInst a
mergeableInst t =
case t of
C.Bool -> MergeableInst
C.Int8 -> MergeableInst ; C.Int16 -> MergeableInst
C.Int32 -> MergeableInst ; C.Int64 -> MergeableInst
C.Word8 -> MergeableInst ; C.Word16 -> MergeableInst
C.Word32 -> MergeableInst ; C.Word64 -> MergeableInst
C.Float -> badInst
C.Double -> badInst
data BitsInst a = (Bits a, S.Bits (S.SBV a)) => BitsInst
bitsInst :: C.Type a -> BitsInst a
bitsInst t =
case t of
C.Bool -> badInst
C.Int8 -> BitsInst ; C.Int16 -> BitsInst
C.Int32 -> BitsInst ; C.Int64 -> BitsInst
C.Word8 -> BitsInst ; C.Word16 -> BitsInst
C.Word32 -> BitsInst ; C.Word64 -> BitsInst
C.Float -> badInst
C.Double -> badInst
data CastInst a b = SBVCast a b => CastInst
castInst :: C.Type a -> C.Type b -> CastInst a b
castInst t0 t1 =
case t0 of
C.Bool -> case t1 of
C.Bool -> CastInst
C.Word8 -> CastInst
C.Word16 -> CastInst
C.Word32 -> CastInst
C.Word64 -> CastInst
C.Int8 -> CastInst
C.Int16 -> CastInst
C.Int32 -> CastInst
C.Int64 -> CastInst
_ -> badInst
C.Word8 -> case t1 of
C.Word8 -> CastInst
C.Word16 -> CastInst
C.Word32 -> CastInst
C.Word64 -> CastInst
C.Int16 -> CastInst
C.Int32 -> CastInst
C.Int64 -> CastInst
_ -> badInst
C.Word16 -> case t1 of
C.Word16 -> CastInst
C.Word32 -> CastInst
C.Word64 -> CastInst
C.Int32 -> CastInst
C.Int64 -> CastInst
_ -> badInst
C.Word32 -> case t1 of
C.Word32 -> CastInst
C.Word64 -> CastInst
C.Int64 -> CastInst
_ -> badInst
C.Word64 -> case t1 of
C.Word64 -> CastInst
_ -> badInst
C.Int8 -> case t1 of
C.Int8 -> CastInst
C.Int16 -> CastInst
C.Int32 -> CastInst
C.Int64 -> CastInst
_ -> badInst
C.Int16 -> case t1 of
C.Int16 -> CastInst
C.Int32 -> CastInst
C.Int64 -> CastInst
_ -> badInst
C.Int32 -> case t1 of
C.Int32 -> CastInst
C.Int64 -> CastInst
_ -> badInst
C.Int64 -> case t1 of
C.Int64 -> CastInst
_ -> badInst
C.Float -> badInst
C.Double -> badInst
class SBVCast a b where
sbvCast :: S.SBV a -> S.SBV b
castBool :: (Num a, S.SymWord a) => S.SBV Bool -> S.SBV a
castBool x = case S.unliteral x of
Just bool -> if bool then 1 else 0
Nothing -> S.ite x 1 0
castErr :: a
castErr = C.badUsage $ "the SBV backend does not currently support casts to signed word types"
instance SBVCast Bool Bool where
sbvCast = id
instance SBVCast Bool Word8 where
sbvCast = castBool
instance SBVCast Bool Word16 where
sbvCast = castBool
instance SBVCast Bool Word32 where
sbvCast = castBool
instance SBVCast Bool Word64 where
sbvCast = castBool
instance SBVCast Bool Int8 where
sbvCast = castErr
instance SBVCast Bool Int16 where
sbvCast = castErr
instance SBVCast Bool Int32 where
sbvCast = castErr
instance SBVCast Bool Int64 where
sbvCast = castErr
instance SBVCast Word8 Word8 where
sbvCast = id
instance SBVCast Word8 Word16 where
sbvCast = S.extend
instance SBVCast Word8 Word32 where
sbvCast = S.extend . S.extend
instance SBVCast Word8 Word64 where
sbvCast = S.extend . S.extend . S.extend
instance SBVCast Word8 Int16 where
sbvCast = castErr
instance SBVCast Word8 Int32 where
sbvCast = castErr
instance SBVCast Word8 Int64 where
sbvCast = castErr
instance SBVCast Word16 Word16 where
sbvCast = id
instance SBVCast Word16 Word32 where
sbvCast = S.extend
instance SBVCast Word16 Word64 where
sbvCast = S.extend . S.extend
instance SBVCast Word16 Int32 where
sbvCast = castErr
instance SBVCast Word16 Int64 where
sbvCast = castErr
instance SBVCast Word32 Word32 where
sbvCast = id
instance SBVCast Word32 Word64 where
sbvCast = S.extend
instance SBVCast Word32 Int64 where
sbvCast = castErr
instance SBVCast Word64 Word64 where
sbvCast = id
instance SBVCast Int8 Int8 where
sbvCast = castErr
instance SBVCast Int8 Int16 where
sbvCast = castErr
instance SBVCast Int8 Int32 where
sbvCast = castErr
instance SBVCast Int8 Int64 where
sbvCast = castErr
instance SBVCast Int16 Int16 where
sbvCast = castErr
instance SBVCast Int16 Int32 where
sbvCast = castErr
instance SBVCast Int16 Int64 where
sbvCast = castErr
instance SBVCast Int32 Int32 where
sbvCast = castErr
instance SBVCast Int32 Int64 where
sbvCast = castErr
instance SBVCast Int64 Int64 where
sbvCast = castErr