1854 lines
77 KiB
C++
1854 lines
77 KiB
C++
/*
|
|
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#pragma once
|
|
#include <stddef.h>
|
|
#include <stdbool.h>
|
|
#include <stdint.h>
|
|
#include <limits.h>
|
|
|
|
#ifdef __cplusplus
|
|
#include <atomic>
|
|
#include <stdlib.h>
|
|
#define _Atomic(t) std::atomic<t>
|
|
#define LEAN_USING_STD using namespace std; /* NOLINT */
|
|
extern "C" {
|
|
#else
|
|
#define LEAN_USING_STD
|
|
#endif
|
|
#include <lean/config.h>
|
|
|
|
#define LEAN_CLOSURE_MAX_ARGS 16
|
|
#define LEAN_OBJECT_SIZE_DELTA 8
|
|
#define LEAN_MAX_SMALL_OBJECT_SIZE 4096
|
|
|
|
#ifdef _MSC_VER
|
|
#define LEAN_ALLOCA(s) _alloca(s)
|
|
#else
|
|
#define LEAN_ALLOCA(s) alloca(s)
|
|
#endif
|
|
|
|
#if defined(__GNUC__) || defined(__clang__)
|
|
#define LEAN_UNLIKELY(x) (__builtin_expect((x), 0))
|
|
#define LEAN_LIKELY(x) (__builtin_expect((x), 1))
|
|
#define LEAN_ALWAYS_INLINE __attribute__((always_inline))
|
|
#else
|
|
#define LEAN_UNLIKELY(x) (x)
|
|
#define LEAN_LIKELY(x) (x)
|
|
#define LEAN_ALWAYS_INLINE
|
|
#endif
|
|
|
|
#ifndef assert
|
|
#ifdef NDEBUG
|
|
#define assert(expr)
|
|
#else
|
|
void lean_notify_assert(const char * fileName, int line, const char * condition);
|
|
#define assert(expr) { if (LEAN_UNLIKELY(!(expr))) lean_notify_assert(__FILE__, __LINE__, #expr); }
|
|
#endif
|
|
#endif
|
|
|
|
#ifdef _WIN32
|
|
#define LEAN_EXPORT __declspec(dllexport)
|
|
#else
|
|
#define LEAN_EXPORT __attribute__((visibility("default")))
|
|
#endif
|
|
|
|
// We set `LEAN_EXPORTING` when compiling objects of libleanshared, but not when including this header in any other context.
|
|
#if defined LEAN_EXPORTING
|
|
#define LEAN_SHARED LEAN_EXPORT
|
|
#else
|
|
#define LEAN_SHARED
|
|
#endif
|
|
|
|
#define LEAN_BYTE(Var, Index) *(((uint8_t*)&Var)+Index)
|
|
|
|
#define LeanMaxCtorTag 244
|
|
#define LeanClosure 245
|
|
#define LeanArray 246
|
|
#define LeanStructArray 247
|
|
#define LeanScalarArray 248
|
|
#define LeanString 249
|
|
#define LeanMPZ 250
|
|
#define LeanThunk 251
|
|
#define LeanTask 252
|
|
#define LeanRef 253
|
|
#define LeanExternal 254
|
|
#define LeanReserved 255
|
|
|
|
#define LEAN_MAX_CTOR_FIELDS 256
|
|
#define LEAN_MAX_CTOR_SCALARS_SIZE 1024
|
|
|
|
static inline bool lean_is_big_object_tag(uint8_t tag) {
|
|
return tag == LeanArray || tag == LeanStructArray || tag == LeanScalarArray || tag == LeanString;
|
|
}
|
|
|
|
#define LEAN_CASSERT(predicate) LEAN_impl_CASSERT_LINE(predicate, __LINE__, __FILE__)
|
|
|
|
#define LEAN_impl_PASTE(a, b) a##b
|
|
#define LEAN_impl_CASSERT_LINE(predicate, line, file) \
|
|
typedef char LEAN_impl_PASTE(assertion_failed_##file##_, line)[2*!!(predicate)-1];
|
|
|
|
LEAN_CASSERT(sizeof(size_t) == sizeof(void*));
|
|
|
|
/*
|
|
Lean object header.
|
|
|
|
The reference counter `m_rc` field also encodes whether the object is single threaded (> 0), multi threaded (< 0), or
|
|
reference counting is not needed (== 0). We don't use reference counting for objects stored in compact regions, or
|
|
marked as persistent.
|
|
|
|
For "small" objects stored in compact regions, the field `m_cs_sz` contains the object size. For "small" objects not
|
|
stored in compact regions, we use the page information to retrieve its size.
|
|
|
|
During deallocation and 64-bit machines, the fields `m_rc` and `m_cs_sz` store the next object in the deletion TODO list.
|
|
These two fields together have 48-bits, and this is enough for modern computers.
|
|
In 32-bit machines, the field `m_rc` is sufficient.
|
|
|
|
The field `m_other` is used to store the number of fields in a constructor object and the element size in a scalar array.
|
|
*/
|
|
typedef struct {
|
|
int m_rc;
|
|
unsigned m_cs_sz:16;
|
|
unsigned m_other:8;
|
|
unsigned m_tag:8;
|
|
} lean_object;
|
|
|
|
/*
|
|
In our runtime, a Lean function consume the reference counter (RC) of its argument or not.
|
|
We say this behavior is part of the "calling convention" for the function. We say an argument uses:
|
|
x
|
|
1- "standard" calling convention if it consumes/decrements the RC.
|
|
In this calling convention each argument should be viewed as a resource that is consumed by the function.
|
|
This is roughly equivalent to `S && a` in C++, where `S` is a smart pointer, and `a` is the argument.
|
|
When this calling convention is used for an argument `x`, then it is safe to perform destructive updates to
|
|
`x` if its RC is 1.
|
|
|
|
2- "borrowed" calling convention if it doesn't consume/decrement the RC, and it is the responsability of the caller
|
|
to decrement the RC.
|
|
This is roughly equivalent to `S const & a` in C++, where `S` is a smart pointer, and `a` is the argument.
|
|
|
|
For returning objects, we also have two conventions
|
|
|
|
1- "standard" result. The caller is responsible for consuming the RC of the result.
|
|
This is roughly equivalent to returning a smart point `S` by value in C++.
|
|
|
|
2- "borrowed" result. The caller is not responsible for decreasing the RC.
|
|
This is roughly equivalent to returning a smart point reference `S const &` in C++.
|
|
|
|
Functions stored in closures use the "standard" calling convention.
|
|
*/
|
|
|
|
/* The following typedef's are used to document the calling convention for the primitives. */
|
|
typedef lean_object * lean_obj_arg; /* Standard object argument. */
|
|
typedef lean_object * b_lean_obj_arg; /* Borrowed object argument. */
|
|
typedef lean_object * u_lean_obj_arg; /* Unique (aka non shared) object argument. */
|
|
typedef lean_object * lean_obj_res; /* Standard object result. */
|
|
typedef lean_object * b_lean_obj_res; /* Borrowed object result. */
|
|
|
|
typedef struct {
|
|
lean_object m_header;
|
|
lean_object * m_objs[0];
|
|
} lean_ctor_object;
|
|
|
|
/* Array arrays */
|
|
typedef struct {
|
|
lean_object m_header;
|
|
size_t m_size;
|
|
size_t m_capacity;
|
|
lean_object * m_data[0];
|
|
} lean_array_object;
|
|
|
|
/* Scalar arrays */
|
|
typedef struct {
|
|
lean_object m_header;
|
|
size_t m_size;
|
|
size_t m_capacity;
|
|
uint8_t m_data[0];
|
|
} lean_sarray_object;
|
|
|
|
typedef struct {
|
|
lean_object m_header;
|
|
size_t m_size; /* byte length including '\0' terminator */
|
|
size_t m_capacity;
|
|
size_t m_length; /* UTF8 length */
|
|
char m_data[0];
|
|
} lean_string_object;
|
|
|
|
typedef struct {
|
|
lean_object m_header;
|
|
void * m_fun;
|
|
uint16_t m_arity; /* Number of arguments expected by m_fun. */
|
|
uint16_t m_num_fixed; /* Number of arguments that have been already fixed. */
|
|
lean_object * m_objs[0];
|
|
} lean_closure_object;
|
|
|
|
typedef struct {
|
|
lean_object m_header;
|
|
lean_object * m_value;
|
|
} lean_ref_object;
|
|
|
|
typedef struct {
|
|
lean_object m_header;
|
|
_Atomic(lean_object *) m_value;
|
|
_Atomic(lean_object *) m_closure;
|
|
} lean_thunk_object;
|
|
|
|
struct lean_task;
|
|
|
|
/* Data required for executing a Lean task. It is released as soon as
|
|
the task terminates even if the task object itself is still referenced. */
|
|
typedef struct {
|
|
lean_object * m_closure;
|
|
struct lean_task * m_head_dep;
|
|
struct lean_task * m_next_dep;
|
|
unsigned m_prio;
|
|
uint8_t m_canceled;
|
|
// If true, task will not be freed until finished
|
|
uint8_t m_keep_alive;
|
|
uint8_t m_deleted;
|
|
} lean_task_imp;
|
|
|
|
/* Object of type `Task _`. The lifetime of a `lean_task` object can be represented as a state machine with atomic
|
|
state transitions.
|
|
|
|
In the following, `condition` describes a predicate uniquely identifying a state.
|
|
|
|
creation:
|
|
* Task.spawn ==> Queued
|
|
* Task.map/bind ==> Waiting
|
|
* Task.pure ==> Finished
|
|
|
|
states:
|
|
* Queued
|
|
* condition: in task_manager::m_queues && m_imp != nullptr && !m_imp->m_deleted
|
|
* invariant: m_value == nullptr
|
|
* transition: RC becomes 0 ==> Deactivated (`deactivate_task` lock)
|
|
* transition: dequeued by worker thread ==> Running (`spawn_worker` lock)
|
|
* Waiting
|
|
* condition: reachable from task via `m_head_dep->m_next_dep->...` && !m_imp->m_deleted
|
|
* invariant: m_imp != nullptr && m_value == nullptr
|
|
* invariant: task dependency is Queued/Waiting/Running
|
|
* It cannot become Deactivated because this task should be holding an owned reference to it
|
|
* transition: RC becomes 0 ==> Deactivated (`deactivate_task` lock)
|
|
* transition: task dependency Finished ==> Queued (`handle_finished` under `spawn_worker` lock)
|
|
* Running
|
|
* condition: m_imp != nullptr && m_imp->m_closure == nullptr
|
|
* The worker takes ownership of the closure when running it
|
|
* invariant: m_value == nullptr
|
|
* transition: RC becomes 0 ==> Deactivated (`deactivate_task` lock)
|
|
* transition: finished execution ==> Finished (`spawn_worker` lock)
|
|
* Deactivated
|
|
* condition: m_imp != nullptr && m_imp->m_deleted
|
|
* invariant: RC == 0
|
|
* invariant: m_imp->m_closure == nullptr && m_imp->m_head_dep == nullptr (both freed by `deactivate_task_core`)
|
|
* Note that all dependent tasks must have already been Deactivated by the converse of the second Waiting invariant
|
|
* invariant: m_value == nullptr
|
|
* transition: dequeued by worker thread ==> freed
|
|
* transition: finished execution ==> freed
|
|
* transition: task dependency Finished ==> freed
|
|
* We must keep the task object alive until one of these transitions because in either case, we have live
|
|
(internal, unowned) references to the task up to that point
|
|
* transition: task dependency Deactivated ==> freed
|
|
* Finished
|
|
* condition: m_value != nullptr
|
|
* invariant: m_imp == nullptr
|
|
* transition: RC becomes 0 ==> freed (`deactivate_task` lock) */
|
|
typedef struct lean_task {
|
|
lean_object m_header;
|
|
_Atomic(lean_object *) m_value;
|
|
lean_task_imp * m_imp;
|
|
} lean_task_object;
|
|
|
|
typedef void (*lean_external_finalize_proc)(void *);
|
|
typedef void (*lean_external_foreach_proc)(void *, b_lean_obj_arg);
|
|
|
|
typedef struct {
|
|
lean_external_finalize_proc m_finalize;
|
|
lean_external_foreach_proc m_foreach;
|
|
} lean_external_class;
|
|
|
|
LEAN_SHARED lean_external_class * lean_register_external_class(lean_external_finalize_proc, lean_external_foreach_proc);
|
|
|
|
/* Object for wrapping external data. */
|
|
typedef struct {
|
|
lean_object m_header;
|
|
lean_external_class * m_class;
|
|
void * m_data;
|
|
} lean_external_object;
|
|
|
|
static inline bool lean_is_scalar(lean_object * o) { return ((size_t)(o) & 1) == 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; }
|
|
|
|
LEAN_SHARED void lean_set_exit_on_panic(bool flag);
|
|
/* Enable/disable panic messages */
|
|
LEAN_SHARED void lean_set_panic_messages(bool flag);
|
|
|
|
LEAN_SHARED lean_object * lean_panic_fn(lean_object * default_val, lean_object * msg);
|
|
|
|
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);
|
|
}
|
|
|
|
static inline unsigned lean_get_slot_idx(unsigned sz) {
|
|
assert(sz > 0);
|
|
assert(lean_align(sz, LEAN_OBJECT_SIZE_DELTA) == sz);
|
|
return sz / LEAN_OBJECT_SIZE_DELTA - 1;
|
|
}
|
|
|
|
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();
|
|
|
|
#ifndef __cplusplus
|
|
void * malloc(size_t); // avoid including big `stdlib.h`
|
|
#endif
|
|
|
|
static inline lean_object * lean_alloc_small_object(unsigned sz) {
|
|
#ifdef LEAN_SMALL_ALLOCATOR
|
|
sz = lean_align(sz, LEAN_OBJECT_SIZE_DELTA);
|
|
unsigned slot_idx = lean_get_slot_idx(sz);
|
|
assert(sz <= LEAN_MAX_SMALL_OBJECT_SIZE);
|
|
return (lean_object*)lean_alloc_small(sz, slot_idx);
|
|
#else
|
|
lean_inc_heartbeat();
|
|
void * mem = malloc(sizeof(size_t) + sz);
|
|
if (mem == 0) lean_internal_panic_out_of_memory();
|
|
*(size_t*)mem = sz;
|
|
return (lean_object*)((size_t*)mem + 1);
|
|
#endif
|
|
}
|
|
|
|
static inline lean_object * lean_alloc_ctor_memory(unsigned sz) {
|
|
#ifdef LEAN_SMALL_ALLOCATOR
|
|
unsigned sz1 = lean_align(sz, LEAN_OBJECT_SIZE_DELTA);
|
|
unsigned slot_idx = lean_get_slot_idx(sz1);
|
|
assert(sz1 <= LEAN_MAX_SMALL_OBJECT_SIZE);
|
|
lean_object* r = (lean_object*)lean_alloc_small(sz1, slot_idx);
|
|
if (sz1 > sz) {
|
|
/* Initialize last word.
|
|
In our runtime `lean_object_byte_size` is always
|
|
a multiple of the machine word size for constructors.
|
|
|
|
By setting the last word to 0, we make sure the sharing
|
|
maximizer procedures at `maxsharing.cpp` and `compact.cpp` are
|
|
not affected by uninitialized data at the (sz1 - sz) last bytes.
|
|
Otherwise, we may mistakenly assume to structurally equal
|
|
objects are not identical because of this uninitialized memory. */
|
|
size_t * end = (size_t*)(((char*)r) + sz1);
|
|
end[-1] = 0;
|
|
}
|
|
return r;
|
|
#else
|
|
return lean_alloc_small_object(sz);
|
|
#endif
|
|
}
|
|
|
|
static inline unsigned lean_small_object_size(lean_object * o) {
|
|
#ifdef LEAN_SMALL_ALLOCATOR
|
|
return lean_small_mem_size(o);
|
|
#else
|
|
return *((size_t*)o - 1);
|
|
#endif
|
|
}
|
|
|
|
#ifndef __cplusplus
|
|
void free(void *); // avoid including big `stdlib.h`
|
|
#endif
|
|
|
|
static inline void lean_free_small_object(lean_object * o) {
|
|
#ifdef LEAN_SMALL_ALLOCATOR
|
|
lean_free_small(o);
|
|
#else
|
|
free((size_t*)o - 1);
|
|
#endif
|
|
}
|
|
|
|
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;
|
|
}
|
|
|
|
static inline unsigned lean_ptr_other(lean_object * o) {
|
|
return o->m_other;
|
|
}
|
|
|
|
/* The object size may be slightly bigger for constructor objects.
|
|
The runtime does not track the size of the scalar size area.
|
|
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 */
|
|
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;
|
|
}
|
|
|
|
static inline bool lean_is_st(lean_object * o) {
|
|
return o->m_rc > 0;
|
|
}
|
|
|
|
/* We never update the reference counter of objects stored in compact regions and allocated at initialization time. */
|
|
static inline bool lean_is_persistent(lean_object * o) {
|
|
return o->m_rc == 0;
|
|
}
|
|
|
|
static inline bool lean_has_rc(lean_object * o) {
|
|
return o->m_rc != 0;
|
|
}
|
|
|
|
static inline _Atomic(int) * lean_get_rc_mt_addr(lean_object* o) {
|
|
return (_Atomic(int)*)(&(o->m_rc));
|
|
}
|
|
|
|
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))) {
|
|
o->m_rc++;
|
|
} else if (o->m_rc != 0) {
|
|
lean_inc_ref_cold(o);
|
|
}
|
|
}
|
|
|
|
static inline void lean_inc_ref_n(lean_object * o, size_t n) {
|
|
if (LEAN_LIKELY(lean_is_st(o))) {
|
|
o->m_rc += n;
|
|
} else if (o->m_rc != 0) {
|
|
lean_inc_ref_n_cold(o, n);
|
|
}
|
|
}
|
|
|
|
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)) {
|
|
o->m_rc--;
|
|
} else if (o->m_rc != 0) {
|
|
lean_dec_ref_cold(o);
|
|
}
|
|
}
|
|
static inline void lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_ref(o); }
|
|
static inline void lean_inc_n(lean_object * o, size_t n) { if (!lean_is_scalar(o)) lean_inc_ref_n(o, n); }
|
|
static inline void lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ref(o); }
|
|
|
|
/* Just free memory */
|
|
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; }
|
|
static inline bool lean_is_array(lean_object * o) { return lean_ptr_tag(o) == LeanArray; }
|
|
static inline bool lean_is_sarray(lean_object * o) { return lean_ptr_tag(o) == LeanScalarArray; }
|
|
static inline bool lean_is_string(lean_object * o) { return lean_ptr_tag(o) == LeanString; }
|
|
static inline bool lean_is_mpz(lean_object * o) { return lean_ptr_tag(o) == LeanMPZ; }
|
|
static inline bool lean_is_thunk(lean_object * o) { return lean_ptr_tag(o) == LeanThunk; }
|
|
static inline bool lean_is_task(lean_object * o) { return lean_ptr_tag(o) == LeanTask; }
|
|
static inline bool lean_is_external(lean_object * o) { return lean_ptr_tag(o) == LeanExternal; }
|
|
static inline bool lean_is_ref(lean_object * o) { return lean_ptr_tag(o) == LeanRef; }
|
|
|
|
static inline unsigned lean_obj_tag(lean_object * o) {
|
|
if (lean_is_scalar(o)) return lean_unbox(o); else return lean_ptr_tag(o);
|
|
}
|
|
|
|
static inline lean_ctor_object * lean_to_ctor(lean_object * o) { assert(lean_is_ctor(o)); return (lean_ctor_object*)(o); }
|
|
static inline lean_closure_object * lean_to_closure(lean_object * o) { assert(lean_is_closure(o)); return (lean_closure_object*)(o); }
|
|
static inline lean_array_object * lean_to_array(lean_object * o) { assert(lean_is_array(o)); return (lean_array_object*)(o); }
|
|
static inline lean_sarray_object * lean_to_sarray(lean_object * o) { assert(lean_is_sarray(o)); return (lean_sarray_object*)(o); }
|
|
static inline lean_string_object * lean_to_string(lean_object * o) { assert(lean_is_string(o)); return (lean_string_object*)(o); }
|
|
static inline lean_thunk_object * lean_to_thunk(lean_object * o) { assert(lean_is_thunk(o)); return (lean_thunk_object*)(o); }
|
|
static inline lean_task_object * lean_to_task(lean_object * o) { assert(lean_is_task(o)); return (lean_task_object*)(o); }
|
|
static inline lean_ref_object * lean_to_ref(lean_object * o) { assert(lean_is_ref(o)); return (lean_ref_object*)(o); }
|
|
static inline lean_external_object * lean_to_external(lean_object * o) { assert(lean_is_external(o)); return (lean_external_object*)(o); }
|
|
|
|
static inline bool lean_is_exclusive(lean_object * o) {
|
|
if (LEAN_LIKELY(lean_is_st(o))) {
|
|
return o->m_rc == 1;
|
|
} else {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
static inline bool lean_is_shared(lean_object * o) {
|
|
if (LEAN_LIKELY(lean_is_st(o))) {
|
|
return o->m_rc > 1;
|
|
} else {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
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;
|
|
o->m_tag = tag;
|
|
o->m_other = other;
|
|
o->m_cs_sz = 0;
|
|
}
|
|
|
|
/* Remark: we don't need a reference counter for objects that are not stored in the heap.
|
|
Thus, we use the area to store the object size for small objects. */
|
|
static inline void lean_set_non_heap_header(lean_object * o, size_t sz, unsigned tag, unsigned other) {
|
|
assert(sz > 0);
|
|
assert(sz < (1ull << 16));
|
|
assert(sz == 1 || !lean_is_big_object_tag(tag));
|
|
o->m_rc = 0;
|
|
o->m_tag = tag;
|
|
o->m_other = other;
|
|
o->m_cs_sz = sz;
|
|
}
|
|
|
|
/* `lean_set_non_heap_header` for (potentially) big objects such as arrays and strings. */
|
|
static inline void lean_set_non_heap_header_for_big(lean_object * o, unsigned tag, unsigned other) {
|
|
lean_set_non_heap_header(o, 1, tag, other);
|
|
}
|
|
|
|
/* Constructor objects */
|
|
|
|
static inline unsigned lean_ctor_num_objs(lean_object * o) {
|
|
assert(lean_is_ctor(o));
|
|
return lean_ptr_other(o);
|
|
}
|
|
|
|
static inline lean_object ** lean_ctor_obj_cptr(lean_object * o) {
|
|
assert(lean_is_ctor(o));
|
|
return lean_to_ctor(o)->m_objs;
|
|
}
|
|
|
|
static inline uint8_t * lean_ctor_scalar_cptr(lean_object * o) {
|
|
assert(lean_is_ctor(o));
|
|
return (uint8_t*)(lean_ctor_obj_cptr(o) + lean_ctor_num_objs(o));
|
|
}
|
|
|
|
static inline lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, unsigned scalar_sz) {
|
|
assert(tag <= LeanMaxCtorTag && num_objs < LEAN_MAX_CTOR_FIELDS && scalar_sz < LEAN_MAX_CTOR_SCALARS_SIZE);
|
|
lean_object * o = lean_alloc_ctor_memory(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz);
|
|
lean_set_st_header(o, tag, num_objs);
|
|
return o;
|
|
}
|
|
|
|
static inline b_lean_obj_res lean_ctor_get(b_lean_obj_arg o, unsigned i) {
|
|
assert(i < lean_ctor_num_objs(o));
|
|
return lean_ctor_obj_cptr(o)[i];
|
|
}
|
|
|
|
static inline void lean_ctor_set(b_lean_obj_arg o, unsigned i, lean_obj_arg v) {
|
|
assert(i < lean_ctor_num_objs(o));
|
|
lean_ctor_obj_cptr(o)[i] = v;
|
|
}
|
|
|
|
static inline void lean_ctor_set_tag(b_lean_obj_arg o, uint8_t new_tag) {
|
|
assert(new_tag <= LeanMaxCtorTag);
|
|
o->m_tag = new_tag;
|
|
}
|
|
|
|
static inline void lean_ctor_release(b_lean_obj_arg o, unsigned i) {
|
|
assert(i < lean_ctor_num_objs(o));
|
|
lean_object ** objs = lean_ctor_obj_cptr(o);
|
|
lean_dec(objs[i]);
|
|
objs[i] = lean_box(0);
|
|
}
|
|
|
|
static inline size_t lean_ctor_get_usize(b_lean_obj_arg o, unsigned i) {
|
|
assert(i >= lean_ctor_num_objs(o));
|
|
return *((size_t*)(lean_ctor_obj_cptr(o) + i));
|
|
}
|
|
|
|
static inline uint8_t lean_ctor_get_uint8(b_lean_obj_arg o, unsigned offset) {
|
|
assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
|
|
return *((uint8_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
|
|
}
|
|
|
|
static inline uint16_t lean_ctor_get_uint16(b_lean_obj_arg o, unsigned offset) {
|
|
assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
|
|
return *((uint16_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
|
|
}
|
|
|
|
static inline uint32_t lean_ctor_get_uint32(b_lean_obj_arg o, unsigned offset) {
|
|
assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
|
|
return *((uint32_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
|
|
}
|
|
|
|
static inline uint64_t lean_ctor_get_uint64(b_lean_obj_arg o, unsigned offset) {
|
|
assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
|
|
return *((uint64_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
|
|
}
|
|
|
|
static inline double lean_ctor_get_float(b_lean_obj_arg o, unsigned offset) {
|
|
assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
|
|
return *((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
|
|
}
|
|
|
|
static inline void lean_ctor_set_usize(b_lean_obj_arg o, unsigned i, size_t v) {
|
|
assert(i >= lean_ctor_num_objs(o));
|
|
*((size_t*)(lean_ctor_obj_cptr(o) + i)) = v;
|
|
}
|
|
|
|
static inline void lean_ctor_set_uint8(b_lean_obj_arg o, unsigned offset, uint8_t v) {
|
|
assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
|
|
*((uint8_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
|
|
}
|
|
|
|
static inline void lean_ctor_set_uint16(b_lean_obj_arg o, unsigned offset, uint16_t v) {
|
|
assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
|
|
*((uint16_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
|
|
}
|
|
|
|
static inline void lean_ctor_set_uint32(b_lean_obj_arg o, unsigned offset, uint32_t v) {
|
|
assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
|
|
*((uint32_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
|
|
}
|
|
|
|
static inline void lean_ctor_set_uint64(b_lean_obj_arg o, unsigned offset, uint64_t v) {
|
|
assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
|
|
*((uint64_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
|
|
}
|
|
|
|
static inline void lean_ctor_set_float(b_lean_obj_arg o, unsigned offset, double v) {
|
|
assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
|
|
*((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
|
|
}
|
|
|
|
/* Closures */
|
|
|
|
static inline void * lean_closure_fun(lean_object * o) { return lean_to_closure(o)->m_fun; }
|
|
static inline unsigned lean_closure_arity(lean_object * o) { return lean_to_closure(o)->m_arity; }
|
|
static inline unsigned lean_closure_num_fixed(lean_object * o) { return lean_to_closure(o)->m_num_fixed; }
|
|
static inline lean_object ** lean_closure_arg_cptr(lean_object * o) { return lean_to_closure(o)->m_objs; }
|
|
static inline lean_obj_res lean_alloc_closure(void * fun, unsigned arity, unsigned num_fixed) {
|
|
assert(arity > 0);
|
|
assert(num_fixed < arity);
|
|
lean_closure_object * o = (lean_closure_object*)lean_alloc_small_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
|
|
lean_set_st_header((lean_object*)o, LeanClosure, 0);
|
|
o->m_fun = fun;
|
|
o->m_arity = arity;
|
|
o->m_num_fixed = num_fixed;
|
|
return (lean_object*)o;
|
|
}
|
|
static inline b_lean_obj_res lean_closure_get(b_lean_obj_arg o, unsigned i) {
|
|
assert(i < lean_closure_num_fixed(o));
|
|
return lean_to_closure(o)->m_objs[i];
|
|
}
|
|
static inline void lean_closure_set(u_lean_obj_arg o, unsigned i, lean_obj_arg a) {
|
|
assert(i < lean_closure_num_fixed(o));
|
|
lean_to_closure(o)->m_objs[i] = a;
|
|
}
|
|
|
|
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_SHARED lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object** args);
|
|
|
|
/* Fixpoint */
|
|
|
|
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) {
|
|
lean_array_object * o = (lean_array_object*)lean_alloc_object(sizeof(lean_array_object) + sizeof(void*)*capacity);
|
|
lean_set_st_header((lean_object*)o, LeanArray, 0);
|
|
o->m_size = size;
|
|
o->m_capacity = capacity;
|
|
return (lean_object*)o;
|
|
}
|
|
static inline size_t lean_array_size(b_lean_obj_arg o) { return lean_to_array(o)->m_size; }
|
|
static inline size_t lean_array_capacity(b_lean_obj_arg o) { return lean_to_array(o)->m_capacity; }
|
|
static inline size_t lean_array_byte_size(lean_object * o) {
|
|
return sizeof(lean_array_object) + sizeof(void*)*lean_array_capacity(o);
|
|
}
|
|
static inline lean_object ** lean_array_cptr(lean_object * o) { return lean_to_array(o)->m_data; }
|
|
static inline void lean_array_set_size(u_lean_obj_arg o, size_t sz) {
|
|
assert(lean_is_array(o));
|
|
assert(lean_is_exclusive(o));
|
|
assert(sz <= lean_array_capacity(o));
|
|
lean_to_array(o)->m_size = sz;
|
|
}
|
|
static inline b_lean_obj_res lean_array_get_core(b_lean_obj_arg o, size_t i) {
|
|
assert(i < lean_array_size(o));
|
|
return lean_to_array(o)->m_data[i];
|
|
}
|
|
static inline void lean_array_set_core(u_lean_obj_arg o, size_t i, lean_obj_arg v) {
|
|
/* Remark: we use this procedure to update non shared arrays in the heap,
|
|
and when copying objects to compact region at compact.cpp */
|
|
assert(!lean_has_rc(o) || lean_is_exclusive(o));
|
|
assert(i < lean_array_size(o));
|
|
lean_to_array(o)->m_data[i] = v;
|
|
}
|
|
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) */
|
|
|
|
static inline lean_object * lean_array_sz(lean_obj_arg a) {
|
|
lean_object * r = lean_box(lean_array_size(a));
|
|
lean_dec(a);
|
|
return r;
|
|
}
|
|
|
|
static inline lean_object * lean_array_get_size(b_lean_obj_arg a) {
|
|
return lean_box(lean_array_size(a));
|
|
}
|
|
|
|
static inline lean_object * lean_mk_empty_array() {
|
|
return lean_alloc_array(0, 0);
|
|
}
|
|
|
|
static inline lean_object * lean_mk_empty_array_with_capacity(b_lean_obj_arg capacity) {
|
|
if (!lean_is_scalar(capacity)) lean_internal_panic_out_of_memory();
|
|
return lean_alloc_array(0, lean_unbox(capacity));
|
|
}
|
|
|
|
static inline lean_object * lean_array_uget(b_lean_obj_arg a, size_t i) {
|
|
lean_object * r = lean_array_get_core(a, i); lean_inc(r);
|
|
return r;
|
|
}
|
|
|
|
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_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)) {
|
|
size_t idx = lean_unbox(i);
|
|
if (idx < lean_array_size(a)) {
|
|
lean_dec(def_val);
|
|
return lean_array_uget(a, idx);
|
|
}
|
|
}
|
|
/* Recall that if `i` is not a scalar, then it must be out of bounds because
|
|
i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1
|
|
but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones.
|
|
In both cases, we would be out-of-memory. */
|
|
return lean_array_get_panic(def_val);
|
|
}
|
|
|
|
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);
|
|
}
|
|
|
|
static inline lean_obj_res lean_ensure_exclusive_array(lean_obj_arg a) {
|
|
if (lean_is_exclusive(a)) return a;
|
|
return lean_copy_array(a);
|
|
}
|
|
|
|
static inline lean_object * lean_array_uset(lean_obj_arg a, size_t i, lean_obj_arg v) {
|
|
lean_object * r = lean_ensure_exclusive_array(a);
|
|
lean_object ** it = lean_array_cptr(r) + i;
|
|
lean_dec(*it);
|
|
*it = v;
|
|
return r;
|
|
}
|
|
|
|
static inline lean_object * lean_array_fset(lean_obj_arg a, b_lean_obj_arg i, lean_obj_arg v) {
|
|
return lean_array_uset(a, lean_unbox(i), 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)) {
|
|
size_t idx = lean_unbox(i);
|
|
if (idx < lean_array_size(a))
|
|
return lean_array_uset(a, idx, v);
|
|
}
|
|
return lean_array_set_panic(a, v);
|
|
}
|
|
|
|
static inline lean_object * lean_array_pop(lean_obj_arg a) {
|
|
lean_object * r = lean_ensure_exclusive_array(a);
|
|
size_t sz = lean_to_array(r)->m_size;
|
|
lean_object ** last;
|
|
if (sz == 0) return r;
|
|
sz--;
|
|
last = lean_array_cptr(r) + sz;
|
|
lean_to_array(r)->m_size = sz;
|
|
lean_dec(*last);
|
|
return r;
|
|
}
|
|
|
|
static inline lean_object * lean_array_uswap(lean_obj_arg a, size_t i, size_t j) {
|
|
lean_object * r = lean_ensure_exclusive_array(a);
|
|
lean_object ** it = lean_array_cptr(r);
|
|
lean_object * v1 = it[i];
|
|
it[i] = it[j];
|
|
it[j] = v1;
|
|
return r;
|
|
}
|
|
|
|
static inline lean_object * lean_array_fswap(lean_obj_arg a, b_lean_obj_arg i, b_lean_obj_arg j) {
|
|
return lean_array_uswap(a, lean_unbox(i), lean_unbox(j));
|
|
}
|
|
|
|
static inline lean_object * lean_array_swap(lean_obj_arg a, b_lean_obj_arg i, b_lean_obj_arg j) {
|
|
if (!lean_is_scalar(i) || !lean_is_scalar(j)) return a;
|
|
size_t ui = lean_unbox(i);
|
|
size_t uj = lean_unbox(j);
|
|
size_t sz = lean_to_array(a)->m_size;
|
|
if (ui >= sz || uj >= sz) return a;
|
|
return lean_array_uswap(a, ui, uj);
|
|
}
|
|
|
|
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 */
|
|
|
|
static inline lean_obj_res lean_alloc_sarray(unsigned elem_size, size_t size, size_t capacity) {
|
|
lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(sizeof(lean_sarray_object) + elem_size*capacity);
|
|
lean_set_st_header((lean_object*)o, LeanScalarArray, elem_size);
|
|
o->m_size = size;
|
|
o->m_capacity = capacity;
|
|
return (lean_object*)o;
|
|
}
|
|
static inline unsigned lean_sarray_elem_size(lean_object * o) {
|
|
assert(lean_is_sarray(o));
|
|
return lean_ptr_other(o);
|
|
}
|
|
static inline size_t lean_sarray_capacity(lean_object * o) { return lean_to_sarray(o)->m_capacity; }
|
|
static inline size_t lean_sarray_byte_size(lean_object * o) {
|
|
return sizeof(lean_sarray_object) + lean_sarray_elem_size(o)*lean_sarray_capacity(o);
|
|
}
|
|
static inline size_t lean_sarray_size(b_lean_obj_arg o) { return lean_to_sarray(o)->m_size; }
|
|
static inline void lean_sarray_set_size(u_lean_obj_arg o, size_t sz) {
|
|
assert(lean_is_exclusive(o));
|
|
assert(sz <= lean_sarray_capacity(o));
|
|
lean_to_sarray(o)->m_size = sz;
|
|
}
|
|
static inline uint8_t* lean_sarray_cptr(lean_object * o) { return lean_to_sarray(o)->m_data; }
|
|
|
|
/* Remark: expand sarray API after we add better support in the compiler */
|
|
|
|
/* ByteArray (special case of Array of Scalars) */
|
|
|
|
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();
|
|
return lean_alloc_sarray(1, 0, lean_unbox(capacity));
|
|
}
|
|
|
|
static inline lean_obj_res lean_byte_array_size(b_lean_obj_arg a) {
|
|
return lean_box(lean_sarray_size(a));
|
|
}
|
|
static inline uint8_t lean_byte_array_uget(b_lean_obj_arg a, size_t i) {
|
|
assert(i < lean_sarray_size(a));
|
|
return lean_sarray_cptr(a)[i];
|
|
}
|
|
static inline uint8_t lean_byte_array_get(b_lean_obj_arg a, b_lean_obj_arg i) {
|
|
if (lean_is_scalar(i)) {
|
|
size_t idx = lean_unbox(i);
|
|
return idx < lean_sarray_size(a) ? lean_byte_array_uget(a, idx) : 0;
|
|
} else {
|
|
/* The index must be out of bounds. Otherwise we would be out of memory. */
|
|
return 0;
|
|
}
|
|
}
|
|
static inline uint8_t lean_byte_array_fget(b_lean_obj_arg a, b_lean_obj_arg i) {
|
|
return lean_byte_array_uget(a, lean_unbox(i));
|
|
}
|
|
|
|
LEAN_SHARED lean_obj_res lean_byte_array_push(lean_obj_arg a, uint8_t b);
|
|
|
|
static inline lean_object * lean_byte_array_uset(lean_obj_arg a, size_t i, uint8_t v) {
|
|
lean_obj_res r;
|
|
if (lean_is_exclusive(a)) r = a;
|
|
else r = lean_copy_byte_array(a);
|
|
uint8_t * it = lean_sarray_cptr(r) + i;
|
|
*it = v;
|
|
return r;
|
|
}
|
|
|
|
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)) {
|
|
return a;
|
|
} else {
|
|
size_t idx = lean_unbox(i);
|
|
if (idx >= lean_sarray_size(a)) {
|
|
return a;
|
|
} else {
|
|
return lean_byte_array_uset(a, idx, b);
|
|
}
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_byte_array_fset(lean_obj_arg a, b_lean_obj_arg i, uint8_t b) {
|
|
return lean_byte_array_uset(a, lean_unbox(i), b);
|
|
}
|
|
|
|
/* FloatArray (special case of Array of Scalars) */
|
|
|
|
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();
|
|
return lean_alloc_sarray(sizeof(double), 0, lean_unbox(capacity)); // NOLINT
|
|
}
|
|
|
|
static inline lean_obj_res lean_float_array_size(b_lean_obj_arg a) {
|
|
return lean_box(lean_sarray_size(a));
|
|
}
|
|
|
|
static inline double * lean_float_array_cptr(b_lean_obj_arg a) {
|
|
return (double*)(lean_sarray_cptr(a)); // NOLINT
|
|
}
|
|
|
|
static inline double lean_float_array_uget(b_lean_obj_arg a, size_t i) {
|
|
return lean_float_array_cptr(a)[i];
|
|
}
|
|
|
|
static inline double lean_float_array_fget(b_lean_obj_arg a, b_lean_obj_arg i) {
|
|
return lean_float_array_uget(a, lean_unbox(i));
|
|
}
|
|
|
|
static inline double lean_float_array_get(b_lean_obj_arg a, b_lean_obj_arg i) {
|
|
if (lean_is_scalar(i)) {
|
|
size_t idx = lean_unbox(i);
|
|
return idx < lean_sarray_size(a) ? lean_float_array_uget(a, idx) : 0.0;
|
|
} else {
|
|
/* The index must be out of bounds. Otherwise we would be out of memory. */
|
|
return 0.0;
|
|
}
|
|
}
|
|
|
|
LEAN_SHARED lean_obj_res lean_float_array_push(lean_obj_arg a, double d);
|
|
|
|
static inline lean_obj_res lean_float_array_uset(lean_obj_arg a, size_t i, double d) {
|
|
lean_obj_res r;
|
|
if (lean_is_exclusive(a)) r = a;
|
|
else r = lean_copy_float_array(a);
|
|
double * it = lean_float_array_cptr(r) + i;
|
|
*it = d;
|
|
return r;
|
|
}
|
|
|
|
static inline lean_obj_res lean_float_array_fset(lean_obj_arg a, b_lean_obj_arg i, double d) {
|
|
return lean_float_array_uset(a, lean_unbox(i), 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)) {
|
|
return a;
|
|
} else {
|
|
size_t idx = lean_unbox(i);
|
|
if (idx >= lean_sarray_size(a)) {
|
|
return a;
|
|
} else {
|
|
return lean_float_array_uset(a, idx, d);
|
|
}
|
|
}
|
|
}
|
|
|
|
/* Strings */
|
|
|
|
static inline lean_obj_res lean_alloc_string(size_t size, size_t capacity, size_t len) {
|
|
lean_string_object * o = (lean_string_object*)lean_alloc_object(sizeof(lean_string_object) + capacity);
|
|
lean_set_st_header((lean_object*)o, LeanString, 0);
|
|
o->m_size = size;
|
|
o->m_capacity = capacity;
|
|
o->m_length = len;
|
|
return (lean_object*)o;
|
|
}
|
|
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_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_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_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_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); }
|
|
LEAN_SHARED bool lean_string_eq_cold(b_lean_obj_arg s1, b_lean_obj_arg s2);
|
|
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) && lean_string_eq_cold(s1, s2));
|
|
}
|
|
static inline bool lean_string_ne(b_lean_obj_arg s1, b_lean_obj_arg s2) { return !lean_string_eq(s1, 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); }
|
|
LEAN_SHARED uint64_t lean_string_hash(b_lean_obj_arg);
|
|
|
|
/* Thunks */
|
|
|
|
static inline lean_obj_res lean_mk_thunk(lean_obj_arg c) {
|
|
lean_thunk_object * o = (lean_thunk_object*)lean_alloc_small_object(sizeof(lean_thunk_object));
|
|
lean_set_st_header((lean_object*)o, LeanThunk, 0);
|
|
o->m_value = (lean_object*)0;
|
|
o->m_closure = c;
|
|
return (lean_object*)o;
|
|
}
|
|
|
|
/* Thunk.pure : A -> Thunk A */
|
|
static inline lean_obj_res lean_thunk_pure(lean_obj_arg v) {
|
|
lean_thunk_object * o = (lean_thunk_object*)lean_alloc_small_object(sizeof(lean_thunk_object));
|
|
lean_set_st_header((lean_object*)o, LeanThunk, 0);
|
|
o->m_value = v;
|
|
o->m_closure = (lean_object*)0;
|
|
return (lean_object*)o;
|
|
}
|
|
|
|
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;
|
|
if (r) return r;
|
|
return lean_thunk_get_core(t);
|
|
}
|
|
|
|
/* Primitive for implementing Thunk.get : Thunk A -> A */
|
|
static inline lean_obj_res lean_thunk_get_own(b_lean_obj_arg t) {
|
|
lean_object * r = lean_thunk_get(t);
|
|
lean_inc(r);
|
|
return r;
|
|
}
|
|
|
|
/* Tasks */
|
|
|
|
LEAN_SHARED void lean_init_task_manager();
|
|
LEAN_SHARED void lean_init_task_manager_using(unsigned num_workers);
|
|
LEAN_SHARED void lean_finalize_task_manager();
|
|
|
|
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_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_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); }
|
|
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);
|
|
lean_inc(r);
|
|
lean_dec(t);
|
|
return r;
|
|
}
|
|
|
|
/* primitive for implementing `IO.checkCanceled : IO Bool` */
|
|
LEAN_SHARED bool lean_io_check_canceled_core();
|
|
/* primitive for implementing `IO.cancel : Task a -> IO Unit` */
|
|
LEAN_SHARED void lean_io_cancel_core(b_lean_obj_arg t);
|
|
/* primitive for implementing `IO.hasFinished : Task a -> IO Unit` */
|
|
LEAN_SHARED bool lean_io_has_finished_core(b_lean_obj_arg t);
|
|
/* primitive for implementing `IO.waitAny : List (Task a) -> IO (Task a)` */
|
|
LEAN_SHARED b_lean_obj_res lean_io_wait_any_core(b_lean_obj_arg task_list);
|
|
|
|
/* External objects */
|
|
|
|
static inline lean_object * lean_alloc_external(lean_external_class * cls, void * data) {
|
|
lean_external_object * o = (lean_external_object*)lean_alloc_small_object(sizeof(lean_external_object));
|
|
lean_set_st_header((lean_object*)o, LeanExternal, 0);
|
|
o->m_class = cls;
|
|
o->m_data = data;
|
|
return (lean_object*)o;
|
|
}
|
|
|
|
static inline lean_external_class * lean_get_external_class(lean_object * o) {
|
|
return lean_to_external(o)->m_class;
|
|
}
|
|
|
|
static inline void * lean_get_external_data(lean_object * o) {
|
|
return lean_to_external(o)->m_data;
|
|
}
|
|
|
|
/* Natural numbers */
|
|
|
|
#define LEAN_MAX_SMALL_NAT (SIZE_MAX >> 1)
|
|
|
|
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_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);
|
|
else
|
|
return lean_big_usize_to_nat(n);
|
|
}
|
|
static inline lean_obj_res lean_unsigned_to_nat(unsigned n) {
|
|
return lean_usize_to_nat(n);
|
|
}
|
|
static inline lean_obj_res lean_uint64_to_nat(uint64_t n) {
|
|
if (LEAN_LIKELY(n <= LEAN_MAX_SMALL_NAT))
|
|
return lean_box(n);
|
|
else
|
|
return lean_big_uint64_to_nat(n);
|
|
}
|
|
|
|
static inline lean_obj_res lean_nat_succ(b_lean_obj_arg a) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a)))
|
|
return lean_usize_to_nat(lean_unbox(a) + 1);
|
|
else
|
|
return lean_nat_big_succ(a);
|
|
}
|
|
|
|
static inline lean_obj_res lean_nat_add(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2)))
|
|
return lean_usize_to_nat(lean_unbox(a1) + lean_unbox(a2));
|
|
else
|
|
return lean_nat_big_add(a1, a2);
|
|
}
|
|
|
|
static inline lean_obj_res lean_nat_sub(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
size_t n1 = lean_unbox(a1);
|
|
size_t n2 = lean_unbox(a2);
|
|
if (n1 < n2)
|
|
return lean_box(0);
|
|
else
|
|
return lean_box(n1 - n2);
|
|
} else {
|
|
return lean_nat_big_sub(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_nat_mul(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
size_t n1 = lean_unbox(a1);
|
|
if (n1 == 0)
|
|
return a1;
|
|
size_t n2 = lean_unbox(a2);
|
|
size_t r = n1*n2;
|
|
if (r <= LEAN_MAX_SMALL_NAT && r / n1 == n2)
|
|
return lean_box(r);
|
|
else
|
|
return lean_nat_overflow_mul(n1, n2);
|
|
} else {
|
|
return lean_nat_big_mul(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_nat_div(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
size_t n1 = lean_unbox(a1);
|
|
size_t n2 = lean_unbox(a2);
|
|
if (n2 == 0)
|
|
return lean_box(0);
|
|
else
|
|
return lean_box(n1 / n2);
|
|
} else {
|
|
return lean_nat_big_div(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_nat_mod(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
size_t n1 = lean_unbox(a1);
|
|
size_t n2 = lean_unbox(a2);
|
|
if (n2 == 0)
|
|
return lean_box(n1);
|
|
else
|
|
return lean_box(n1 % n2);
|
|
} else {
|
|
return lean_nat_big_mod(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline bool lean_nat_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
return a1 == a2;
|
|
} else {
|
|
return lean_nat_big_eq(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline uint8_t lean_nat_dec_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
return lean_nat_eq(a1, a2);
|
|
}
|
|
|
|
static inline bool lean_nat_ne(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
return !lean_nat_eq(a1, a2);
|
|
}
|
|
|
|
static inline bool lean_nat_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
return a1 <= a2;
|
|
} else {
|
|
return lean_nat_big_le(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline uint8_t lean_nat_dec_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
return lean_nat_le(a1, a2);
|
|
}
|
|
|
|
static inline bool lean_nat_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
return a1 < a2;
|
|
} else {
|
|
return lean_nat_big_lt(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline uint8_t lean_nat_dec_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
return lean_nat_lt(a1, a2);
|
|
}
|
|
|
|
static inline lean_obj_res lean_nat_land(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
return (lean_object*)((size_t)(a1) & (size_t)(a2));
|
|
} else {
|
|
return lean_nat_big_land(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_nat_lor(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
return (lean_object*)((size_t)(a1) | (size_t)(a2));
|
|
} else {
|
|
return lean_nat_big_lor(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_nat_lxor(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
return lean_box(lean_unbox(a1) ^ lean_unbox(a2));
|
|
} else {
|
|
return lean_nat_big_xor(a1, 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);
|
|
LEAN_SHARED lean_obj_res lean_nat_log2(b_lean_obj_arg a);
|
|
|
|
/* 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_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_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)
|
|
return lean_box((unsigned)(n));
|
|
else if (LEAN_MIN_SMALL_INT <= n && n <= LEAN_MAX_SMALL_INT)
|
|
return lean_box((unsigned)(n));
|
|
else
|
|
return lean_big_int_to_int(n);
|
|
}
|
|
|
|
static inline lean_obj_res lean_int64_to_int(int64_t n) {
|
|
if (LEAN_LIKELY(LEAN_MIN_SMALL_INT <= n && n <= LEAN_MAX_SMALL_INT))
|
|
return lean_box((unsigned)((int)n)); /* NOLINT */
|
|
else
|
|
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);
|
|
if (v <= LEAN_MAX_SMALL_INT)
|
|
return a;
|
|
else
|
|
return lean_big_size_t_to_int(v);
|
|
} else {
|
|
return a;
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_int_neg(b_lean_obj_arg a) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a))) {
|
|
return lean_int64_to_int(-lean_scalar_to_int64(a));
|
|
} else {
|
|
return lean_int_big_neg(a);
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_int_neg_succ_of_nat(lean_obj_arg a) {
|
|
lean_obj_res s = lean_nat_succ(a); lean_dec(a);
|
|
lean_obj_res i = lean_nat_to_int(s); /* Recall that `lean_nat_to_int` consumes the argument */
|
|
lean_obj_res r = lean_int_neg(i); lean_dec(i);
|
|
return r;
|
|
}
|
|
|
|
static inline lean_obj_res lean_int_add(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
return lean_int64_to_int(lean_scalar_to_int64(a1) + lean_scalar_to_int64(a2));
|
|
} else {
|
|
return lean_int_big_add(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_int_sub(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
return lean_int64_to_int(lean_scalar_to_int64(a1) - lean_scalar_to_int64(a2));
|
|
} else {
|
|
return lean_int_big_sub(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_int_mul(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
return lean_int64_to_int(lean_scalar_to_int64(a1) * lean_scalar_to_int64(a2));
|
|
} else {
|
|
return lean_int_big_mul(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_int_div(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
if (sizeof(void*) == 8) {
|
|
/* 64-bit version, we use 64-bit numbers to avoid overflow when v1 == LEAN_MIN_SMALL_INT. */
|
|
int64_t v1 = lean_scalar_to_int(a1);
|
|
int64_t v2 = lean_scalar_to_int(a2);
|
|
if (v2 == 0)
|
|
return lean_box(0);
|
|
else
|
|
return lean_int64_to_int(v1 / v2);
|
|
} else {
|
|
/* 32-bit version */
|
|
int v1 = lean_scalar_to_int(a1);
|
|
int v2 = lean_scalar_to_int(a2);
|
|
if (v2 == 0)
|
|
return lean_box(0);
|
|
else
|
|
return lean_int_to_int(v1 / v2);
|
|
}
|
|
} else {
|
|
return lean_int_big_div(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_int_mod(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
if (sizeof(void*) == 8) {
|
|
/* 64-bit version, we use 64-bit numbers to avoid overflow when v1 == LEAN_MIN_SMALL_INT. */
|
|
int64_t v1 = lean_scalar_to_int64(a1);
|
|
int64_t v2 = lean_scalar_to_int64(a2);
|
|
if (v2 == 0)
|
|
return a1;
|
|
else
|
|
return lean_int64_to_int(v1 % v2);
|
|
} else {
|
|
/* 32-bit version */
|
|
int v1 = lean_scalar_to_int(a1);
|
|
int v2 = lean_scalar_to_int(a2);
|
|
if (v2 == 0)
|
|
return a1;
|
|
else
|
|
return lean_int_to_int(v1 % v2);
|
|
}
|
|
} else {
|
|
return lean_int_big_mod(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline bool lean_int_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
return a1 == a2;
|
|
} else {
|
|
return lean_int_big_eq(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline bool lean_int_ne(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
return !lean_int_eq(a1, a2);
|
|
}
|
|
|
|
static inline bool lean_int_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
return lean_scalar_to_int(a1) <= lean_scalar_to_int(a2);
|
|
} else {
|
|
return lean_int_big_le(a1, a2);
|
|
}
|
|
}
|
|
|
|
static inline bool lean_int_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
|
|
return lean_scalar_to_int(a1) < lean_scalar_to_int(a2);
|
|
} else {
|
|
return lean_int_big_lt(a1, a2);
|
|
}
|
|
}
|
|
|
|
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)) {
|
|
return a;
|
|
} else {
|
|
return lean_big_int_to_nat(a);
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_nat_abs(b_lean_obj_arg i) {
|
|
if (lean_int_lt(i, lean_box(0))) {
|
|
return lean_int_to_nat(lean_int_neg(i));
|
|
} else {
|
|
lean_inc(i);
|
|
return lean_int_to_nat(i);
|
|
}
|
|
}
|
|
|
|
static inline uint8_t lean_int_dec_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) { return lean_int_eq(a1, a2); }
|
|
|
|
static inline uint8_t lean_int_dec_le(b_lean_obj_arg a1, b_lean_obj_arg a2) { return lean_int_le(a1, a2); }
|
|
|
|
static inline uint8_t lean_int_dec_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) { return lean_int_lt(a1, a2); }
|
|
|
|
static inline uint8_t lean_int_dec_nonneg(b_lean_obj_arg a) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a)))
|
|
return lean_scalar_to_int(a) >= 0;
|
|
else
|
|
return lean_int_big_nonneg(a);
|
|
}
|
|
|
|
/* Bool */
|
|
|
|
static inline uint64_t lean_bool_to_uint64(uint8_t a) { return ((uint64_t)a); }
|
|
|
|
|
|
/* UInt8 */
|
|
|
|
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; }
|
|
static inline lean_obj_res lean_uint8_to_nat(uint8_t a) { return lean_usize_to_nat((size_t)a); }
|
|
static inline uint8_t lean_uint8_add(uint8_t a1, uint8_t a2) { return a1+a2; }
|
|
static inline uint8_t lean_uint8_sub(uint8_t a1, uint8_t a2) { return a1-a2; }
|
|
static inline uint8_t lean_uint8_mul(uint8_t a1, uint8_t a2) { return a1*a2; }
|
|
static inline uint8_t lean_uint8_div(uint8_t a1, uint8_t a2) { return a2 == 0 ? 0 : a1/a2; }
|
|
static inline uint8_t lean_uint8_mod(uint8_t a1, uint8_t a2) { return a2 == 0 ? a1 : a1%a2; }
|
|
static inline uint8_t lean_uint8_land(uint8_t a, uint8_t b) { return a & b; }
|
|
static inline uint8_t lean_uint8_lor(uint8_t a, uint8_t b) { return a | b; }
|
|
static inline uint8_t lean_uint8_xor(uint8_t a, uint8_t b) { return a ^ b; }
|
|
static inline uint8_t lean_uint8_shift_left(uint8_t a, uint8_t b) { return a << (b % 8); }
|
|
static inline uint8_t lean_uint8_shift_right(uint8_t a, uint8_t b) { return a >> (b % 8); }
|
|
static inline uint8_t lean_uint8_complement(uint8_t a) { return ~a; }
|
|
static inline uint8_t lean_uint8_modn(uint8_t a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a2))) {
|
|
unsigned n2 = lean_unbox(a2);
|
|
return n2 == 0 ? a1 : a1 % n2;
|
|
} else {
|
|
return a1;
|
|
}
|
|
}
|
|
static inline uint8_t lean_uint8_dec_eq(uint8_t a1, uint8_t a2) { return a1 == a2; }
|
|
static inline uint8_t lean_uint8_dec_lt(uint8_t a1, uint8_t a2) { return a1 < a2; }
|
|
static inline uint8_t lean_uint8_dec_le(uint8_t a1, uint8_t a2) { return a1 <= a2; }
|
|
|
|
|
|
/* Unit8 -> other */
|
|
static inline uint16_t lean_uint8_to_uint16(uint8_t a) { return ((uint16_t)a); }
|
|
static inline uint32_t lean_uint8_to_uint32(uint8_t a) { return ((uint32_t)a); }
|
|
static inline uint64_t lean_uint8_to_uint64(uint8_t a) { return ((uint64_t)a); }
|
|
|
|
/* UInt16 */
|
|
|
|
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; }
|
|
static inline lean_obj_res lean_uint16_to_nat(uint16_t a) { return lean_usize_to_nat((size_t)a); }
|
|
static inline uint16_t lean_uint16_add(uint16_t a1, uint16_t a2) { return a1+a2; }
|
|
static inline uint16_t lean_uint16_sub(uint16_t a1, uint16_t a2) { return a1-a2; }
|
|
static inline uint16_t lean_uint16_mul(uint16_t a1, uint16_t a2) { return a1*a2; }
|
|
static inline uint16_t lean_uint16_div(uint16_t a1, uint16_t a2) { return a2 == 0 ? 0 : a1/a2; }
|
|
static inline uint16_t lean_uint16_mod(uint16_t a1, uint16_t a2) { return a2 == 0 ? a1 : a1%a2; }
|
|
static inline uint16_t lean_uint16_land(uint16_t a, uint16_t b) { return a & b; }
|
|
static inline uint16_t lean_uint16_lor(uint16_t a, uint16_t b) { return a | b; }
|
|
static inline uint16_t lean_uint16_xor(uint16_t a, uint16_t b) { return a ^ b; }
|
|
static inline uint16_t lean_uint16_shift_left(uint16_t a, uint16_t b) { return a << (b % 16); }
|
|
static inline uint16_t lean_uint16_shift_right(uint16_t a, uint16_t b) { return a >> (b % 16); }
|
|
static inline uint16_t lean_uint16_complement(uint16_t a) { return ~a; }
|
|
static inline uint16_t lean_uint16_modn(uint16_t a1, b_lean_obj_arg a2) {
|
|
if (LEAN_LIKELY(lean_is_scalar(a2))) {
|
|
unsigned n2 = lean_unbox(a2);
|
|
return n2 == 0 ? a1 : a1 % n2;
|
|
} else {
|
|
return a1;
|
|
}
|
|
}
|
|
static inline uint8_t lean_uint16_dec_eq(uint16_t a1, uint16_t a2) { return a1 == a2; }
|
|
static inline uint8_t lean_uint16_dec_lt(uint16_t a1, uint16_t a2) { return a1 < a2; }
|
|
static inline uint8_t lean_uint16_dec_le(uint16_t a1, uint16_t a2) { return a1 <= a2; }
|
|
|
|
/*uint16 -> other */
|
|
static inline uint8_t lean_uint16_to_uint8(uint16_t a) { return ((uint8_t)a); }
|
|
static inline uint32_t lean_uint16_to_uint32(uint16_t a) { return ((uint32_t)a); }
|
|
static inline uint64_t lean_uint16_to_uint64(uint16_t a) { return ((uint64_t)a); }
|
|
|
|
/* UInt32 */
|
|
|
|
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; }
|
|
static inline lean_obj_res lean_uint32_to_nat(uint32_t a) { return lean_usize_to_nat((size_t)a); }
|
|
static inline uint32_t lean_uint32_add(uint32_t a1, uint32_t a2) { return a1+a2; }
|
|
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; }
|
|
static inline uint32_t lean_uint32_land(uint32_t a, uint32_t b) { return a & b; }
|
|
static inline uint32_t lean_uint32_lor(uint32_t a, uint32_t b) { return a | b; }
|
|
static inline uint32_t lean_uint32_xor(uint32_t a, uint32_t b) { return a ^ b; }
|
|
static inline uint32_t lean_uint32_shift_left(uint32_t a, uint32_t b) { return a << (b % 32); }
|
|
static inline uint32_t lean_uint32_shift_right(uint32_t a, uint32_t b) { return a >> (b % 32); }
|
|
static inline uint32_t lean_uint32_complement(uint32_t a) { return ~a; }
|
|
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);
|
|
return n2 == 0 ? a1 : a1 % n2;
|
|
} else if (sizeof(void*) == 4) {
|
|
/* 32-bit */
|
|
return lean_uint32_big_modn(a1, a2);
|
|
} else {
|
|
/* 64-bit */
|
|
return a1;
|
|
}
|
|
}
|
|
static inline uint8_t lean_uint32_dec_eq(uint32_t a1, uint32_t a2) { return a1 == a2; }
|
|
static inline uint8_t lean_uint32_dec_lt(uint32_t a1, uint32_t a2) { return a1 < a2; }
|
|
static inline uint8_t lean_uint32_dec_le(uint32_t a1, uint32_t a2) { return a1 <= a2; }
|
|
|
|
/* uint32 -> other */
|
|
static inline uint8_t lean_uint32_to_uint8(uint32_t a) { return ((uint8_t)a); }
|
|
static inline uint16_t lean_uint32_to_uint16(uint32_t a) { return ((uint16_t)a); }
|
|
static inline uint64_t lean_uint32_to_uint64(uint32_t a) { return ((uint64_t)a); }
|
|
static inline size_t lean_uint32_to_usize(uint32_t a) { return a; }
|
|
|
|
|
|
/* UInt64 */
|
|
|
|
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; }
|
|
static inline uint64_t lean_uint64_add(uint64_t a1, uint64_t a2) { return a1+a2; }
|
|
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; }
|
|
static inline uint64_t lean_uint64_land(uint64_t a, uint64_t b) { return a & b; }
|
|
static inline uint64_t lean_uint64_lor(uint64_t a, uint64_t b) { return a | b; }
|
|
static inline uint64_t lean_uint64_xor(uint64_t a, uint64_t b) { return a ^ b; }
|
|
static inline uint64_t lean_uint64_shift_left(uint64_t a, uint64_t b) { return a << (b % 64); }
|
|
static inline uint64_t lean_uint64_shift_right(uint64_t a, uint64_t b) { return a >> (b % 64); }
|
|
static inline uint64_t lean_uint64_complement(uint64_t a) { return ~a; }
|
|
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);
|
|
return n2 == 0 ? a1 : a1 % n2;
|
|
} else {
|
|
return lean_uint64_big_modn(a1, 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; }
|
|
LEAN_SHARED uint64_t lean_uint64_mix_hash(uint64_t a1, uint64_t a2);
|
|
|
|
|
|
/* uint64 -> other */
|
|
static inline uint8_t lean_uint64_to_uint8(uint64_t a) { return ((uint8_t)a); }
|
|
static inline uint16_t lean_uint64_to_uint16(uint64_t a) { return ((uint16_t)a); }
|
|
static inline uint32_t lean_uint64_to_uint32(uint64_t a) { return ((uint32_t)a); }
|
|
static inline size_t lean_uint64_to_usize(uint64_t a) { return ((size_t)a); }
|
|
|
|
/* USize */
|
|
|
|
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; }
|
|
static inline size_t lean_usize_add(size_t a1, size_t a2) { return a1+a2; }
|
|
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; }
|
|
static inline size_t lean_usize_land(size_t a, size_t b) { return a & b; }
|
|
static inline size_t lean_usize_lor(size_t a, size_t b) { return a | b; }
|
|
static inline size_t lean_usize_xor(size_t a, size_t b) { return a ^ b; }
|
|
static inline size_t lean_usize_shift_left(size_t a, size_t b) { return a << (b % (sizeof(size_t) * 8)); }
|
|
static inline size_t lean_usize_shift_right(size_t a, size_t b) { return a >> (b % (sizeof(size_t) * 8)); }
|
|
static inline size_t lean_usize_complement(size_t a) { return ~a; }
|
|
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);
|
|
return n2 == 0 ? a1 : a1 % n2;
|
|
} else {
|
|
return lean_usize_big_modn(a1, 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; }
|
|
LEAN_SHARED size_t lean_usize_mix_hash(size_t a1, size_t a2);
|
|
|
|
|
|
|
|
/* usize -> other */
|
|
static inline uint32_t lean_usize_to_uint32(size_t a) { return ((uint32_t)a); }
|
|
static inline uint64_t lean_usize_to_uint64(size_t a) { return ((uint64_t)a); }
|
|
|
|
/* Float */
|
|
|
|
LEAN_SHARED lean_obj_res lean_float_to_string(double a);
|
|
LEAN_SHARED double lean_float_scaleb(double a, b_lean_obj_arg b);
|
|
|
|
/* Boxing primitives */
|
|
|
|
static inline lean_obj_res lean_box_uint32(uint32_t v) {
|
|
if (sizeof(void*) == 4) {
|
|
/* 32-bit implementation */
|
|
lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(uint32_t));
|
|
lean_ctor_set_uint32(r, 0, v);
|
|
return r;
|
|
} else {
|
|
/* 64-bit implementation */
|
|
return lean_box(v);
|
|
}
|
|
}
|
|
|
|
static inline unsigned lean_unbox_uint32(b_lean_obj_arg o) {
|
|
if (sizeof(void*) == 4) {
|
|
/* 32-bit implementation */
|
|
return lean_ctor_get_uint32(o, 0);
|
|
} else {
|
|
/* 64-bit implementation */
|
|
return lean_unbox(o);
|
|
}
|
|
}
|
|
|
|
static inline lean_obj_res lean_box_uint64(uint64_t v) {
|
|
lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(uint64_t));
|
|
lean_ctor_set_uint64(r, 0, v);
|
|
return r;
|
|
}
|
|
|
|
static inline uint64_t lean_unbox_uint64(b_lean_obj_arg o) {
|
|
return lean_ctor_get_uint64(o, 0);
|
|
}
|
|
|
|
static inline lean_obj_res lean_box_usize(size_t v) {
|
|
lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(size_t));
|
|
lean_ctor_set_usize(r, 0, v);
|
|
return r;
|
|
}
|
|
|
|
static inline size_t lean_unbox_usize(b_lean_obj_arg o) {
|
|
return lean_ctor_get_usize(o, 0);
|
|
}
|
|
|
|
static inline lean_obj_res lean_box_float(double v) {
|
|
lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(double)); // NOLINT
|
|
lean_ctor_set_float(r, 0, v);
|
|
return r;
|
|
}
|
|
|
|
static inline double lean_unbox_float(b_lean_obj_arg o) {
|
|
return lean_ctor_get_float(o, 0);
|
|
}
|
|
|
|
/* Debugging helper functions */
|
|
|
|
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_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); }
|
|
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);
|
|
lean_ctor_set(r, 1, lean_box(0));
|
|
return r;
|
|
}
|
|
static inline lean_obj_res lean_io_result_mk_error(lean_obj_arg e) {
|
|
lean_object * r = lean_alloc_ctor(1, 2, 0);
|
|
lean_ctor_set(r, 0, e);
|
|
lean_ctor_set(r, 1, lean_box(0));
|
|
return r;
|
|
}
|
|
|
|
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_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 */
|
|
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));
|
|
return lean_ctor_get_uint64(n, sizeof(lean_object*)*2);
|
|
}
|
|
|
|
static inline uint64_t lean_name_hash(b_lean_obj_arg n) {
|
|
if (lean_is_scalar(n))
|
|
return 1723;
|
|
else
|
|
return lean_name_hash_ptr(n);
|
|
}
|
|
|
|
/* float primitives */
|
|
static inline uint8_t lean_float_to_uint8(double a) { return (uint8_t)a; }
|
|
static inline uint16_t lean_float_to_uint16(double a) { return (uint16_t)a; }
|
|
static inline uint32_t lean_float_to_uint32(double a) { return (uint32_t)a; }
|
|
static inline uint64_t lean_float_to_uint64(double a) { return (uint64_t)a; }
|
|
static inline size_t lean_float_to_usize(double a) { return (size_t)a; }
|
|
static inline double lean_float_add(double a, double b) { return a + b; }
|
|
static inline double lean_float_sub(double a, double b) { return a - b; }
|
|
static inline double lean_float_mul(double a, double b) { return a * b; }
|
|
static inline double lean_float_div(double a, double b) { return a / b; }
|
|
static inline double lean_float_negate(double a) { return -a; }
|
|
static inline uint8_t lean_float_beq(double a, double b) { return a == b; }
|
|
static inline uint8_t lean_float_decLe(double a, double b) { return a <= b; }
|
|
static inline uint8_t lean_float_decLt(double a, double b) { return a < b; }
|
|
static inline double lean_uint64_to_float(uint64_t a) { return (double) a; }
|
|
|
|
#ifdef __cplusplus
|
|
}
|
|
#endif
|