feat(library/init/lean/ir): add instructions for (big) integer arithmetic

library/init/lean/ir/extract_cpp.lean

@@ -194,6 +194,11 @@ match op with
 | assign_binop.mul  := emit_arith t x y z "*" "lean::nat_mul"
 | assign_binop.div  := emit_arith t x y z "/" "lean::nat_div"
 | assign_binop.mod  := emit_arith t x y z "%" "lean::nat_mod"
+| assign_binop.iadd := emit_big_binop x y z "lean::int_add"
+| assign_binop.isub := emit_big_binop x y z "lean::int_sub"
+| assign_binop.imul := emit_big_binop x y z "lean::int_mul"
+| assign_binop.idiv := emit_big_binop x y z "lean::int_div"
+| assign_binop.imod := emit_big_binop x y z "lean::int_mod"
 | assign_binop.shl  := emit_infix x y z "<<"
 | assign_binop.shr  := emit_infix x y z ">>"
 | assign_binop.and  := emit_logical_arith t x y z "&&" "&" "lean::nat_land"
@@ -203,6 +208,10 @@ match op with
 | assign_binop.lt   := emit_arith t x y z "<"  "lean::nat_lt"
 | assign_binop.eq   := emit_arith t x y z "==" "lean::nat_eq"
 | assign_binop.ne   := emit_arith t x y z "!=" "lean::nat_ne"
+| assign_binop.ile  := emit_big_binop x y z "lean::int_le"
+| assign_binop.ilt  := emit_big_binop x y z "lean::int_lt"
+| assign_binop.ieq  := emit_big_binop x y z "lean::int_eq"
+| assign_binop.ine  := emit_big_binop x y z "lean::int_ne"
 | assign_binop.array_read :=
   (match t with
    | type.object := emit_var x >> emit " = lean::array_obj" >> paren (emit_var y <+> emit_var z)
@@ -220,7 +229,9 @@ emit_var x >> emit " = " >> emit op >> paren(emit_var y)
 
 def assign_unop2cpp (t : type) : assign_unop → string
 | assign_unop.not          := if t = type.bool then "!" else "~"
-| assign_unop.neg          := if t = type.object then "lean::neg" else "-"
+| assign_unop.neg          := "-"
+| assign_unop.ineg         := "lean::int_neg"
+| assign_unop.nat2int      := "lean::nat2int"
 | assign_unop.is_scalar    := "lean::is_scalar"
 | assign_unop.is_shared    := "lean::is_shared"
 | assign_unop.is_null      := "lean::is_null"

library/init/lean/ir/format.lean

@@ -49,7 +49,8 @@ instance type.has_to_format : has_to_format type := ⟨type.to_format⟩
 instance type.has_to_string : has_to_string type := ⟨pretty ∘ to_fmt⟩
 
 def assign_unop.to_format : assign_unop → format
-| assign_unop.not           := "not"        | assign_unop.neg          := "neg"
+| assign_unop.not           := "not"        | assign_unop.neg          := "neg"       | assign_unop.ineg    := "ineg"
+| assign_unop.nat2int       := "nat2int"
 | assign_unop.is_scalar     := "is_scalar"  | assign_unop.is_shared    := "is_shared" | assign_unop.is_null := "is_null"
 | assign_unop.box           := "box"        | assign_unop.unbox        := "unbox"
 | assign_unop.cast          := "cast"
@@ -62,10 +63,12 @@ instance assign_unop.has_to_format : has_to_format assign_unop := ⟨assign_unop
 instance assign_unop.has_to_string : has_to_string assign_unop := ⟨pretty ∘ to_fmt⟩
 
 def assign_binop.to_format : assign_binop → format
-| assign_binop.add  := "add"  | assign_binop.sub  := "sub" | assign_binop.mul  := "mul"  | assign_binop.div  := "div"
-| assign_binop.mod  := "mod"  | assign_binop.shl  := "shl" | assign_binop.shr  := "shr"
-| assign_binop.and  := "and"  | assign_binop.or   := "or"  | assign_binop.xor  := "xor"  | assign_binop.le   := "le"
-| assign_binop.lt   := "lt"   | assign_binop.eq   := "eq"  | assign_binop.ne   := "ne"
+| assign_binop.add  := "add"  | assign_binop.sub  := "sub"  | assign_binop.mul  := "mul"   | assign_binop.div   := "div"  | assign_binop.mod  := "mod"
+| assign_binop.iadd := "iadd" | assign_binop.isub := "isub" | assign_binop.imul := "imul"  | assign_binop.idiv  := "idiv" | assign_binop.imod := "imod"
+| assign_binop.shl  := "shl"  | assign_binop.shr  := "shr"
+| assign_binop.and  := "and"  | assign_binop.or   := "or"   | assign_binop.xor  := "xor"
+| assign_binop.le   := "le"   | assign_binop.lt   := "lt"   | assign_binop.eq   := "eq"  | assign_binop.ne   := "ne"
+| assign_binop.ile  := "ile"  | assign_binop.ilt  := "ilt"  | assign_binop.ieq  := "ieq" | assign_binop.ine  := "ine"
 | assign_binop.array_read    := "array_read"
 | assign_binop.array_push    := "array_push"
 | assign_binop.string_push   := "string_push"

library/init/lean/ir/ir.lean

@@ -31,8 +31,11 @@ uint64 | usize | int16 | int32 | int64 | float | double | object
 - `x : t := not y`, if `t = bool`, then it is the logical negation.
 Otherwise, it is bitwise negation if `t` is `uint32/uint64/usize`.
 
-- `x : t := neg y`, arithmetical `-`. `t` is `int16/int32/int64/float/double/object`.
-If `t = object`, the instruction is unspecified if `t` is not a big number nor a tagged pointer.
+- `x : t := neg y`, arithmetical `-`. `t` is `int16/int32/int64/float/double`.
+
+- `x : object := ineg y`, integer `-`.
+
+- `x : object := nat2int y`, convert a natural (big) number into an integer (big) number.
 
 - `x : bool := is_scalar y`, set `x` to `tt` iff `y : object` is a tagged
 pointer.
@@ -76,7 +79,7 @@ The behavior is unspecified if `y` is not a string.
 - `x : uint32 := tag y` return the tag of the (constructor) object `y` OR tagged pointer.
 -/
 inductive assign_unop
-| not | neg | is_scalar | is_shared | is_null | cast | box | unbox
+| not | neg | ineg | nat2int | is_scalar | is_shared | is_null | cast | box | unbox
 | array_copy | sarray_copy | array_size | sarray_size | string_len
 | succ | tag | tag_ref
 
@@ -94,6 +97,16 @@ if the result does not fit in a tagged pointer.
 
 - `x : t := mod y z`: modulo. Remark: `t ≠ bool`, `t ≠ float` and `t ≠ double`. See `add` for big number case.
 
+- `x : object := iadd y z`: (big) integer addition.
+
+- `x : object := isub y z`: (big) integer subtraction.
+
+- `x : object := imul y z`: (big) integer multiplication.
+
+- `x : object := idiv y z`: (big) integer division.
+
+- `x : object := imod y z`: (big) integer modulo.
+
 - `x : t := shl y z`: bit shift left. Remark: `t ≠ bool`, `t ≠ float`, `t ≠ double` and `t ≠ object`.
 
 - `x : t := shr y z`: bit shift right. Remark: `t ≠ bool`, `t ≠ float`, `t ≠ double` and `t ≠ object`.
@@ -118,6 +131,14 @@ If `y` and `z` are `object`, then they must be big numbers.
 
 - `x : bool := ne y z`: disequality test. If `y` and `z` are `object`, then they must be big numbers.
 
+- `x : bool := ile y z`: (big) integer less than or equal to. `y` and `z` have type `object`.
+
+- `x : bool := ilt y z`: (big) integer less than. `y` and `z` have type `object`.
+
+- `x : bool := ieq y z`: (big) integer equality. `y` and `z` have type `object`.
+
+- `x : bool := ine y z`: (big) integer disequality. `y` and `z` have type `object`.
+
 - `x : t := array_read a i`: Read position `i` of the array `a`. `a` must be an (array) `object`.
 If `a` is a scalar array, then `t ≠ object`. If `a` is an (non-scalar) array, then `t = object`.
 
@@ -138,8 +159,11 @@ and `s₁` is deleted.
 Remark: in the future we may add instructions for performing updates destructively on big numbers. Example:
 `add_acc x y` would be `x += y`, and require `RC(x) = 1`. -/
 inductive assign_binop
-| add | sub | mul | div | mod | shl | shr | and | or | xor
-| le  | lt  | eq  | ne
+| add  | sub  | mul  | div  | mod
+| iadd | isub | imul | idiv | imod
+| shl  | shr  | and  | or   | xor
+| le   | lt   | eq   | ne
+| ile  | ilt  | ieq  | ine
 | array_read | array_push | string_push | string_append
 
 /-- Operators for instructions of the form `op x`

library/init/lean/ir/parser.lean

@@ -35,6 +35,8 @@ def parse_type : parser type :=
 def parse_assign_unop : parser assign_unop :=
     (keyword "not" >> return assign_unop.not)
 <|> (keyword "neg" >> return assign_unop.neg)
+<|> (keyword "ineg" >> return assign_unop.ineg)
+<|> (keyword "nat2int" >> return assign_unop.nat2int)
 <|> (keyword "is_scalar" >> return assign_unop.is_scalar)
 <|> (keyword "is_shared" >> return assign_unop.is_shared)
 <|> (keyword "is_null" >> return assign_unop.is_null)
@@ -56,6 +58,11 @@ def parse_assign_binop : parser assign_binop :=
 <|> (keyword "mul" >> return assign_binop.mul)
 <|> (keyword "div" >> return assign_binop.div)
 <|> (keyword "mod" >> return assign_binop.mod)
+<|> (keyword "iadd" >> return assign_binop.iadd)
+<|> (keyword "isub" >> return assign_binop.isub)
+<|> (keyword "imul" >> return assign_binop.imul)
+<|> (keyword "idiv" >> return assign_binop.idiv)
+<|> (keyword "imod" >> return assign_binop.imod)
 <|> (keyword "shl" >> return assign_binop.shl)
 <|> (keyword "shr" >> return assign_binop.shr)
 <|> (keyword "and" >> return assign_binop.and)
@@ -65,6 +72,10 @@ def parse_assign_binop : parser assign_binop :=
 <|> (keyword "lt" >> return assign_binop.lt)
 <|> (keyword "eq" >> return assign_binop.eq)
 <|> (keyword "ne" >> return assign_binop.ne)
+<|> (keyword "ile" >> return assign_binop.ile)
+<|> (keyword "ilt" >> return assign_binop.ilt)
+<|> (keyword "ieq" >> return assign_binop.ieq)
+<|> (keyword "ine" >> return assign_binop.ine)
 <|> (keyword "array_read" >> return assign_binop.array_read)
 <|> (keyword "array_push" >> return assign_binop.array_push)
 <|> (keyword "string_push" >> return assign_binop.string_push)

library/init/lean/ir/reserved.lean

@@ -10,12 +10,18 @@ namespace lean
 namespace ir
 
 def reserved := [ "bool", "byte", "uint16", "uint32", "uint64", "usize",
- "int16", "int32", "int64", "float", "double", "object", "not", "neg",
+ "int16", "int32", "int64", "float", "double", "object",
+ "not", "neg", "ineg", "nat2int",
  "is_scalar", "is_shared", "is_null", "unbox", "box", "cast",
  "array_copy", "sarray_copy", "array_size", "sarray_size", "string_len",
  "succ", "tag", "tag_ref",
- "add", "sub", "mul", "div", "mod", "shl", "shr", "and",
- "or", "xor", "le", "lt", "eq", "ne", "array_read", "array_push",
+ "add", "sub", "mul", "div", "mod",
+ "iadd", "isub", "imul", "idiv", "imod",
+ "shl", "shr", "and",
+ "or", "xor",
+ "le", "lt", "eq", "ne",
+ "ile", "ilt", "ieq", "ine",
+ "array_read", "array_push",
  "string_push", "string_append", "inc_ref", "dec_ref", "dec_sref",
  "inc", "dec", "free", "dealloc", "array_pop", "sarray_pop",
  "call", "cnstr", "set", "get", "sset", "sget", "closure", "apply",

library/init/lean/ir/type_check.lean

@@ -13,7 +13,6 @@ def is_signed_arith_ty (ty : type) : bool :=
 match ty with
 | type.int16  := tt | type.int32 := tt  | type.int64 := tt
 | type.float  := tt | type.double := tt
-| type.object := tt -- big numbers
 | _ := ff
 
 /-- Return `tt` iff `ty` is a type that may occur in arithmetical operations. -/
@@ -45,6 +44,8 @@ def valid_assign_unop_types (op : assign_unop) (r : type) (t : type) : bool :=
 match op with
 | assign_unop.not           := t = r && is_bitwise_ty t
 | assign_unop.neg           := t = r && is_signed_arith_ty t
+| assign_unop.ineg          := t = r && t = type.object
+| assign_unop.nat2int       := t = r && t = type.object
 | assign_unop.is_scalar     := t = type.object && r = type.bool
 | assign_unop.is_shared     := t = type.object && r = type.bool
 | assign_unop.is_null       := t = type.object && r = type.bool
@@ -68,6 +69,11 @@ match op with
 | assign_binop.mul  := r = t₁ && r = t₂ && is_arith_ty r
 | assign_binop.div  := r = t₁ && r = t₂ && is_arith_ty r
 | assign_binop.mod  := r = t₁ && r = t₂ && is_nonfloat_arith_ty r
+| assign_binop.iadd := r = t₁ && r = t₂ && r = type.object
+| assign_binop.isub := r = t₁ && r = t₂ && r = type.object
+| assign_binop.imul := r = t₁ && r = t₂ && r = type.object
+| assign_binop.idiv := r = t₁ && r = t₂ && r = type.object
+| assign_binop.imod := r = t₁ && r = t₂ && r = type.object
 | assign_binop.shl  := r = t₁ && r = t₂ && is_bitshift_ty r
 | assign_binop.shr  := r = t₁ && r = t₂ && is_bitshift_ty r
 | assign_binop.and  := r = t₁ && r = t₂ && is_bitwise_ty r
@@ -77,6 +83,10 @@ match op with
 | assign_binop.lt   := r = type.bool && t₁ = t₂ && is_arith_ty t₁
 | assign_binop.eq   := r = type.bool && t₁ = t₂
 | assign_binop.ne   := r = type.bool && t₁ = t₂
+| assign_binop.ile  := r = type.bool && t₁ = t₂ && t₁ = type.object
+| assign_binop.ilt  := r = type.bool && t₁ = t₂ && t₁ = type.object
+| assign_binop.ieq  := r = type.bool && t₁ = t₂ && t₁ = type.object
+| assign_binop.ine  := r = type.bool && t₁ = t₂ && t₁ = type.object
 | assign_binop.array_read    := t₁ = type.object && t₂ = type.usize
 | assign_binop.array_push    := r = type.object && t₁ = type.object
 | assign_binop.string_push   := r = type.object && t₁ = type.object && t₂ = type.uint32

src/runtime/lean_obj.h

@@ -557,6 +557,27 @@ inline int int2int(lean_obj * a) {
     }
 }
 
+inline lean_obj * nat2int(lean_obj * a) {
+    if (is_scalar(a)) {
+        unsigned v = unbox(a);
+        if (v <= LEAN_MAX_SMALL_INT) {
+            return a;
+        } else {
+            return alloc_mpz(mpz(v));
+        }
+    } else {
+        return a;
+    }
+}
+
+inline lean_obj * int_neg(lean_obj * a) {
+    if (LEAN_LIKELY(is_scalar(a))) {
+        return mk_int_obj(-int2int64(a));
+    } else {
+        return mk_int_obj(neg(mpz_value(a)));
+    }
+}
+
 lean_obj * int_big_add(lean_obj * a1, lean_obj * a2);
 
 inline lean_obj * int_add(lean_obj * a1, lean_obj * a2) {

tests/ir/tst5.ir

@@ -0,0 +1,31 @@
+[lean_dbg_print_num] external print_num (s : object)
+[lean_dbg_print_str] external print_str (s : object)
+
+def print_bool (b : bool) :=
+entry:
+  case b [false_lbl, true_lbl];
+true_lbl:
+  s1 : object := "true";
+  call print_str s1;
+  ret;
+false_lbl:
+  s2 : object := "false";
+  call print_str s2;
+  ret;
+
+def main : int32 :=
+entry:
+  n : object := 4294967295;
+  b : bool   := is_scalar n;
+  call print_num n;
+  call print_bool b;
+  i : object := nat2int n;
+  b : bool   := is_scalar i;
+  call print_num i;
+  call print_bool b;
+  i : object := ineg i;
+  call print_num i;
+  i : object := iadd i i;
+  call print_num i;
+  r : int32  := 0;
+  ret r;