#pragma once

#include <stddef.h>

#include <stdbool.h>

#include <stdint.h>

#include <limits.h>

#include <lean/config.h>

#ifdef LEAN_MIMALLOC

#include <lean/mimalloc.h>

#endif

#ifdef __cplusplus

#include <atomic>

#include <stdlib.h>

#define _Atomic(t) std::atomic<t>

#define LEAN_USING_STD using namespace std; /* NOLINT */

extern "C" {

#else

#include <stdatomic.h>

#define LEAN_USING_STD

#endif

#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)

#include <stdnoreturn.h>

#define LEAN_NORETURN _Noreturn

#else

#define LEAN_ALLOCA(s) alloca(s)

#define LEAN_NORETURN __attribute__((noreturn))

#endif

#if defined(__GNUC__) || defined(__clang__)

#define LEAN_UNLIKELY(x) (__builtin_expect((x), 0))

#define LEAN_LIKELY(x) (__builtin_expect((x), 1))

#ifdef NDEBUG

#define LEAN_ALWAYS_INLINE __attribute__((always_inline))

#else

#define LEAN_ALWAYS_INLINE

#endif

#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 LEAN_EXPORTING

#ifdef _WIN32

#define LEAN_EXPORT __declspec(dllexport)

#else

#define LEAN_EXPORT __attribute__((visibility("default")))

#endif

#else

#define LEAN_EXPORT

#endif

#define LEAN_BYTE(Var, Index) *(((uint8_t*)&Var)+Index)

#define LeanMaxCtorTag 243

#define LeanPromise 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*));

typedef struct {

int m_rc;

unsigned m_cs_sz:16;

unsigned m_other:8;

unsigned m_tag:8;

} lean_object;

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[];

} lean_ctor_object;

typedef struct {

lean_object m_header;

size_t m_size;

size_t m_capacity;

lean_object * m_data[];

} lean_array_object;

typedef struct {

lean_object m_header;

size_t m_size;

size_t m_capacity;

uint8_t m_data[];

} 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[];

} 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[];

} 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;

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;

typedef struct lean_task {

} lean_task_object;

typedef struct lean_promise {

lean_object m_header;

lean_task_object * m_result;

} lean_promise_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_EXPORT lean_external_class * lean_register_external_class(lean_external_finalize_proc, lean_external_foreach_proc);

typedef struct {

lean_object m_header;

lean_external_class * m_class;

void * m_data;

} lean_external_object;

static inline LEAN_ALWAYS_INLINE uint8_t 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_EXPORT void lean_set_exit_on_panic(bool flag);

LEAN_EXPORT void lean_set_panic_messages(bool flag);

LEAN_EXPORT void lean_panic(char const * msg, bool force_stderr);

LEAN_EXPORT lean_object * lean_panic_fn(lean_object * default_val, lean_object * msg);

LEAN_EXPORT lean_object * lean_panic_fn_borrowed(b_lean_obj_arg default_val, lean_object * msg);

LEAN_EXPORT LEAN_NORETURN void lean_internal_panic(char const * msg);

LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_out_of_memory(void);

LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_unreachable(void);

LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_rc_overflow(void);

LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_overflow(void);

static inline bool lean_usize_mul_would_overflow(size_t a, size_t b) {

}

static inline bool lean_usize_add_would_overflow(size_t a, size_t b) {

}

static inline size_t lean_usize_mul_checked(size_t a, size_t b) {

}

static inline size_t lean_usize_add_checked(size_t a, size_t b) {

}

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) {

}

LEAN_EXPORT void * lean_alloc_small(unsigned sz, unsigned slot_idx);

LEAN_EXPORT void lean_free_small(void * p);

LEAN_EXPORT unsigned lean_small_mem_size(void * p);

LEAN_EXPORT void lean_inc_heartbeat(void);

#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();

#ifdef LEAN_MIMALLOC

// HACK: emulate behavior of small allocator to avoid `leangz` breakage for now

sz = lean_align(sz, LEAN_OBJECT_SIZE_DELTA);

void * mem = mi_malloc_small(sz);

if (mem == 0) lean_internal_panic_out_of_memory();

lean_object * o = (lean_object*)mem;

o->m_cs_sz = sz;

return o;

#else

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

#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.

size_t * end = (size_t*)(((char*)r) + sz1);

end[-1] = 0;

}

return r;

#elif defined(LEAN_MIMALLOC)

unsigned sz1 = lean_align(sz, LEAN_OBJECT_SIZE_DELTA);

lean_object* r = lean_alloc_small_object(sz);

if (sz1 > sz) {

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) {

}

#ifndef __cplusplus

void free(void *); // avoid including big `stdlib.h`

#endif

#if !defined(__STDC_VERSION_STDLIB_H__) || __STDC_VERSION_STDLIB_H__ < 202311L

#if defined(__GLIBC__) && (defined(__GNUC__) || defined(__clang__))

__attribute__((nothrow))

#endif

void free_sized(void* ptr, size_t);

#endif

static inline void lean_free_small_object(lean_object * o) {

}

LEAN_EXPORT lean_object * lean_alloc_object(size_t sz);

LEAN_EXPORT void lean_free_object(lean_object * o);

static inline void lean_del_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;

}

LEAN_EXPORT size_t lean_object_byte_size(lean_object * o);

LEAN_EXPORT size_t lean_object_data_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;

}

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

}

static inline void lean_inc_ref_n(lean_object * o, size_t n) {

}

static inline void lean_inc_ref(lean_object * o) {

lean_inc_ref_n(o, 1);

}

LEAN_EXPORT void lean_dec_ref_cold(lean_object * o);

static inline LEAN_ALWAYS_INLINE void lean_dec_ref(lean_object * o) {

}

static inline void LEAN_ALWAYS_INLINE 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_ALWAYS_INLINE lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ref(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_promise(lean_object * o) { return lean_ptr_tag(o) == LeanPromise; }

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_promise_object * lean_to_promise(lean_object * o) { assert(lean_is_promise(o)); return (lean_promise_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) {

}

static inline uint8_t lean_is_exclusive_obj(lean_object * o) {

return lean_is_exclusive(o);

}

static inline bool lean_is_shared(lean_object * o) {

}

LEAN_EXPORT void lean_mark_mt(lean_object * o);

LEAN_EXPORT void lean_mark_persistent(lean_object * o);

static inline void lean_set_st_header(lean_object * o, unsigned tag, unsigned other) {

}

static inline void lean_set_non_heap_header(lean_object * o, size_t sz, unsigned tag, unsigned other) {

}

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

}

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(lean_usize_add_checked(lean_usize_add_checked(sizeof(lean_ctor_object), lean_usize_mul_checked(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) {

}

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 float lean_ctor_get_float32(b_lean_obj_arg o, unsigned offset) {

assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));

return *((float*)((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;

}

static inline void lean_ctor_set_float32(b_lean_obj_arg o, unsigned offset, float v) {

assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));

*((float*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;

}

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) {

}

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;

}

static inline size_t lean_closure_byte_size(lean_object * o) {

return sizeof(lean_closure_object) + sizeof(void*)*lean_closure_num_fixed(o);

}

static inline size_t lean_closure_data_byte_size(lean_object * o) {

// Matches for closures.

return lean_closure_byte_size(o);

}

LEAN_EXPORT lean_object* lean_apply_1(lean_object* f, lean_object* a1);

LEAN_EXPORT lean_object* lean_apply_2(lean_object* f, lean_object* a1, lean_object* a2);

LEAN_EXPORT lean_object* lean_apply_3(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3);

LEAN_EXPORT lean_object* lean_apply_4(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4);

LEAN_EXPORT lean_object* lean_apply_5(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5);

LEAN_EXPORT 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_EXPORT 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_EXPORT 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_EXPORT 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_EXPORT 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_EXPORT 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_EXPORT 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_EXPORT 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_EXPORT 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_EXPORT 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_EXPORT 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_EXPORT lean_object* lean_apply_n(lean_object* f, unsigned n, lean_object** args);

LEAN_EXPORT lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object** args);

static inline lean_obj_res lean_alloc_array(size_t size, size_t capacity) {

}

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 size_t lean_array_data_byte_size(lean_object * o) {

return sizeof(lean_array_object) + sizeof(void*)*lean_array_size(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) {

}

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) {

}

LEAN_EXPORT lean_object * lean_array_mk(lean_obj_arg l);

LEAN_EXPORT lean_object * lean_array_to_list(lean_obj_arg a);

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 b_lean_obj_res lean_array_uget_borrowed(b_lean_obj_arg a, size_t i) {

return lean_array_get_core(a, i);

}

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

}

static inline lean_obj_res lean_array_fget_borrowed(b_lean_obj_arg a, b_lean_obj_arg i) {

return lean_array_get_core(a, lean_unbox(i));

}

LEAN_EXPORT lean_obj_res lean_array_get_panic(lean_obj_arg def_val);

static inline lean_object * lean_array_get(b_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)) {

return lean_array_uget(a, idx);

}

}

/* Recall that if `i` is not a scalar, then it must be out of bounds because

lean_inc(def_val);

return lean_array_get_panic(def_val);

}

static inline lean_object * lean_array_get_borrowed(b_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)) {

return lean_array_get_core(a, idx);

}

}

/* Recall that if `i` is not a scalar, then it must be out of bounds because

lean_inc(def_val);

return lean_array_get_panic(def_val);

}

LEAN_EXPORT lean_obj_res lean_copy_expand_array(lean_obj_arg a, bool expand);

LEAN_EXPORT lean_obj_res lean_copy_expand_array_nonlinear(lean_obj_arg a, bool expand);

static inline lean_obj_res lean_ensure_exclusive_array(lean_obj_arg a) {

if (lean_is_exclusive(a)) return a;

return lean_copy_expand_array_nonlinear(a, false);

}

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_EXPORT 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_EXPORT lean_object * lean_array_push(lean_obj_arg a, lean_obj_arg v);

LEAN_EXPORT lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v);