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

Amend GMP changes #18

Closed
wants to merge 2 commits into from
Closed

Amend GMP changes #18

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
6bf521b
chore(runtime/object): fix `usize_to_nat` name
Kha Jul 5, 2019
8dc7a6f
fix(runtime/mpz): fix and document size_t functions
Kha Jul 5, 2019
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
5 changes: 4 additions & 1 deletion src/runtime/mpz.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,10 @@ mpz::mpz(int64 v) {
}

size_t mpz::get_size_t() const {
static_assert(sizeof(size_t) <= sizeof(mp_limb_t), "GMP word size should be not greater than system word size");
// GMP only features accessors up to `unsigned long`, which is smaller than `size_t` on Windows.
// So we directly access the lowest mpz word instead.
static_assert(sizeof(size_t) == sizeof(mp_limb_t), "GMP word size should be equal system word size");
// NOTE: mpz_getlimbn returns 0 if the index is out of range (i.e. `m_val == 0`)
return static_cast<size_t>(mpz_getlimbn(m_val, 0));
}

Expand Down
7 changes: 6 additions & 1 deletion src/runtime/mpz.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,12 @@ class mpz {
bool is_unsigned_int() const { return mpz_fits_uint_p(m_val) != 0; }
bool is_long_int() const { return mpz_fits_slong_p(m_val) != 0; }
bool is_unsigned_long_int() const { return mpz_fits_ulong_p(m_val) != 0; }
bool is_size_t() const { return is_nonneg() && mpz_size(m_val) * sizeof(mp_limb_t) <= sizeof(size_t); }
bool is_size_t() const {
// GMP only features `fits` functions up to `unsigned long`, which is smaller than `size_t` on Windows.
// So we directly count the number of mpz words instead.
static_assert(sizeof(size_t) == sizeof(mp_limb_t), "GMP word size should be equal to system word size");
return is_nonneg() && mpz_size(m_val) <= 1;
}

long int get_long_int() const { lean_assert(is_long_int()); return mpz_get_si(m_val); }
int get_int() const { lean_assert(is_int()); return static_cast<int>(get_long_int()); }
Expand Down
2 changes: 1 addition & 1 deletion src/runtime/object.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1702,7 +1702,7 @@ extern "C" object * lean_closure_max_args(object *) {
}

extern "C" object * lean_max_small_nat(object *) {
return unsigned_to_nat(LEAN_MAX_SMALL_NAT);
return usize_to_nat(LEAN_MAX_SMALL_NAT);
}

// =======================================
Expand Down
17 changes: 7 additions & 10 deletions src/runtime/object.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -773,7 +773,7 @@ inline obj_res mk_nat_obj(mpz const & m) {
return mk_nat_obj_core(m);
}

inline obj_res unsigned_to_nat(usize n) {
inline obj_res usize_to_nat(usize n) {
if (n <= LEAN_MAX_SMALL_NAT) {
return box(n);
} else {
Expand All @@ -782,7 +782,7 @@ inline obj_res unsigned_to_nat(usize n) {
}

inline obj_res mk_nat_obj(unsigned n) {
return unsigned_to_nat(static_cast<usize>(n));
return usize_to_nat(static_cast<usize>(n));
}

inline obj_res uint64_to_nat(uint64 n) {
Expand Down Expand Up @@ -1167,7 +1167,7 @@ inline size_t string_size(b_obj_arg o) { return to_string(o)->m_size; }
inline size_t string_len(b_obj_arg o) { return to_string(o)->m_length; }
obj_res string_push(obj_arg s, uint32 c);
obj_res string_append(obj_arg s1, b_obj_arg s2);
inline obj_res string_length(b_obj_arg s) { return unsigned_to_nat(string_len(s)); } // TODO(Leo): improve
inline obj_res string_length(b_obj_arg s) { return usize_to_nat(string_len(s)); } // TODO(Leo): improve
obj_res string_mk(obj_arg cs);
obj_res string_data(obj_arg s);

Expand All @@ -1177,7 +1177,7 @@ obj_res string_utf8_prev(b_obj_arg s, b_obj_arg i);
obj_res string_utf8_set(obj_arg s, b_obj_arg i, uint32 c);
inline uint8 string_utf8_at_end(b_obj_arg s, b_obj_arg i) { return !is_scalar(i) || unbox(i) >= string_size(s) - 1; }
obj_res string_utf8_extract(b_obj_arg s, b_obj_arg b, b_obj_arg e);
inline obj_res string_utf8_byte_size(b_obj_arg s) { return unsigned_to_nat(string_size(s) - 1); }
inline obj_res string_utf8_byte_size(b_obj_arg s) { return usize_to_nat(string_size(s) - 1); }

inline bool string_eq(b_obj_arg s1, b_obj_arg s2) { return s1 == s2 || (string_size(s1) == string_size(s2) && std::memcmp(string_cstr(s1), string_cstr(s2), string_size(s1)) == 0); }
bool string_eq(b_obj_arg s1, char const * s2);
Expand Down Expand Up @@ -1232,7 +1232,7 @@ inline obj_res byte_array_set(obj_arg a, b_obj_arg i, uint8 b) {
// uint8
uint8 uint8_of_big_nat(b_obj_arg a);
inline uint8 uint8_of_nat(b_obj_arg a) { return is_scalar(a) ? static_cast<uint8>(unbox(a)) : uint8_of_big_nat(a); }
inline obj_res uint8_to_nat(uint8 a) { return unsigned_to_nat(static_cast<usize>(a)); }
inline obj_res uint8_to_nat(uint8 a) { return usize_to_nat(static_cast<usize>(a)); }
inline uint8 uint8_add(uint8 a1, uint8 a2) { return a1+a2; }
inline uint8 uint8_sub(uint8 a1, uint8 a2) { return a1-a2; }
inline uint8 uint8_mul(uint8 a1, uint8 a2) { return a1*a2; }
Expand All @@ -1254,7 +1254,7 @@ inline uint8 uint8_dec_le(uint8 a1, uint8 a2) { return a1 <= a2; }
// uint16
uint16 uint16_of_big_nat(b_obj_arg a);
inline uint16 uint16_of_nat(b_obj_arg a) { return is_scalar(a) ? static_cast<uint16>(unbox(a)) : uint16_of_big_nat(a); }
inline obj_res uint16_to_nat(uint16 a) { return unsigned_to_nat(static_cast<usize>(a)); }
inline obj_res uint16_to_nat(uint16 a) { return usize_to_nat(static_cast<usize>(a)); }
inline uint16 uint16_add(uint16 a1, uint16 a2) { return a1+a2; }
inline uint16 uint16_sub(uint16 a1, uint16 a2) { return a1-a2; }
inline uint16 uint16_mul(uint16 a1, uint16 a2) { return a1*a2; }
Expand All @@ -1276,7 +1276,7 @@ inline uint8 uint16_dec_le(uint16 a1, uint16 a2) { return a1 <= a2; }
// uint32
uint32 uint32_of_big_nat(b_obj_arg a);
inline uint32 uint32_of_nat(b_obj_arg a) { return is_scalar(a) ? static_cast<uint32>(unbox(a)) : uint32_of_big_nat(a); }
inline obj_res uint32_to_nat(uint32 a) { return unsigned_to_nat(static_cast<usize>(a)); }
inline obj_res uint32_to_nat(uint32 a) { return usize_to_nat(static_cast<usize>(a)); }
inline uint32 uint32_add(uint32 a1, uint32 a2) { return a1+a2; }
inline uint32 uint32_sub(uint32 a1, uint32 a2) { return a1-a2; }
inline uint32 uint32_mul(uint32 a1, uint32 a2) { return a1*a2; }
Expand Down Expand Up @@ -1326,9 +1326,6 @@ inline uint8 uint64_dec_le(uint64 a1, uint64 a2) { return a1 <= a2; }
// usize
usize usize_of_big_nat(b_obj_arg a);
inline usize usize_of_nat(b_obj_arg a) { return is_scalar(a) ? unbox(a) : usize_of_big_nat(a); }
inline obj_res usize_to_nat(usize a) {
return unsigned_to_nat(a);
}
inline usize usize_add(usize a1, usize a2) { return a1+a2; }
inline usize usize_sub(usize a1, usize a2) { return a1-a2; }
inline usize usize_mul(usize a1, usize a2) { return a1*a2; }
Expand Down
4 changes: 2 additions & 2 deletions src/util/nat.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,9 @@ class nat : public object_ref {
nat():object_ref(box(0)) {}
explicit nat(obj_arg o):object_ref(o) {}
nat(b_obj_arg o, bool b):object_ref(o, b) {}
explicit nat(int v):object_ref(unsigned_to_nat(v < 0 ? static_cast<usize>(0) : static_cast<usize>(v))) {}
explicit nat(int v):object_ref(usize_to_nat(v < 0 ? static_cast<usize>(0) : static_cast<usize>(v))) {}
explicit nat(unsigned v):object_ref(mk_nat_obj(v)) {}
explicit nat(unsigned long v):object_ref(unsigned_to_nat(v)) {}
explicit nat(unsigned long v):object_ref(usize_to_nat(v)) {}
explicit nat(mpz const & v):object_ref(mk_nat_obj(v)) {}
explicit nat(char const * v):object_ref(box(0)) {
mpz m(v);
Expand Down