feat: IntX.ofBitVec (#7048)

This PR adds the functions `IntX.ofBitVec`.

src/Init/Data/SInt/Basic.lean

@@ -85,6 +85,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
 If you want to obtain the 2's complement representation use `toBitVec`.
 -/
 @[inline] def Int8.toNat (i : Int8) : Nat := i.toInt.toNat
+/-- Obtains the `Int8` whose 2's complement representation is the given `BitVec 8`. -/
+@[inline] def Int8.ofBitVec (b : BitVec 8) : Int8 := ⟨⟨b⟩⟩
 @[extern "lean_int8_neg"]
 def Int8.neg (i : Int8) : Int8 := ⟨⟨-i.toBitVec⟩⟩
 
@@ -185,6 +187,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
 If you want to obtain the 2's complement representation use `toBitVec`.
 -/
 @[inline] def Int16.toNat (i : Int16) : Nat := i.toInt.toNat
+/-- Obtains the `Int16` whose 2's complement representation is the given `BitVec 16`. -/
+@[inline] def Int16.ofBitVec (b : BitVec 16) : Int16 := ⟨⟨b⟩⟩
 @[extern "lean_int16_to_int8"]
 def Int16.toInt8 (a : Int16) : Int8 := ⟨⟨a.toBitVec.signExtend 8⟩⟩
 @[extern "lean_int8_to_int16"]
@@ -289,6 +293,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
 If you want to obtain the 2's complement representation use `toBitVec`.
 -/
 @[inline] def Int32.toNat (i : Int32) : Nat := i.toInt.toNat
+/-- Obtains the `Int32` whose 2's complement representation is the given `BitVec 32`. -/
+@[inline] def Int32.ofBitVec (b : BitVec 32) : Int32 := ⟨⟨b⟩⟩
 @[extern "lean_int32_to_int8"]
 def Int32.toInt8 (a : Int32) : Int8 := ⟨⟨a.toBitVec.signExtend 8⟩⟩
 @[extern "lean_int32_to_int16"]
@@ -397,6 +403,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
 If you want to obtain the 2's complement representation use `toBitVec`.
 -/
 @[inline] def Int64.toNat (i : Int64) : Nat := i.toInt.toNat
+/-- Obtains the `Int64` whose 2's complement representation is the given `BitVec 64`. -/
+@[inline] def Int64.ofBitVec (b : BitVec 64) : Int64 := ⟨⟨b⟩⟩
 @[extern "lean_int64_to_int8"]
 def Int64.toInt8 (a : Int64) : Int8 := ⟨⟨a.toBitVec.signExtend 8⟩⟩
 @[extern "lean_int64_to_int16"]
@@ -509,6 +517,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
 If you want to obtain the 2's complement representation use `toBitVec`.
 -/
 @[inline] def ISize.toNat (i : ISize) : Nat := i.toInt.toNat
+/-- Obtains the `ISize` whose 2's complement representation is the given `BitVec`. -/
+@[inline] def ISize.ofBitVec (b : BitVec System.Platform.numBits) : ISize := ⟨⟨b⟩⟩
 @[extern "lean_isize_to_int32"]
 def ISize.toInt32 (a : ISize) : Int32 := ⟨⟨a.toBitVec.signExtend 32⟩⟩
 /--

tests/lean/sint_basic.lean

@@ -98,7 +98,7 @@ def test {α : Type} [BEq α] (w : Nat) (ofBitVec : BitVec w → α) (ofInt : In
       return false
   return true
 
-#eval test 8 (⟨⟨·⟩⟩) Int8.ofInt Int8.ofNat
+#eval test 8 Int8.ofBitVec Int8.ofInt Int8.ofNat
 
 -- runtime representation
 set_option trace.compiler.ir.result true in
@@ -179,7 +179,7 @@ def myId8 (x : Int8) : Int8 := x
 #eval min (10 : Int16) (-1) = -1
 
 
-#eval test 16 (⟨⟨·⟩⟩) Int16.ofInt Int16.ofNat
+#eval test 16 Int16.ofBitVec Int16.ofInt Int16.ofNat
 
 -- runtime representation
 set_option trace.compiler.ir.result true in
@@ -261,7 +261,7 @@ def myId16 (x : Int16) : Int16 := x
 #eval min (10 : Int32) (-1) = -1
 
 
-#eval test 32 (⟨⟨·⟩⟩) Int32.ofInt Int32.ofNat
+#eval test 32 Int32.ofBitVec Int32.ofInt Int32.ofNat
 
 -- runtime representation
 set_option trace.compiler.ir.result true in
@@ -342,7 +342,7 @@ def myId32 (x : Int32) : Int32 := x
 #eval min (10 : Int64) (-1) = -1
 
 
-#eval test 64 (⟨⟨·⟩⟩) Int64.ofInt Int64.ofNat
+#eval test 64 Int64.ofBitVec Int64.ofInt Int64.ofNat
 
 -- runtime representation
 set_option trace.compiler.ir.result true in
@@ -424,7 +424,7 @@ def myId64 (x : Int64) : Int64 := x
 #eval min (10 : ISize) (-1) = -1
 
 
-#eval test System.Platform.numBits (⟨⟨·⟩⟩) ISize.ofInt ISize.ofNat
+#eval test System.Platform.numBits ISize.ofBitVec ISize.ofInt ISize.ofNat
 
 -- runtime representation
 set_option trace.compiler.ir.result true in