feat(runtime/cpp): add runtime library for Lean -> C++ compiler
This commit is contained in:
Leonardo de Moura
parent
f941af03ba
commit
e36fde4d45
2 changed files with 605 additions and 0 deletions
467
src/runtime/cpp/lean_runtime.cpp
Normal file
467
src/runtime/cpp/lean_runtime.cpp
Normal file
|
|
@ -0,0 +1,467 @@
|
|||
/*
|
||||
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "util/thread.h"
|
||||
#include "util/buffer.h"
|
||||
#include "runtime/cpp/lean_runtime.h"
|
||||
|
||||
#define LEAN_NUM_OBJ_FREE_LISTS 32
|
||||
|
||||
namespace lean {
|
||||
class obj_pool {
|
||||
void * m_free_list[LEAN_NUM_OBJ_FREE_LISTS];
|
||||
public:
|
||||
obj_pool() {
|
||||
for (unsigned i = 0; i < LEAN_NUM_OBJ_FREE_LISTS; i++)
|
||||
m_free_list[i] = nullptr;
|
||||
}
|
||||
|
||||
~obj_pool() {
|
||||
for (unsigned i = 0; i < LEAN_NUM_OBJ_FREE_LISTS; i++) {
|
||||
void * lst = m_free_list[i];
|
||||
while (lst != nullptr) {
|
||||
void * r = lst;
|
||||
lst = *(reinterpret_cast<void **>(r));
|
||||
free(r);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void * allocate(unsigned n) {
|
||||
if (n < LEAN_NUM_OBJ_FREE_LISTS && m_free_list[n] != nullptr) {
|
||||
void * r = m_free_list[n];
|
||||
m_free_list[n] = *(reinterpret_cast<void **>(r));
|
||||
return r;
|
||||
} else {
|
||||
return malloc(sizeof(obj) + sizeof(void*)*n);
|
||||
}
|
||||
}
|
||||
|
||||
void recycle(void * ptr, unsigned n) {
|
||||
if (n < LEAN_NUM_OBJ_FREE_LISTS) {
|
||||
*(reinterpret_cast<void**>(ptr)) = m_free_list[n];
|
||||
m_free_list[n] = ptr;
|
||||
} else {
|
||||
free(ptr);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
LEAN_THREAD_PTR(obj_pool, g_obj_pool);
|
||||
|
||||
static void finalize_obj_pool(void * p) {
|
||||
obj_pool * pool = reinterpret_cast<obj_pool*>(p);
|
||||
delete pool;
|
||||
g_obj_pool = nullptr;
|
||||
}
|
||||
|
||||
void * alloc_obj(unsigned n) {
|
||||
if (!g_obj_pool) {
|
||||
g_obj_pool = new obj_pool();
|
||||
register_post_thread_finalizer(finalize_obj_pool, g_obj_pool);
|
||||
}
|
||||
return g_obj_pool->allocate(n);
|
||||
}
|
||||
|
||||
obj_cell::obj_cell(unsigned cidx, unsigned sz, obj const * fs):
|
||||
m_rc(0), m_kind(static_cast<unsigned>(obj_kind::Constructor)), m_size(sz), m_cidx(cidx) {
|
||||
void ** mem = field_addr();
|
||||
for (unsigned i = 0; i < sz; i++, mem++)
|
||||
new (mem) obj(fs[i]);
|
||||
}
|
||||
|
||||
obj_cell::obj_cell(void * fn, unsigned arity, unsigned sz, obj const * fs):
|
||||
m_rc(0), m_kind(static_cast<unsigned>(obj_kind::Closure)), m_size(sz), m_cidx(arity) {
|
||||
void ** mem = field_addr();
|
||||
for (unsigned i = 0; i < sz; i++, mem++)
|
||||
new (mem) obj(fs[i]);
|
||||
*fn_ptr_addr() = fn;
|
||||
}
|
||||
|
||||
void obj_cell::copy_fields(obj_cell const & src) {
|
||||
obj const * from = src.field_ptr();
|
||||
void ** mem = field_addr();
|
||||
for (unsigned i = 0; i < src.m_size; i++, from++, mem++)
|
||||
new (mem) obj(*from);
|
||||
}
|
||||
|
||||
obj_cell::obj_cell(obj_cell const & src, obj const & a1):
|
||||
m_rc(0), m_kind(static_cast<unsigned>(obj_kind::Closure)), m_size(src.m_size+1), m_cidx(src.m_cidx) {
|
||||
copy_fields(src);
|
||||
void ** f = field_addr();
|
||||
new (f + src.m_size) obj(a1);
|
||||
}
|
||||
|
||||
obj_cell::obj_cell(obj_cell const & src, obj const & a1, obj const & a2):
|
||||
m_rc(0), m_kind(static_cast<unsigned>(obj_kind::Closure)), m_size(src.m_size+2), m_cidx(src.m_cidx) {
|
||||
copy_fields(src);
|
||||
void ** f = field_addr();
|
||||
new (f + src.m_size) obj(a1);
|
||||
new (f + src.m_size + 1) obj(a2);
|
||||
}
|
||||
|
||||
obj_cell::obj_cell(obj_cell const & src, obj const & a1, obj const & a2, obj const & a3):
|
||||
m_rc(0), m_kind(static_cast<unsigned>(obj_kind::Closure)), m_size(src.m_size+3), m_cidx(src.m_cidx) {
|
||||
copy_fields(src);
|
||||
void ** f = field_addr();
|
||||
new (f + src.m_size) obj(a1);
|
||||
new (f + src.m_size + 1) obj(a2);
|
||||
new (f + src.m_size + 2) obj(a3);
|
||||
}
|
||||
|
||||
obj_cell::obj_cell(obj_cell const & src, obj const & a1, obj const & a2, obj const & a3, obj const & a4):
|
||||
m_rc(0), m_kind(static_cast<unsigned>(obj_kind::Closure)), m_size(src.m_size+4), m_cidx(src.m_cidx) {
|
||||
copy_fields(src);
|
||||
void ** f = field_addr();
|
||||
new (f + src.m_size) obj(a1);
|
||||
new (f + src.m_size + 1) obj(a2);
|
||||
new (f + src.m_size + 2) obj(a3);
|
||||
new (f + src.m_size + 3) obj(a4);
|
||||
}
|
||||
|
||||
obj_cell::obj_cell(obj_cell const & src, obj const & a1, obj const & a2, obj const & a3, obj const & a4, obj const & a5):
|
||||
m_rc(0), m_kind(static_cast<unsigned>(obj_kind::Closure)), m_size(src.m_size+5), m_cidx(src.m_cidx) {
|
||||
copy_fields(src);
|
||||
void ** f = field_addr();
|
||||
new (f + src.m_size) obj(a1);
|
||||
new (f + src.m_size + 1) obj(a2);
|
||||
new (f + src.m_size + 2) obj(a3);
|
||||
new (f + src.m_size + 3) obj(a4);
|
||||
new (f + src.m_size + 4) obj(a5);
|
||||
}
|
||||
|
||||
obj_cell::obj_cell(obj_cell const & src, obj const & a1, obj const & a2, obj const & a3, obj const & a4, obj const & a5,
|
||||
obj const & a6):
|
||||
m_rc(0), m_kind(static_cast<unsigned>(obj_kind::Closure)), m_size(src.m_size+6), m_cidx(src.m_cidx) {
|
||||
copy_fields(src);
|
||||
void ** f = field_addr();
|
||||
new (f + src.m_size) obj(a1);
|
||||
new (f + src.m_size + 1) obj(a2);
|
||||
new (f + src.m_size + 2) obj(a3);
|
||||
new (f + src.m_size + 3) obj(a4);
|
||||
new (f + src.m_size + 4) obj(a5);
|
||||
new (f + src.m_size + 5) obj(a6);
|
||||
}
|
||||
|
||||
obj_cell::obj_cell(obj_cell const & src, obj const & a1, obj const & a2, obj const & a3, obj const & a4, obj const & a5,
|
||||
obj const & a6, obj const & a7):
|
||||
m_rc(0), m_kind(static_cast<unsigned>(obj_kind::Closure)), m_size(src.m_size+7), m_cidx(src.m_cidx) {
|
||||
copy_fields(src);
|
||||
void ** f = field_addr();
|
||||
new (f + src.m_size) obj(a1);
|
||||
new (f + src.m_size + 1) obj(a2);
|
||||
new (f + src.m_size + 2) obj(a3);
|
||||
new (f + src.m_size + 3) obj(a4);
|
||||
new (f + src.m_size + 4) obj(a5);
|
||||
new (f + src.m_size + 5) obj(a6);
|
||||
new (f + src.m_size + 6) obj(a7);
|
||||
}
|
||||
|
||||
obj_cell::obj_cell(obj_cell const & src, obj const & a1, obj const & a2, obj const & a3, obj const & a4, obj const & a5,
|
||||
obj const & a6, obj const & a7, obj const & a8):
|
||||
m_rc(0), m_kind(static_cast<unsigned>(obj_kind::Closure)), m_size(src.m_size+8), m_cidx(src.m_cidx) {
|
||||
copy_fields(src);
|
||||
void ** f = field_addr();
|
||||
new (f + src.m_size) obj(a1);
|
||||
new (f + src.m_size + 1) obj(a2);
|
||||
new (f + src.m_size + 2) obj(a3);
|
||||
new (f + src.m_size + 3) obj(a4);
|
||||
new (f + src.m_size + 4) obj(a5);
|
||||
new (f + src.m_size + 5) obj(a6);
|
||||
new (f + src.m_size + 6) obj(a7);
|
||||
new (f + src.m_size + 7) obj(a8);
|
||||
}
|
||||
|
||||
#define DEC_FIELDS(o, todo) { \
|
||||
void ** f = o->field_addr(); \
|
||||
for (unsigned i = 0; i < o->m_size; i++, f++) { \
|
||||
obj_cell * c = reinterpret_cast<obj*>(f)->steal_ptr(); \
|
||||
if (LEAN_IS_PTR(c) && c->dec_ref_core()) \
|
||||
todo.push_back(c); \
|
||||
} \
|
||||
}
|
||||
|
||||
void obj_cell::dealloc() {
|
||||
try {
|
||||
buffer<obj_cell*> todo;
|
||||
todo.push_back(this);
|
||||
while (!todo.empty()) {
|
||||
obj_cell * it = todo.back();
|
||||
unsigned sz = it->m_size;
|
||||
todo.pop_back();
|
||||
switch (it->kind()) {
|
||||
case obj_kind::Constructor:
|
||||
DEC_FIELDS(it, todo);
|
||||
it->~obj_cell();
|
||||
g_obj_pool->recycle(it, sz);
|
||||
break;
|
||||
case obj_kind::Closure:
|
||||
DEC_FIELDS(it, todo);
|
||||
it->~obj_cell();
|
||||
g_obj_pool->recycle(it, sz+1);
|
||||
break;
|
||||
case obj_kind::MPN:
|
||||
// TODO(Leo):
|
||||
break;
|
||||
}
|
||||
}
|
||||
} catch (std::bad_alloc&) {
|
||||
// We need this catch, because push_back may fail when expanding the buffer.
|
||||
// In this case, we avoid the crash, and "accept" the memory leak.
|
||||
}
|
||||
}
|
||||
|
||||
obj mk_obj(unsigned cidx, unsigned n, obj const * fs) {
|
||||
void * mem = alloc_obj(n);
|
||||
return obj(new (mem) obj_cell(cidx, n, fs));
|
||||
}
|
||||
|
||||
obj mk_closure_core(void * fn, unsigned arity, unsigned n, obj const * fs) {
|
||||
void * mem = alloc_obj(n+1);
|
||||
return obj(new (mem) obj_cell(fn, arity, n, fs));
|
||||
}
|
||||
|
||||
static obj mk_closure(obj const & f, obj const & a1) {
|
||||
void * mem = alloc_obj(f.size()+1);
|
||||
return obj(new (mem) obj_cell(f.data(), a1));
|
||||
}
|
||||
|
||||
static obj mk_closure(obj const & f, obj const & a1, obj const & a2) {
|
||||
void * mem = alloc_obj(f.size()+2);
|
||||
return obj(new (mem) obj_cell(f.data(), a1, a2));
|
||||
}
|
||||
|
||||
static obj mk_closure(obj const & f, obj const & a1, obj const & a2, obj const & a3) {
|
||||
void * mem = alloc_obj(f.size()+3);
|
||||
return obj(new (mem) obj_cell(f.data(), a1, a2, a3));
|
||||
}
|
||||
|
||||
static obj mk_closure(obj const & f, obj const & a1, obj const & a2, obj const & a3, obj const & a4) {
|
||||
void * mem = alloc_obj(f.size()+4);
|
||||
return obj(new (mem) obj_cell(f.data(), a1, a2, a3, a4));
|
||||
}
|
||||
|
||||
static obj mk_closure(obj const & f, obj const & a1, obj const & a2, obj const & a3, obj const & a4,
|
||||
obj const & a5) {
|
||||
void * mem = alloc_obj(f.size()+5);
|
||||
return obj(new (mem) obj_cell(f.data(), a1, a2, a3, a4, a5));
|
||||
}
|
||||
|
||||
static obj mk_closure(obj const & f, obj const & a1, obj const & a2, obj const & a3, obj const & a4,
|
||||
obj const & a5, obj const & a6) {
|
||||
void * mem = alloc_obj(f.size()+6);
|
||||
return obj(new (mem) obj_cell(f.data(), a1, a2, a3, a4, a5, a6));
|
||||
}
|
||||
|
||||
static obj mk_closure(obj const & f, obj const & a1, obj const & a2, obj const & a3, obj const & a4,
|
||||
obj const & a5, obj const & a6, obj const & a7) {
|
||||
void * mem = alloc_obj(f.size()+7);
|
||||
return obj(new (mem) obj_cell(f.data(), a1, a2, a3, a4, a5, a6, a7));
|
||||
}
|
||||
|
||||
static obj mk_closure(obj const & f, obj const & a1, obj const & a2, obj const & a3, obj const & a4,
|
||||
obj const & a5, obj const & a6, obj const & a7, obj const & a8) {
|
||||
void * mem = alloc_obj(f.size()+8);
|
||||
return obj(new (mem) obj_cell(f.data(), a1, a2, a3, a4, a5, a6, a7, a8));
|
||||
}
|
||||
|
||||
typedef obj (*fn1)(obj const &);
|
||||
typedef obj (*fn2)(obj const &, obj const &);
|
||||
typedef obj (*fn3)(obj const &, obj const &, obj const &);
|
||||
typedef obj (*fn4)(obj const &, obj const &, obj const &, obj const &);
|
||||
typedef obj (*fn5)(obj const &, obj const &, obj const &, obj const &, obj const &);
|
||||
typedef obj (*fn6)(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &);
|
||||
typedef obj (*fn7)(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &);
|
||||
typedef obj (*fn8)(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &);
|
||||
typedef obj (*fn9)(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &, obj const &);
|
||||
typedef obj (*fn10)(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &, obj const &, obj const &);
|
||||
typedef obj (*fn11)(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &, obj const &, obj const &, obj const &);
|
||||
typedef obj (*fn12)(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &, obj const &, obj const &, obj const &, obj const &);
|
||||
typedef obj (*fn13)(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &);
|
||||
typedef obj (*fn14)(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &);
|
||||
typedef obj (*fn15)(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &, obj const &);
|
||||
typedef obj (*fn16)(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &, obj const &, obj const &);
|
||||
typedef obj (*fnN)(unsigned, obj const *);
|
||||
|
||||
inline fn1 to_fn1(obj const & o) { return reinterpret_cast<fn1>(o.fn_ptr()); }
|
||||
inline fn2 to_fn2(obj const & o) { return reinterpret_cast<fn2>(o.fn_ptr()); }
|
||||
inline fn3 to_fn3(obj const & o) { return reinterpret_cast<fn3>(o.fn_ptr()); }
|
||||
inline fn4 to_fn4(obj const & o) { return reinterpret_cast<fn4>(o.fn_ptr()); }
|
||||
inline fn5 to_fn5(obj const & o) { return reinterpret_cast<fn5>(o.fn_ptr()); }
|
||||
inline fn6 to_fn6(obj const & o) { return reinterpret_cast<fn6>(o.fn_ptr()); }
|
||||
inline fn7 to_fn7(obj const & o) { return reinterpret_cast<fn7>(o.fn_ptr()); }
|
||||
inline fn8 to_fn8(obj const & o) { return reinterpret_cast<fn8>(o.fn_ptr()); }
|
||||
inline fnN to_fnN(obj const & o) { return reinterpret_cast<fnN>(o.fn_ptr()); }
|
||||
|
||||
#define FN1 to_fn1(*this)
|
||||
#define FN2 to_fn2(*this)
|
||||
#define FN3 to_fn3(*this)
|
||||
#define FN4 to_fn4(*this)
|
||||
#define FN5 to_fn5(*this)
|
||||
#define FN6 to_fn6(*this)
|
||||
#define FN7 to_fn7(*this)
|
||||
#define FN8 to_fn8(*this)
|
||||
#define FNN to_fnN(*this)
|
||||
|
||||
obj obj::apply() const {
|
||||
unsigned ar = arity();
|
||||
if (ar == size()) {
|
||||
switch (ar) {
|
||||
case 1: return FN1(fld(0));
|
||||
case 2: return FN2(fld(0), fld(1));
|
||||
case 3: return FN3(fld(0), fld(1), fld(2));
|
||||
case 4: return FN4(fld(0), fld(1), fld(2), fld(3));
|
||||
case 5: return FN5(fld(0), fld(1), fld(2), fld(3), fld(4));
|
||||
case 6: return FN6(fld(0), fld(1), fld(2), fld(3), fld(4), fld(5));
|
||||
case 7: return FN7(fld(0), fld(1), fld(2), fld(3), fld(4), fld(5), fld(6));
|
||||
case 8: return FN8(fld(0), fld(1), fld(2), fld(3), fld(4), fld(5), fld(6), fld(7));
|
||||
default: return FNN(ar, m_data->field_ptr());
|
||||
}
|
||||
} else {
|
||||
return *this;
|
||||
}
|
||||
}
|
||||
|
||||
obj obj::apply(obj const & a1) const {
|
||||
unsigned ar = arity();
|
||||
if (ar == size() + 1) {
|
||||
switch (ar) {
|
||||
case 1: return FN1(a1);
|
||||
case 2: return FN2(fld(0), a1);
|
||||
case 3: return FN3(fld(0), fld(1), a1);
|
||||
case 4: return FN4(fld(0), fld(1), fld(2), a1);
|
||||
case 5: return FN5(fld(0), fld(1), fld(2), fld(3), a1);
|
||||
case 6: return FN6(fld(0), fld(1), fld(2), fld(3), fld(4), a1);
|
||||
case 7: return FN7(fld(0), fld(1), fld(2), fld(3), fld(4), fld(5), a1);
|
||||
case 8: return FN8(fld(0), fld(1), fld(2), fld(3), fld(4), fld(5), fld(6), a1);
|
||||
default: return mk_closure(*this, a1).apply();
|
||||
}
|
||||
} else {
|
||||
return mk_closure(*this, a1);
|
||||
}
|
||||
}
|
||||
|
||||
obj obj::apply(obj const & a1, obj const & a2) const {
|
||||
unsigned ar = arity();
|
||||
if (ar == size() + 2) {
|
||||
switch (ar) {
|
||||
case 2: return FN2(a1, a2);
|
||||
case 3: return FN3(fld(0), a1, a2);
|
||||
case 4: return FN4(fld(0), fld(1), a1, a2);
|
||||
case 5: return FN5(fld(0), fld(1), fld(2), a1, a2);
|
||||
case 6: return FN6(fld(0), fld(1), fld(2), fld(3), a1, a2);
|
||||
case 7: return FN7(fld(0), fld(1), fld(2), fld(3), fld(4), a1, a2);
|
||||
case 8: return FN8(fld(0), fld(1), fld(2), fld(3), fld(4), fld(5), a1, a2);
|
||||
default: return mk_closure(*this, a1, a2).apply();
|
||||
}
|
||||
} else {
|
||||
return mk_closure(*this, a1, a2);
|
||||
}
|
||||
}
|
||||
|
||||
obj obj::apply(obj const & a1, obj const & a2, obj const & a3) const {
|
||||
unsigned ar = arity();
|
||||
if (ar == size() + 3) {
|
||||
switch (ar) {
|
||||
case 3: return FN3(a1, a2, a3);
|
||||
case 4: return FN4(fld(0), a1, a2, a3);
|
||||
case 5: return FN5(fld(0), fld(1), a1, a2, a3);
|
||||
case 6: return FN6(fld(0), fld(1), fld(2), a1, a2, a3);
|
||||
case 7: return FN7(fld(0), fld(1), fld(2), fld(3), a1, a2, a3);
|
||||
case 8: return FN8(fld(0), fld(1), fld(2), fld(3), fld(4), a1, a2, a3);
|
||||
default: return mk_closure(*this, a1, a2, a3).apply();
|
||||
}
|
||||
} else {
|
||||
return mk_closure(*this, a1, a2, a3);
|
||||
}
|
||||
}
|
||||
|
||||
obj obj::apply(obj const & a1, obj const & a2, obj const & a3, obj const & a4) const {
|
||||
unsigned ar = arity();
|
||||
if (ar == size() + 4) {
|
||||
switch (ar) {
|
||||
case 4: return FN4(a1, a2, a3, a4);
|
||||
case 5: return FN5(fld(0), a1, a2, a3, a4);
|
||||
case 6: return FN6(fld(0), fld(1), a1, a2, a3, a4);
|
||||
case 7: return FN7(fld(0), fld(1), fld(2), a1, a2, a3, a4);
|
||||
case 8: return FN8(fld(0), fld(1), fld(2), fld(3), a1, a2, a3, a4);
|
||||
default: return mk_closure(*this, a1, a2, a3, a4).apply();
|
||||
}
|
||||
} else {
|
||||
return mk_closure(*this, a1, a2, a3, a4);
|
||||
}
|
||||
}
|
||||
|
||||
obj obj::apply(obj const & a1, obj const & a2, obj const & a3, obj const & a4, obj const & a5) const {
|
||||
unsigned ar = arity();
|
||||
if (ar == size() + 5) {
|
||||
switch (ar) {
|
||||
case 5: return FN5(a1, a2, a3, a4, a5);
|
||||
case 6: return FN6(fld(0), a1, a2, a3, a4, a5);
|
||||
case 7: return FN7(fld(0), fld(1), a1, a2, a3, a4, a5);
|
||||
case 8: return FN8(fld(0), fld(1), fld(2), a1, a2, a3, a4, a5);
|
||||
default: return mk_closure(*this, a1, a2, a3, a4, a5).apply();
|
||||
}
|
||||
} else {
|
||||
return mk_closure(*this, a1, a2, a3, a4, a5);
|
||||
}
|
||||
}
|
||||
|
||||
obj obj::apply(obj const & a1, obj const & a2, obj const & a3, obj const & a4, obj const & a5, obj const & a6) const {
|
||||
unsigned ar = arity();
|
||||
if (ar == size() + 6) {
|
||||
switch (ar) {
|
||||
case 6: return FN6(a1, a2, a3, a4, a5, a6);
|
||||
case 7: return FN7(fld(0), a1, a2, a3, a4, a5, a6);
|
||||
case 8: return FN8(fld(0), fld(1), a1, a2, a3, a4, a5, a6);
|
||||
default: return mk_closure(*this, a1, a2, a3, a4, a5, a6).apply();
|
||||
}
|
||||
} else {
|
||||
return mk_closure(*this, a1, a2, a3, a4, a5, a6);
|
||||
}
|
||||
}
|
||||
|
||||
obj obj::apply(obj const & a1, obj const & a2, obj const & a3, obj const & a4, obj const & a5, obj const & a6,
|
||||
obj const & a7) const {
|
||||
unsigned ar = arity();
|
||||
if (ar == size() + 7) {
|
||||
switch (ar) {
|
||||
case 7: return FN7(a1, a2, a3, a4, a5, a6, a7);
|
||||
case 8: return FN8(fld(0), a1, a2, a3, a4, a5, a6, a7);
|
||||
default: return mk_closure(*this, a1, a2, a3, a4, a5, a6, a7).apply();
|
||||
}
|
||||
} else {
|
||||
return mk_closure(*this, a1, a2, a3, a4, a5, a6, a7);
|
||||
}
|
||||
}
|
||||
|
||||
obj obj::apply(obj const & a1, obj const & a2, obj const & a3, obj const & a4, obj const & a5, obj const & a6,
|
||||
obj const & a7, obj const & a8) const {
|
||||
unsigned ar = arity();
|
||||
if (ar == size() + 8) {
|
||||
switch (ar) {
|
||||
case 8: return FN8(a1, a2, a3, a4, a5, a6, a7, a8);
|
||||
default: return mk_closure(*this, a1, a2, a3, a4, a5, a6, a7, a8).apply();
|
||||
}
|
||||
} else {
|
||||
return mk_closure(*this, a1, a2, a3, a4, a5, a6, a7, a8);
|
||||
}
|
||||
}
|
||||
}
|
||||
138
src/runtime/cpp/lean_runtime.h
Normal file
138
src/runtime/cpp/lean_runtime.h
Normal file
|
|
@ -0,0 +1,138 @@
|
|||
/*
|
||||
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/thread.h"
|
||||
#include <vector>
|
||||
#include <gmp.h>
|
||||
|
||||
namespace lean {
|
||||
class obj;
|
||||
enum class obj_kind { Constructor, Closure, MPN };
|
||||
|
||||
class obj_cell {
|
||||
atomic<unsigned> m_rc;
|
||||
unsigned m_kind:2;
|
||||
unsigned m_size:14;
|
||||
unsigned m_cidx:16; // constructor idx if Constructor, and arity if closure
|
||||
bool dec_ref_core() {
|
||||
if (atomic_fetch_sub_explicit(&m_rc, 1u, memory_order_release) == 1u) {
|
||||
atomic_thread_fence(memory_order_acquire);
|
||||
return true;
|
||||
} else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
void dealloc();
|
||||
obj_cell(unsigned cidx, unsigned sz, obj const * fs);
|
||||
obj_cell(void * fn, unsigned arity, unsigned sz, obj const * fs);
|
||||
friend obj mk_obj(unsigned cidx, unsigned n, obj const * fs);
|
||||
friend obj mk_closure_core(void * fn, unsigned arity, unsigned n, obj const * fs);
|
||||
void ** field_addr() {
|
||||
return reinterpret_cast<void **>(reinterpret_cast<char*>(this)+sizeof(obj_cell));
|
||||
}
|
||||
void ** fn_ptr_addr() { return field_addr() + m_size; }
|
||||
void copy_fields(obj_cell const & src);
|
||||
public:
|
||||
obj_cell(obj_cell const & src, obj const & a1);
|
||||
obj_cell(obj_cell const & src, obj const & a1, obj const & a2);
|
||||
obj_cell(obj_cell const & src, obj const & a1, obj const & a2, obj const & a3);
|
||||
obj_cell(obj_cell const & src, obj const & a1, obj const & a2, obj const & a3, obj const & a4);
|
||||
obj_cell(obj_cell const & src, obj const & a1, obj const & a2, obj const & a3, obj const & a4, obj const & a5);
|
||||
obj_cell(obj_cell const & src, obj const & a1, obj const & a2, obj const & a3, obj const & a4, obj const & a5,
|
||||
obj const & a6);
|
||||
obj_cell(obj_cell const & src, obj const & a1, obj const & a2, obj const & a3, obj const & a4, obj const & a5,
|
||||
obj const & a6, obj const & a7);
|
||||
obj_cell(obj_cell const & src, obj const & a1, obj const & a2, obj const & a3, obj const & a4, obj const & a5,
|
||||
obj const & a6, obj const & a7, obj const & a8);
|
||||
unsigned get_rc() const { return atomic_load(&m_rc); }
|
||||
void inc_ref() { atomic_fetch_add_explicit(&m_rc, 1u, memory_order_relaxed); }
|
||||
void dec_ref() { if (dec_ref_core()) { dealloc(); } }
|
||||
obj_kind kind() const { return static_cast<obj_kind>(m_kind); }
|
||||
size_t cidx() const { return m_cidx; }
|
||||
unsigned size() const { return m_size; }
|
||||
unsigned arity() const { return m_cidx; }
|
||||
obj const * field_ptr() const {
|
||||
return reinterpret_cast<obj const *>(reinterpret_cast<char const *>(this)+sizeof(obj_cell));
|
||||
}
|
||||
void * fn_ptr() const {
|
||||
return *(reinterpret_cast<void **>(const_cast<obj*>(field_ptr()))+m_size);
|
||||
}
|
||||
};
|
||||
|
||||
#define LEAN_IS_PTR(obj) ((reinterpret_cast<size_t>(obj) & 1) == 0)
|
||||
#define LEAN_BOX(num) (reinterpret_cast<obj_cell*>((num << 1) | 1))
|
||||
#define LEAN_UNBOX(obj) (reinterpret_cast<size_t>(obj) >> 1)
|
||||
|
||||
class obj {
|
||||
friend class obj_cell;
|
||||
obj_cell * m_data;
|
||||
void copy_fields(std::vector<obj> & r);
|
||||
obj apply() const;
|
||||
obj_cell * steal_ptr() { obj_cell * r = m_data; m_data = LEAN_BOX(0); return r; }
|
||||
public:
|
||||
obj():m_data(LEAN_BOX(0)) { static_assert(sizeof(obj) == sizeof(void *), "unexpected class obj size"); }
|
||||
obj(unsigned cidx):m_data(LEAN_BOX(cidx)) {}
|
||||
obj(obj_cell * c):m_data(c) { m_data->inc_ref(); }
|
||||
obj(obj const & o):m_data(o.m_data) { if (LEAN_IS_PTR(m_data)) m_data->inc_ref(); }
|
||||
obj(obj && o):m_data(o.m_data) { o.m_data = LEAN_BOX(0); }
|
||||
~obj() { if (LEAN_IS_PTR(m_data)) m_data->dec_ref(); }
|
||||
|
||||
obj & operator=(obj const & s) {
|
||||
if (LEAN_IS_PTR(s.m_data))
|
||||
s.m_data->inc_ref();
|
||||
auto new_data = s.m_data;
|
||||
if (LEAN_IS_PTR(m_data))
|
||||
m_data->dec_ref();
|
||||
m_data = new_data;
|
||||
return *this;
|
||||
}
|
||||
|
||||
obj & operator=(obj && s) {
|
||||
if (LEAN_IS_PTR(m_data))
|
||||
m_data->dec_ref();
|
||||
m_data = s.m_data;
|
||||
s.m_data = LEAN_BOX(0);
|
||||
return *this;
|
||||
}
|
||||
|
||||
obj_cell const & data() const { return *m_data; }
|
||||
size_t cidx() const { return LEAN_IS_PTR(m_data) ? m_data->cidx() : LEAN_UNBOX(m_data); }
|
||||
unsigned size() const { return m_data->size(); }
|
||||
obj const & fld(unsigned fidx) const { return m_data->field_ptr()[fidx]; }
|
||||
obj const & operator[](unsigned fidx) const { return fld(fidx); }
|
||||
|
||||
unsigned arity() const { return m_data->arity(); }
|
||||
void * fn_ptr() const { return m_data->fn_ptr(); }
|
||||
|
||||
obj apply(obj const &) const;
|
||||
obj apply(obj const &, obj const &) const;
|
||||
obj apply(obj const &, obj const &, obj const &) const;
|
||||
obj apply(obj const &, obj const &, obj const &, obj const &) const;
|
||||
obj apply(obj const &, obj const &, obj const &, obj const &, obj const &) const;
|
||||
obj apply(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &) const;
|
||||
obj apply(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &) const;
|
||||
obj apply(obj const &, obj const &, obj const &, obj const &, obj const &, obj const &,
|
||||
obj const &, obj const &) const;
|
||||
obj apply(unsigned, obj const *) const;
|
||||
};
|
||||
|
||||
inline obj mk_obj(unsigned cidx) { return obj(cidx); }
|
||||
obj mk_obj(unsigned cidx, unsigned n, obj const * fs);
|
||||
inline obj mk_obj(unsigned cidx, obj const & o) { return mk_obj(cidx, 1, &o); }
|
||||
inline obj mk_obj(unsigned cidx, std::initializer_list<obj> const & os) { return mk_obj(cidx, os.size(), os.begin()); }
|
||||
|
||||
obj mk_closure_core(void * fn, unsigned arity, unsigned n, obj const * fs);
|
||||
template<typename T>
|
||||
obj mk_closure(T fn, unsigned arity, unsigned n, obj const * fs) {
|
||||
return mk_closure_core(reinterpret_cast<void*>(fn), arity, n, fs);
|
||||
}
|
||||
template<typename T>
|
||||
obj mk_closure(T fn, unsigned arity, std::initializer_list<obj> const & os) {
|
||||
return mk_closure_core(reinterpret_cast<void*>(fn), arity, os.size(), os.begin());
|
||||
}
|
||||
}
|
||||
Loading…
Reference in a new issue