🔀 Merge pull request #71 from lsrcz/feat-somebv-dynselect

Dynamic operations on somebv

src/Grisette/Core.hs

@@ -181,13 +181,8 @@ module Grisette.Core
     SEq (..),
     SymBoolOp,
     SOrd (..),
-    SomeBV (..),
-    someBVZext',
-    someBVSext',
-    someBVExt',
-    someBVSelect',
-    someBVExtract,
-    someBVExtract',
+    BV (..),
+    bvExtract,
     SizedBV (..),
     sizedBVExtract,
     SafeDivision (..),

src/Grisette/Core/Data/BV.hs

@@ -624,71 +624,58 @@ instance SizedBV IntN where
     IntN w
   sizedBVSelect pix pw (IntN v) = IntN $ unWordN $ sizedBVSelect pix pw (WordN v :: WordN n)
 
-instance SomeBV SomeWordN where
-  someBVConcat (SomeWordN (a :: WordN l)) (SomeWordN (b :: WordN r)) =
+instance BV SomeWordN where
+  bvConcat (SomeWordN (a :: WordN l)) (SomeWordN (b :: WordN r)) =
     case (leqAddPos (Proxy @l) (Proxy @r), knownAdd @l @r KnownProof KnownProof) of
       (LeqProof, KnownProof) ->
         SomeWordN $ sizedBVConcat a b
-  someBVZext (p :: p l) (SomeWordN (a :: WordN n))
-    | l < n = error "someBVZext: trying to zero extend a value to a smaller size"
-    | otherwise =
-        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of
-          (LeqProof, LeqProof) -> SomeWordN $ sizedBVZext p a
+  {-# INLINE bvConcat #-}
+  bvZext l (SomeWordN (a :: WordN n))
+    | l < n = error "bvZext: trying to zero extend a value to a smaller size"
+    | otherwise = res (Proxy @n)
     where
-      l = natVal p
-      n = natVal (Proxy @n)
-  someBVSext (p :: p l) (SomeWordN (a :: WordN n))
-    | l < n = error "someBVSext: trying to zero extend a value to a smaller size"
-    | otherwise =
-        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of
-          (LeqProof, LeqProof) -> SomeWordN $ sizedBVSext p a
+      n = fromIntegral $ natVal (Proxy @n)
+      res :: forall (l :: Nat). Proxy l -> SomeWordN
+      res p =
+        case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of
+          (KnownProof, LeqProof, LeqProof) -> SomeWordN $ sizedBVZext p a
+  bvSext l (SomeWordN (a :: WordN n))
+    | l < n = error "bvSext: trying to zero extend a value to a smaller size"
+    | otherwise = res (Proxy @n)
     where
-      l = natVal p
-      n = natVal (Proxy @n)
-  someBVExt = someBVZext
-  someBVSelect (p :: p ix) (q :: q w) (SomeWordN (a :: WordN n))
-    | ix + w > n = error "someBVSelect: trying to select a bitvector outside the bounds of the input"
-    | w == 0 = error "someBVSelect: trying to select a bitvector of size 0"
-    | otherwise =
-        case (unsafeLeqProof @1 @w, unsafeLeqProof @(ix + w) @n) of
-          (LeqProof, LeqProof) -> SomeWordN $ sizedBVSelect (Proxy @ix) (Proxy @w) a
+      n = fromIntegral $ natVal (Proxy @n)
+      res :: forall (l :: Nat). Proxy l -> SomeWordN
+      res p =
+        case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of
+          (KnownProof, LeqProof, LeqProof) -> SomeWordN $ sizedBVSext p a
+  bvExt = bvZext
+  bvSelect ix w (SomeWordN (a :: WordN n))
+    | ix + w > n = error "bvSelect: trying to select a bitvector outside the bounds of the input"
+    | w == 0 = error "bvSelect: trying to select a bitvector of size 0"
+    | otherwise = res (Proxy @n) (Proxy @n)
     where
-      ix = natVal p
-      w = natVal q
-      n = natVal (Proxy @n)
-
-instance SomeBV SomeIntN where
-  someBVConcat (SomeIntN (a :: IntN l)) (SomeIntN (b :: IntN r)) =
-    case (leqAddPos (Proxy @l) (Proxy @r), knownAdd (KnownProof @l) (KnownProof @r)) of
-      (LeqProof, KnownProof) ->
-        SomeIntN $ sizedBVConcat a b
-  someBVZext (p :: p l) (SomeIntN (a :: IntN n))
-    | l < n = error "someBVZext: trying to zero extend a value to a smaller size"
-    | otherwise =
-        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of
-          (LeqProof, LeqProof) -> SomeIntN $ sizedBVZext p a
-    where
-      l = natVal p
-      n = natVal (Proxy @n)
-  someBVSext (p :: p l) (SomeIntN (a :: IntN n))
-    | l < n = error "someBVSext: trying to zero extend a value to a smaller size"
-    | otherwise =
-        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of
-          (LeqProof, LeqProof) -> SomeIntN $ sizedBVSext p a
-    where
-      l = natVal p
-      n = natVal (Proxy @n)
-  someBVExt = someBVZext
-  someBVSelect (p :: p ix) (q :: q w) (SomeIntN (a :: IntN n))
-    | ix + w > n = error "someBVSelect: trying to select a bitvector outside the bounds of the input"
-    | w == 0 = error "someBVSelect: trying to select a bitvector of size 0"
-    | otherwise =
-        case (unsafeLeqProof @1 @w, unsafeLeqProof @(ix + w) @n) of
-          (LeqProof, LeqProof) -> SomeIntN $ sizedBVSelect (Proxy @ix) (Proxy @w) a
-    where
-      ix = natVal p
-      w = natVal q
-      n = natVal (Proxy @n)
+      n = fromIntegral $ natVal (Proxy @n)
+      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeWordN
+      res p1 p2 =
+        case ( unsafeKnownProof @ix (fromIntegral ix),
+               unsafeKnownProof @w (fromIntegral w),
+               unsafeLeqProof @1 @w,
+               unsafeLeqProof @(ix + w) @n
+             ) of
+          (KnownProof, KnownProof, LeqProof, LeqProof) ->
+            SomeWordN $ sizedBVSelect (Proxy @ix) (Proxy @w) a
+
+instance BV SomeIntN where
+  bvConcat l r = toSigned $ bvConcat (toUnsigned l) (toUnsigned l)
+  {-# INLINE bvConcat #-}
+  bvZext l = toSigned . bvZext l . toUnsigned
+  {-# INLINE bvZext #-}
+  bvSext l = toSigned . bvSext l . toUnsigned
+  {-# INLINE bvSext #-}
+  bvExt l = toSigned . bvExt l . toUnsigned
+  {-# INLINE bvExt #-}
+  bvSelect ix w = toSigned . bvSelect ix w . toUnsigned
+  {-# INLINE bvSelect #-}
 
 instance (KnownNat n, 1 <= n) => BVSignConversion (WordN n) (IntN n) where
   toSigned (WordN i) = IntN i

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

@@ -20,13 +20,8 @@
 -- Portability :   GHC only
 module Grisette.Core.Data.Class.BitVector
   ( -- * Bit vector operations
-    SomeBV (..),
-    someBVZext',
-    someBVSext',
-    someBVExt',
-    someBVSelect',
-    someBVExtract,
-    someBVExtract',
+    BV (..),
+    bvExtract,
     SizedBV (..),
     sizedBVExtract,
     BVSignConversion (..),
@@ -47,58 +42,52 @@ import Grisette.Utils.Parameterized
 -- >>> :set -XFlexibleInstances
 -- >>> :set -XFunctionalDependencies
 
--- | Bit vector operations. Including concatenation ('someBVConcat'),
--- extension ('someBVZext', 'someBVSext', 'someBVExt'), and selection
--- ('someBVSelect').
-class SomeBV bv where
+-- | Bit vector operations. Including concatenation ('bvConcat'),
+-- extension ('bvZext', 'bvSext', 'bvExt'), and selection
+-- ('bvSelect').
+class BV bv where
   -- | Concatenation of two bit vectors.
   --
-  -- >>> someBVConcat (SomeSymWordN (0b101 :: SymWordN 3)) (SomeSymWordN (0b010 :: SymWordN 3))
+  -- >>> bvConcat (SomeSymWordN (0b101 :: SymWordN 3)) (SomeSymWordN (0b010 :: SymWordN 3))
   -- 0b101010
-  someBVConcat :: bv -> bv -> bv
+  bvConcat :: bv -> bv -> bv
 
   -- | Zero extension of a bit vector.
   --
-  -- >>> someBVZext (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))
+  -- >>> bvZext 6 (SomeSymWordN (0b101 :: SymWordN 3))
   -- 0b000101
-  someBVZext ::
-    forall p l.
-    (KnownNat l) =>
+  bvZext ::
     -- | Desired output length
-    p l ->
+    Int ->
     -- | Bit vector to extend
     bv ->
     bv
 
   -- | Sign extension of a bit vector.
   --
-  -- >>> someBVSext (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))
+  -- >>> bvSext 6 (SomeSymWordN (0b101 :: SymWordN 3))
   -- 0b111101
-  someBVSext ::
-    forall p l.
-    (KnownNat l) =>
+  bvSext ::
     -- | Desired output length
-    p l ->
+    Int ->
     -- | Bit vector to extend
     bv ->
     bv
 
   -- | Extension of a bit vector.
   -- Signedness is determined by the input bit vector type.
   --
-  -- >>> someBVExt (Proxy @6) (SomeSymIntN (0b101 :: SymIntN 3))
+  -- >>> bvExt 6 (SomeSymIntN (0b101 :: SymIntN 3))
   -- 0b111101
-  -- >>> someBVExt (Proxy @6) (SomeSymIntN (0b001 :: SymIntN 3))
+  -- >>> bvExt 6 (SomeSymIntN (0b001 :: SymIntN 3))
   -- 0b000001
-  -- >>> someBVExt (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))
+  -- >>> bvExt 6 (SomeSymWordN (0b101 :: SymWordN 3))
   -- 0b000101
-  -- >>> someBVExt (Proxy @6) (SomeSymWordN (0b001 :: SymWordN 3))
+  -- >>> bvExt 6 (SomeSymWordN (0b001 :: SymWordN 3))
   -- 0b000001
-  someBVExt ::
-    forall p l.
-    (KnownNat l) =>
+  bvExt ::
     -- | Desired output length
-    p l ->
+    Int ->
     -- | Bit vector to extend
     bv ->
     bv
@@ -108,136 +97,37 @@ class SomeBV bv where
   --
   -- The least significant bit is indexed as 0.
   --
-  -- >>> someBVSelect (Proxy @1) (Proxy @3) (SomeSymIntN (0b001010 :: SymIntN 6))
+  -- >>> bvSelect 1 3 (SomeSymIntN (0b001010 :: SymIntN 6))
   -- 0b101
-  someBVSelect ::
-    forall p ix q w.
-    (KnownNat ix, KnownNat w) =>
+  bvSelect ::
     -- | Index of the least significant bit of the slice
-    p ix ->
+    Int ->
     -- | Desired output width, @ix + w <= n@ must hold where @n@ is
     -- the size of the input bit vector
-    q w ->
+    Int ->
     -- | Bit vector to select from
     bv ->
     bv
 
--- | Zero extension of a bit vector.
---
--- >>> someBVZext' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))
--- 0b000101
-someBVZext' ::
-  forall l bv.
-  (SomeBV bv) =>
-  -- | Desired output length
-  NatRepr l ->
-  -- | Bit vector to extend
-  bv ->
-  bv
-someBVZext' p@(_ :: NatRepr l) = withKnownProof (hasRepr p) $ someBVZext (Proxy @l)
-{-# INLINE someBVZext' #-}
-
--- | Sign extension of a bit vector.
---
--- >>> someBVSext' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))
--- 0b111101
-someBVSext' ::
-  forall l bv.
-  (SomeBV bv) =>
-  NatRepr l ->
-  -- | Desired output length
-  bv ->
-  -- | Bit vector to extend
-  bv
-someBVSext' p@(_ :: NatRepr l) = withKnownProof (hasRepr p) $ someBVSext (Proxy @l)
-{-# INLINE someBVSext' #-}
-
--- | Extension of a bit vector.
--- Signedness is determined by the input bit vector type.
---
--- >>> someBVExt' (natRepr @6) (SomeSymIntN (0b101 :: SymIntN 3))
--- 0b111101
--- >>> someBVExt' (natRepr @6) (SomeSymIntN (0b001 :: SymIntN 3))
--- 0b000001
--- >>> someBVExt' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))
--- 0b000101
--- >>> someBVExt' (natRepr @6) (SomeSymWordN (0b001 :: SymWordN 3))
--- 0b000001
-someBVExt' ::
-  forall l bv.
-  (SomeBV bv) =>
-  -- | Desired output length
-  NatRepr l ->
-  -- | Bit vector to extend
-  bv ->
-  bv
-someBVExt' p@(_ :: NatRepr l) = withKnownProof (hasRepr p) $ someBVExt (Proxy @l)
-{-# INLINE someBVExt' #-}
-
--- | Slicing out a smaller bit vector from a larger one,
--- selecting a slice with width @w@ starting from index @ix@.
---
--- The least significant bit is indexed as 0.
---
--- >>> someBVSelect' (natRepr @1) (natRepr @3) (SomeSymIntN (0b001010 :: SymIntN 6))
--- 0b101
-someBVSelect' ::
-  forall ix w bv.
-  (SomeBV bv) =>
-  -- | Index of the least significant bit of the slice
-  NatRepr ix ->
-  -- | Desired output width, @ix + w <= n@ must hold where @n@ is
-  -- the size of the input bit vector
-  NatRepr w ->
-  -- | Bit vector to select from
-  bv ->
-  bv
-someBVSelect' p@(_ :: NatRepr l) q@(_ :: NatRepr r) = withKnownProof (hasRepr p) $ withKnownProof (hasRepr q) $ someBVSelect p q
-{-# INLINE someBVSelect' #-}
-
--- | Slicing out a smaller bit vector from a larger one, extract a slice from
--- bit @i@ down to @j@.
---
--- The least significant bit is indexed as 0.
---
--- >>> someBVExtract (Proxy @4) (Proxy @2) (SomeSymIntN (0b010100 :: SymIntN 6))
--- 0b101
-someBVExtract ::
-  forall p (i :: Nat) q (j :: Nat) bv.
-  (SomeBV bv, KnownNat i, KnownNat j) =>
-  -- | The start position to extract from, @i < n@ must hold where @n@ is
-  -- the size of the output bit vector
-  p i ->
-  -- | The end position to extract from, @j <= i@ must hold
-  q j ->
-  -- | Bit vector to extract from
-  bv ->
-  bv
-someBVExtract _ _ =
-  withKnownProof (unsafeKnownProof @(i - j + 1) (fromIntegral (natVal (Proxy @i)) - fromIntegral (natVal (Proxy @j)) + 1)) $
-    someBVSelect (Proxy @j) (Proxy @(i - j + 1))
-{-# INLINE someBVExtract #-}
-
 -- | Slicing out a smaller bit vector from a larger one, extract a slice from
 -- bit @i@ down to @j@.
 --
 -- The least significant bit is indexed as 0.
 --
--- >>> someBVExtract' (natRepr @4) (natRepr @2) (SomeSymIntN (0b010100 :: SymIntN 6))
+-- >>> bvExtract 4 2 (SomeSymIntN (0b010100 :: SymIntN 6))
 -- 0b101
-someBVExtract' ::
-  forall (i :: Nat) (j :: Nat) bv.
-  (SomeBV bv) =>
+bvExtract ::
+  (BV bv) =>
   -- | The start position to extract from, @i < n@ must hold where @n@ is
   -- the size of the output bit vector
-  NatRepr i ->
+  Int ->
   -- | The end position to extract from, @j <= i@ must hold
-  NatRepr j ->
+  Int ->
   -- | Bit vector to extract from
   bv ->
   bv
-someBVExtract' p@(_ :: NatRepr l) q@(_ :: NatRepr r) = withKnownProof (hasRepr p) $ withKnownProof (hasRepr q) $ someBVExtract p q
-{-# INLINE someBVExtract' #-}
+bvExtract i j = bvSelect j (i - j + 1)
+{-# INLINE bvExtract #-}
 
 -- | Sized bit vector operations. Including concatenation ('sizedBVConcat'),
 -- extension ('sizedBVZext', 'sizedBVSext', 'sizedBVExt'), and selection