fix: annotate lean.h functions with LEAN_SHARED
This commit is contained in:
Sebastian Ullrich
parent
da516f5aa7
commit
60ffdd094c
2 changed files with 172 additions and 172 deletions
|
|
@ -272,7 +272,7 @@ typedef struct {
|
|||
lean_external_foreach_proc m_foreach;
|
||||
} lean_external_class;
|
||||
|
||||
lean_external_class * lean_register_external_class(lean_external_finalize_proc, lean_external_foreach_proc);
|
||||
LEAN_SHARED lean_external_class * lean_register_external_class(lean_external_finalize_proc, lean_external_foreach_proc);
|
||||
|
||||
/* Object for wrapping external data. */
|
||||
typedef struct {
|
||||
|
|
@ -285,16 +285,16 @@ static inline bool lean_is_scalar(lean_object * o) { return ((size_t)(o) & 1) ==
|
|||
static inline lean_object * lean_box(size_t n) { return (lean_object*)(((size_t)(n) << 1) | 1); }
|
||||
static inline size_t lean_unbox(lean_object * o) { return (size_t)(o) >> 1; }
|
||||
|
||||
void lean_set_exit_on_panic(bool flag);
|
||||
LEAN_SHARED void lean_set_exit_on_panic(bool flag);
|
||||
/* Enable/disable panic messages */
|
||||
void lean_set_panic_messages(bool flag);
|
||||
LEAN_SHARED void lean_set_panic_messages(bool flag);
|
||||
|
||||
lean_object * lean_panic_fn(lean_object * default_val, lean_object * msg);
|
||||
LEAN_SHARED lean_object * lean_panic_fn(lean_object * default_val, lean_object * msg);
|
||||
|
||||
__attribute__((noreturn)) void lean_internal_panic(char const * msg);
|
||||
__attribute__((noreturn)) void lean_internal_panic_out_of_memory();
|
||||
__attribute__((noreturn)) void lean_internal_panic_unreachable();
|
||||
__attribute__((noreturn)) void lean_internal_panic_rc_overflow();
|
||||
LEAN_SHARED __attribute__((noreturn)) void lean_internal_panic(char const * msg);
|
||||
LEAN_SHARED __attribute__((noreturn)) void lean_internal_panic_out_of_memory();
|
||||
LEAN_SHARED __attribute__((noreturn)) void lean_internal_panic_unreachable();
|
||||
LEAN_SHARED __attribute__((noreturn)) void lean_internal_panic_rc_overflow();
|
||||
|
||||
static inline size_t lean_align(size_t v, size_t a) {
|
||||
return (v / a)*a + a * (v % a != 0);
|
||||
|
|
@ -306,10 +306,10 @@ static inline unsigned lean_get_slot_idx(unsigned sz) {
|
|||
return sz / LEAN_OBJECT_SIZE_DELTA - 1;
|
||||
}
|
||||
|
||||
void * lean_alloc_small(unsigned sz, unsigned slot_idx);
|
||||
void lean_free_small(void * p);
|
||||
unsigned lean_small_mem_size(void * p);
|
||||
void lean_inc_heartbeat();
|
||||
LEAN_SHARED void * lean_alloc_small(unsigned sz, unsigned slot_idx);
|
||||
LEAN_SHARED void lean_free_small(void * p);
|
||||
LEAN_SHARED unsigned lean_small_mem_size(void * p);
|
||||
LEAN_SHARED void lean_inc_heartbeat();
|
||||
|
||||
static inline lean_object * lean_alloc_small_object(unsigned sz) {
|
||||
#ifdef LEAN_SMALL_ALLOCATOR
|
||||
|
|
@ -367,8 +367,8 @@ static inline void lean_free_small_object(lean_object * o) {
|
|||
#endif
|
||||
}
|
||||
|
||||
lean_object * lean_alloc_object(size_t sz);
|
||||
void lean_free_object(lean_object * o);
|
||||
LEAN_SHARED lean_object * lean_alloc_object(size_t sz);
|
||||
LEAN_SHARED void lean_free_object(lean_object * o);
|
||||
|
||||
static inline uint8_t lean_ptr_tag(lean_object * o) {
|
||||
return o->m_tag;
|
||||
|
|
@ -383,7 +383,7 @@ static inline unsigned lean_ptr_other(lean_object * o) {
|
|||
All constructor objects are "small", and allocated into pages.
|
||||
We retrieve their size by accessing the page header. The size of
|
||||
small objects is a multiple of LEAN_OBJECT_SIZE_DELTA */
|
||||
size_t lean_object_byte_size(lean_object * o);
|
||||
LEAN_SHARED size_t lean_object_byte_size(lean_object * o);
|
||||
|
||||
static inline bool lean_is_mt(lean_object * o) {
|
||||
return o->m_rc < 0;
|
||||
|
|
@ -406,8 +406,8 @@ static inline _Atomic(int) * lean_get_rc_mt_addr(lean_object* o) {
|
|||
return (_Atomic(int)*)(&(o->m_rc));
|
||||
}
|
||||
|
||||
void lean_inc_ref_cold(lean_object * o);
|
||||
void lean_inc_ref_n_cold(lean_object * o, unsigned n);
|
||||
LEAN_SHARED void lean_inc_ref_cold(lean_object * o);
|
||||
LEAN_SHARED void lean_inc_ref_n_cold(lean_object * o, unsigned n);
|
||||
|
||||
static inline void lean_inc_ref(lean_object * o) {
|
||||
if (LEAN_LIKELY(lean_is_st(o))) {
|
||||
|
|
@ -425,7 +425,7 @@ static inline void lean_inc_ref_n(lean_object * o, size_t n) {
|
|||
}
|
||||
}
|
||||
|
||||
void lean_dec_ref_cold(lean_object * o);
|
||||
LEAN_SHARED void lean_dec_ref_cold(lean_object * o);
|
||||
|
||||
static inline void lean_dec_ref(lean_object * o) {
|
||||
if (LEAN_LIKELY(o->m_rc > 1)) {
|
||||
|
|
@ -439,7 +439,7 @@ static inline void lean_inc_n(lean_object * o, size_t n) { if (!lean_is_scalar(o
|
|||
static inline void lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ref(o); }
|
||||
|
||||
/* Just free memory */
|
||||
void lean_dealloc(lean_object * o);
|
||||
LEAN_SHARED void lean_dealloc(lean_object * o);
|
||||
|
||||
static inline bool lean_is_ctor(lean_object * o) { return lean_ptr_tag(o) <= LeanMaxCtorTag; }
|
||||
static inline bool lean_is_closure(lean_object * o) { return lean_ptr_tag(o) == LeanClosure; }
|
||||
|
|
@ -482,8 +482,8 @@ static inline bool lean_is_shared(lean_object * o) {
|
|||
}
|
||||
}
|
||||
|
||||
void lean_mark_mt(lean_object * o);
|
||||
void lean_mark_persistent(lean_object * o);
|
||||
LEAN_SHARED void lean_mark_mt(lean_object * o);
|
||||
LEAN_SHARED void lean_mark_persistent(lean_object * o);
|
||||
|
||||
static inline void lean_set_st_header(lean_object * o, unsigned tag, unsigned other) {
|
||||
o->m_rc = 1;
|
||||
|
|
@ -640,34 +640,34 @@ static inline void lean_closure_set(u_lean_obj_arg o, unsigned i, lean_obj_arg a
|
|||
lean_to_closure(o)->m_objs[i] = a;
|
||||
}
|
||||
|
||||
lean_object* lean_apply_1(lean_object* f, lean_object* a1);
|
||||
lean_object* lean_apply_2(lean_object* f, lean_object* a1, lean_object* a2);
|
||||
lean_object* lean_apply_3(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3);
|
||||
lean_object* lean_apply_4(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4);
|
||||
lean_object* lean_apply_5(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5);
|
||||
lean_object* lean_apply_6(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6);
|
||||
lean_object* lean_apply_7(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7);
|
||||
lean_object* lean_apply_8(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8);
|
||||
lean_object* lean_apply_9(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9);
|
||||
lean_object* lean_apply_10(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10);
|
||||
lean_object* lean_apply_11(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11);
|
||||
lean_object* lean_apply_12(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12);
|
||||
lean_object* lean_apply_13(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13);
|
||||
lean_object* lean_apply_14(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14);
|
||||
lean_object* lean_apply_15(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14, lean_object* a15);
|
||||
lean_object* lean_apply_16(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14, lean_object* a15, lean_object* a16);
|
||||
lean_object* lean_apply_n(lean_object* f, unsigned n, lean_object** args);
|
||||
LEAN_SHARED lean_object* lean_apply_1(lean_object* f, lean_object* a1);
|
||||
LEAN_SHARED lean_object* lean_apply_2(lean_object* f, lean_object* a1, lean_object* a2);
|
||||
LEAN_SHARED lean_object* lean_apply_3(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3);
|
||||
LEAN_SHARED lean_object* lean_apply_4(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4);
|
||||
LEAN_SHARED lean_object* lean_apply_5(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5);
|
||||
LEAN_SHARED lean_object* lean_apply_6(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6);
|
||||
LEAN_SHARED lean_object* lean_apply_7(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7);
|
||||
LEAN_SHARED lean_object* lean_apply_8(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8);
|
||||
LEAN_SHARED lean_object* lean_apply_9(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9);
|
||||
LEAN_SHARED lean_object* lean_apply_10(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10);
|
||||
LEAN_SHARED lean_object* lean_apply_11(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11);
|
||||
LEAN_SHARED lean_object* lean_apply_12(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12);
|
||||
LEAN_SHARED lean_object* lean_apply_13(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13);
|
||||
LEAN_SHARED lean_object* lean_apply_14(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14);
|
||||
LEAN_SHARED lean_object* lean_apply_15(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14, lean_object* a15);
|
||||
LEAN_SHARED lean_object* lean_apply_16(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14, lean_object* a15, lean_object* a16);
|
||||
LEAN_SHARED lean_object* lean_apply_n(lean_object* f, unsigned n, lean_object** args);
|
||||
/* Pre: n > 16 */
|
||||
lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object** args);
|
||||
LEAN_SHARED lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object** args);
|
||||
|
||||
/* Fixpoint */
|
||||
|
||||
lean_obj_res lean_fixpoint(lean_obj_arg rec, lean_obj_arg a);
|
||||
lean_obj_res lean_fixpoint2(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2);
|
||||
lean_obj_res lean_fixpoint3(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3);
|
||||
lean_obj_res lean_fixpoint4(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4);
|
||||
lean_obj_res lean_fixpoint5(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4, lean_obj_arg a5);
|
||||
lean_obj_res lean_fixpoint6(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4, lean_obj_arg a5, lean_obj_arg a6);
|
||||
LEAN_SHARED lean_obj_res lean_fixpoint(lean_obj_arg rec, lean_obj_arg a);
|
||||
LEAN_SHARED lean_obj_res lean_fixpoint2(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2);
|
||||
LEAN_SHARED lean_obj_res lean_fixpoint3(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3);
|
||||
LEAN_SHARED lean_obj_res lean_fixpoint4(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4);
|
||||
LEAN_SHARED lean_obj_res lean_fixpoint5(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4, lean_obj_arg a5);
|
||||
LEAN_SHARED lean_obj_res lean_fixpoint6(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4, lean_obj_arg a5, lean_obj_arg a6);
|
||||
|
||||
/* Arrays of objects (low level API) */
|
||||
static inline lean_obj_res lean_alloc_array(size_t size, size_t capacity) {
|
||||
|
|
@ -700,8 +700,8 @@ static inline void lean_array_set_core(u_lean_obj_arg o, size_t i, lean_obj_arg
|
|||
assert(i < lean_array_size(o));
|
||||
lean_to_array(o)->m_data[i] = v;
|
||||
}
|
||||
lean_object * lean_array_mk(lean_obj_arg l);
|
||||
lean_object * lean_array_data(lean_obj_arg a);
|
||||
LEAN_SHARED lean_object * lean_array_mk(lean_obj_arg l);
|
||||
LEAN_SHARED lean_object * lean_array_data(lean_obj_arg a);
|
||||
|
||||
/* Arrays of objects (high level API) */
|
||||
|
||||
|
|
@ -733,7 +733,7 @@ static inline lean_obj_res lean_array_fget(b_lean_obj_arg a, b_lean_obj_arg i) {
|
|||
return lean_array_uget(a, lean_unbox(i));
|
||||
}
|
||||
|
||||
lean_obj_res lean_array_get_panic(lean_obj_arg def_val);
|
||||
LEAN_SHARED lean_obj_res lean_array_get_panic(lean_obj_arg def_val);
|
||||
|
||||
static inline lean_object * lean_array_get(lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
|
||||
if (lean_is_scalar(i)) {
|
||||
|
|
@ -750,7 +750,7 @@ static inline lean_object * lean_array_get(lean_obj_arg def_val, b_lean_obj_arg
|
|||
return lean_array_get_panic(def_val);
|
||||
}
|
||||
|
||||
lean_obj_res lean_copy_expand_array(lean_obj_arg a, bool expand);
|
||||
LEAN_SHARED lean_obj_res lean_copy_expand_array(lean_obj_arg a, bool expand);
|
||||
|
||||
static inline lean_obj_res lean_copy_array(lean_obj_arg a) {
|
||||
return lean_copy_expand_array(a, false);
|
||||
|
|
@ -773,7 +773,7 @@ static inline lean_object * lean_array_fset(lean_obj_arg a, b_lean_obj_arg i, le
|
|||
return lean_array_uset(a, lean_unbox(i), v);
|
||||
}
|
||||
|
||||
lean_obj_res lean_array_set_panic(lean_obj_arg a, lean_obj_arg v);
|
||||
LEAN_SHARED lean_obj_res lean_array_set_panic(lean_obj_arg a, lean_obj_arg v);
|
||||
|
||||
static inline lean_object * lean_array_set(lean_obj_arg a, b_lean_obj_arg i, lean_obj_arg v) {
|
||||
if (lean_is_scalar(i)) {
|
||||
|
|
@ -818,8 +818,8 @@ static inline lean_object * lean_array_swap(lean_obj_arg a, b_lean_obj_arg i, b_
|
|||
return lean_array_uswap(a, ui, uj);
|
||||
}
|
||||
|
||||
lean_object * lean_array_push(lean_obj_arg a, lean_obj_arg v);
|
||||
lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v);
|
||||
LEAN_SHARED lean_object * lean_array_push(lean_obj_arg a, lean_obj_arg v);
|
||||
LEAN_SHARED lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v);
|
||||
|
||||
/* Array of scalars */
|
||||
|
||||
|
|
@ -850,9 +850,9 @@ static inline uint8_t* lean_sarray_cptr(lean_object * o) { return lean_to_sarray
|
|||
|
||||
/* ByteArray (special case of Array of Scalars) */
|
||||
|
||||
lean_obj_res lean_byte_array_mk(lean_obj_arg a);
|
||||
lean_obj_res lean_byte_array_data(lean_obj_arg a);
|
||||
lean_obj_res lean_copy_byte_array(lean_obj_arg a);
|
||||
LEAN_SHARED lean_obj_res lean_byte_array_mk(lean_obj_arg a);
|
||||
LEAN_SHARED lean_obj_res lean_byte_array_data(lean_obj_arg a);
|
||||
LEAN_SHARED lean_obj_res lean_copy_byte_array(lean_obj_arg a);
|
||||
|
||||
static inline lean_obj_res lean_mk_empty_byte_array(b_lean_obj_arg capacity) {
|
||||
if (!lean_is_scalar(capacity)) lean_internal_panic_out_of_memory();
|
||||
|
|
@ -873,7 +873,7 @@ static inline uint8_t lean_byte_array_get(b_lean_obj_arg a, b_lean_obj_arg i) {
|
|||
}
|
||||
}
|
||||
|
||||
lean_obj_res lean_byte_array_push(lean_obj_arg a, uint8_t b);
|
||||
LEAN_SHARED lean_obj_res lean_byte_array_push(lean_obj_arg a, uint8_t b);
|
||||
|
||||
static inline lean_obj_res lean_byte_array_set(lean_obj_arg a, b_lean_obj_arg i, uint8_t b) {
|
||||
if (!lean_is_scalar(i)) {
|
||||
|
|
@ -895,9 +895,9 @@ static inline lean_obj_res lean_byte_array_set(lean_obj_arg a, b_lean_obj_arg i,
|
|||
|
||||
/* FloatArray (special case of Array of Scalars) */
|
||||
|
||||
lean_obj_res lean_float_array_mk(lean_obj_arg a);
|
||||
lean_obj_res lean_float_array_data(lean_obj_arg a);
|
||||
lean_obj_res lean_copy_float_array(lean_obj_arg a);
|
||||
LEAN_SHARED lean_obj_res lean_float_array_mk(lean_obj_arg a);
|
||||
LEAN_SHARED lean_obj_res lean_float_array_data(lean_obj_arg a);
|
||||
LEAN_SHARED lean_obj_res lean_copy_float_array(lean_obj_arg a);
|
||||
|
||||
static inline lean_obj_res lean_mk_empty_float_array(b_lean_obj_arg capacity) {
|
||||
if (!lean_is_scalar(capacity)) lean_internal_panic_out_of_memory();
|
||||
|
|
@ -922,7 +922,7 @@ static inline double lean_float_array_get(b_lean_obj_arg a, b_lean_obj_arg i) {
|
|||
}
|
||||
}
|
||||
|
||||
lean_obj_res lean_float_array_push(lean_obj_arg a, double d);
|
||||
LEAN_SHARED lean_obj_res lean_float_array_push(lean_obj_arg a, double d);
|
||||
|
||||
static inline lean_obj_res lean_float_array_set(lean_obj_arg a, b_lean_obj_arg i, double d) {
|
||||
if (!lean_is_scalar(i)) {
|
||||
|
|
@ -967,42 +967,42 @@ static inline lean_obj_res lean_alloc_string(size_t size, size_t capacity, size_
|
|||
o->m_length = len;
|
||||
return (lean_object*)o;
|
||||
}
|
||||
size_t lean_utf8_strlen(char const * str);
|
||||
size_t lean_utf8_n_strlen(char const * str, size_t n);
|
||||
LEAN_SHARED size_t lean_utf8_strlen(char const * str);
|
||||
LEAN_SHARED size_t lean_utf8_n_strlen(char const * str, size_t n);
|
||||
static inline size_t lean_string_capacity(lean_object * o) { return lean_to_string(o)->m_capacity; }
|
||||
static inline size_t lean_string_byte_size(lean_object * o) { return sizeof(lean_string_object) + lean_string_capacity(o); }
|
||||
/* instance : inhabited char := ⟨'A'⟩ */
|
||||
static inline uint32_t lean_char_default_value() { return 'A'; }
|
||||
lean_obj_res lean_mk_string(char const * s);
|
||||
LEAN_SHARED lean_obj_res lean_mk_string(char const * s);
|
||||
static inline char const * lean_string_cstr(b_lean_obj_arg o) {
|
||||
assert(lean_is_string(o));
|
||||
return lean_to_string(o)->m_data;
|
||||
}
|
||||
static inline size_t lean_string_size(b_lean_obj_arg o) { return lean_to_string(o)->m_size; }
|
||||
static inline size_t lean_string_len(b_lean_obj_arg o) { return lean_to_string(o)->m_length; }
|
||||
lean_obj_res lean_string_push(lean_obj_arg s, uint32_t c);
|
||||
lean_obj_res lean_string_append(lean_obj_arg s1, b_lean_obj_arg s2);
|
||||
LEAN_SHARED lean_obj_res lean_string_push(lean_obj_arg s, uint32_t c);
|
||||
LEAN_SHARED lean_obj_res lean_string_append(lean_obj_arg s1, b_lean_obj_arg s2);
|
||||
static inline lean_obj_res lean_string_length(b_lean_obj_arg s) { return lean_box(lean_string_len(s)); }
|
||||
lean_obj_res lean_string_mk(lean_obj_arg cs);
|
||||
lean_obj_res lean_string_data(lean_obj_arg s);
|
||||
uint32_t lean_string_utf8_get(b_lean_obj_arg s, b_lean_obj_arg i);
|
||||
lean_obj_res lean_string_utf8_next(b_lean_obj_arg s, b_lean_obj_arg i);
|
||||
lean_obj_res lean_string_utf8_prev(b_lean_obj_arg s, b_lean_obj_arg i);
|
||||
lean_obj_res lean_string_utf8_set(lean_obj_arg s, b_lean_obj_arg i, uint32_t c);
|
||||
LEAN_SHARED lean_obj_res lean_string_mk(lean_obj_arg cs);
|
||||
LEAN_SHARED lean_obj_res lean_string_data(lean_obj_arg s);
|
||||
LEAN_SHARED uint32_t lean_string_utf8_get(b_lean_obj_arg s, b_lean_obj_arg i);
|
||||
LEAN_SHARED lean_obj_res lean_string_utf8_next(b_lean_obj_arg s, b_lean_obj_arg i);
|
||||
LEAN_SHARED lean_obj_res lean_string_utf8_prev(b_lean_obj_arg s, b_lean_obj_arg i);
|
||||
LEAN_SHARED lean_obj_res lean_string_utf8_set(lean_obj_arg s, b_lean_obj_arg i, uint32_t c);
|
||||
static inline uint8_t lean_string_utf8_at_end(b_lean_obj_arg s, b_lean_obj_arg i) {
|
||||
return !lean_is_scalar(i) || lean_unbox(i) >= lean_string_size(s) - 1;
|
||||
}
|
||||
lean_obj_res lean_string_utf8_extract(b_lean_obj_arg s, b_lean_obj_arg b, b_lean_obj_arg e);
|
||||
LEAN_SHARED lean_obj_res lean_string_utf8_extract(b_lean_obj_arg s, b_lean_obj_arg b, b_lean_obj_arg e);
|
||||
static inline lean_obj_res lean_string_utf8_byte_size(b_lean_obj_arg s) { return lean_box(lean_string_size(s) - 1); }
|
||||
static inline bool lean_string_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) {
|
||||
return s1 == s2 ||
|
||||
(lean_string_size(s1) == lean_string_size(s2) && memcmp(lean_string_cstr(s1), lean_string_cstr(s2), lean_string_size(s1)) == 0);
|
||||
}
|
||||
static inline bool lean_string_ne(b_lean_obj_arg s1, b_lean_obj_arg s2) { return !lean_string_eq(s1, s2); }
|
||||
bool lean_string_lt(b_lean_obj_arg s1, b_lean_obj_arg s2);
|
||||
LEAN_SHARED bool lean_string_lt(b_lean_obj_arg s1, b_lean_obj_arg s2);
|
||||
static inline uint8_t lean_string_dec_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) { return lean_string_eq(s1, s2); }
|
||||
static inline uint8_t lean_string_dec_lt(b_lean_obj_arg s1, b_lean_obj_arg s2) { return lean_string_lt(s1, s2); }
|
||||
uint64_t lean_string_hash(b_lean_obj_arg);
|
||||
LEAN_SHARED uint64_t lean_string_hash(b_lean_obj_arg);
|
||||
|
||||
/* Thunks */
|
||||
|
||||
|
|
@ -1023,7 +1023,7 @@ static inline lean_obj_res lean_thunk_pure(lean_obj_arg v) {
|
|||
return (lean_object*)o;
|
||||
}
|
||||
|
||||
lean_object * lean_thunk_get_core(lean_object * t);
|
||||
LEAN_SHARED lean_object * lean_thunk_get_core(lean_object * t);
|
||||
|
||||
static inline b_lean_obj_res lean_thunk_get(b_lean_obj_arg t) {
|
||||
lean_object * r = lean_to_thunk(t)->m_value;
|
||||
|
|
@ -1040,21 +1040,21 @@ static inline lean_obj_res lean_thunk_get_own(b_lean_obj_arg t) {
|
|||
|
||||
/* Tasks */
|
||||
|
||||
void lean_init_task_manager();
|
||||
void lean_init_task_manager_using(unsigned num_workers);
|
||||
LEAN_SHARED void lean_init_task_manager();
|
||||
LEAN_SHARED void lean_init_task_manager_using(unsigned num_workers);
|
||||
|
||||
lean_obj_res lean_task_spawn_core(lean_obj_arg c, unsigned prio, bool keep_alive);
|
||||
LEAN_SHARED lean_obj_res lean_task_spawn_core(lean_obj_arg c, unsigned prio, bool keep_alive);
|
||||
/* Run a closure `Unit -> A` as a `Task A` */
|
||||
static inline lean_obj_res lean_task_spawn(lean_obj_arg c, lean_obj_arg prio) { return lean_task_spawn_core(c, lean_unbox(prio), false); }
|
||||
/* Convert a value `a : A` into `Task A` */
|
||||
lean_obj_res lean_task_pure(lean_obj_arg a);
|
||||
lean_obj_res lean_task_bind_core(lean_obj_arg x, lean_obj_arg f, unsigned prio, bool keep_alive);
|
||||
LEAN_SHARED lean_obj_res lean_task_pure(lean_obj_arg a);
|
||||
LEAN_SHARED lean_obj_res lean_task_bind_core(lean_obj_arg x, lean_obj_arg f, unsigned prio, bool keep_alive);
|
||||
/* Task.bind (x : Task A) (f : A -> Task B) (prio : Nat) : Task B */
|
||||
static inline lean_obj_res lean_task_bind(lean_obj_arg x, lean_obj_arg f, lean_obj_arg prio) { return lean_task_bind_core(x, f, lean_unbox(prio), false); }
|
||||
lean_obj_res lean_task_map_core(lean_obj_arg f, lean_obj_arg t, unsigned prio, bool keep_alive);
|
||||
LEAN_SHARED lean_obj_res lean_task_map_core(lean_obj_arg f, lean_obj_arg t, unsigned prio, bool keep_alive);
|
||||
/* Task.map (f : A -> B) (t : Task A) (prio : Nat) : Task B */
|
||||
static inline lean_obj_res lean_task_map(lean_obj_arg f, lean_obj_arg t, lean_obj_arg prio) { return lean_task_map_core(f, t, lean_unbox(prio), false); }
|
||||
b_lean_obj_res lean_task_get(b_lean_obj_arg t);
|
||||
LEAN_SHARED b_lean_obj_res lean_task_get(b_lean_obj_arg t);
|
||||
/* Primitive for implementing Task.get : Task A -> A */
|
||||
static inline lean_obj_res lean_task_get_own(lean_obj_arg t) {
|
||||
lean_object * r = lean_task_get(t);
|
||||
|
|
@ -1064,13 +1064,13 @@ static inline lean_obj_res lean_task_get_own(lean_obj_arg t) {
|
|||
}
|
||||
|
||||
/* primitive for implementing `IO.checkCanceled : IO Bool` */
|
||||
bool lean_io_check_canceled_core();
|
||||
LEAN_SHARED bool lean_io_check_canceled_core();
|
||||
/* primitive for implementing `IO.cancel : Task a -> IO Unit` */
|
||||
void lean_io_cancel_core(b_lean_obj_arg t);
|
||||
LEAN_SHARED void lean_io_cancel_core(b_lean_obj_arg t);
|
||||
/* primitive for implementing `IO.hasFinished : Task a -> IO Unit` */
|
||||
bool lean_io_has_finished_core(b_lean_obj_arg t);
|
||||
LEAN_SHARED bool lean_io_has_finished_core(b_lean_obj_arg t);
|
||||
/* primitive for implementing `IO.waitAny : List (Task a) -> IO (Task a)` */
|
||||
b_lean_obj_res lean_io_wait_any_core(b_lean_obj_arg task_list);
|
||||
LEAN_SHARED b_lean_obj_res lean_io_wait_any_core(b_lean_obj_arg task_list);
|
||||
|
||||
/* External objects */
|
||||
|
||||
|
|
@ -1094,23 +1094,23 @@ static inline void * lean_get_external_data(lean_object * o) {
|
|||
|
||||
#define LEAN_MAX_SMALL_NAT (SIZE_MAX >> 1)
|
||||
|
||||
lean_object * lean_nat_big_succ(lean_object * a);
|
||||
lean_object * lean_nat_big_add(lean_object * a1, lean_object * a2);
|
||||
lean_object * lean_nat_big_sub(lean_object * a1, lean_object * a2);
|
||||
lean_object * lean_nat_big_mul(lean_object * a1, lean_object * a2);
|
||||
lean_object * lean_nat_overflow_mul(size_t a1, size_t a2);
|
||||
lean_object * lean_nat_big_div(lean_object * a1, lean_object * a2);
|
||||
lean_object * lean_nat_big_mod(lean_object * a1, lean_object * a2);
|
||||
bool lean_nat_big_eq(lean_object * a1, lean_object * a2);
|
||||
bool lean_nat_big_le(lean_object * a1, lean_object * a2);
|
||||
bool lean_nat_big_lt(lean_object * a1, lean_object * a2);
|
||||
lean_object * lean_nat_big_land(lean_object * a1, lean_object * a2);
|
||||
lean_object * lean_nat_big_lor(lean_object * a1, lean_object * a2);
|
||||
lean_object * lean_nat_big_xor(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED lean_object * lean_nat_big_succ(lean_object * a);
|
||||
LEAN_SHARED lean_object * lean_nat_big_add(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED lean_object * lean_nat_big_sub(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED lean_object * lean_nat_big_mul(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED lean_object * lean_nat_overflow_mul(size_t a1, size_t a2);
|
||||
LEAN_SHARED lean_object * lean_nat_big_div(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED lean_object * lean_nat_big_mod(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED bool lean_nat_big_eq(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED bool lean_nat_big_le(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED bool lean_nat_big_lt(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED lean_object * lean_nat_big_land(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED lean_object * lean_nat_big_lor(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED lean_object * lean_nat_big_xor(lean_object * a1, lean_object * a2);
|
||||
|
||||
lean_obj_res lean_cstr_to_nat(char const * n);
|
||||
lean_obj_res lean_big_usize_to_nat(size_t n);
|
||||
lean_obj_res lean_big_uint64_to_nat(uint64_t n);
|
||||
LEAN_SHARED lean_obj_res lean_cstr_to_nat(char const * n);
|
||||
LEAN_SHARED lean_obj_res lean_big_usize_to_nat(size_t n);
|
||||
LEAN_SHARED lean_obj_res lean_big_uint64_to_nat(uint64_t 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);
|
||||
|
|
@ -1260,30 +1260,30 @@ static inline lean_obj_res lean_nat_lxor(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|||
}
|
||||
}
|
||||
|
||||
lean_obj_res lean_nat_shiftl(b_lean_obj_arg a1, b_lean_obj_arg a2);
|
||||
lean_obj_res lean_nat_shiftr(b_lean_obj_arg a1, b_lean_obj_arg a2);
|
||||
lean_obj_res lean_nat_pow(b_lean_obj_arg a1, b_lean_obj_arg a2);
|
||||
lean_obj_res lean_nat_gcd(b_lean_obj_arg a1, b_lean_obj_arg a2);
|
||||
LEAN_SHARED lean_obj_res lean_nat_shiftl(b_lean_obj_arg a1, b_lean_obj_arg a2);
|
||||
LEAN_SHARED lean_obj_res lean_nat_shiftr(b_lean_obj_arg a1, b_lean_obj_arg a2);
|
||||
LEAN_SHARED lean_obj_res lean_nat_pow(b_lean_obj_arg a1, b_lean_obj_arg a2);
|
||||
LEAN_SHARED lean_obj_res lean_nat_gcd(b_lean_obj_arg a1, b_lean_obj_arg a2);
|
||||
|
||||
/* Integers */
|
||||
|
||||
#define LEAN_MAX_SMALL_INT (sizeof(void*) == 8 ? INT_MAX : (1 << 30))
|
||||
#define LEAN_MIN_SMALL_INT (sizeof(void*) == 8 ? INT_MIN : -(1 << 30))
|
||||
lean_object * lean_int_big_neg(lean_object * a);
|
||||
lean_object * lean_int_big_add(lean_object * a1, lean_object * a2);
|
||||
lean_object * lean_int_big_sub(lean_object * a1, lean_object * a2);
|
||||
lean_object * lean_int_big_mul(lean_object * a1, lean_object * a2);
|
||||
lean_object * lean_int_big_div(lean_object * a1, lean_object * a2);
|
||||
lean_object * lean_int_big_mod(lean_object * a1, lean_object * a2);
|
||||
bool lean_int_big_eq(lean_object * a1, lean_object * a2);
|
||||
bool lean_int_big_le(lean_object * a1, lean_object * a2);
|
||||
bool lean_int_big_lt(lean_object * a1, lean_object * a2);
|
||||
bool lean_int_big_nonneg(lean_object * a);
|
||||
LEAN_SHARED lean_object * lean_int_big_neg(lean_object * a);
|
||||
LEAN_SHARED lean_object * lean_int_big_add(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED lean_object * lean_int_big_sub(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED lean_object * lean_int_big_mul(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED lean_object * lean_int_big_div(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED lean_object * lean_int_big_mod(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED bool lean_int_big_eq(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED bool lean_int_big_le(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED bool lean_int_big_lt(lean_object * a1, lean_object * a2);
|
||||
LEAN_SHARED bool lean_int_big_nonneg(lean_object * a);
|
||||
|
||||
lean_object * lean_cstr_to_int(char const * n);
|
||||
lean_object * lean_big_int_to_int(int n);
|
||||
lean_object * lean_big_size_t_to_int(size_t n);
|
||||
lean_object * lean_big_int64_to_int(int64_t n);
|
||||
LEAN_SHARED lean_object * lean_cstr_to_int(char const * n);
|
||||
LEAN_SHARED lean_object * lean_big_int_to_int(int n);
|
||||
LEAN_SHARED lean_object * lean_big_size_t_to_int(size_t n);
|
||||
LEAN_SHARED lean_object * lean_big_int64_to_int(int64_t n);
|
||||
|
||||
static inline lean_obj_res lean_int_to_int(int n) {
|
||||
if (sizeof(void*) == 8)
|
||||
|
|
@ -1444,7 +1444,7 @@ static inline bool lean_int_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|||
}
|
||||
}
|
||||
|
||||
lean_obj_res lean_big_int_to_nat(lean_obj_arg a);
|
||||
LEAN_SHARED lean_obj_res lean_big_int_to_nat(lean_obj_arg 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)) {
|
||||
|
|
@ -1479,7 +1479,7 @@ static inline uint8_t lean_int_dec_nonneg(b_lean_obj_arg a) {
|
|||
|
||||
/* UInt8 */
|
||||
|
||||
uint8_t lean_uint8_of_big_nat(b_lean_obj_arg a);
|
||||
LEAN_SHARED uint8_t lean_uint8_of_big_nat(b_lean_obj_arg a);
|
||||
static inline uint8_t lean_uint8_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (uint8_t)(lean_unbox(a)) : lean_uint8_of_big_nat(a); }
|
||||
/* Remark: the following function is used to implement the constructor `UInt8.mk`. We can't annotate constructors with `@&` */
|
||||
static inline uint8_t lean_uint8_of_nat_mk(lean_obj_arg a) { uint8_t r = lean_uint8_of_nat(a); lean_dec(a); return r; }
|
||||
|
|
@ -1503,7 +1503,7 @@ static inline uint8_t lean_uint8_dec_le(uint8_t a1, uint8_t a2) { return a1 <= a
|
|||
|
||||
/* UInt16 */
|
||||
|
||||
uint16_t lean_uint16_of_big_nat(b_lean_obj_arg a);
|
||||
LEAN_SHARED uint16_t lean_uint16_of_big_nat(b_lean_obj_arg a);
|
||||
static inline uint16_t lean_uint16_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (int16_t)(lean_unbox(a)) : lean_uint16_of_big_nat(a); }
|
||||
/* Remark: the following function is used to implement the constructor `UInt16.mk`. We can't annotate constructors with `@&` */
|
||||
static inline uint16_t lean_uint16_of_nat_mk(lean_obj_arg a) { uint16_t r = lean_uint16_of_nat(a); lean_dec(a); return r; }
|
||||
|
|
@ -1527,7 +1527,7 @@ static inline uint8_t lean_uint16_dec_le(uint16_t a1, uint16_t a2) { return a1 <
|
|||
|
||||
/* UInt32 */
|
||||
|
||||
uint32_t lean_uint32_of_big_nat(b_lean_obj_arg a);
|
||||
LEAN_SHARED uint32_t lean_uint32_of_big_nat(b_lean_obj_arg a);
|
||||
static inline uint32_t lean_uint32_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (uint32_t)(lean_unbox(a)) : lean_uint32_of_big_nat(a); }
|
||||
/* Remark: the following function is used to implement the constructor `UInt32.mk`. We can't annotate constructors with `@&` */
|
||||
static inline uint32_t lean_uint32_of_nat_mk(lean_obj_arg a) { uint32_t r = lean_uint32_of_nat(a); lean_dec(a); return r; }
|
||||
|
|
@ -1537,7 +1537,7 @@ static inline uint32_t lean_uint32_sub(uint32_t a1, uint32_t a2) { return a1-a2;
|
|||
static inline uint32_t lean_uint32_mul(uint32_t a1, uint32_t a2) { return a1*a2; }
|
||||
static inline uint32_t lean_uint32_div(uint32_t a1, uint32_t a2) { return a2 == 0 ? 0 : a1/a2; }
|
||||
static inline uint32_t lean_uint32_mod(uint32_t a1, uint32_t a2) { return a2 == 0 ? a1 : a1%a2; }
|
||||
uint32_t lean_uint32_big_modn(uint32_t a1, b_lean_obj_arg a2);
|
||||
LEAN_SHARED uint32_t lean_uint32_big_modn(uint32_t a1, b_lean_obj_arg a2);
|
||||
static inline uint32_t lean_uint32_modn(uint32_t a1, b_lean_obj_arg a2) {
|
||||
if (LEAN_LIKELY(lean_is_scalar(a2))) {
|
||||
size_t n2 = lean_unbox(a2);
|
||||
|
|
@ -1556,7 +1556,7 @@ static inline uint8_t lean_uint32_dec_le(uint32_t a1, uint32_t a2) { return a1 <
|
|||
|
||||
/* UInt64 */
|
||||
|
||||
uint64_t lean_uint64_of_big_nat(b_lean_obj_arg a);
|
||||
LEAN_SHARED uint64_t lean_uint64_of_big_nat(b_lean_obj_arg a);
|
||||
static inline uint64_t lean_uint64_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (uint64_t)(lean_unbox(a)) : lean_uint64_of_big_nat(a); }
|
||||
/* Remark: the following function is used to implement the constructor `UInt64.mk`. We can't annotate constructors with `@&` */
|
||||
static inline uint64_t lean_uint64_of_nat_mk(lean_obj_arg a) { uint64_t r = lean_uint64_of_nat(a); lean_dec(a); return r; }
|
||||
|
|
@ -1565,7 +1565,7 @@ static inline uint64_t lean_uint64_sub(uint64_t a1, uint64_t a2) { return a1-a2;
|
|||
static inline uint64_t lean_uint64_mul(uint64_t a1, uint64_t a2) { return a1*a2; }
|
||||
static inline uint64_t lean_uint64_div(uint64_t a1, uint64_t a2) { return a2 == 0 ? 0 : a1/a2; }
|
||||
static inline uint64_t lean_uint64_mod(uint64_t a1, uint64_t a2) { return a2 == 0 ? a1 : a1%a2; }
|
||||
uint64_t lean_uint64_big_modn(uint64_t a1, b_lean_obj_arg a2);
|
||||
LEAN_SHARED uint64_t lean_uint64_big_modn(uint64_t a1, b_lean_obj_arg a2);
|
||||
static inline uint64_t lean_uint64_modn(uint64_t a1, b_lean_obj_arg a2) {
|
||||
if (LEAN_LIKELY(lean_is_scalar(a2))) {
|
||||
size_t n2 = lean_unbox(a2);
|
||||
|
|
@ -1577,11 +1577,11 @@ static inline uint64_t lean_uint64_modn(uint64_t a1, b_lean_obj_arg a2) {
|
|||
static inline uint8_t lean_uint64_dec_eq(uint64_t a1, uint64_t a2) { return a1 == a2; }
|
||||
static inline uint8_t lean_uint64_dec_lt(uint64_t a1, uint64_t a2) { return a1 < a2; }
|
||||
static inline uint8_t lean_uint64_dec_le(uint64_t a1, uint64_t a2) { return a1 <= a2; }
|
||||
uint64_t lean_uint64_mix_hash(uint64_t a1, uint64_t a2);
|
||||
LEAN_SHARED uint64_t lean_uint64_mix_hash(uint64_t a1, uint64_t a2);
|
||||
|
||||
/* USize */
|
||||
|
||||
size_t lean_usize_of_big_nat(b_lean_obj_arg a);
|
||||
LEAN_SHARED size_t lean_usize_of_big_nat(b_lean_obj_arg a);
|
||||
static inline size_t lean_usize_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? lean_unbox(a) : lean_usize_of_big_nat(a); }
|
||||
/* Remark: the following function is used to implement the constructor `USize.mk`. We can't annotate constructors with `@&` */
|
||||
static inline size_t lean_usize_of_nat_mk(lean_obj_arg a) { size_t r = lean_usize_of_nat(a); lean_dec(a); return r; }
|
||||
|
|
@ -1590,7 +1590,7 @@ static inline size_t lean_usize_sub(size_t a1, size_t a2) { return a1-a2; }
|
|||
static inline size_t lean_usize_mul(size_t a1, size_t a2) { return a1*a2; }
|
||||
static inline size_t lean_usize_div(size_t a1, size_t a2) { return a2 == 0 ? 0 : a1/a2; }
|
||||
static inline size_t lean_usize_mod(size_t a1, size_t a2) { return a2 == 0 ? a1 : a1%a2; }
|
||||
size_t lean_usize_big_modn(size_t a1, b_lean_obj_arg a2);
|
||||
LEAN_SHARED size_t lean_usize_big_modn(size_t a1, b_lean_obj_arg a2);
|
||||
static inline size_t lean_usize_modn(size_t a1, b_lean_obj_arg a2) {
|
||||
if (LEAN_LIKELY(lean_is_scalar(a2))) {
|
||||
size_t n2 = lean_unbox(a2);
|
||||
|
|
@ -1602,12 +1602,12 @@ static inline size_t lean_usize_modn(size_t a1, b_lean_obj_arg a2) {
|
|||
static inline uint8_t lean_usize_dec_eq(size_t a1, size_t a2) { return a1 == a2; }
|
||||
static inline uint8_t lean_usize_dec_lt(size_t a1, size_t a2) { return a1 < a2; }
|
||||
static inline uint8_t lean_usize_dec_le(size_t a1, size_t a2) { return a1 <= a2; }
|
||||
size_t lean_usize_mix_hash(size_t a1, size_t a2);
|
||||
LEAN_SHARED size_t lean_usize_mix_hash(size_t a1, size_t a2);
|
||||
|
||||
/* Float */
|
||||
|
||||
double lean_float_of_nat(b_lean_obj_arg a);
|
||||
lean_obj_res lean_float_to_string(double a);
|
||||
LEAN_SHARED double lean_float_of_nat(b_lean_obj_arg a);
|
||||
LEAN_SHARED lean_obj_res lean_float_to_string(double a);
|
||||
|
||||
/* Boxing primitives */
|
||||
|
||||
|
|
@ -1665,21 +1665,21 @@ static inline double lean_unbox_float(b_lean_obj_arg o) {
|
|||
|
||||
/* Debugging helper functions */
|
||||
|
||||
lean_object * lean_dbg_trace(lean_obj_arg s, lean_obj_arg fn);
|
||||
lean_object * lean_dbg_sleep(uint32_t ms, lean_obj_arg fn);
|
||||
lean_object * lean_dbg_trace_if_shared(lean_obj_arg s, lean_obj_arg a);
|
||||
LEAN_SHARED lean_object * lean_dbg_trace(lean_obj_arg s, lean_obj_arg fn);
|
||||
LEAN_SHARED lean_object * lean_dbg_sleep(uint32_t ms, lean_obj_arg fn);
|
||||
LEAN_SHARED lean_object * lean_dbg_trace_if_shared(lean_obj_arg s, lean_obj_arg a);
|
||||
|
||||
/* IO Helper functions */
|
||||
|
||||
lean_obj_res lean_decode_io_error(int errnum, b_lean_obj_arg fname);
|
||||
LEAN_SHARED lean_obj_res lean_decode_io_error(int errnum, b_lean_obj_arg fname);
|
||||
|
||||
static inline lean_obj_res lean_io_mk_world() { return lean_box(0); }
|
||||
static inline bool lean_io_result_is_ok(b_lean_obj_arg r) { return lean_ptr_tag(r) == 0; }
|
||||
static inline bool lean_io_result_is_error(b_lean_obj_arg r) { return lean_ptr_tag(r) == 1; }
|
||||
static inline b_lean_obj_res lean_io_result_get_value(b_lean_obj_arg r) { assert(lean_io_result_is_ok(r)); return lean_ctor_get(r, 0); }
|
||||
static inline b_lean_obj_res lean_io_result_get_error(b_lean_obj_arg r) { assert(lean_io_result_is_error(r)); return lean_ctor_get(r, 0); }
|
||||
void lean_io_result_show_error(b_lean_obj_arg r);
|
||||
void lean_io_mark_end_initialization();
|
||||
LEAN_SHARED void lean_io_result_show_error(b_lean_obj_arg r);
|
||||
LEAN_SHARED void lean_io_mark_end_initialization();
|
||||
static inline lean_obj_res lean_io_result_mk_ok(lean_obj_arg a) {
|
||||
lean_object * r = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(r, 0, a);
|
||||
|
|
@ -1693,45 +1693,45 @@ static inline lean_obj_res lean_io_result_mk_error(lean_obj_arg e) {
|
|||
return r;
|
||||
}
|
||||
|
||||
lean_obj_res lean_mk_io_error_already_exists(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_already_exists_file(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_eof(lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_hardware_fault(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_illegal_operation(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_inappropriate_type(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_inappropriate_type_file(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_interrupted(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_invalid_argument(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_invalid_argument_file(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_no_file_or_directory(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_no_such_thing(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_no_such_thing_file(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_other_error(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_permission_denied(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_permission_denied_file(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_protocol_error(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_resource_busy(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_resource_exhausted(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_resource_exhausted_file(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_resource_vanished(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_time_expired(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_unsatisfied_constraints(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_error_unsupported_operation(uint32_t, lean_obj_arg);
|
||||
lean_obj_res lean_mk_io_user_error(lean_obj_arg str);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_already_exists(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_already_exists_file(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_eof(lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_hardware_fault(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_illegal_operation(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_inappropriate_type(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_inappropriate_type_file(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_interrupted(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_invalid_argument(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_invalid_argument_file(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_no_file_or_directory(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_no_such_thing(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_no_such_thing_file(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_other_error(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_permission_denied(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_permission_denied_file(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_protocol_error(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_resource_busy(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_resource_exhausted(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_resource_exhausted_file(lean_obj_arg, uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_resource_vanished(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_time_expired(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_unsatisfied_constraints(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_error_unsupported_operation(uint32_t, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_mk_io_user_error(lean_obj_arg str);
|
||||
|
||||
|
||||
/* ST Ref primitives */
|
||||
lean_obj_res lean_st_mk_ref(lean_obj_arg, lean_obj_arg);
|
||||
lean_obj_res lean_st_ref_get(b_lean_obj_arg, lean_obj_arg);
|
||||
lean_obj_res lean_st_ref_set(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
|
||||
lean_obj_res lean_st_ref_reset(b_lean_obj_arg, lean_obj_arg);
|
||||
lean_obj_res lean_st_ref_swap(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_st_mk_ref(lean_obj_arg, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_st_ref_get(b_lean_obj_arg, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_st_ref_set(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_st_ref_reset(b_lean_obj_arg, lean_obj_arg);
|
||||
LEAN_SHARED lean_obj_res lean_st_ref_swap(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
|
||||
|
||||
/* pointer address unsafe primitive */
|
||||
static inline size_t lean_ptr_addr(b_lean_obj_arg a) { return (size_t)a; }
|
||||
|
||||
/* Name primitives */
|
||||
uint8_t lean_name_eq(b_lean_obj_arg n1, b_lean_obj_arg n2);
|
||||
LEAN_SHARED uint8_t lean_name_eq(b_lean_obj_arg n1, b_lean_obj_arg n2);
|
||||
|
||||
static inline uint64_t lean_name_hash_ptr(b_lean_obj_arg n) {
|
||||
assert(!lean_is_scalar(n));
|
||||
|
|
|
|||
|
|
@ -12,12 +12,12 @@ Author: Leonardo de Moura
|
|||
extern "C" {
|
||||
#endif
|
||||
|
||||
lean_object * lean_alloc_mpz(mpz_t);
|
||||
LEAN_SHARED lean_object * lean_alloc_mpz(mpz_t);
|
||||
/* Set `v` with the value stored in `o`.
|
||||
- pre: `lean_is_mpz(o)`
|
||||
- pre: `v` has already been initialized using `mpz_init` (or equivalent).
|
||||
*/
|
||||
void lean_extract_mpz_value(lean_object * o, mpz_t v);
|
||||
LEAN_SHARED void lean_extract_mpz_value(lean_object * o, mpz_t v);
|
||||
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue