max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: lean_nat_abs

Browse source 
It must not assume a nonnegative big integer is a big nat.
This commit is contained in:
Leonardo de Moura 2019-12-14 08:07:32 -08:00
parent f183ea6fae
commit 54e5ca0c7b
3 changed files with 20 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/runtime/lean.h
View file

@ -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);
}
}

7
src/runtime/object.cpp
View file

@ -1232,6 +1232,13 @@ static object * mpz_to_int(mpz const & m) {
return lean_box(static_cast<unsigned>(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));
}

1
tests/lean/run/int_to_nat_bug.lean Normal file
View file

@ -0,0 +1 @@
#eval (4294967295 : Int)