chore: Make signExtend use output number of bits. (leanprover-communi…

…ty#308)
thorimur · Oct 20, 2023 · e13fb47 · e13fb47
1 parent 0b07a6e
commit e13fb47
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 4 deletions.
diff --git a/Std/Data/BitVec/Basic.lean b/Std/Data/BitVec/Basic.lean
@@ -416,5 +416,4 @@ bit in `x`. If `x` is an empty vector, then the sign is treated as zero.
 
 SMT-Lib name: `sign_extend`.
 -/
-def signExtend (i : Nat) (x : BitVec w) : BitVec (w+i) :=
-  Nat.add_comm .. ▸ (fill i x.msb ++ x)
+def signExtend (v : Nat) (x : BitVec w) : BitVec v := .ofInt v x.toInt
diff --git a/test/bitvec.lean b/test/bitvec.lean
@@ -8,11 +8,19 @@ open Std.BitVec
 #guard 3#5 * 7#5 = 0x15#5
 #guard 3#4 * 7#4 = 0x05#4
 
--- Division and mod/rem
+#guard zeroExtend  4 0x7f#8 = 0xf#4
+#guard zeroExtend 12 0x7f#8 = 0x07f#12
+#guard zeroExtend 12 0x80#8 = 0x080#12
+#guard zeroExtend 16 0xff#8 = 0x00ff#16
 
+#guard signExtend  4 0x7f#8 = 0xf#4
+#guard signExtend 12 0x7f#8 = 0x07f#12
+#guard signExtend 12 0x80#8 = 0xf80#12
+#guard signExtend 16 0xff#8 = 0xffff#16
 
-#guard 3#4 / 0 = 0
+-- Division and mod/rem
 
+#guard 3#4 / 0 = 0
 #guard 10#4 / 2 = 5
 
 #guard 8#4 % 0 = 8