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

fix(runtime/lean_obj): test

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-17 17:14:24 -07:00
parent 5d8501acf5
commit b4fb4385a2
2 changed files with 27 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/runtime/lean_obj.cpp
View file

@ -175,11 +175,11 @@ lean_obj * string_append(lean_obj * s1, lean_obj * s2) {
lean_obj * nat_big_add(lean_obj * a1, lean_obj * a2) {
lean_assert(!is_scalar(a1) || !is_scalar(a2));
if (is_scalar(a1))
return mk_mpz_core(unbox(a1) + mpz_value(a2));
return mk_nat_obj_core(unbox(a1) + mpz_value(a2));
else if (is_scalar(a2))
return mk_mpz_core(mpz_value(a1) + unbox(a2));
return mk_nat_obj_core(mpz_value(a1) + unbox(a2));
else
return mk_mpz_core(mpz_value(a1) + mpz_value(a2));
return mk_nat_obj_core(mpz_value(a1) + mpz_value(a2));
}
lean_obj * nat_big_sub(lean_obj * a1, lean_obj * a2) {
@ -189,23 +189,23 @@ lean_obj * nat_big_sub(lean_obj * a1, lean_obj * a2) {
return box(0);
} else if (is_scalar(a2)) {
lean_assert(mpz_value(a1) > unbox(a2));
return mk_mpz(mpz_value(a1) - unbox(a2));
return mk_nat_obj(mpz_value(a1) - unbox(a2));
} else {
if (mpz_value(a1) < mpz_value(a2))
return box(0);
else
return mk_mpz(mpz_value(a1) - mpz_value(a2));
return mk_nat_obj(mpz_value(a1) - mpz_value(a2));
}
}
lean_obj * nat_big_mul(lean_obj * a1, lean_obj * a2) {
lean_assert(!is_scalar(a1) || !is_scalar(a2));
if (is_scalar(a1))
return mk_mpz_core(unbox(a1) * mpz_value(a2));
return mk_nat_obj_core(unbox(a1) * mpz_value(a2));
else if (is_scalar(a2))
return mk_mpz_core(mpz_value(a1) * unbox(a2));
return mk_nat_obj_core(mpz_value(a1) * unbox(a2));
else
return mk_mpz_core(mpz_value(a1) * mpz_value(a2));
return mk_nat_obj_core(mpz_value(a1) * mpz_value(a2));
}
lean_obj * nat_big_div(lean_obj * a1, lean_obj * a2) {
@ -216,10 +216,10 @@ lean_obj * nat_big_div(lean_obj * a1, lean_obj * a2) {
return box(0);
} else if (is_scalar(a2)) {
unsigned n2 = unbox(a2);
return n2 == 0 ? a2 : mk_mpz(mpz_value(a1) / n2);
return n2 == 0 ? a2 : mk_nat_obj(mpz_value(a1) / n2);
} else {
lean_assert(mpz_value(a2) != 0);
return mk_mpz(mpz_value(a1) / mpz_value(a2));
return mk_nat_obj(mpz_value(a1) / mpz_value(a2));
}
}
@ -233,7 +233,7 @@ lean_obj * nat_big_mod(lean_obj * a1, lean_obj * a2) {
return n2 == 0 ? a2 : box((mpz_value(a1) % mpz(n2)).get_unsigned_int());
} else {
lean_assert(mpz_value(a2) != 0);
return mk_mpz(mpz_value(a1) % mpz_value(a2));
return mk_nat_obj(mpz_value(a1) % mpz_value(a2));
}
}
@ -267,31 +267,31 @@ bool nat_big_lt(lean_obj * a1, lean_obj * a2) {
lean_obj * nat_big_land(lean_obj * a1, lean_obj * a2) {
lean_assert(!is_scalar(a1) || !is_scalar(a2));
if (is_scalar(a1))
return mk_mpz(mpz(unbox(a1)) & mpz_value(a2));
return mk_nat_obj(mpz(unbox(a1)) & mpz_value(a2));
else if (is_scalar(a2))
return mk_mpz(mpz_value(a1) & mpz(unbox(a2)));
return mk_nat_obj(mpz_value(a1) & mpz(unbox(a2)));
else
return mk_mpz(mpz_value(a1) & mpz_value(a2));
return mk_nat_obj(mpz_value(a1) & mpz_value(a2));
}
lean_obj * nat_big_lor(lean_obj * a1, lean_obj * a2) {
lean_assert(!is_scalar(a1) || !is_scalar(a2));
if (is_scalar(a1))
return mk_mpz(mpz(unbox(a1)) | mpz_value(a2));
return mk_nat_obj(mpz(unbox(a1)) | mpz_value(a2));
else if (is_scalar(a2))
return mk_mpz(mpz_value(a1) | mpz(unbox(a2)));
return mk_nat_obj(mpz_value(a1) | mpz(unbox(a2)));
else
return mk_mpz(mpz_value(a1) | mpz_value(a2));
return mk_nat_obj(mpz_value(a1) | mpz_value(a2));
}
lean_obj * nat_big_lxor(lean_obj * a1, lean_obj * a2) {
lean_assert(!is_scalar(a1) || !is_scalar(a2));
if (is_scalar(a1))
return mk_mpz(mpz(unbox(a1)) ^ mpz_value(a2));
return mk_nat_obj(mpz(unbox(a1)) ^ mpz_value(a2));
else if (is_scalar(a2))
return mk_mpz(mpz_value(a1) ^ mpz(unbox(a2)));
return mk_nat_obj(mpz_value(a1) ^ mpz(unbox(a2)));
else
return mk_mpz(mpz_value(a1) ^ mpz_value(a2));
return mk_nat_obj(mpz_value(a1) ^ mpz_value(a2));
}
/* Debugging helper functions */

14
src/runtime/lean_obj.h
View file

@ -332,14 +332,14 @@ lean_obj * string_append(lean_obj * s1, lean_obj * s2);
#define LEAN_MAX_SMALL_NAT (sizeof(void*) == 8 ? std::numeric_limits<unsigned>::max() : (std::numeric_limits<unsigned>::max() >> 1)) // NOLINT
inline lean_obj * mk_mpz_core(mpz const & m) {
inline lean_obj * mk_nat_obj_core(mpz const & m) {
lean_assert(m > LEAN_MAX_SMALL_NAT);
return alloc_mpz(m);
}
inline lean_obj * mk_mpz(mpz const & m) {
inline lean_obj * mk_nat_obj(mpz const & m) {
if (m > LEAN_MAX_SMALL_NAT)
return mk_mpz_core(m);
return mk_nat_obj_core(m);
else
return box(m.get_unsigned_int());
}
@ -350,15 +350,15 @@ inline lean_obj * mk_nat_obj(unsigned n) {
} else if (n <= LEAN_MAX_SMALL_NAT) {
return box(n);
} else {
return mk_mpz_core(mpz(n));
return mk_nat_obj_core(mpz(n));
}
}
inline lean_obj * mk_nat_obj(uint64 n) {
if (LEAN_LIKELY(n < LEAN_MAX_SMALL_NAT)) {
if (LEAN_LIKELY(n <= LEAN_MAX_SMALL_NAT)) {
return box(n);
} else {
return mk_mpz_core(mpz(n));
return mk_nat_obj_core(mpz(n));
}
}
@ -371,7 +371,7 @@ inline lean_obj * nat_succ(lean_obj * a) {
if (LEAN_LIKELY(is_scalar(a))) {
return mk_nat_obj(nat2uint64(a) + 1);
} else {
return mk_mpz_core(mpz_value(a) + 1);
return mk_nat_obj_core(mpz_value(a) + 1);
}
}