From b7aea79772bd55f3f60ddae4fa2b1eabc71a9d91 Mon Sep 17 00:00:00 2001
From: Sirui Lu <siruilu@cs.washington.edu>
Date: Fri, 12 May 2023 17:15:18 +0800
Subject: [PATCH] :sparkles: dynamic operations on somebv

---
 src/Grisette/Core.hs                      |   9 +-
 src/Grisette/Core/Data/BV.hs              | 105 ++++++-------
 src/Grisette/Core/Data/Class/BitVector.hs | 172 ++++------------------
 src/Grisette/IR/SymPrim/Data/SymPrim.hs   |  73 ++++++---
 4 files changed, 129 insertions(+), 230 deletions(-)

diff --git a/src/Grisette/Core.hs b/src/Grisette/Core.hs
index 703302e3..eb35e1b7 100644
--- a/src/Grisette/Core.hs
+++ b/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 (..),
diff --git a/src/Grisette/Core/Data/BV.hs b/src/Grisette/Core/Data/BV.hs
index 8d4132b1..e20da500 100644
--- a/src/Grisette/Core/Data/BV.hs
+++ b/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
diff --git a/src/Grisette/Core/Data/Class/BitVector.hs b/src/Grisette/Core/Data/Class/BitVector.hs
index 1761a4e8..c0f7380f 100644
--- a/src/Grisette/Core/Data/Class/BitVector.hs
+++ b/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,38 +42,34 @@ 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
@@ -86,19 +77,17 @@ class SomeBV bv where
   -- | 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
diff --git a/src/Grisette/IR/SymPrim/Data/SymPrim.hs b/src/Grisette/IR/SymPrim/Data/SymPrim.hs
index 3887edf6..71a4fe74 100644
--- a/src/Grisette/IR/SymPrim/Data/SymPrim.hs
+++ b/src/Grisette/IR/SymPrim/Data/SymPrim.hs
@@ -309,7 +309,7 @@ instance (KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) wher
 -- >>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
 -- >>> (SomeSymIntN ("a" :: SymIntN 5)) + (SomeSymIntN (5 :: SymIntN 5))
 -- (+ 0b00101 a)
--- >>> someBVConcat (SomeSymIntN (con 0b101 :: SymIntN 3)) (SomeSymIntN (con 0b110 :: SymIntN 3))
+-- >>> bvConcat (SomeSymIntN (con 0b101 :: SymIntN 3)) (SomeSymIntN (con 0b110 :: SymIntN 3))
 -- 0b101110
 --
 -- More symbolic operations are available. Please refer to the documentation
@@ -421,7 +421,7 @@ instance (KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) whe
 -- >>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
 -- >>> (SomeSymWordN ("a" :: SymWordN 5)) + (SomeSymWordN (5 :: SymWordN 5))
 -- (+ 0b00101 a)
--- >>> someBVConcat (SomeSymWordN (con 0b101 :: SymWordN 3)) (SomeSymWordN (con 0b110 :: SymWordN 3))
+-- >>> bvConcat (SomeSymWordN (con 0b101 :: SymWordN 3)) (SomeSymWordN (con 0b110 :: SymWordN 3))
 -- 0b101110
 --
 -- More symbolic operations are available. Please refer to the documentation
@@ -1254,47 +1254,74 @@ instance SizedBV SymWordN where
 -- BV
 
 #define BVCONCAT(somety, origty) \
-someBVConcat (somety (a :: origty l)) (somety (b :: origty r)) = \
+bvConcat (somety (a :: origty l)) (somety (b :: origty r)) = \
   case (leqAddPos (Proxy @l) (Proxy @r), knownAdd @l @r KnownProof KnownProof) of \
     (LeqProof, KnownProof) -> \
       somety $ sizedBVConcat a b
 
 #define BVZEXT(somety, origty) \
-someBVZext (p :: p l) (somety (a :: origty n)) \
-  | natVal p < natVal (Proxy @n) = error "zextBV: trying to zero extend a value to a smaller size" \
-  | otherwise = \
-    case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
-      (LeqProof, LeqProof) -> somety $ sizedBVZext p a
+bvZext l (somety (a :: origty n)) \
+  | l < n = error "bvZext: trying to zero extend a value to a smaller size" \
+  | otherwise = res (Proxy @n) \
+  where \
+    n = fromIntegral $ natVal (Proxy @n); \
+    res :: forall (l :: Nat). Proxy l -> somety; \
+    res p = \
+      case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
+        (KnownProof, LeqProof, LeqProof) -> somety $ sizedBVZext p a
 
 #define BVSEXT(somety, origty) \
-someBVSext (p :: p l) (somety (a :: origty n)) \
-  | natVal p < natVal (Proxy @n) = error "zextBV: trying to zero extend a value to a smaller size" \
-  | otherwise = \
-    case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
-      (LeqProof, LeqProof) -> somety $ sizedBVSext p a
+bvSext l (somety (a :: origty n)) \
+  | l < n = error "bvZext: trying to zero extend a value to a smaller size" \
+  | otherwise = res (Proxy @n) \
+  where \
+    n = fromIntegral $ natVal (Proxy @n); \
+    res :: forall (l :: Nat). Proxy l -> somety; \
+    res p = \
+      case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
+        (KnownProof, LeqProof, LeqProof) -> somety $ sizedBVSext p a
 
 #define BVSELECT(somety, origty) \
-someBVSelect (p :: p ix) (q :: q w) (somety (a :: origty n)) \
-  | natVal p + natVal q > natVal (Proxy @n) = error "selectBV: trying to select a bitvector outside the bounds of the input" \
-  | natVal q == 0 = error "selectBV: trying to select a bitvector of size 0" \
-  | otherwise = \
-    case (unsafeLeqProof @1 @w, unsafeLeqProof @(ix + w) @n) of \
-      (LeqProof, LeqProof) -> somety $ sizedBVSelect (Proxy @ix) (Proxy @w) a
+bvSelect ix w (somety (a :: origty 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 \
+      n = fromIntegral $ natVal (Proxy @n); \
+      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> somety; \
+      res p1 p2 = \
+        case ( unsafeKnownProof @ix (fromIntegral ix), \
+               unsafeKnownProof @w (fromIntegral w), \
+               unsafeLeqProof @1 @w, \
+               unsafeLeqProof @(ix + w) @n \
+             ) of \
+          (KnownProof, KnownProof, LeqProof, LeqProof) -> \
+            somety $ sizedBVSelect (Proxy @ix) (Proxy @w) a
 
 #if 1
-instance SomeBV SomeSymIntN where
+instance BV SomeSymIntN where
   BVCONCAT(SomeSymIntN, SymIntN)
+  {-# INLINE bvConcat #-}
   BVZEXT(SomeSymIntN, SymIntN)
+  {-# INLINE bvZext #-}
   BVSEXT(SomeSymIntN, SymIntN)
-  someBVExt = someBVSext
+  {-# INLINE bvSext #-}
+  bvExt = bvSext
+  {-# INLINE bvExt #-}
   BVSELECT(SomeSymIntN, SymIntN)
+  {-# INLINE bvSelect #-}
 
-instance SomeBV SomeSymWordN where
+instance BV SomeSymWordN where
   BVCONCAT(SomeSymWordN, SymWordN)
+  {-# INLINE bvConcat #-}
   BVZEXT(SomeSymWordN, SymWordN)
+  {-# INLINE bvZext #-}
   BVSEXT(SomeSymWordN, SymWordN)
-  someBVExt = someBVZext
+  {-# INLINE bvSext #-}
+  bvExt = bvZext
+  {-# INLINE bvExt #-}
   BVSELECT(SomeSymWordN, SymWordN)
+  {-# INLINE bvSelect #-}
 #endif
 
 -- BVSignConversion