From acdcbdb71e32bfc32a0e885c32d08b89996cd4fb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 17 May 2018 18:17:23 -0700 Subject: [PATCH] feat(library/init/lean/ir): add instructions for (big) integer arithmetic --- library/init/lean/ir/extract_cpp.lean | 13 +++++++++- library/init/lean/ir/format.lean | 13 ++++++---- library/init/lean/ir/ir.lean | 34 +++++++++++++++++++++++---- library/init/lean/ir/parser.lean | 11 +++++++++ library/init/lean/ir/reserved.lean | 12 +++++++--- library/init/lean/ir/type_check.lean | 12 +++++++++- src/runtime/lean_obj.h | 21 +++++++++++++++++ tests/ir/tst5.ir | 31 ++++++++++++++++++++++++ 8 files changed, 132 insertions(+), 15 deletions(-) create mode 100644 tests/ir/tst5.ir diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean index 3713ff945d..7fb3fc1e8b 100644 --- a/library/init/lean/ir/extract_cpp.lean +++ b/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" diff --git a/library/init/lean/ir/format.lean b/library/init/lean/ir/format.lean index 7d5dd36e06..b0021ebc99 100644 --- a/library/init/lean/ir/format.lean +++ b/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" diff --git a/library/init/lean/ir/ir.lean b/library/init/lean/ir/ir.lean index e385f74ba7..7cd30cbb09 100644 --- a/library/init/lean/ir/ir.lean +++ b/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` diff --git a/library/init/lean/ir/parser.lean b/library/init/lean/ir/parser.lean index f3f687a330..6adae3d2b0 100644 --- a/library/init/lean/ir/parser.lean +++ b/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) diff --git a/library/init/lean/ir/reserved.lean b/library/init/lean/ir/reserved.lean index ced742531d..64c92583a8 100644 --- a/library/init/lean/ir/reserved.lean +++ b/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", diff --git a/library/init/lean/ir/type_check.lean b/library/init/lean/ir/type_check.lean index 541128cb69..b27ae38da9 100644 --- a/library/init/lean/ir/type_check.lean +++ b/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 diff --git a/src/runtime/lean_obj.h b/src/runtime/lean_obj.h index 10d93e563c..30a6956ef5 100644 --- a/src/runtime/lean_obj.h +++ b/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) { diff --git a/tests/ir/tst5.ir b/tests/ir/tst5.ir new file mode 100644 index 0000000000..6d5b647a96 --- /dev/null +++ b/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;