diff --git a/src/runtime/lean.h b/src/runtime/lean.h index 6b37fd91ab..b1e657b0fa 100644 --- a/src/runtime/lean.h +++ b/src/runtime/lean.h @@ -1434,12 +1434,22 @@ static inline bool lean_int_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) { } } +lean_obj_res lean_big_int_to_nat(lean_obj_arg a); +static inline lean_obj_res lean_int_to_nat(lean_obj_arg a) { + assert(!lean_int_lt(a, lean_box(0))); + if (lean_is_scalar(a)) { + return a; + } else { + return lean_big_int_to_nat(a); + } +} + static inline lean_obj_res lean_nat_abs(b_lean_obj_arg i) { if (lean_int_lt(i, lean_box(0))) { - return lean_int_neg(i); + return lean_int_to_nat(lean_int_neg(i)); } else { lean_inc(i); - return i; + return lean_int_to_nat(i); } } diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index c88b83876c..1b0322ed3d 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -1232,6 +1232,13 @@ static object * mpz_to_int(mpz const & m) { return lean_box(static_cast(m.get_int())); } +extern "C" lean_obj_res lean_big_int_to_nat(lean_obj_arg a) { + lean_assert(!lean_is_scalar(a)); + mpz m = mpz_value(a); + lean_dec(a); + return mpz_to_nat(m); +} + extern "C" object * lean_cstr_to_int(char const * n) { return mpz_to_int(mpz(n)); } diff --git a/tests/lean/run/int_to_nat_bug.lean b/tests/lean/run/int_to_nat_bug.lean new file mode 100644 index 0000000000..b0068696fb --- /dev/null +++ b/tests/lean/run/int_to_nat_bug.lean @@ -0,0 +1 @@ +#eval (4294967295 : Int)