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

fix: assertion violation

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-31 08:24:51 -08:00
parent 2f74415eaf
commit 3d0bfcd36a
3 changed files with 17 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/runtime/object.cpp
View file

@ -1139,15 +1139,15 @@ extern "C" object * lean_nat_big_sub(object * a1, object * a2) {
extern "C" object * lean_nat_big_mul(object * a1, object * a2) {
lean_assert(!lean_is_scalar(a1) || !lean_is_scalar(a2));
if (lean_is_scalar(a1))
return mpz_to_nat_core(mpz::of_size_t(lean_unbox(a1)) * mpz_value(a2));
return mpz_to_nat(mpz::of_size_t(lean_unbox(a1)) * mpz_value(a2));
else if (lean_is_scalar(a2))
return mpz_to_nat_core(mpz_value(a1) * mpz::of_size_t(lean_unbox(a2)));
return mpz_to_nat(mpz_value(a1) * mpz::of_size_t(lean_unbox(a2)));
else
return mpz_to_nat_core(mpz_value(a1) * mpz_value(a2));
}
extern "C" object * lean_nat_overflow_mul(size_t a1, size_t a2) {
return mpz_to_nat_core(mpz::of_size_t(a1) * mpz::of_size_t(a2));
return mpz_to_nat(mpz::of_size_t(a1) * mpz::of_size_t(a2));
}
extern "C" object * lean_nat_big_div(object * a1, object * a2) {

6
stage0/src/runtime/object.cpp
View file

@ -1139,15 +1139,15 @@ extern "C" object * lean_nat_big_sub(object * a1, object * a2) {
extern "C" object * lean_nat_big_mul(object * a1, object * a2) {
lean_assert(!lean_is_scalar(a1) || !lean_is_scalar(a2));
if (lean_is_scalar(a1))
return mpz_to_nat_core(mpz::of_size_t(lean_unbox(a1)) * mpz_value(a2));
return mpz_to_nat(mpz::of_size_t(lean_unbox(a1)) * mpz_value(a2));
else if (lean_is_scalar(a2))
return mpz_to_nat_core(mpz_value(a1) * mpz::of_size_t(lean_unbox(a2)));
return mpz_to_nat(mpz_value(a1) * mpz::of_size_t(lean_unbox(a2)));
else
return mpz_to_nat_core(mpz_value(a1) * mpz_value(a2));
}
extern "C" object * lean_nat_overflow_mul(size_t a1, size_t a2) {
return mpz_to_nat_core(mpz::of_size_t(a1) * mpz::of_size_t(a2));
return mpz_to_nat(mpz::of_size_t(a1) * mpz::of_size_t(a2));
}
extern "C" object * lean_nat_big_div(object * a1, object * a2) {

11
tests/lean/run/bigmul.lean Normal file
View file

@ -0,0 +1,11 @@
@[noinline] def f (x : Nat) :=
1000000000000000000000000000000
@[noinline] def tst1 (n : Nat) : IO Unit := do
IO.println (n * f n)
@[noinline] def tst2 (n : Nat) : IO Unit := do
IO.println (f n * n)
#eval tst1 0
#eval tst2 0