Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: runtime primitives for mpz objects #6395

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
+154 −57
Draft

feat: runtime primitives for mpz objects #6395

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
724bacc
feat: runtime primitives for mpz objects
tydeu Dec 16, 2024
dc5e674
feat: `of_nat`/`of_int`
tydeu Dec 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
111 changes: 89 additions & 22 deletions src/include/lean/lean.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1183,6 +1183,67 @@ static inline lean_object * lean_set_external_data(lean_object * o, void * data)
}
}

/* Integer scalars */

static inline int64_t lean_scalar_to_int64(b_lean_obj_arg a) {
assert(lean_is_scalar(a));
if (sizeof(void*) == 8)
return (int)((unsigned)lean_unbox(a)); /* NOLINT */
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't this truncating to 32 bits?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@eric-wieser Scalar integers in the Lean runtime are <= 32 bits. These definitions were just moved up.

else
return ((int)((size_t)a)) >> 1; /* NOLINT */
}

static inline int lean_scalar_to_int(b_lean_obj_arg a) {
assert(lean_is_scalar(a));
if (sizeof(void*) == 8)
return (int)((unsigned)lean_unbox(a)); /* NOLINT */
else
return ((int)((size_t)a)) >> 1; /* NOLINT */
}

/* 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);

static inline lean_obj_res lean_mpz_of_nat(lean_obj_arg a) {
if (lean_is_scalar(a))
return lean_mpz_of_usize(lean_unbox(a));
else
return a;
}

static inline lean_obj_res lean_mpz_of_int(lean_obj_arg a) {
if (lean_is_scalar(a))
return lean_mpz_of_signed(lean_scalar_to_int(a));
else
return 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 +1263,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 +1450,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 All @@ -1403,22 +1482,6 @@ static inline lean_obj_res lean_int64_to_int(int64_t n) {
return lean_big_int64_to_int(n);
}

static inline int64_t lean_scalar_to_int64(b_lean_obj_arg a) {
assert(lean_is_scalar(a));
if (sizeof(void*) == 8)
return (int)((unsigned)lean_unbox(a)); /* NOLINT */
else
return ((int)((size_t)a)) >> 1; /* NOLINT */
}

static inline int lean_scalar_to_int(b_lean_obj_arg a) {
assert(lean_is_scalar(a));
if (sizeof(void*) == 8)
return (int)((unsigned)lean_unbox(a)); /* NOLINT */
else
return ((int)((size_t)a)) >> 1; /* NOLINT */
}

static inline lean_obj_res lean_nat_to_int(lean_obj_arg a) {
if (lean_is_scalar(a)) {
size_t v = lean_unbox(a);
Expand Down Expand Up @@ -1621,7 +1684,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
Open in desktop
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))));
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why the pair of casts vs letting a constructor overload handle it?

Copy link
Member Author

@tydeu tydeu Jan 13, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@eric-wieser There is not int32_t/int32 constructor for mpz. I also wanted to avoid changes to the mpz implentation, focusing instead on just the public API.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

However, perhaps adding more constructor overloads to mpz would be clearer?

}

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
Loading