feat: define ISize and basic operations on it (#5961)

src/Init/Data/SInt/Basic.lean

@@ -52,6 +52,18 @@ structure Int64 where
   -/
   toUInt64 : UInt64
 
+/--
+A `ISize` is a signed integer with the size of a word for the platform's architecture.
+
+For example, if running on a 32-bit machine, ISize is equivalent to `Int32`.
+Or on a 64-bit machine, `Int64`.
+-/
+structure ISize where
+  /--
+  Obtain the `USize` that is 2's complement equivalent to the `ISize`.
+  -/
+  toUSize : USize
+
 /-- The size of type `Int8`, that is, `2^8 = 256`. -/
 abbrev Int8.size : Nat := 256
 
@@ -463,3 +475,114 @@ instance (a b : Int64) : Decidable (a < b) := Int64.decLt a b
 instance (a b : Int64) : Decidable (a ≤ b) := Int64.decLe a b
 instance : Max Int64 := maxOfLe
 instance : Min Int64 := minOfLe
+
+/-- The size of type `ISize`, that is, `2^System.Platform.numBits`. -/
+abbrev ISize.size : Nat := 2^System.Platform.numBits
+
+/--
+Obtain the `BitVec` that contains the 2's complement representation of the `ISize`.
+-/
+@[inline] def ISize.toBitVec (x : ISize) : BitVec System.Platform.numBits := x.toUSize.toBitVec
+
+@[extern "lean_isize_of_int"]
+def ISize.ofInt (i : @& Int) : ISize := ⟨⟨BitVec.ofInt System.Platform.numBits i⟩⟩
+@[extern "lean_isize_of_nat"]
+def ISize.ofNat (n : @& Nat) : ISize := ⟨⟨BitVec.ofNat System.Platform.numBits n⟩⟩
+abbrev Int.toISize := ISize.ofInt
+abbrev Nat.toISize := ISize.ofNat
+@[extern "lean_isize_to_int"]
+def ISize.toInt (i : ISize) : Int := i.toBitVec.toInt
+/--
+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
+@[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`.
+-/
+@[extern "lean_isize_to_int64"]
+def ISize.toInt64 (a : ISize) : Int64 := ⟨⟨a.toBitVec.signExtend 64⟩⟩
+/--
+Upcast `Int32` to `ISize`. This function is losless as `ISize` is either `Int32` or `Int64`.
+-/
+@[extern "lean_int32_to_isize"]
+def Int32.toISize (a : Int32) : ISize := ⟨⟨a.toBitVec.signExtend System.Platform.numBits⟩⟩
+@[extern "lean_int64_to_isize"]
+def Int64.toISize (a : Int64) : ISize := ⟨⟨a.toBitVec.signExtend System.Platform.numBits⟩⟩
+@[extern "lean_isize_neg"]
+def ISize.neg (i : ISize) : ISize := ⟨⟨-i.toBitVec⟩⟩
+
+instance : ToString ISize where
+  toString i := toString i.toInt
+
+instance : OfNat ISize n := ⟨ISize.ofNat n⟩
+instance : Neg ISize where
+  neg := ISize.neg
+
+@[extern "lean_isize_add"]
+def ISize.add (a b : ISize) : ISize := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
+@[extern "lean_isize_sub"]
+def ISize.sub (a b : ISize) : ISize := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
+@[extern "lean_isize_mul"]
+def ISize.mul (a b : ISize) : ISize := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
+@[extern "lean_isize_div"]
+def ISize.div (a b : ISize) : ISize := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
+@[extern "lean_isize_mod"]
+def ISize.mod (a b : ISize) : ISize := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
+@[extern "lean_isize_land"]
+def ISize.land (a b : ISize) : ISize := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
+@[extern "lean_isize_lor"]
+def ISize.lor (a b : ISize) : ISize := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
+@[extern "lean_isize_xor"]
+def ISize.xor (a b : ISize) : ISize := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
+@[extern "lean_isize_shift_left"]
+def ISize.shiftLeft (a b : ISize) : ISize := ⟨⟨a.toBitVec <<< (b.toBitVec.smod System.Platform.numBits)⟩⟩
+@[extern "lean_isize_shift_right"]
+def ISize.shiftRight (a b : ISize) : ISize := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod System.Platform.numBits)⟩⟩
+@[extern "lean_isize_complement"]
+def ISize.complement (a : ISize) : ISize := ⟨⟨~~~a.toBitVec⟩⟩
+
+@[extern "lean_isize_dec_eq"]
+def ISize.decEq (a b : ISize) : Decidable (a = b) :=
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ =>
+    if h : n = m then
+      isTrue <| h ▸ rfl
+    else
+      isFalse (fun h' => ISize.noConfusion h' (fun h' => absurd h' h))
+
+def ISize.lt (a b : ISize) : Prop := a.toBitVec.slt b.toBitVec
+def ISize.le (a b : ISize) : Prop := a.toBitVec.sle b.toBitVec
+
+instance : Inhabited ISize where
+  default := 0
+
+instance : Add ISize         := ⟨ISize.add⟩
+instance : Sub ISize         := ⟨ISize.sub⟩
+instance : Mul ISize         := ⟨ISize.mul⟩
+instance : Mod ISize         := ⟨ISize.mod⟩
+instance : Div ISize         := ⟨ISize.div⟩
+instance : LT ISize          := ⟨ISize.lt⟩
+instance : LE ISize          := ⟨ISize.le⟩
+instance : Complement ISize  := ⟨ISize.complement⟩
+instance : AndOp ISize       := ⟨ISize.land⟩
+instance : OrOp ISize        := ⟨ISize.lor⟩
+instance : Xor ISize         := ⟨ISize.xor⟩
+instance : ShiftLeft ISize   := ⟨ISize.shiftLeft⟩
+instance : ShiftRight ISize  := ⟨ISize.shiftRight⟩
+instance : DecidableEq ISize := ISize.decEq
+
+@[extern "lean_isize_dec_lt"]
+def ISize.decLt (a b : ISize) : Decidable (a < b) :=
+  inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
+
+@[extern "lean_isize_dec_le"]
+def ISize.decLe (a b : ISize) : Decidable (a ≤ b) :=
+  inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
+
+instance (a b : ISize) : Decidable (a < b) := ISize.decLt a b
+instance (a b : ISize) : Decidable (a ≤ b) := ISize.decLe a b
+instance : Max ISize := maxOfLe
+instance : Min ISize := minOfLe

src/include/lean/lean.h

@@ -2229,6 +2229,7 @@ static inline uint8_t lean_int32_dec_le(uint32_t a1, uint32_t a2) {
 static inline uint8_t lean_int32_to_int8(uint32_t a) { return (uint8_t)(int8_t)(int32_t)a; }
 static inline uint16_t lean_int32_to_int16(uint32_t a) { return (uint16_t)(int16_t)(int32_t)a; }
 static inline uint64_t lean_int32_to_int64(uint32_t a) { return (uint64_t)(int64_t)(int32_t)a; }
+static inline size_t lean_int32_to_isize(uint32_t a) { return (size_t)(ptrdiff_t)(int32_t)a; }
 
 /* Int64 */
 LEAN_EXPORT int64_t lean_int64_of_big_int(b_lean_obj_arg a);
@@ -2368,6 +2369,147 @@ static inline uint8_t lean_int64_dec_le(uint64_t a1, uint64_t a2) {
 static inline uint8_t lean_int64_to_int8(uint64_t a) { return (uint8_t)(int8_t)(int64_t)a; }
 static inline uint16_t lean_int64_to_int16(uint64_t a) { return (uint16_t)(int16_t)(int64_t)a; }
 static inline uint32_t lean_int64_to_int32(uint64_t a) { return (uint32_t)(int32_t)(int64_t)a; }
+static inline size_t lean_int64_to_isize(uint64_t a) { return (size_t)(ptrdiff_t)(int64_t)a; }
+
+/* ISize */
+LEAN_EXPORT ptrdiff_t lean_isize_of_big_int(b_lean_obj_arg a);
+static inline size_t lean_isize_of_int(b_lean_obj_arg a) {
+    ptrdiff_t res;
+
+    if (lean_is_scalar(a)) {
+        res = (ptrdiff_t)lean_scalar_to_int64(a);
+    } else {
+        res = lean_isize_of_big_int(a);
+    }
+
+    return (size_t)res;
+}
+
+static inline size_t lean_isize_of_nat(b_lean_obj_arg a) {
+    ptrdiff_t res;
+
+    if (lean_is_scalar(a)) {
+        res = (ptrdiff_t)lean_unbox(a);
+    } else {
+        res = lean_isize_of_big_int(a);
+    }
+
+    return (size_t)res;
+}
+
+static inline lean_obj_res lean_isize_to_int(size_t a) {
+    ptrdiff_t arg = (ptrdiff_t)a;
+    return lean_int64_to_int((int64_t)arg);
+}
+
+static inline size_t lean_isize_neg(size_t a) {
+    ptrdiff_t arg = (ptrdiff_t)a;
+
+    return (size_t)(-arg);
+}
+
+static inline size_t lean_isize_add(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(lhs + rhs);
+}
+
+static inline size_t lean_isize_sub(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(lhs - rhs);
+}
+
+static inline size_t lean_isize_mul(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(lhs * rhs);
+}
+
+static inline size_t lean_isize_div(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(rhs == 0 ? 0 : lhs / rhs);
+}
+
+static inline size_t lean_isize_mod(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(rhs == 0 ? lhs : lhs % rhs);
+}
+
+static inline size_t lean_isize_land(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(lhs & rhs);
+}
+
+static inline size_t lean_isize_lor(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(lhs | rhs);
+}
+
+static inline size_t lean_isize_xor(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(lhs ^ rhs);
+}
+
+static inline size_t lean_isize_shift_right(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t size = sizeof(ptrdiff_t) * 8;
+    ptrdiff_t rhs = (((ptrdiff_t)a2 % size) + size) % size; // this is smod
+
+    return (size_t)(lhs >> rhs);
+}
+
+static inline size_t lean_isize_shift_left(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t size = sizeof(ptrdiff_t) * 8;
+    ptrdiff_t rhs = (((ptrdiff_t)a2 % size) + size) % size; // this is smod
+
+    return (size_t)(lhs << rhs);
+}
+
+static inline size_t lean_isize_complement(size_t a) {
+    ptrdiff_t arg = (ptrdiff_t)a;
+
+    return (size_t)(~arg);
+}
+
+static inline uint8_t lean_isize_dec_eq(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return lhs == rhs;
+}
+
+static inline uint8_t lean_isize_dec_lt(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return lhs < rhs;
+}
+
+static inline uint8_t lean_isize_dec_le(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return lhs <= rhs;
+}
+
+/* ISize -> other */
+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; }
 
 /* Float */
 

src/runtime/int.h

@@ -29,5 +29,9 @@ static_assert(sizeof(int64) == 8,  "unexpected int64 size");  // NOLINT
 static_assert(sizeof(uint64) == 8, "unexpected uint64 size"); // NOLINT
                                                               //
 typedef size_t usize;
+typedef ptrdiff_t isize;
+static_assert(sizeof(usize) == sizeof(isize), "unexpected size difference usize/isize");   // NOLINT
+static_assert(sizeof(usize) == 4 || sizeof(usize) == 8, "usize is neither 32 nor 64 bit"); // NOLINT
+                                                                                           //
 
 }

src/runtime/object.cpp

@@ -1578,6 +1578,15 @@ extern "C" LEAN_EXPORT int64 lean_int64_of_big_int(b_obj_arg a) {
     return mpz_value(a).smod64();
 }
 
+extern "C" LEAN_EXPORT isize lean_isize_of_big_int(b_obj_arg a) {
+    if (sizeof(ptrdiff_t) == 8) {
+        return static_cast<isize>(mpz_value(a).smod64());
+    } else {
+        // We assert in int.h that the size of ptrdiff_t is 8 or 4.
+        return static_cast<isize>(mpz_value(a).smod32());
+    }
+}
+
 // =======================================
 // Float