/*
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 <stdlib.h>
#include <stdbool.h>
#include <stdint.h>
#include <assert.h>
#include <string.h>
#include <stdatomic.h>
#include <limits.h>
#if !defined(__APPLE__)
#include <malloc.h>
#endif

#ifdef __cplusplus
extern "C" {
#endif

#define LEAN_CLOSURE_MAX_ARGS 16

#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

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

#define LeanMaxCtorTag  245
#define LeanClosure     246
#define LeanArray       247
#define LeanStructArray 248
#define LeanScalarArray 249
#define LeanString      250
#define LeanMPZ         251
#define LeanThunk       252
#define LeanTask        253
#define LeanRef         254
#define LeanExternal    255

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

#ifdef LEAN_COMPRESSED_OBJECT_HEADER
// Compressed headers are only supported in 64-bit machines
LEAN_CASSERT(sizeof(void*) == 8);
#endif

/* Lean object header */
typedef struct {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    /* (high) 8-bits  : tag
              8-bits  : num fields for constructors, element size for scalar arrays
              1-bit   : single-threaded
              1-bit   : multi-threaded
              1-bit   : persistent
       (low)  45-bits : RC */
    _Atomic size_t m_header;
#define LEAN_PERSISTENT_BIT 45
#define LEAN_MT_BIT 46
#define LEAN_ST_BIT 47
#else
    _Atomic size_t m_rc;
    uint8_t        m_tag;
    uint8_t        m_mem_kind;
    uint16_t       m_other;  /* num fields for constructors, element size for scalar arrays, etc. */
#define LEAN_ST_MEM_KIND 0
#define LEAN_MT_MEM_KIND 1
#define LEAN_PERSISTENT_MEM_KIND 2
#define LEAN_OTHER_MEM_KIND 3
#endif
} 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:

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;
    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. */
typedef struct {
    lean_object *        m_closure;
    struct lean_task *   m_head_dep;
    struct lean_task *   m_next_dep;
    unsigned             m_prio;
    uint8_t              m_interrupted;
    uint8_t              m_deleted;
} lean_task_imp;

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

void lean_panic_out_of_memory();

void * lean_alloc_heap_object(size_t sz);
void lean_free_heap_obj(lean_object * o);

static inline bool lean_is_mt(lean_object * o) {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    return ((o->m_header >> LEAN_MT_BIT) & 1) != 0;
#else
    return o->m_mem_kind == LEAN_MT_MEM_KIND;
#endif
}

static inline bool lean_is_st(lean_object * o) {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    return ((o->m_header >> LEAN_ST_BIT) & 1) != 0;
#else
    return o->m_mem_kind == LEAN_ST_MEM_KIND;
#endif
}

static inline bool lean_is_heap_obj(lean_object * o) {
    return lean_is_st(o) || lean_is_mt(o);
}

static inline void lean_inc_ref(lean_object * o) {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    if (LEAN_LIKELY(lean_is_st(o))) {
        o->m_header++;
    } else if (lean_is_mt(o)) {
        atomic_fetch_add_explicit(&(o->m_header), 1, memory_order_relaxed);
    }
#else
    if (LEAN_LIKELY(lean_is_st(o))) {
        o->m_rc++;
    } else if (lean_is_mt(o)) {
        atomic_fetch_add_explicit(&(o->m_rc), 1, memory_order_relaxed);
    }
#endif
}

static inline void lean_inc_ref_n(lean_object * o, size_t n) {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    if (LEAN_LIKELY(lean_is_st(o))) {
        o->m_header += n;
    } else if (lean_is_mt(o)) {
        atomic_fetch_add_explicit(&(o->m_header), n, memory_order_relaxed);
    }
#else
    if (LEAN_LIKELY(lean_is_st(o))) {
        o->m_rc += n;
    } else if (lean_is_mt(o)) {
        atomic_fetch_add_explicit(&(o->m_rc), n, memory_order_relaxed);
    }
#endif
}

static inline bool lean_dec_ref_core(lean_object * o) {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    if (LEAN_LIKELY(lean_is_st(o))) {
        o->m_header--;
        return ((o->m_header) & ((1ull << 45) - 1)) == 0;
    } else if (lean_is_mt(o)) {
        return (atomic_fetch_sub_explicit(&(o->m_header), 1, memory_order_acq_rel) & ((1ull << 45) - 1)) == 1;
    } else {
        return false;
    }
#else
    if (LEAN_LIKELY(lean_is_st(o))) {
        o->m_rc--;
        return o->m_rc == 0;
    } else if (lean_is_mt(o)) {
        return atomic_fetch_sub_explicit(&(o->m_rc), 1, memory_order_acq_rel) == 1;
    } else {
        return false;
    }
#endif
}

/* Generic Lean object delete operation. */
void lean_del(lean_object * o);

static inline void lean_dec_ref(lean_object * o) { if (lean_dec_ref_core(o)) lean_del(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 */
void lean_dealloc(lean_object * o);

static inline uint8_t lean_ptr_tag(lean_object * o) {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    return LEAN_BYTE(o->m_header, 7);
#else
    return o->m_tag;
#endif
}

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) {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    if (LEAN_LIKELY(lean_is_st(o))) {
        return ((o->m_header) & ((1ull << 45) - 1)) == 1;
    } else if (lean_is_mt(o)) {
        return (atomic_load_explicit(&(o->m_header), memory_order_acquire) & ((1ull << 45) - 1)) == 1;
    } else {
        return false;
    }
#else
    if (LEAN_LIKELY(lean_is_st(o))) {
        return o->m_rc == 1;
    } else if (lean_is_mt(o)) {
        return atomic_load_explicit(&(o->m_rc), memory_order_acquire) == 1;
    } else {
        return false;
    }
#endif
}

static inline bool lean_is_shared(lean_object * o) {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    if (LEAN_LIKELY(lean_is_st(o))) {
        return ((o->m_header) & ((1ull << 45) - 1)) > 1;
    } else if (lean_is_mt(o)) {
        return (atomic_load_explicit(&(o->m_header), memory_order_acquire) & ((1ull << 45) - 1)) > 1;
    } else {
        return false;
    }
#else
    if (LEAN_LIKELY(lean_is_st(o))) {
        return o->m_rc > 1;
    } else if (lean_is_mt(o)) {
        return atomic_load_explicit(&(o->m_rc), memory_order_acquire) > 1;
    } else {
        return false;
    }
#endif
}

void lean_mark_mt(lean_object * o);
void lean_mark_persistent(lean_object * o);

static inline void lean_set_header(lean_object * o, unsigned tag, unsigned other) {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    o->m_header   = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | (1ull << LEAN_ST_BIT) | 1;
#else
    o->m_rc       = 1;
    o->m_tag      = tag;
    o->m_mem_kind = LEAN_ST_MEM_KIND;
    o->m_other    = other;
#endif
}

/* Constructor objects */

static inline unsigned lean_ctor_num_objs(lean_object * o) {
    assert(lean_is_ctor(o));
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    return LEAN_BYTE(o->m_header, 6);
#else
    return o->m_other;
#endif
}

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 < 256 && scalar_sz < 1024);
    lean_object * o = (lean_object*)lean_alloc_heap_object(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz);
    lean_set_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);
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    LEAN_BYTE(o->m_header, 7) = new_tag;
#else
    o->m_tag = new_tag;
#endif
}

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

/* 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_heap_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
    lean_set_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_object* lean_apply_1(lean_object* f, lean_object* a1);
lean_object* lean_apply_2(lean_object* f, lean_object* a1, lean_object* a2);
lean_object* lean_apply_3(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3);
lean_object* lean_apply_4(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4);
lean_object* lean_apply_5(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5);
lean_object* lean_apply_6(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6);
lean_object* lean_apply_7(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7);
lean_object* lean_apply_8(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8);
lean_object* lean_apply_9(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9);
lean_object* lean_apply_10(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10);
lean_object* lean_apply_11(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11);
lean_object* lean_apply_12(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12);
lean_object* lean_apply_13(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13);
lean_object* lean_apply_14(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14);
lean_object* lean_apply_15(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14, lean_object* a15);
lean_object* lean_apply_16(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14, lean_object* a15, lean_object* a16);
lean_object* lean_apply_n(lean_object* f, unsigned n, lean_object** args);
/* Pre: n > 16 */
lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object** args);

/* Fixpoint */

lean_obj_res lean_fixpoint(lean_obj_arg rec, lean_obj_arg a);
lean_obj_res lean_fixpoint2(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2);
lean_obj_res lean_fixpoint3(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3);
lean_obj_res lean_fixpoint4(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4);
lean_obj_res lean_fixpoint5(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4, lean_obj_arg a5);
lean_obj_res lean_fixpoint6(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4, lean_obj_arg a5, lean_obj_arg a6);

/* 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_heap_object(sizeof(lean_array_object) + sizeof(void*)*capacity);
    lean_set_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 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) {
    assert(lean_is_exclusive(o));
    assert(i < lean_array_size(o));
    lean_to_array(o)->m_data[i] = v;
}

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

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);
        } else {
            return def_val;
        }
    } else {
        /* The index 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 def_val;
    }
}

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

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);
    }
    lean_dec(v);
    return a;
}

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

/* 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_heap_object(sizeof(lean_sarray_object) + elem_size*capacity);
    lean_set_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));
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
    return LEAN_BYTE(o->m_header, 6);
#else
    return o->m_other;
#endif
}
static inline size_t lean_sarray_capacity(lean_object * o) { return lean_to_sarray(o)->m_capacity; }
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_obj_res lean_byte_array_mk(lean_obj_arg a);
lean_obj_res lean_byte_array_data(lean_obj_arg a);
lean_obj_res lean_copy_byte_array(lean_obj_arg a);

static inline lean_obj_res lean_mk_empty_byte_array(b_lean_obj_arg capacity) {
    if (!lean_is_scalar(capacity)) lean_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_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_sarray_cptr(a)[idx] : 0;
    } else {
        /* The index must be out of bounds. Otherwise we would be out of memory. */
        return 0;
    }
}

lean_obj_res lean_byte_array_push(lean_obj_arg a, uint8_t b);

static inline lean_obj_res lean_byte_array_set(lean_obj_arg a, b_lean_obj_arg i, uint8_t b) {
    if (!lean_is_scalar(i)) {
        return a;
    } else {
        size_t idx = lean_unbox(i);
        if (idx >= lean_sarray_size(a)) {
            return a;
        } else {
            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) + idx;
            *it = b;
            return r;
        }
    }
}

/* 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_heap_object(sizeof(lean_string_object) + capacity);
    lean_set_header((lean_object*)o, LeanString, 0);
    o->m_size = size;
    o->m_capacity = capacity;
    o->m_length = len;
    return (lean_object*)o;
}
static inline size_t lean_string_capacity(lean_object * o) { return lean_to_string(o)->m_capacity; }
/* instance : inhabited char := ⟨'A'⟩ */
static inline uint32_t lean_char_default_value() { return 'A'; }
lean_obj_res lean_mk_string(char const * s);
static inline char const * lean_string_cstr(b_lean_obj_arg o) {
    assert(lean_is_string(o));
    return lean_to_string(o)->m_data;
}
static inline size_t lean_string_size(b_lean_obj_arg o) { return lean_to_string(o)->m_size; }
static inline size_t lean_string_len(b_lean_obj_arg o) { return lean_to_string(o)->m_length; }
lean_obj_res lean_string_push(lean_obj_arg s, uint32_t c);
lean_obj_res lean_string_append(lean_obj_arg s1, b_lean_obj_arg s2);
static inline lean_obj_res lean_string_length(b_lean_obj_arg s) { return lean_box(lean_string_len(s)); }
lean_obj_res lean_string_mk(lean_obj_arg cs);
lean_obj_res lean_string_data(lean_obj_arg s);
uint32_t  lean_string_utf8_get(b_lean_obj_arg s, b_lean_obj_arg i);
lean_obj_res lean_string_utf8_next(b_lean_obj_arg s, b_lean_obj_arg i);
lean_obj_res lean_string_utf8_prev(b_lean_obj_arg s, b_lean_obj_arg i);
lean_obj_res lean_string_utf8_set(lean_obj_arg s, b_lean_obj_arg i, uint32_t c);
static inline uint8_t lean_string_utf8_at_end(b_lean_obj_arg s, b_lean_obj_arg i) {
    return !lean_is_scalar(i) || lean_unbox(i) >= lean_string_size(s) - 1;
}
lean_obj_res lean_string_utf8_extract(b_lean_obj_arg s, b_lean_obj_arg b, b_lean_obj_arg e);
static inline lean_obj_res lean_string_utf8_byte_size(b_lean_obj_arg s) { return lean_box(lean_string_size(s) - 1); }
static inline bool lean_string_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) {
    return s1 == s2 ||
        (lean_string_size(s1) == lean_string_size(s2) && memcmp(lean_string_cstr(s1), lean_string_cstr(s2), lean_string_size(s1)) == 0);
}
static inline bool lean_string_ne(b_lean_obj_arg s1, b_lean_obj_arg s2) { return !lean_string_eq(s1, s2); }
bool lean_string_lt(b_lean_obj_arg s1, b_lean_obj_arg s2);
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); }
size_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_heap_object(sizeof(lean_thunk_object));
    lean_set_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_heap_object(sizeof(lean_thunk_object));
    lean_set_header((lean_object*)o, LeanThunk, 0);
    o->m_value   = v;
    o->m_closure = (lean_object*)0;
    return (lean_object*)o;
}

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 the IR instruction for 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;
}

lean_obj_res lean_thunk_map(lean_obj_arg f, lean_obj_arg t);
lean_obj_res lean_thunk_bind(lean_obj_arg x, lean_obj_arg f);

/* Tasks */

void lean_init_task_manager();
void lean_init_task_manager_using(unsigned num_workers);

lean_obj_res lean_mk_task_with_prio(lean_obj_arg c, unsigned prio);
/* Convert a closure `Unit -> A` into a `Task A` */
static inline lean_obj_res lean_mk_task(lean_obj_arg c) { return lean_mk_task_with_prio(c, 0); }
/* Convert a value `a : A` into `Task A` */
lean_obj_res lean_task_pure(lean_obj_arg a);
lean_obj_res lean_task_bind_with_prio(lean_obj_arg x, lean_obj_arg f, unsigned prio);
/* Task.bind (x : Task A) (f : A -> Task B) : Task B */
static inline lean_obj_res lean_task_bind(lean_obj_arg x, lean_obj_arg f) { return lean_task_bind_with_prio(x, f, 0); }
lean_obj_res lean_task_map_with_prio(lean_obj_arg f, lean_obj_arg t, unsigned prio);
/* Task.map (f : A -> B) (t : Task A) : Task B */
static inline lean_obj_res lean_task_map(lean_obj_arg f, lean_obj_arg t) { return lean_task_map_with_prio(f, t, 0); }
/* Task.get (t : Task A) : A */
b_lean_obj_res lean_task_get(b_lean_obj_arg t);

/* External objects */

static inline lean_object * alloc_external(lean_external_class * cls, void * data) {
    lean_external_object * o = (lean_external_object*)lean_alloc_heap_object(sizeof(lean_external_object));
    lean_set_header((lean_object*)o, LeanExternal, 0);
    o->m_class   = cls;
    o->m_data    = data;
    return (lean_object*)o;
}

static inline lean_external_class * lena_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_object * lean_nat_big_succ(lean_object * a);
lean_object * lean_nat_big_add(lean_object * a1, lean_object * a2);
lean_object * lean_nat_big_sub(lean_object * a1, lean_object * a2);
lean_object * lean_nat_big_mul(lean_object * a1, lean_object * a2);
lean_object * lean_nat_overflow_mul(size_t a1, size_t a2);
lean_object * lean_nat_big_div(lean_object * a1, lean_object * a2);
lean_object * lean_nat_big_mod(lean_object * a1, lean_object * a2);
bool lean_nat_big_eq(lean_object * a1, lean_object * a2);
bool lean_nat_big_le(lean_object * a1, lean_object * a2);
bool lean_nat_big_lt(lean_object * a1, lean_object * a2);
lean_object * lean_nat_big_land(lean_object * a1, lean_object * a2);
lean_object * lean_nat_big_lor(lean_object * a1, lean_object * a2);
lean_object * lean_nat_big_xor(lean_object * a1, lean_object * a2);

lean_obj_res lean_cstr_to_nat(char const * n);
lean_obj_res lean_big_size_t_to_nat(size_t n);
lean_obj_res lean_big_uint64_to_nat(size_t n);
static inline lean_obj_res lean_size_t_to_nat(size_t n) {
    if (LEAN_LIKELY(n <= LEAN_MAX_SMALL_NAT))
        return lean_box(n);
    else
        return lean_big_size_t_to_nat(n);
}
static inline lean_obj_res lean_unsigned_to_nat(unsigned n) {
    return lean_size_t_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_size_t_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_size_t_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(0);
        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);
    }
}

/* Integers */

#define LEAN_MAX_SMALL_INT (sizeof(void*) == 8 ? INT_MAX : (1 << 30))
#define LEAN_MIN_SMALL_INT (sizeof(void*) == 8 ? INT_MIN : -(1 << 30))
lean_object * lean_int_big_neg(lean_object * a);
lean_object * lean_int_big_add(lean_object * a1, lean_object * a2);
lean_object * lean_int_big_sub(lean_object * a1, lean_object * a2);
lean_object * lean_int_big_mul(lean_object * a1, lean_object * a2);
lean_object * lean_int_big_div(lean_object * a1, lean_object * a2);
lean_object * lean_int_big_mod(lean_object * a1, lean_object * a2);
bool lean_int_big_eq(lean_object * a1, lean_object * a2);
bool lean_int_big_le(lean_object * a1, lean_object * a2);
bool lean_int_big_lt(lean_object * a1, lean_object * a2);
bool lean_int_big_nonneg(lean_object * a);

lean_object * lean_cstr_to_int(char const * n);
lean_object * lean_big_int_to_int(int n);
lean_object * lean_big_size_t_to_int(size_t n);
lean_object * lean_big_int64_to_int(int64_t n);

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));
    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));
    else
        return ((int)((size_t)a)) >> 1;
}

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));
    else
        return ((int)((size_t)a)) >> 1;
}

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);  lean_dec(s);
    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))) {
        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))) {
        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_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);
    }
}

static inline lean_obj_res nat_abs(b_lean_obj_arg i) {
    if (lean_int_lt(i, lean_box(0))) {
        return lean_int_neg(i);
    } else {
        lean_inc(i);
        return 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);
}


/* UInt8 */

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); }
static inline lean_obj_res lean_uint8_to_nat(uint8_t a) { return lean_size_t_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 ? 0 : a1%a2; }
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 ? 0 : 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; }

/* UInt16 */

uint16_t lean_uint16_of_big_nat(b_lean_obj_arg a);
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); }
inline lean_obj_res lean_uint16_to_nat(uint16_t a) { return lean_size_t_to_nat((size_t)a); }
inline uint16_t lean_uint16_add(uint16_t a1, uint16_t a2) { return a1+a2; }
inline uint16_t lean_uint16_sub(uint16_t a1, uint16_t a2) { return a1-a2; }
inline uint16_t lean_uint16_mul(uint16_t a1, uint16_t a2) { return a1*a2; }
inline uint16_t lean_uint16_div(uint16_t a1, uint16_t a2) { return a2 == 0 ? 0 : a1/a2; }
inline uint16_t lean_uint16_mod(uint16_t a1, uint16_t a2) { return a2 == 0 ? 0 : a1%a2; }
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 ? 0 : a1 % n2;
    } else {
        return a1;
    }
}
inline uint8_t lean_uint16_dec_eq(uint16_t a1, uint16_t a2) { return a1 == a2; }
inline uint8_t lean_uint16_dec_lt(uint16_t a1, uint16_t a2) { return a1 < a2; }
inline uint8_t lean_uint16_dec_le(uint16_t a1, uint16_t a2) { return a1 <= a2; }

/* UInt32 */

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); }
static inline lean_obj_res lean_uint32_to_nat(uint32_t a) { return lean_size_t_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 ? 0 : a1%a2; }
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 ? 0 : 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; }

/* UInt64 */

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); }
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 ? 0 : a1%a2; }
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 ? 0 : 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; }

/* USize */

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); }
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 ? 0 : a1%a2; }
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 ? 0 : 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; }
size_t lean_usize_mix_hash(size_t a1, size_t a2);

/* 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, 1, 0);
    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);
}

/* Debugging helper functions */

lean_object * lean_dbg_trace(lean_obj_arg s, lean_obj_arg fn);
lean_object * lean_dbg_sleep(uint32_t ms, lean_obj_arg fn);
lean_object * lean_dbg_trace_if_shared(lean_obj_arg s, lean_obj_arg a);

/* IO Helper functions */

static inline lean_obj_res lean_io_mk_world() {
    lean_object * r = lean_alloc_ctor(0, 2, 0);
    lean_ctor_set(r, 0, lean_box(0));
    lean_ctor_set(r, 1, lean_box(0));
    return r;
}
static inline bool lean_io_result_is_ok(b_lean_obj_arg r) { return lean_ptr_tag(r) == 0; }
static inline bool lean_io_result_is_error(b_lean_obj_arg r) { return lean_ptr_tag(r) == 1; }
static inline b_lean_obj_res lean_io_result_get_value(b_lean_obj_arg r) { assert(lean_io_result_is_ok(r)); return lean_ctor_get(r, 0); }
static inline b_lean_obj_res lean_io_result_get_error(b_lean_obj_arg r) { assert(lean_io_result_is_error(r)); return lean_ctor_get(r, 0); }
void lean_io_result_show_error(b_lean_obj_arg r);
void lean_io_mark_end_initialization();

/* IO Ref primitives */

lean_obj_res lean_io_mk_ref(lean_obj_arg, lean_obj_arg);
lean_obj_res lean_io_ref_get(b_lean_obj_arg, lean_obj_arg);
lean_obj_res lean_io_ref_set(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
lean_obj_res lean_io_ref_reset(b_lean_obj_arg, lean_obj_arg);
lean_obj_res lean_io_ref_swap(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);

#ifdef __cplusplus
}
#endif