Skip to content

Commit

Permalink
feat: runtime primitives for mpz objects
Browse files Browse the repository at this point in the history
  • Loading branch information
@tydeu
tydeu committed Dec 16, 2024
1 parent 48be424 commit 4a08e12
Show file tree
Hide file tree
Showing 2 changed files with 122 additions and 41 deletions.
63 changes: 57 additions & 6 deletions src/include/lean/lean.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1183,6 +1183,35 @@ static inline lean_object * lean_set_external_data(lean_object * o, void * data)
}
}

/* Big numbers */

LEAN_EXPORT lean_obj_res lean_mpz_of_usize(size_t a);
LEAN_EXPORT lean_obj_res lean_mpz_of_uint64(uint64_t a);
LEAN_EXPORT lean_obj_res lean_mpz_of_uint32(uint32_t a);
LEAN_EXPORT lean_obj_res lean_mpz_of_unsigned(unsigned a);
LEAN_EXPORT lean_obj_res lean_mpz_of_isize(size_t a);
LEAN_EXPORT lean_obj_res lean_mpz_of_int64(uint64_t a);
LEAN_EXPORT lean_obj_res lean_mpz_of_int32(uint32_t a);
LEAN_EXPORT lean_obj_res lean_mpz_of_signed(int a);
LEAN_EXPORT lean_obj_res lean_mpz_to_nat(lean_obj_arg a);
LEAN_EXPORT lean_obj_res lean_mpz_to_int(lean_obj_arg a);

LEAN_EXPORT bool lean_mpz_eq(b_lean_obj_arg a1, b_lean_obj_arg a2);
LEAN_EXPORT bool lean_mpz_le(b_lean_obj_arg a1, b_lean_obj_arg a2);
LEAN_EXPORT bool lean_mpz_lt(b_lean_obj_arg a1, b_lean_obj_arg a2);

static inline LEAN_ALWAYS_INLINE uint8_t lean_mpz_dec_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
return lean_mpz_eq(a1, a2);
}

static inline LEAN_ALWAYS_INLINE uint8_t lean_mpz_dec_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
return lean_mpz_le(a1, a2);
}

static inline LEAN_ALWAYS_INLINE uint8_t lean_mpz_dec_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
return lean_mpz_lt(a1, a2);
}

/* Natural numbers */

#define LEAN_MAX_SMALL_NAT (SIZE_MAX >> 1)
Expand All @@ -1202,8 +1231,14 @@ LEAN_EXPORT lean_object * lean_nat_big_lor(lean_object * a1, lean_object * a2);
LEAN_EXPORT lean_object * lean_nat_big_xor(lean_object * a1, lean_object * a2);

LEAN_EXPORT lean_obj_res lean_cstr_to_nat(char const * n);
LEAN_EXPORT lean_obj_res lean_big_usize_to_nat(size_t n);
LEAN_EXPORT lean_obj_res lean_big_uint64_to_nat(uint64_t n);
static inline LEAN_ALWAYS_INLINE LEAN_EXPORT lean_obj_res lean_big_usize_to_nat(size_t n) {
assert(n <= LEAN_MAX_SMALL_NAT);
return lean_mpz_of_usize(n);
}
static inline LEAN_ALWAYS_INLINE LEAN_EXPORT lean_obj_res lean_big_uint64_to_nat(uint64_t n) {
assert(n <= LEAN_MAX_SMALL_NAT);
return lean_mpz_of_uint64(n);
}
static inline lean_obj_res lean_usize_to_nat(size_t n) {
if (LEAN_LIKELY(n <= LEAN_MAX_SMALL_NAT))
return lean_box(n);
Expand Down Expand Up @@ -1383,9 +1418,21 @@ LEAN_EXPORT bool lean_int_big_lt(lean_object * a1, lean_object * a2);
LEAN_EXPORT bool lean_int_big_nonneg(lean_object * a);

LEAN_EXPORT lean_object * lean_cstr_to_int(char const * n);
LEAN_EXPORT lean_object * lean_big_int_to_int(int n);
LEAN_EXPORT lean_object * lean_big_size_t_to_int(size_t n);
LEAN_EXPORT lean_object * lean_big_int64_to_int(int64_t n);

static inline LEAN_ALWAYS_INLINE lean_object * lean_big_int_to_int(int n) {
assert(n < LEAN_MIN_SMALL_INT || n > LEAN_MAX_SMALL_INT);
return lean_mpz_of_signed(n);
}

static inline LEAN_ALWAYS_INLINE lean_object * lean_big_size_t_to_int(size_t n) {
assert(n <= LEAN_MAX_SMALL_INT);
return lean_mpz_of_usize(n);
}

static inline LEAN_ALWAYS_INLINE lean_object * lean_big_int64_to_int(int64_t n) {
assert(n < LEAN_MIN_SMALL_INT || n > LEAN_MAX_SMALL_INT);
return lean_mpz_of_int64((uint64_t)n);
}

static inline lean_obj_res lean_int_to_int(int n) {
if (sizeof(void*) == 8)
Expand Down Expand Up @@ -1621,7 +1668,11 @@ static inline bool lean_int_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
}
}

LEAN_EXPORT lean_obj_res lean_big_int_to_nat(lean_obj_arg a);
static inline LEAN_ALWAYS_INLINE lean_obj_res lean_big_int_to_nat(lean_obj_arg a) {
assert(!lean_is_scalar(a));
return lean_mpz_to_nat(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)) {
Expand Down
100 changes: 65 additions & 35 deletions src/runtime/object.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1114,7 +1114,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_promise_result(obj_arg promise) {
}

// =======================================
// Natural numbers
// Big numbers

object * alloc_mpz(mpz const & m) {
void * mem = lean_alloc_small_object(sizeof(mpz_object));
Expand All @@ -1133,6 +1133,55 @@ extern "C" LEAN_EXPORT void lean_extract_mpz_value(lean_object * o, mpz_t v) {
}
#endif

extern "C" LEAN_EXPORT obj_res lean_mpz_of_usize(usize n) {
return alloc_mpz(mpz::of_size_t(n));
}

extern "C" LEAN_EXPORT obj_res lean_mpz_of_uint64(uint64 n) {
return alloc_mpz(mpz(n));
}

extern "C" LEAN_EXPORT obj_res lean_mpz_of_uint32(uint32 n) {
static_assert(sizeof(uint32_t) <= sizeof(unsigned), "unsigned should be at least the size of a uint32");
return alloc_mpz(mpz(static_cast<unsigned>(n)));
}

extern "C" LEAN_EXPORT obj_res lean_mpz_of_unsigned(unsigned n) {
return alloc_mpz(mpz(n));
}

extern "C" LEAN_EXPORT obj_res lean_mpz_of_isize(size_t a) {
return alloc_mpz(mpz(static_cast<int64>(static_cast<ptrdiff_t>(a))));
}

extern "C" LEAN_EXPORT obj_res lean_mpz_of_int64(uint64_t n) {
return alloc_mpz(mpz(static_cast<int64>(n)));
}

extern "C" LEAN_EXPORT obj_res lean_mpz_of_int32(uint32_t n) {
static_assert(sizeof(uint32_t) <= sizeof(int), "int should be at least the size of a uint32");
return alloc_mpz(mpz(static_cast<int>(static_cast<int32_t>(n))));
}

extern "C" LEAN_EXPORT obj_res lean_mpz_of_signed(int n) {
return alloc_mpz(mpz(n));
}

extern "C" LEAN_EXPORT bool lean_mpz_eq(b_obj_arg a1, b_obj_arg a2) {
return mpz_value(a1) == mpz_value(a2);
}

extern "C" LEAN_EXPORT bool lean_mpz_le(b_obj_arg a1, b_obj_arg a2) {
return mpz_value(a1) <= mpz_value(a2);
}

extern "C" LEAN_EXPORT bool lean_mpz_lt(b_obj_arg a1, b_obj_arg a2) {
return mpz_value(a1) < mpz_value(a2);
}

// =======================================
// Natural numbers

object * mpz_to_nat_core(mpz const & m) {
lean_assert(!m.is_size_t() || m.get_size_t() > LEAN_MAX_SMALL_NAT);
return alloc_mpz(m);
Expand All @@ -1145,24 +1194,18 @@ static inline obj_res mpz_to_nat(mpz const & m) {
return mpz_to_nat_core(m);
}

extern "C" LEAN_EXPORT object * lean_cstr_to_nat(char const * n) {
return mpz_to_nat(mpz(n));
}

extern "C" LEAN_EXPORT object * lean_big_usize_to_nat(size_t n) {
if (n <= LEAN_MAX_SMALL_NAT) {
return lean_box(n);
extern "C" LEAN_EXPORT obj_res lean_mpz_to_nat(obj_arg a) {
mpz m = mpz_value(a);
if (m.is_size_t() && m.get_size_t() <= LEAN_MAX_SMALL_NAT) {
lean_dec(a);
return lean_box(m.get_size_t());
} else {
return mpz_to_nat_core(mpz::of_size_t(n));
return a;
}
}

extern "C" LEAN_EXPORT object * lean_big_uint64_to_nat(uint64_t n) {
if (LEAN_LIKELY(n <= LEAN_MAX_SMALL_NAT)) {
return lean_box(n);
} else {
return mpz_to_nat_core(mpz(n));
}
extern "C" LEAN_EXPORT object * lean_cstr_to_nat(char const * n) {
return mpz_to_nat(mpz(n));
}

extern "C" LEAN_EXPORT object * lean_nat_big_succ(object * a) {
Expand Down Expand Up @@ -1400,33 +1443,20 @@ static object * mpz_to_int(mpz const & m) {
return lean_box(static_cast<unsigned>(m.get_int()));
}

extern "C" LEAN_EXPORT lean_obj_res lean_big_int_to_nat(lean_obj_arg a) {
lean_assert(!lean_is_scalar(a));
extern "C" LEAN_EXPORT obj_res lean_mpz_to_int(obj_arg a) {
mpz m = mpz_value(a);
lean_dec(a);
return mpz_to_nat(m);
if (m < LEAN_MIN_SMALL_INT || m > LEAN_MAX_SMALL_INT) {
return a;
} else {
lean_dec(a);
return lean_box(static_cast<unsigned>(m.get_int()));
}
}

extern "C" LEAN_EXPORT object * lean_cstr_to_int(char const * n) {
return mpz_to_int(mpz(n));
}

extern "C" LEAN_EXPORT object * lean_big_int_to_int(int n) {
return alloc_mpz(mpz(n));
}

extern "C" LEAN_EXPORT object * lean_big_size_t_to_int(size_t n) {
return alloc_mpz(mpz::of_size_t(n));
}

extern "C" LEAN_EXPORT object * lean_big_int64_to_int(int64_t n) {
if (LEAN_LIKELY(LEAN_MIN_SMALL_INT <= n && n <= LEAN_MAX_SMALL_INT)) {
return lean_box(static_cast<unsigned>(static_cast<int>(n)));
} else {
return mpz_to_int_core(mpz(n));
}
}

extern "C" LEAN_EXPORT object * lean_int_big_neg(object * a) {
return mpz_to_int(neg(mpz_value(a)));
}
Expand Down

0 comments on commit 4a08e12

Please sign in to comment.