🐛 Make symCountLeadingZeros/symPopCount/symCountTrailingZeros less co…

…nfusing by returning the arg type

src/Grisette/Core.hs

@@ -358,6 +358,18 @@ module Grisette.Core
     SymRotate (..),
     SafeSymRotate (..),
     SignConversion (..),
+    lsb,
+    msb,
+    setBitTo,
+    bitBlast,
+    FromBits (..),
+    SymFiniteBits (..),
+    symBitBlast,
+    symLsb,
+    symMsb,
+    symPopCount,
+    symCountLeadingZeros,
+    symCountTrailingZeros,
 
     -- ** Safe operation for Numbers
     DivOr (..),
@@ -1725,6 +1737,20 @@ import Grisette.Internal.Core.Data.Class.SymEq
     symEq1,
     symEq2,
   )
+import Grisette.Internal.Core.Data.Class.SymFiniteBits
+  ( FromBits (..),
+    SymFiniteBits (..),
+    bitBlast,
+    lsb,
+    msb,
+    setBitTo,
+    symBitBlast,
+    symCountLeadingZeros,
+    symCountTrailingZeros,
+    symLsb,
+    symMsb,
+    symPopCount,
+  )
 import Grisette.Internal.Core.Data.Class.SymFromIntegral
   ( SymFromIntegral (..),
   )

src/Grisette/Internal/Core/Data/Class/SymFiniteBits.hs

@@ -182,12 +182,14 @@ symMsb :: (SymFiniteBits a) => a -> SymBool
 symMsb x = symTestBit x (finiteBitSize x - 1)
 
 -- | Count the number of set bits in a symbolic value.
-symPopCount :: (Num b, ITEOp b, SymFiniteBits a) => a -> b
-symPopCount v = sum $ (\b -> symIte b 1 0) <$> symBitBlast v
+symPopCount :: (Num a, ITEOp a, SymFiniteBits a) => a -> a
+-- Node: v - v + is a trick to assign the correct bit-width to the result.
+symPopCount v = v - v + sum ((\b -> symIte b 1 0) <$> symBitBlast v)
 
 -- | Count the number of leading zeros in a symbolic value.
-symCountLeadingZeros :: (Num b, ITEOp b, SymFiniteBits a) => a -> b
-symCountLeadingZeros v = go bits rs
+symCountLeadingZeros :: (Num a, ITEOp a, SymFiniteBits a) => a -> a
+-- Node: v - v + is a trick to assign the correct bit-width to the result.
+symCountLeadingZeros v = v - v + go bits rs
   where
     bits = reverse $ symBitBlast v
     rs = fromIntegral <$> [0 ..]
@@ -196,8 +198,9 @@ symCountLeadingZeros v = go bits rs
     go _ [] = error "Should not happen"
 
 -- | Count the number of trailing zeros in a symbolic value.
-symCountTrailingZeros :: (Num b, ITEOp b, SymFiniteBits a) => a -> b
-symCountTrailingZeros v = go bits rs
+symCountTrailingZeros :: (Num a, ITEOp a, SymFiniteBits a) => a -> a
+-- Node: v - v + is a trick to assign the correct bit-width to the result.
+symCountTrailingZeros v = v - v + go bits rs
   where
     bits = symBitBlast v
     rs = fromIntegral <$> [0 ..]

src/Grisette/Unified/Internal/Class/UnifiedFiniteBits.hs

@@ -130,43 +130,43 @@ symMsb a =
 
 -- | Unified `Grisette.Internal.Core.Data.Class.SymFiniteBits.symPopCount`.
 symPopCount ::
-  forall mode a b.
-  (Typeable mode, UnifiedFiniteBits mode a, Num b, UnifiedITEOp mode b) =>
+  forall mode a.
+  (Typeable mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) =>
   a ->
-  b
+  a
 symPopCount a =
   withMode @mode
     (withBaseFiniteBits @mode @a (fromIntegral $ popCount a))
     ( withBaseFiniteBits @mode @a $
-        withBaseITEOp @mode @b (SymFiniteBits.symPopCount a)
+        withBaseITEOp @mode @a (SymFiniteBits.symPopCount a)
     )
 
 -- | Unified
 -- `Grisette.Internal.Core.Data.Class.SymFiniteBits.symCountLeadingZeros`.
 symCountLeadingZeros ::
-  forall mode a b.
-  (Typeable mode, UnifiedFiniteBits mode a, Num b, UnifiedITEOp mode b) =>
+  forall mode a.
+  (Typeable mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) =>
   a ->
-  b
+  a
 symCountLeadingZeros a =
   withMode @mode
     (withBaseFiniteBits @mode @a (fromIntegral $ countLeadingZeros a))
     ( withBaseFiniteBits @mode @a $
-        withBaseITEOp @mode @b (SymFiniteBits.symCountLeadingZeros a)
+        withBaseITEOp @mode @a (SymFiniteBits.symCountLeadingZeros a)
     )
 
 -- | Unified
 -- `Grisette.Internal.Core.Data.Class.SymFiniteBits.symCountTrailingZeros`.
 symCountTrailingZeros ::
-  forall mode a b.
-  (Typeable mode, UnifiedFiniteBits mode a, Num b, UnifiedITEOp mode b) =>
+  forall mode a.
+  (Typeable mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) =>
   a ->
-  b
+  a
 symCountTrailingZeros a =
   withMode @mode
     (withBaseFiniteBits @mode @a (fromIntegral $ countTrailingZeros a))
     ( withBaseFiniteBits @mode @a $
-        withBaseITEOp @mode @b (SymFiniteBits.symCountTrailingZeros a)
+        withBaseITEOp @mode @a (SymFiniteBits.symCountTrailingZeros a)
     )
 
 -- | A class that provides unified equality comparison.

test/Grisette/Core/Data/Class/SymFiniteBitsTests.hs

@@ -16,7 +16,6 @@ import Grisette
     SomeSymWordN,
     SymEq,
     SymIntN,
-    SymInteger,
     SymWordN,
   )
 import Grisette.Internal.Core.Data.Class.SymFiniteBits
@@ -41,6 +40,7 @@ someBVSymFiniteBitsTest ::
     SymFiniteBits bv,
     Show bv,
     SymEq bv,
+    Num bv,
     EvalSym bv
   ) =>
   p bv ->
@@ -75,20 +75,20 @@ someBVSymFiniteBitsTest _ =
         symMsb (bv 4 0b0101 :: bv) @?= false
         symMsb (bv 4 0b1101 :: bv) @?= true,
       testCase "symPopCount" $ do
-        symPopCount (bv 4 0 :: bv) @?= (0 :: SymInteger)
-        symPopCount (bv 4 0b0101 :: bv) @?= (2 :: SymInteger)
-        symPopCount (bv 4 0b1101 :: bv) @?= (3 :: SymInteger)
-        symPopCount (bv 4 0b1111 :: bv) @?= (4 :: SymInteger),
+        symPopCount (bv 4 0 :: bv) @?= 0
+        symPopCount (bv 4 0b0101 :: bv) @?= 2
+        symPopCount (bv 4 0b1101 :: bv) @?= 3
+        symPopCount (bv 4 0b1111 :: bv) @?= 4,
       testCase "symCountLeadingZeros" $ do
-        symCountLeadingZeros (bv 4 0 :: bv) @?= (4 :: SymInteger)
-        symCountLeadingZeros (bv 4 0b0101 :: bv) @?= (1 :: SymInteger)
-        symCountLeadingZeros (bv 4 0b1101 :: bv) @?= (0 :: SymInteger)
-        symCountLeadingZeros (bv 4 0b0011 :: bv) @?= (2 :: SymInteger),
+        symCountLeadingZeros (bv 4 0 :: bv) @?= 4
+        symCountLeadingZeros (bv 4 0b0101 :: bv) @?= 1
+        symCountLeadingZeros (bv 4 0b1101 :: bv) @?= 0
+        symCountLeadingZeros (bv 4 0b0011 :: bv) @?= 2,
       testCase "symCountTrailingZeros" $ do
-        symCountTrailingZeros (bv 4 0 :: bv) @?= (4 :: SymInteger)
-        symCountTrailingZeros (bv 4 0b1010 :: bv) @?= (1 :: SymInteger)
-        symCountTrailingZeros (bv 4 0b1011 :: bv) @?= (0 :: SymInteger)
-        symCountTrailingZeros (bv 4 0b1100 :: bv) @?= (2 :: SymInteger)
+        symCountTrailingZeros (bv 4 0 :: bv) @?= 4
+        symCountTrailingZeros (bv 4 0b1010 :: bv) @?= 1
+        symCountTrailingZeros (bv 4 0b1011 :: bv) @?= 0
+        symCountTrailingZeros (bv 4 0b1100 :: bv) @?= 2
     ]
 
 bvSymFiniteBitsTest ::
@@ -132,20 +132,20 @@ bvSymFiniteBitsTest _ =
         symMsb (0b0101 :: bv 4) @?= false
         symMsb (0b1101 :: bv 4) @?= true,
       testCase "symPopCount" $ do
-        symPopCount (0 :: bv 4) @?= (0 :: SymInteger)
-        symPopCount (0b0101 :: bv 4) @?= (2 :: SymInteger)
-        symPopCount (0b1101 :: bv 4) @?= (3 :: SymInteger)
-        symPopCount (0b1111 :: bv 4) @?= (4 :: SymInteger),
+        symPopCount (0 :: bv 4) @?= 0
+        symPopCount (0b0101 :: bv 4) @?= 2
+        symPopCount (0b1101 :: bv 4) @?= 3
+        symPopCount (0b1111 :: bv 4) @?= 4,
       testCase "symCountLeadingZeros" $ do
-        symCountLeadingZeros (0 :: bv 4) @?= (4 :: SymInteger)
-        symCountLeadingZeros (0b0101 :: bv 4) @?= (1 :: SymInteger)
-        symCountLeadingZeros (0b1101 :: bv 4) @?= (0 :: SymInteger)
-        symCountLeadingZeros (0b0011 :: bv 4) @?= (2 :: SymInteger),
+        symCountLeadingZeros (0 :: bv 4) @?= 4
+        symCountLeadingZeros (0b0101 :: bv 4) @?= 1
+        symCountLeadingZeros (0b1101 :: bv 4) @?= 0
+        symCountLeadingZeros (0b0011 :: bv 4) @?= 2,
       testCase "symCountTrailingZeros" $ do
-        symCountTrailingZeros (0 :: bv 4) @?= (4 :: SymInteger)
-        symCountTrailingZeros (0b1010 :: bv 4) @?= (1 :: SymInteger)
-        symCountTrailingZeros (0b1011 :: bv 4) @?= (0 :: SymInteger)
-        symCountTrailingZeros (0b1100 :: bv 4) @?= (2 :: SymInteger)
+        symCountTrailingZeros (0 :: bv 4) @?= 4
+        symCountTrailingZeros (0b1010 :: bv 4) @?= 1
+        symCountTrailingZeros (0b1011 :: bv 4) @?= 0
+        symCountTrailingZeros (0b1100 :: bv 4) @?= 2
     ]
 
 symFiniteBitsTests :: Test