max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: missing conversion functions for ISize (#7063)

Browse source 
This PR adds `ISize.toInt8`, `ISize.toInt16`, `Int8.toISize`,
`Int16.toISize`.
This commit is contained in:
Markus Himmel 2025-02-13 12:02:00 +01:00 • committed by GitHub
parent a833afa935
commit 04fe72fee0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 65 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Init/Data/SInt/Basic.lean
View file

@ -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⟩⟩

4
src/include/lean/lean.h
View file

@ -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; }

51
tests/lean/run/sint_conversions.lean Normal file
View file

@ -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