From dfc5adbd2a87164d7f7abecb79a38846acf3b185 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 17 May 2018 17:47:06 -0700 Subject: [PATCH] feat(runtime/lean_obj): add integer primitives --- src/runtime/lean_obj.cpp | 79 +++++++++++++++++++++ src/runtime/lean_obj.h | 147 +++++++++++++++++++++++++++++++++++++++ src/runtime/mpz.cpp | 12 ++++ src/runtime/mpz.h | 1 + 4 files changed, 239 insertions(+) diff --git a/src/runtime/lean_obj.cpp b/src/runtime/lean_obj.cpp index c31a691442..6b05283de9 100644 --- a/src/runtime/lean_obj.cpp +++ b/src/runtime/lean_obj.cpp @@ -303,6 +303,85 @@ lean_obj * nat_big_lxor(lean_obj * a1, lean_obj * a2) { return mk_nat_obj(mpz_value(a1) ^ mpz_value(a2)); } +/* Integers */ + +lean_obj * int_big_add(lean_obj * a1, lean_obj * a2) { + if (is_scalar(a1)) + return mk_int_obj(int2int(a1) + mpz_value(a2)); + else if (is_scalar(a2)) + return mk_int_obj(mpz_value(a1) + int2int(a2)); + else + return mk_int_obj(mpz_value(a1) + mpz_value(a2)); +} + +lean_obj * int_big_sub(lean_obj * a1, lean_obj * a2) { + if (is_scalar(a1)) + return mk_int_obj(int2int(a1) - mpz_value(a2)); + else if (is_scalar(a2)) + return mk_int_obj(mpz_value(a1) - int2int(a2)); + else + return mk_int_obj(mpz_value(a1) - mpz_value(a2)); +} + +lean_obj * int_big_mul(lean_obj * a1, lean_obj * a2) { + if (is_scalar(a1)) + return mk_int_obj(int2int(a1) * mpz_value(a2)); + else if (is_scalar(a2)) + return mk_int_obj(mpz_value(a1) * int2int(a2)); + else + return mk_int_obj(mpz_value(a1) * mpz_value(a2)); +} + +lean_obj * int_big_div(lean_obj * a1, lean_obj * a2) { + if (is_scalar(a1)) + return mk_int_obj(int2int(a1) / mpz_value(a2)); + else if (is_scalar(a2)) + return mk_int_obj(mpz_value(a1) / int2int(a2)); + else + return mk_int_obj(mpz_value(a1) / mpz_value(a2)); +} + +lean_obj * int_big_rem(lean_obj * a1, lean_obj * a2) { + if (is_scalar(a1)) + return mk_int_obj(mpz(int2int(a1)) % mpz_value(a2)); + else if (is_scalar(a2)) + return mk_int_obj(mpz_value(a1) % mpz(int2int(a2))); + else + return mk_int_obj(mpz_value(a1) % mpz_value(a2)); +} + +bool int_big_eq(lean_obj * a1, lean_obj * a2) { + if (is_scalar(a1)) { + lean_assert(int2int(a1) != mpz_value(a2)) + return false; + } else if (is_scalar(a2)) { + lean_assert(mpz_value(a1) != int2int(a2)) + return false; + } else { + return mpz_value(a1) == mpz_value(a2); + } +} + +bool int_big_le(lean_obj * a1, lean_obj * a2) { + if (is_scalar(a1)) { + return int2int(a1) <= mpz_value(a2); + } else if (is_scalar(a2)) { + return mpz_value(a1) <= int2int(a2); + } else { + return mpz_value(a1) <= mpz_value(a2); + } +} + +bool int_big_lt(lean_obj * a1, lean_obj * a2) { + if (is_scalar(a1)) { + return int2int(a1) < mpz_value(a2); + } else if (is_scalar(a2)) { + return mpz_value(a1) < int2int(a2); + } else { + return mpz_value(a1) < mpz_value(a2); + } +} + /* Debugging helper functions */ void dbg_print_str(lean_obj * o) { diff --git a/src/runtime/lean_obj.h b/src/runtime/lean_obj.h index a9bbfe0930..10d93e563c 100644 --- a/src/runtime/lean_obj.h +++ b/src/runtime/lean_obj.h @@ -503,4 +503,151 @@ inline lean_obj * nat_lxor(lean_obj * a1, lean_obj * a2) { return nat_big_xor(a1, a2); } } + +/* Integers */ + +#define LEAN_MAX_SMALL_INT (sizeof(void*) == 8 ? std::numeric_limits::max() : (1 << 30)) // NOLINT +#define LEAN_MIN_SMALL_INT (sizeof(void*) == 8 ? std::numeric_limits::min() : -(1 << 30)) // NOLINT + +inline lean_obj * mk_int_obj_core(mpz const & m) { + lean_assert(m < LEAN_MIN_SMALL_INT || m > LEAN_MAX_SMALL_INT); + return alloc_mpz(m); +} + +inline lean_obj * mk_int_obj(mpz const & m) { + if (m < LEAN_MIN_SMALL_INT || m > LEAN_MAX_SMALL_INT) + return mk_int_obj_core(m); + else + return box(static_cast(m.get_int())); +} + +inline lean_obj * mk_int_obj(int n) { + if (sizeof(void*) == 8) { // NOLINT + return box(static_cast(n)); + } else if (LEAN_MIN_SMALL_INT <= n && n <= LEAN_MAX_SMALL_INT) { + return box(static_cast(n)); + } else { + return alloc_mpz(mpz(n)); + } +} + +inline lean_obj * mk_int_obj(int64 n) { + if (LEAN_LIKELY(LEAN_MIN_SMALL_INT <= n && n <= LEAN_MAX_SMALL_INT)) { + return box(static_cast(static_cast(n))); + } else { + return mk_int_obj_core(mpz(n)); + } +} + +inline int64 int2int64(lean_obj * a) { + lean_assert(is_scalar(a)); + if (sizeof(void*) == 8) { // NOLINT + return static_cast(unbox(a)); + } else { + return static_cast(reinterpret_cast(a)) >> 1; + } +} + +inline int int2int(lean_obj * a) { + lean_assert(is_scalar(a)); + if (sizeof(void*) == 8) { // NOLINT + return static_cast(unbox(a)); + } else { + return static_cast(reinterpret_cast(a)) >> 1; + } +} + +lean_obj * int_big_add(lean_obj * a1, lean_obj * a2); + +inline lean_obj * int_add(lean_obj * a1, lean_obj * a2) { + if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) { + return mk_int_obj(int2int64(a1) + int2int64(a2)); + } else { + return int_big_add(a1, a2); + } +} + +lean_obj * int_big_sub(lean_obj * a1, lean_obj * a2); + +inline lean_obj * int_sub(lean_obj * a1, lean_obj * a2) { + if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) { + return mk_int_obj(int2int64(a1) - int2int64(a2)); + } else { + return int_big_sub(a1, a2); + } +} + +lean_obj * int_big_mul(lean_obj * a1, lean_obj * a2); + +inline lean_obj * int_mul(lean_obj * a1, lean_obj * a2) { + if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) { + return mk_int_obj(int2int64(a1) * int2int64(a2)); + } else { + return int_big_mul(a1, a2); + } +} + +lean_obj * int_big_div(lean_obj * a1, lean_obj * a2); + +inline lean_obj * int_div(lean_obj * a1, lean_obj * a2) { + if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) { + int v1 = int2int(a1); + int v2 = int2int(a2); + if (v2 == 0) + return box(0); + else + return mk_int_obj(v1 / v2); + } else { + return int_big_div(a1, a2); + } +} + +lean_obj * int_big_rem(lean_obj * a1, lean_obj * a2); + +inline lean_obj * int_rem(lean_obj * a1, lean_obj * a2) { + if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) { + int v1 = int2int(a1); + int v2 = int2int(a2); + if (v2 == 0) + return box(0); + else + return mk_int_obj(v1 % v2); + } else { + return int_big_rem(a1, a2); + } +} + +bool int_big_eq(lean_obj * a1, lean_obj * a2); + +inline bool int_eq(lean_obj * a1, lean_obj * a2) { + if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) { + return a1 == a2; + } else { + return int_big_eq(a1, a2); + } +} + +inline bool int_ne(lean_obj * a1, lean_obj * a2) { + return !int_eq(a1, a2); +} + +bool int_big_le(lean_obj * a1, lean_obj * a2); + +inline bool int_le(lean_obj * a1, lean_obj * a2) { + if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) { + return int2int(a1) <= int2int(a2); + } else { + return int_big_le(a1, a2); + } +} + +bool int_big_lt(lean_obj * a1, lean_obj * a2); + +inline bool int_lt(lean_obj * a1, lean_obj * a2) { + if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) { + return int2int(a1) < int2int(a2); + } else { + return int_big_lt(a1, a2); + } +} } diff --git a/src/runtime/mpz.cpp b/src/runtime/mpz.cpp index 886dad133d..e5353be775 100644 --- a/src/runtime/mpz.cpp +++ b/src/runtime/mpz.cpp @@ -18,6 +18,18 @@ mpz::mpz(uint64 v): mpz_add(m_val, m_val, tmp.m_val); } +mpz::mpz(int64 v) { + uint64 w; + if (v < 0) w = -v; + else w = v; + mpz_init_set_ui(m_val, static_cast(w)); + mpz tmp(static_cast(w >> 32)); + mpz_mul_2exp(tmp.m_val, tmp.m_val, 32); + mpz_add(m_val, m_val, tmp.m_val); + if (v < 0) + mpz_neg(m_val, m_val); +} + unsigned mpz::log2() const { if (is_nonpos()) return 0; diff --git a/src/runtime/mpz.h b/src/runtime/mpz.h index 2ddba6e4ed..91d5ebabce 100644 --- a/src/runtime/mpz.h +++ b/src/runtime/mpz.h @@ -30,6 +30,7 @@ public: explicit mpz(unsigned int v) { mpz_init_set_ui(m_val, v); } explicit mpz(int v) { mpz_init_set_si(m_val, v); } explicit mpz(uint64 v); + explicit mpz(int64 v); mpz(mpz const & s) { mpz_init_set(m_val, s.m_val); } mpz(mpz && s):mpz() { mpz_swap(m_val, s.m_val); } ~mpz() { mpz_clear(m_val); }