feat: SIntX as native ABI types

doc/dev/ffi.md

@@ -34,7 +34,8 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
 
 ### Translating Types from Lean to C
 
-* The integer types `UInt8`, ..., `UInt64`, `USize` are represented by the C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively
+* The integer types `UInt8`, ..., `UInt64`, `USize`, `Int8`, ..., `Int64`, `ISize` are represented by
+  the C types `uint8_t`, ..., `uint64_t`, `size_t`, `int8_t`, ..., `int64_t`, `ptrdiff_t` respectively
 * `Char` is represented by `uint32_t`
 * `Float` is represented by `double`
 * An *enum* inductive type of at least 2 and at most 2^32 constructors, each of which with no parameters, is represented by the first type of `uint8_t`, `uint16_t`, `uint32_t` that is sufficient to represent all constructor indices.
@@ -49,7 +50,6 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   is represented by the representation of that parameter's type.
 
   For example, `{ x : α // p }`, the `Subtype` structure of a value of type `α` and an irrelevant proof, is represented by the representation of `α`.
-  Similarly, the signed integer types `Int8`, ..., `Int64`, `ISize` are also represented by the unsigned C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively, because they have a trivial structure.
 * `Nat` and `Int` are represented by `lean_object *`.
   Their runtime values is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number or integer (`lean_box`/`lean_unbox`).
 * A universe `Sort u`, type constructor `... → Sort u`, `Void α` or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`

src/Init/Data/SInt/Basic.lean

@@ -30,6 +30,9 @@ structure Int8 where
   -/
   toUInt8 : UInt8
 
+attribute [extern "lean_int8_of_uint8_mk"] Int8.ofUInt8
+attribute [extern "lean_int8_to_uint8"] Int8.toUInt8
+
 /--
 Signed 16-bit integers.
 
@@ -43,6 +46,9 @@ structure Int16 where
   -/
   toUInt16 : UInt16
 
+attribute [extern "lean_int16_of_uint16_mk"] Int16.ofUInt16
+attribute [extern "lean_int16_to_uint16"] Int16.toUInt16
+
 /--
 Signed 32-bit integers.
 
@@ -56,6 +62,9 @@ structure Int32 where
   -/
   toUInt32 : UInt32
 
+attribute [extern "lean_int32_of_uint32_mk"] Int32.ofUInt32
+attribute [extern "lean_int32_to_uint32"] Int32.toUInt32
+
 /--
 Signed 64-bit integers.
 
@@ -69,6 +78,9 @@ structure Int64 where
   -/
   toUInt64 : UInt64
 
+attribute [extern "lean_int64_of_uint64_mk"] Int64.ofUInt64
+attribute [extern "lean_int64_to_uint64"] Int64.toUInt64
+
 /--
 Signed integers that are the size of a word on the platform's architecture.
 
@@ -83,6 +95,9 @@ structure ISize where
   -/
   toUSize : USize
 
+attribute [extern "lean_isize_of_usize_mk"] ISize.ofUSize
+attribute [extern "lean_isize_to_usize"] ISize.toUSize
+
 /-- The number of distinct values representable by `Int8`, that is, `2^8 = 256`. -/
 abbrev Int8.size : Nat := 256
 

src/Lean/Compiler/IR/Basic.lean

@@ -82,6 +82,7 @@ inductive IRType where
   -- TODO: Move this upwards after a stage0 update.
   | tagged
   | void
+  | int8 | int16 | int32 | int64 | isize
   deriving Inhabited, BEq, Repr
 
 namespace IRType
@@ -94,6 +95,11 @@ def isScalar : IRType → Bool
   | uint32   => true
   | uint64   => true
   | usize    => true
+  | int8    => true
+  | int16   => true
+  | int32   => true
+  | int64   => true
+  | isize    => true
   | _        => false
 
 def isObj : IRType → Bool
@@ -124,6 +130,9 @@ def boxed : IRType → IRType
   | void | tagged | uint8 | uint16 => tagged
   | _ => tobject
 
+def ptrSizedTypeForSign (signed : Bool) : IRType :=
+  if signed then .isize else .usize
+
 end IRType
 
 /-- Arguments to applications, constructors, etc.
@@ -185,7 +194,7 @@ inductive Expr where
   We also use `proj` for extracting fields from `struct` return values, and casting `union` return values. -/
   |  proj (i : Nat) (x : VarId)
   /-- Extract the `Usize` value at Position `sizeof(void*)*i` from `x`. -/
-  | uproj (i : Nat) (x : VarId)
+  | uproj (i : Nat) (signed : Bool) (x : VarId)
   /-- Extract the scalar value at Position `sizeof(void*)*n + offset` from `x`. -/
   | sproj (n : Nat) (offset : Nat) (x : VarId)
   /-- Full application. -/
@@ -226,7 +235,7 @@ inductive FnBody where
   | set (x : VarId) (i : Nat) (y : Arg) (b : FnBody)
   | setTag (x : VarId) (cidx : Nat) (b : FnBody)
   /-- Store `y : Usize` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. -/
-  | uset (x : VarId) (i : Nat) (y : VarId) (b : FnBody)
+  | uset (x : VarId) (i : Nat) (y : VarId) (signed : Bool) (b : FnBody)
   /-- Store `y : ty` at Position `sizeof(void*)*i + offset` in `x`. `x` must be a Constructor object and `RC(x)` must be 1.
   `ty` must not be `object`, `tobject`, `erased` nor `Usize`. -/
   | sset (x : VarId) (i : Nat) (offset : Nat) (y : VarId) (ty : IRType) (b : FnBody)
@@ -261,7 +270,7 @@ def FnBody.body : FnBody → FnBody
   | FnBody.vdecl _ _ _ b    => b
   | FnBody.jdecl _ _ _ b    => b
   | FnBody.set _ _ _ b      => b
-  | FnBody.uset _ _ _ b     => b
+  | FnBody.uset _ _ _ _ b   => b
   | FnBody.sset _ _ _ _ _ b => b
   | FnBody.setTag _ _ b     => b
   | FnBody.inc _ _ _ _ b    => b
@@ -273,7 +282,7 @@ def FnBody.setBody : FnBody → FnBody → FnBody
   | FnBody.vdecl x t v _,    b => FnBody.vdecl x t v b
   | FnBody.jdecl j xs v _,   b => FnBody.jdecl j xs v b
   | FnBody.set x i y _,      b => FnBody.set x i y b
-  | FnBody.uset x i y _,     b => FnBody.uset x i y b
+  | FnBody.uset x i y s _,   b => FnBody.uset x i y s b
   | FnBody.sset x i o y t _, b => FnBody.sset x i o y t b
   | FnBody.setTag x i _,     b => FnBody.setTag x i b
   | FnBody.inc x n c p _,    b => FnBody.inc x n c p b
@@ -484,7 +493,7 @@ def Expr.alphaEqv (ρ : IndexRenaming) : Expr → Expr → Bool
   | Expr.reset n₁ x₁,        Expr.reset n₂ x₂        => n₁ == n₂ && aeqv ρ x₁ x₂
   | Expr.reuse x₁ i₁ u₁ ys₁, Expr.reuse x₂ i₂ u₂ ys₂ => aeqv ρ x₁ x₂ && i₁ == i₂ && u₁ == u₂ && aeqv ρ ys₁ ys₂
   | Expr.proj i₁ x₁,         Expr.proj i₂ x₂         => i₁ == i₂ && aeqv ρ x₁ x₂
-  | Expr.uproj i₁ x₁,        Expr.uproj i₂ x₂        => i₁ == i₂ && aeqv ρ x₁ x₂
+  | Expr.uproj i₁ s₁ x₁,     Expr.uproj i₂ s₂ x₂     => i₁ == i₂ && s₁ == s₂ && aeqv ρ x₁ x₂
   | Expr.sproj n₁ o₁ x₁,     Expr.sproj n₂ o₂ x₂     => n₁ == n₂ && o₁ == o₂ && aeqv ρ x₁ x₂
   | Expr.fap c₁ ys₁,         Expr.fap c₂ ys₂         => c₁ == c₂ && aeqv ρ ys₁ ys₂
   | Expr.pap c₁ ys₁,         Expr.pap c₂ ys₂         => c₁ == c₂ && aeqv ρ ys₁ ys₂
@@ -521,7 +530,7 @@ partial def FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool
     | some ρ' => alphaEqv ρ' v₁ v₂ && alphaEqv (addVarRename ρ j₁.idx j₂.idx) b₁ b₂
     | none    => false
   | ρ, FnBody.set x₁ i₁ y₁ b₁,        FnBody.set x₂ i₂ y₂ b₂        => aeqv ρ x₁ x₂ && i₁ == i₂ && aeqv ρ y₁ y₂ && alphaEqv ρ b₁ b₂
-  | ρ, FnBody.uset x₁ i₁ y₁ b₁,       FnBody.uset x₂ i₂ y₂ b₂       => aeqv ρ x₁ x₂ && i₁ == i₂ && aeqv ρ y₁ y₂ && alphaEqv ρ b₁ b₂
+  | ρ, FnBody.uset x₁ i₁ y₁ s₁ b₁,    FnBody.uset x₂ i₂ y₂ s₂ b₂    => aeqv ρ x₁ x₂ && i₁ == i₂ && aeqv ρ y₁ y₂ && s₁ == s₂ && alphaEqv ρ b₁ b₂
   | ρ, FnBody.sset x₁ i₁ o₁ y₁ t₁ b₁, FnBody.sset x₂ i₂ o₂ y₂ t₂ b₂ =>
     aeqv ρ x₁ x₂ && i₁ = i₂ && o₁ = o₂ && aeqv ρ y₁ y₂ && t₁ == t₂ && alphaEqv ρ b₁ b₂
   | ρ, FnBody.setTag x₁ i₁ b₁,        FnBody.setTag x₂ i₂ b₂        => aeqv ρ x₁ x₂ && i₁ == i₂ && alphaEqv ρ b₁ b₂
@@ -556,6 +565,9 @@ def getUnboxOpName (t : IRType) : String :=
   | IRType.usize    => "lean_unbox_usize"
   | IRType.uint32   => "lean_unbox_uint32"
   | IRType.uint64   => "lean_unbox_uint64"
+  | IRType.isize    => "lean_unbox_isize"
+  | IRType.int32   => "lean_unbox_int32"
+  | IRType.int64   => "lean_unbox_int64"
   | IRType.float    => "lean_unbox_float"
   | IRType.float32  => "lean_unbox_float32"
   | _               => "lean_unbox"

src/Lean/Compiler/IR/Boxing.lean

@@ -281,10 +281,10 @@ partial def visitFnBody : FnBody → M FnBody
     let v ← withParams xs (visitFnBody v)
     let b ← withJDecl j xs v (visitFnBody b)
     return .jdecl j xs v b
-  | .uset x i y b      => do
+  | .uset x i y s b      => do
     let b ← visitFnBody b
-    castVarIfNeeded y IRType.usize fun y =>
-      return .uset x i y b
+    castVarIfNeeded y (IRType.ptrSizedTypeForSign s) fun y =>
+      return .uset x i y s b
   | .sset x i o y ty b => do
     let b ← visitFnBody b
     castVarIfNeeded y ty fun y =>

src/Lean/Compiler/IR/Checker.lean

@@ -168,9 +168,9 @@ def checkExpr (ty : IRType) (e : Expr) : M Unit := do
       else
         throwCheckerError "invalid proj index"
     | _ => throwCheckerError s!"unexpected IR type '{xType}'"
-  | .uproj _ x =>
+  | .uproj _ s x =>
     checkObjVar x
-    checkType ty (· == .usize)
+    checkType ty (· == IRType.ptrSizedTypeForSign s)
   | .sproj _ _ x =>
     checkObjVar x
     checkScalarType ty
@@ -202,7 +202,7 @@ partial def checkFnBody (fnBody : FnBody) : M Unit := do
     checkVar x
     checkArg y
     checkFnBody b
-  | .uset x _ y b =>
+  | .uset x _ y _ b =>
     checkVar x
     checkVar y
     checkFnBody b

src/Lean/Compiler/IR/EmitC.lean

@@ -61,6 +61,11 @@ def toCType : IRType → String
   | IRType.uint32     => "uint32_t"
   | IRType.uint64     => "uint64_t"
   | IRType.usize      => "size_t"
+  | IRType.int8      => "int8_t"
+  | IRType.int16     => "int16_t"
+  | IRType.int32     => "int32_t"
+  | IRType.int64     => "int64_t"
+  | IRType.isize      => "ptrdiff_t"
   | IRType.object     => "lean_object*"
   | IRType.tagged     => "lean_object*"
   | IRType.tobject    => "lean_object*"
@@ -314,8 +319,13 @@ def emitOffset (n : Nat) (offset : Nat) : M Unit := do
   else
     emit offset
 
-def emitUSet (x : VarId) (n : Nat) (y : VarId) : M Unit := do
-  emit "lean_ctor_set_usize("; emit x; emit ", "; emit n; emit ", "; emit y; emitLn ");"
+def emitUSet (x : VarId) (n : Nat) (s : Bool) (y : VarId) : M Unit := do
+  if s then
+    emit "lean_ctor_set_isize(";
+  else
+    emit "lean_ctor_set_usize(";
+
+  emit x; emit ", "; emit n; emit ", "; emit y; emitLn ");"
 
 def emitSSet (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M Unit := do
   match t with
@@ -325,6 +335,10 @@ def emitSSet (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M U
   | IRType.uint16  => emit "lean_ctor_set_uint16"
   | IRType.uint32  => emit "lean_ctor_set_uint32"
   | IRType.uint64  => emit "lean_ctor_set_uint64"
+  | IRType.int8    => emit "lean_ctor_set_int8"
+  | IRType.int16   => emit "lean_ctor_set_int16"
+  | IRType.int32   => emit "lean_ctor_set_int32"
+  | IRType.int64   => emit "lean_ctor_set_int64"
   | _              => throw "invalid instruction";
   emit "("; emit x; emit ", "; emitOffset n offset; emit ", "; emit y; emitLn ");"
 
@@ -389,8 +403,13 @@ def emitReuse (z : VarId) (x : VarId) (c : CtorInfo) (updtHeader : Bool) (ys : A
 def emitProj (z : VarId) (i : Nat) (x : VarId) : M Unit := do
   emitLhs z; emit "lean_ctor_get("; emit x; emit ", "; emit i; emitLn ");"
 
-def emitUProj (z : VarId) (i : Nat) (x : VarId) : M Unit := do
-  emitLhs z; emit "lean_ctor_get_usize("; emit x; emit ", "; emit i; emitLn ");"
+def emitUProj (z : VarId) (i : Nat) (s : Bool) (x : VarId) : M Unit := do
+  emitLhs z;
+  if s then
+    emit "lean_ctor_get_isize("
+  else
+    emit "lean_ctor_get_usize("
+  emit x; emit ", "; emit i; emitLn ");"
 
 def emitSProj (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M Unit := do
   emitLhs z;
@@ -401,6 +420,10 @@ def emitSProj (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M Unit :=
   | IRType.uint16   => emit "lean_ctor_get_uint16"
   | IRType.uint32   => emit "lean_ctor_get_uint32"
   | IRType.uint64   => emit "lean_ctor_get_uint64"
+  | IRType.int8     => emit "lean_ctor_get_int8"
+  | IRType.int16    => emit "lean_ctor_get_int16"
+  | IRType.int32    => emit "lean_ctor_get_int32"
+  | IRType.int64    => emit "lean_ctor_get_int64"
   | _               => throw "invalid instruction"
   emit "("; emit x; emit ", "; emitOffset n offset; emitLn ");"
 
@@ -461,6 +484,9 @@ def emitBoxFn (xType : IRType) : M Unit :=
   | IRType.usize   => emit "lean_box_usize"
   | IRType.uint32  => emit "lean_box_uint32"
   | IRType.uint64  => emit "lean_box_uint64"
+  | IRType.isize   => emit "lean_box_isize"
+  | IRType.int32   => emit "lean_box_int32"
+  | IRType.int64   => emit "lean_box_int64"
   | IRType.float   => emit "lean_box_float"
   | IRType.float32 => emit "lean_box_float32"
   | _              => emit "lean_box"
@@ -529,7 +555,7 @@ def emitVDecl (z : VarId) (t : IRType) (v : Expr) : M Unit :=
   | Expr.reset n x      => emitReset z n x
   | Expr.reuse x c u ys => emitReuse z x c u ys
   | Expr.proj i x       => emitProj z i x
-  | Expr.uproj i x      => emitUProj z i x
+  | Expr.uproj i s x    => emitUProj z i s x
   | Expr.sproj n o x    => emitSProj z t n o x
   | Expr.fap c ys       => emitFullApp z c ys
   | Expr.pap c ys       => emitPartialApp z c ys
@@ -639,7 +665,7 @@ partial def emitBlock (b : FnBody) : M Unit := do
   | FnBody.del x b             => emitDel x; emitBlock b
   | FnBody.setTag x i b        => emitSetTag x i; emitBlock b
   | FnBody.set x i y b         => emitSet x i y; emitBlock b
-  | FnBody.uset x i y b        => emitUSet x i y; emitBlock b
+  | FnBody.uset x i y s b      => emitUSet x i s y; emitBlock b
   | FnBody.sset x i o y t b    => emitSSet x i o y t; emitBlock b
   | FnBody.ret x               => emit "return "; emitArg x; emitLn ";"
   | FnBody.case _ x xType alts => emitCase x xType alts