💥 Changed BVSignConversion to SignConversion, add instances to it.

CHANGELOG.md

@@ -13,6 +13,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Added `toGuardList` function. ([#137](https://github.com/lsrcz/grisette/pull/137))
 - Exported some previously hidden API (`BVSignConversion`, `runFreshTFromIndex`) that we found useful or forgot to export. ([#138](https://github.com/lsrcz/grisette/pull/138), [#139](https://github.com/lsrcz/grisette/pull/139))
 - Provided `mrgRunFreshT` to run `FreshT` with merging. ([#140](https://github.com/lsrcz/grisette/pull/140))
+- Added `Grisette.Data.Class.SignConversion.SignConversion` for types from `Data.Int` and `Data.Word`. ([#142](https://github.com/lsrcz/grisette/pull/142))
 
 ### Removed
 
@@ -31,6 +32,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - [Breaking] Changed the name of `Union` constructors and patterns. ([#133](https://github.com/lsrcz/grisette/pull/133))
 - The `Union` patterns, when used as constructors, now merges the result. ([#133](https://github.com/lsrcz/grisette/pull/133))
 - Changed the symbolic identifier type from `String` to `Data.Text.Text`. ([#141](https://github.com/lsrcz/grisette/pull/141))
+- `Grisette.Data.Class.BitVector.BVSignConversion` is now `Grisette.Data.Class.SignConversion.SignConversion`. ([#142](https://github.com/lsrcz/grisette/pull/142))
 
 ## [0.3.1.1] -- 2023-09-29
 

grisette.cabal

@@ -70,6 +70,7 @@ library
       Grisette.Core.Data.Class.Mergeable
       Grisette.Core.Data.Class.ModelOps
       Grisette.Core.Data.Class.SafeArith
+      Grisette.Core.Data.Class.SignConversion
       Grisette.Core.Data.Class.SimpleMergeable
       Grisette.Core.Data.Class.Solvable
       Grisette.Core.Data.Class.Solver

src/Grisette/Backend/SBV/Data/SMT/Lowering.hs

@@ -93,8 +93,6 @@ import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
         BVConcatTerm,
         BVExtendTerm,
         BVSelectTerm,
-        BVToSignedTerm,
-        BVToUnsignedTerm,
         BinaryTerm,
         ComplementBitsTerm,
         ConTerm,
@@ -121,6 +119,8 @@ import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
         TabularFunApplyTerm,
         TernaryTerm,
         TimesNumTerm,
+        ToSignedTerm,
+        ToUnsignedTerm,
         UMinusNumTerm,
         UnaryTerm,
         XorBitsTerm
@@ -783,22 +783,22 @@ lowerSinglePrimImpl config t@(RotateBitsTerm _ arg n) m =
   case (config, R.typeRep @a) of
     ResolvedBitsType -> lowerUnaryTerm config t arg (`rotate` n) m
     _ -> translateBinaryError "rotate" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)
-lowerSinglePrimImpl config t@(BVToSignedTerm _ (bv :: Term x)) m =
+lowerSinglePrimImpl config t@(ToSignedTerm _ (bv :: Term x)) m =
   case (R.typeRep @a, R.typeRep @x) of
     (SignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx)) ->
       case R.eqTypeRep (R.typeRep @na) (R.typeRep @nx) of
         Just R.HRefl ->
           lowerUnaryTerm config t bv SBV.sFromIntegral m
-        _ -> translateUnaryError "bvu2s" (R.typeRep @x) (R.typeRep @a)
-    _ -> translateUnaryError "bvu2s" (R.typeRep @x) (R.typeRep @a)
-lowerSinglePrimImpl config t@(BVToUnsignedTerm _ (bv :: Term x)) m =
+        _ -> translateUnaryError "u2s" (R.typeRep @x) (R.typeRep @a)
+    _ -> translateUnaryError "u2s" (R.typeRep @x) (R.typeRep @a)
+lowerSinglePrimImpl config t@(ToUnsignedTerm _ (bv :: Term x)) m =
   case (R.typeRep @a, R.typeRep @x) of
     (UnsignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx)) ->
       case R.eqTypeRep (R.typeRep @na) (R.typeRep @nx) of
         Just R.HRefl ->
           lowerUnaryTerm config t bv SBV.sFromIntegral m
-        _ -> translateUnaryError "bvs2u" (R.typeRep @x) (R.typeRep @a)
-    _ -> translateUnaryError "bvs2u" (R.typeRep @x) (R.typeRep @a)
+        _ -> translateUnaryError "s2u" (R.typeRep @x) (R.typeRep @a)
+    _ -> translateUnaryError "s2u" (R.typeRep @x) (R.typeRep @a)
 lowerSinglePrimImpl config t@(BVConcatTerm _ (bv1 :: Term x) (bv2 :: Term y)) m =
   case (R.typeRep @a, R.typeRep @x, R.typeRep @y) of
     (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx), UnsignedBVType (_ :: Proxy ny)) ->

src/Grisette/Core.hs

@@ -187,7 +187,7 @@ module Grisette.Core
     bvExtract,
     SizedBV (..),
     sizedBVExtract,
-    BVSignConversion (..),
+    SignConversion (..),
     SafeDivision (..),
     SafeLinearArith (..),
     SymIntegerOp,
@@ -1055,7 +1055,6 @@ import Grisette.Core.Control.Monad.UnionM
   )
 import Grisette.Core.Data.Class.BitVector
   ( BV (..),
-    BVSignConversion (..),
     SizedBV (..),
     bvExtract,
     sizedBVExtract,
@@ -1153,6 +1152,7 @@ import Grisette.Core.Data.Class.SafeArith
     SafeLinearArith (..),
     SymIntegerOp,
   )
+import Grisette.Core.Data.Class.SignConversion (SignConversion (..))
 import Grisette.Core.Data.Class.SimpleMergeable
   ( SimpleMergeable (..),
     SimpleMergeable1 (..),

src/Grisette/Core/Data/BV.hs

@@ -108,9 +108,11 @@ import GHC.TypeNats
   )
 import Grisette.Core.Data.Class.BitVector
   ( BV (bvConcat, bvExt, bvSelect, bvSext, bvZext),
-    BVSignConversion (toSigned, toUnsigned),
     SizedBV (sizedBVConcat, sizedBVExt, sizedBVSelect, sizedBVSext, sizedBVZext),
   )
+import Grisette.Core.Data.Class.SignConversion
+  ( SignConversion (toSigned, toUnsigned),
+  )
 import Grisette.Utils.Parameterized
   ( KnownProof (KnownProof),
     LeqProof (LeqProof),
@@ -784,10 +786,10 @@ instance BV SomeIntN where
   bvSelect ix w = toSigned . bvSelect ix w . toUnsigned
   {-# INLINE bvSelect #-}
 
-instance (KnownNat n, 1 <= n) => BVSignConversion (WordN n) (IntN n) where
+instance (KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n) where
   toSigned (WordN i) = IntN i
   toUnsigned (IntN i) = WordN i
 
-instance BVSignConversion SomeWordN SomeIntN where
+instance SignConversion SomeWordN SomeIntN where
   toSigned (SomeWordN i) = SomeIntN $ toSigned i
   toUnsigned (SomeIntN i) = SomeWordN $ toUnsigned i

src/Grisette/Core/Data/Class/BitVector.hs

@@ -1,7 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE RankNTypes #-}
@@ -24,7 +23,6 @@ module Grisette.Core.Data.Class.BitVector
     bvExtract,
     SizedBV (..),
     sizedBVExtract,
-    BVSignConversion (..),
   )
 where
 
@@ -234,11 +232,3 @@ sizedBVExtract _ _ =
     (KnownProof, LeqProof, LeqProof) ->
       sizedBVSelect (Proxy @j) (Proxy @(i - j + 1))
 {-# INLINE sizedBVExtract #-}
-
--- | Convert bitvectors from and to signed
-class BVSignConversion ubv sbv | ubv -> sbv, sbv -> ubv where
-  -- | Convert unsigned bitvector to signed
-  toSigned :: ubv -> sbv
-
-  -- | Convert signed bitvector to unsigned
-  toUnsigned :: sbv -> ubv

src/Grisette/Core/Data/Class/SignConversion.hs

@@ -0,0 +1,37 @@
+{-# LANGUAGE FunctionalDependencies #-}
+
+module Grisette.Core.Data.Class.SignConversion
+  ( SignConversion (..),
+  )
+where
+
+import Data.Int (Int16, Int32, Int64, Int8)
+import Data.Word (Word16, Word32, Word64, Word8)
+
+-- | Convert values between signed and unsigned.
+class SignConversion ubv sbv | ubv -> sbv, sbv -> ubv where
+  -- | Convert unsigned value to the corresponding signed value.
+  toSigned :: ubv -> sbv
+
+  -- | Convert signed value to the corresponding unsigned value.
+  toUnsigned :: sbv -> ubv
+
+instance SignConversion Word8 Int8 where
+  toSigned = fromIntegral
+  toUnsigned = fromIntegral
+
+instance SignConversion Word16 Int16 where
+  toSigned = fromIntegral
+  toUnsigned = fromIntegral
+
+instance SignConversion Word32 Int32 where
+  toSigned = fromIntegral
+  toUnsigned = fromIntegral
+
+instance SignConversion Word64 Int64 where
+  toSigned = fromIntegral
+  toUnsigned = fromIntegral
+
+instance SignConversion Word Int where
+  toSigned = fromIntegral
+  toUnsigned = fromIntegral

src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs

@@ -45,8 +45,8 @@ module Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
     complementBitsTerm,
     shiftBitsTerm,
     rotateBitsTerm,
-    bvToSignedTerm,
-    bvToUnsignedTerm,
+    toSignedTerm,
+    toUnsignedTerm,
     bvconcatTerm,
     bvselectTerm,
     bvextendTerm,
@@ -82,9 +82,9 @@ import qualified Data.Text as T
 import GHC.IO (unsafeDupablePerformIO)
 import GHC.TypeNats (KnownNat, type (+), type (<=))
 import Grisette.Core.Data.Class.BitVector
-  ( BVSignConversion,
-    SizedBV,
+  ( SizedBV,
   )
+import Grisette.Core.Data.Class.SignConversion (SignConversion)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
   ( BinaryOp,
     SupportedPrim,
@@ -99,8 +99,6 @@ import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
         UBVConcatTerm,
         UBVExtendTerm,
         UBVSelectTerm,
-        UBVToSignedTerm,
-        UBVToUnsignedTerm,
         UBinaryTerm,
         UComplementBitsTerm,
         UConTerm,
@@ -127,6 +125,8 @@ import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
         UTabularFunApplyTerm,
         UTernaryTerm,
         UTimesNumTerm,
+        UToSignedTerm,
+        UToUnsignedTerm,
         UUMinusNumTerm,
         UUnaryTerm,
         UXorBitsTerm
@@ -287,31 +287,23 @@ rotateBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Int -> Term a
 rotateBitsTerm t n = internTerm $ URotateBitsTerm t n
 {-# INLINE rotateBitsTerm #-}
 
-bvToSignedTerm ::
-  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
-    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
-    Typeable ubv,
-    Typeable sbv,
-    KnownNat n,
-    1 <= n,
-    BVSignConversion (ubv n) (sbv n)
+toSignedTerm ::
+  ( SupportedPrim u,
+    SupportedPrim s,
+    SignConversion u s
   ) =>
-  Term (ubv n) ->
-  Term (sbv n)
-bvToSignedTerm = internTerm . UBVToSignedTerm
-
-bvToUnsignedTerm ::
-  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
-    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
-    Typeable ubv,
-    Typeable sbv,
-    KnownNat n,
-    1 <= n,
-    BVSignConversion (ubv n) (sbv n)
+  Term u ->
+  Term s
+toSignedTerm = internTerm . UToSignedTerm
+
+toUnsignedTerm ::
+  ( SupportedPrim u,
+    SupportedPrim s,
+    SignConversion u s
   ) =>
-  Term (sbv n) ->
-  Term (ubv n)
-bvToUnsignedTerm = internTerm . UBVToUnsignedTerm
+  Term s ->
+  Term u
+toUnsignedTerm = internTerm . UToUnsignedTerm
 
 bvconcatTerm ::
   ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),

src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot

@@ -34,8 +34,8 @@ module Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
     complementBitsTerm,
     shiftBitsTerm,
     rotateBitsTerm,
-    bvToSignedTerm,
-    bvToUnsignedTerm,
+    toSignedTerm,
+    toUnsignedTerm,
     bvconcatTerm,
     bvselectTerm,
     bvextendTerm,
@@ -61,9 +61,9 @@ import qualified Data.Text as T
 import Data.Typeable (Typeable)
 import GHC.TypeNats (KnownNat, type (+), type (<=))
 import Grisette.Core.Data.Class.BitVector
-  ( BVSignConversion,
-    SizedBV,
+  ( SizedBV,
   )
+import Grisette.Core.Data.Class.SignConversion (SignConversion)
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
   ( BinaryOp,
     SupportedPrim,
@@ -132,28 +132,20 @@ xorBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
 complementBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a
 shiftBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Int -> Term a
 rotateBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Int -> Term a
-bvToSignedTerm ::
-  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
-    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
-    Typeable ubv,
-    Typeable sbv,
-    KnownNat n,
-    1 <= n,
-    BVSignConversion (ubv n) (sbv n)
+toSignedTerm ::
+  ( SupportedPrim u,
+    SupportedPrim s,
+    SignConversion u s
   ) =>
-  Term (ubv n) ->
-  Term (sbv n)
-bvToUnsignedTerm ::
-  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
-    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
-    Typeable ubv,
-    Typeable sbv,
-    KnownNat n,
-    1 <= n,
-    BVSignConversion (ubv n) (sbv n)
+  Term u ->
+  Term s
+toUnsignedTerm ::
+  ( SupportedPrim u,
+    SupportedPrim s,
+    SignConversion u s
   ) =>
-  Term (sbv n) ->
-  Term (ubv n)
+  Term s ->
+  Term u
 bvconcatTerm ::
   ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
     Typeable bv,