feat: missing conversion functions for ISize (#7063)

This PR adds `ISize.toInt8`, `ISize.toInt16`, `Int8.toISize`,
`Int16.toISize`.

src/Init/Data/SInt/Basic.lean

@@ -519,15 +519,23 @@ 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_int8"]
+def ISize.toInt8 (a : ISize) : Int8 := ⟨⟨a.toBitVec.signExtend 8⟩⟩
+@[extern "lean_isize_to_int16"]
+def ISize.toInt16 (a : ISize) : Int16 := ⟨⟨a.toBitVec.signExtend 16⟩⟩
 @[extern "lean_isize_to_int32"]
 def ISize.toInt32 (a : ISize) : Int32 := ⟨⟨a.toBitVec.signExtend 32⟩⟩
 /--
-Upcast `ISize` to `Int64`. This function is losless as `ISize` is either `Int32` or `Int64`.
+Upcasts `ISize` to `Int64`. This function is lossless as `ISize` is either `Int32` or `Int64`.
 -/
 @[extern "lean_isize_to_int64"]
 def ISize.toInt64 (a : ISize) : Int64 := ⟨⟨a.toBitVec.signExtend 64⟩⟩
+@[extern "lean_int8_to_isize"]
+def Int8.toISize (a : Int8) : ISize := ⟨⟨a.toBitVec.signExtend System.Platform.numBits⟩⟩
+@[extern "lean_int16_to_isize"]
+def Int16.toISize (a : Int16) : ISize := ⟨⟨a.toBitVec.signExtend System.Platform.numBits⟩⟩
 /--
-Upcast `Int32` to `ISize`. This function is losless as `ISize` is either `Int32` or `Int64`.
+Upcasts `Int32` to `ISize`. This function is lossless as `ISize` is either `Int32` or `Int64`.
 -/
 @[extern "lean_int32_to_isize"]
 def Int32.toISize (a : Int32) : ISize := ⟨⟨a.toBitVec.signExtend System.Platform.numBits⟩⟩

src/include/lean/lean.h

@@ -2015,6 +2015,7 @@ static inline uint8_t lean_int8_dec_le(uint8_t a1, uint8_t a2) {
 static inline uint16_t lean_int8_to_int16(uint8_t a) { return (uint16_t)(int16_t)(int8_t)a; }
 static inline uint32_t lean_int8_to_int32(uint8_t a) { return (uint32_t)(int32_t)(int8_t)a; }
 static inline uint64_t lean_int8_to_int64(uint8_t a) { return (uint64_t)(int64_t)(int8_t)a; }
+static inline size_t lean_int8_to_isize(uint8_t a) { return (size_t)(ptrdiff_t)(int8_t)a; }
 
 
 /* Int16 */
@@ -2155,6 +2156,7 @@ static inline uint8_t lean_int16_dec_le(uint16_t a1, uint16_t a2) {
 static inline uint8_t lean_int16_to_int8(uint16_t a) { return (uint8_t)(int8_t)(int16_t)a; }
 static inline uint32_t lean_int16_to_int32(uint16_t a) { return (uint32_t)(int32_t)(int16_t)a; }
 static inline uint64_t lean_int16_to_int64(uint16_t a) { return (uint64_t)(int64_t)(int16_t)a; }
+static inline size_t lean_int16_to_isize(uint16_t a) { return (size_t)(ptrdiff_t)(int16_t)a; }
 
 /* Int32 */
 LEAN_EXPORT int32_t lean_int32_of_big_int(b_lean_obj_arg a);
@@ -2573,6 +2575,8 @@ static inline uint8_t lean_isize_dec_le(size_t a1, size_t a2) {
 }
 
 /* ISize -> other */
+static inline uint8_t lean_isize_to_int8(size_t a) { return (uint8_t)(int8_t)(ptrdiff_t)a; }
+static inline uint16_t lean_isize_to_int16(size_t a) { return (uint16_t)(int16_t)(ptrdiff_t)a; }
 static inline uint32_t lean_isize_to_int32(size_t a) { return (uint32_t)(int32_t)(ptrdiff_t)a; }
 static inline uint64_t lean_isize_to_int64(size_t a) { return (uint64_t)(int64_t)(ptrdiff_t)a; }
 

tests/lean/run/sint_conversions.lean

@@ -0,0 +1,51 @@
+example : (-2147483649 : Int8).toInt16 = -1 := by native_decide
+example : (-2147483649 : Int8).toInt16 = -1 := by rfl
+example : (-2147483649 : Int8).toInt32 = -1 := by native_decide
+example : (-2147483649 : Int8).toInt32 = -1 := by rfl
+example : (-2147483649 : Int8).toInt64 = -1 := by native_decide
+example : (-2147483649 : Int8).toInt64 = -1 := by rfl
+example : (-2147483649 : Int8).toISize = -1 := by native_decide
+-- TODO: add proof once the theory is available
+-- example : (-2147483649 : Int8).toISize = -1 := by rfl
+
+example : (-2147483649 : Int16).toInt8 = -1 := by native_decide
+example : (-2147483649 : Int16).toInt8 = -1 := by rfl
+example : (-2147483649 : Int16).toInt32 = -1 := by native_decide
+example : (-2147483649 : Int16).toInt32 = -1 := by rfl
+example : (-2147483649 : Int16).toInt64 = -1 := by native_decide
+example : (-2147483649 : Int16).toInt64 = -1 := by rfl
+example : (-2147483649 : Int16).toISize = -1 := by native_decide
+-- TODO: add proof once the theory is available
+-- example : (-2147483649 : Int16).toISize = -1 := by rfl
+
+example : (-2147483649 : Int32).toInt8 = -1 := by native_decide
+example : (-2147483649 : Int32).toInt8 = -1 := by rfl
+example : (-2147483649 : Int32).toInt16 = -1 := by native_decide
+example : (-2147483649 : Int32).toInt16 = -1 := by rfl
+example : (-2147483649 : Int32).toInt64 = 2147483647 := by native_decide
+example : (-2147483649 : Int32).toInt64 = 2147483647 := by rfl
+example : (-2147483649 : Int32).toISize = 2147483647 := by native_decide
+example : (-2147483649 : Int32).toISize = 2147483647 := by rfl
+
+example : (-2147483649 : Int64).toInt8 = -1 := by native_decide
+example : (-2147483649 : Int64).toInt8 = -1 := by rfl
+example : (-2147483649 : Int64).toInt16 = -1 := by native_decide
+example : (-2147483649 : Int64).toInt16 = -1 := by rfl
+example : (-2147483649 : Int64).toInt32 = 2147483647 := by native_decide
+example : (-2147483649 : Int64).toInt32 = 2147483647 := by rfl
+example : (-2147483649 : Int64).toISize = 2147483647 ∨ (-2147483649 : Int64).toISize = -2147483649 := by native_decide
+-- TODO: add proof once the theory is available
+-- example : (-2147483649 : Int64).toISize = 2147483647 := by rfl
+
+example : (-2147483649 : ISize).toInt8 = -1 := by native_decide
+-- TODO: add proof once the theory is available
+-- example : (-2147483649 : ISize).toInt8 = -1 := by rfl
+example : (-2147483649 : ISize).toInt16 = -1 := by native_decide
+-- TODO: add proof once the theory is available
+-- example : (-2147483649 : ISize).toInt16 = -1 := by rfl
+example : (-2147483649 : ISize).toInt32 = 2147483647 := by native_decide
+-- TODO: add proof once the theory is available
+-- example : (-2147483649 : ISize).toInt32 = 2147483647 := by rfl
+example : (-2147483649 : ISize).toInt64 = 2147483647 ∨ (-2147483649 : ISize).toInt64 = -2147483649 := by native_decide
+-- TODO: add proof once the theory is available
+-- example : (-2147483649 : ISize).toInt64 = 2147483647 := by decide