max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/vm/vm): add dynamic declare_vm_builtin

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-31 17:42:42 -07:00
parent b31a7bd3e7
commit 032750f4cb
2 changed files with 69 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

57
src/library/vm/vm.cpp
View file

@ -543,13 +543,10 @@ static vm_instr read_vm_instr(deserializer & d, name_map<unsigned> const & name2
}
vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn):
m_rc(0), m_kind(vm_decl_kind::Builtin), m_name(n), m_idx(idx), m_arity(arity), m_fn(fn), m_cfn(nullptr) {}
m_rc(0), m_kind(vm_decl_kind::Builtin), m_name(n), m_idx(idx), m_arity(arity), m_fn(fn) {}
vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfunction fn):
m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(arity), m_fn(nullptr), m_cfn(fn) {}
vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn1, vm_cfunction fn2):
m_rc(0), m_kind(vm_decl_kind::BuiltinCFun), m_name(n), m_idx(idx), m_arity(arity), m_fn(fn1), m_cfn(fn2) {}
m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(arity), m_cfn(fn) {}
vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code):
m_rc(0), m_kind(vm_decl_kind::Bytecode), m_name(n), m_idx(idx), m_expr(e), m_arity(0),
@ -683,6 +680,54 @@ static environment update(environment const & env, vm_decls const & ext) {
return env.update(g_ext->m_ext_id, std::make_shared<vm_decls>(ext));
}
static environment declare_vm_builtin(environment const & env, name const & n, unsigned arity, vm_cfunction fn) {
auto ext = get_extension(env);
if (auto idx = ext.m_name2idx.find(n)) {
vm_decl d = ext.m_decls[*idx];
lean_assert(d.get_arity() == arity);
ext.m_decls.set(*idx, vm_decl(n, *idx, arity, fn));
} else {
ext.add(vm_decl(n, ext.m_decls.size(), arity, fn));
}
return update(env, ext);
}
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_1 fn) {
return declare_vm_builtin(env, n, 1, reinterpret_cast<vm_cfunction>(fn));
}
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_2 fn) {
return declare_vm_builtin(env, n, 2, reinterpret_cast<vm_cfunction>(fn));
}
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_3 fn) {
return declare_vm_builtin(env, n, 3, reinterpret_cast<vm_cfunction>(fn));
}
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_4 fn) {
return declare_vm_builtin(env, n, 4, reinterpret_cast<vm_cfunction>(fn));
}
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_5 fn) {
return declare_vm_builtin(env, n, 5, reinterpret_cast<vm_cfunction>(fn));
}
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_6 fn) {
return declare_vm_builtin(env, n, 6, reinterpret_cast<vm_cfunction>(fn));
}
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_7 fn) {
return declare_vm_builtin(env, n, 7, reinterpret_cast<vm_cfunction>(fn));
}
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_8 fn) {
return declare_vm_builtin(env, n, 8, reinterpret_cast<vm_cfunction>(fn));
}
environment declare_vm_builtin(environment const & env, name const & n, unsigned arity, vm_cfunction_N fn) {
return declare_vm_builtin(env, n, arity, reinterpret_cast<vm_cfunction>(fn));
}
bool is_vm_function(environment const & env, name const & fn) {
auto const & ext = get_extension(env);
return ext.m_name2idx.contains(fn) || g_vm_builtins->contains(fn);
@ -1393,7 +1438,7 @@ void vm_state::invoke(vm_decl const & d) {
switch (d.kind()) {
case vm_decl_kind::Bytecode:
invoke_global(d); break;
case vm_decl_kind::Builtin: case vm_decl_kind::BuiltinCFun:
case vm_decl_kind::Builtin:
invoke_builtin(d); break;
case vm_decl_kind::CFun:
invoke_cfun(d); break;

35
src/library/vm/vm.h
View file

@ -376,7 +376,7 @@ vm_instr mk_closure_instr(unsigned fn_idx, unsigned n);
class vm_state;
class vm_instr;
enum class vm_decl_kind { Bytecode, Builtin, CFun, BuiltinCFun };
enum class vm_decl_kind { Bytecode, Builtin, CFun };
/** \brief VM function/constant declaration cell */
struct vm_decl_cell {
@ -391,14 +391,11 @@ struct vm_decl_cell {
unsigned m_code_size;
vm_instr * m_code;
};
struct {
vm_function m_fn;
vm_cfunction m_cfn;
};
vm_function m_fn;
vm_cfunction m_cfn;
};
vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn);
vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfunction fn);
vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn1, vm_cfunction fn2);
vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code);
~vm_decl_cell();
void dealloc();
@ -414,8 +411,6 @@ public:
vm_decl(new vm_decl_cell(n, idx, arity, fn)) {}
vm_decl(name const & n, unsigned idx, unsigned arity, vm_cfunction fn):
vm_decl(new vm_decl_cell(n, idx, arity, fn)) {}
vm_decl(name const & n, unsigned idx, unsigned arity, vm_function fn1, vm_cfunction fn2):
vm_decl(new vm_decl_cell(n, idx, arity, fn1, fn2)) {}
vm_decl(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code):
vm_decl(new vm_decl_cell(n, idx, e, code_sz, code)) {}
vm_decl(vm_decl const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
@ -429,14 +424,8 @@ public:
vm_decl_kind kind() const { return m_ptr->m_kind; }
bool is_bytecode() const { lean_assert(m_ptr); return m_ptr->m_kind == vm_decl_kind::Bytecode; }
bool is_builtin() const {
lean_assert(m_ptr);
return m_ptr->m_kind == vm_decl_kind::Builtin || m_ptr->m_kind == vm_decl_kind::BuiltinCFun;
}
bool is_cfun() const {
lean_assert(m_ptr);
return m_ptr->m_kind == vm_decl_kind::CFun || m_ptr->m_kind == vm_decl_kind::BuiltinCFun;
}
bool is_builtin() const { lean_assert(m_ptr); return m_ptr->m_kind == vm_decl_kind::Builtin; }
bool is_cfun() const { lean_assert(m_ptr); return m_ptr->m_kind == vm_decl_kind::CFun; }
unsigned get_idx() const { lean_assert(m_ptr); return m_ptr->m_idx; }
name get_name() const { lean_assert(m_ptr); return m_ptr->m_name; }
unsigned get_arity() const { lean_assert(m_ptr); return m_ptr->m_arity; }
@ -531,7 +520,8 @@ public:
};
/** \brief Add builtin implementation for the function named \c n.
All environment objects will contain this builtin. */
All environment objects will contain this builtin.
\pre These procedures can only be invoked at initialization time. */
void declare_vm_builtin(name const & n, unsigned arity, vm_function fn);
void declare_vm_builtin(name const & n, vm_cfunction_1 fn);
void declare_vm_builtin(name const & n, vm_cfunction_2 fn);
@ -543,6 +533,17 @@ void declare_vm_builtin(name const & n, vm_cfunction_7 fn);
void declare_vm_builtin(name const & n, vm_cfunction_8 fn);
void declare_vm_builtin(name const & n, unsigned arity, vm_cfunction_N fn);
/** Register in the given environment \c fn as the implementation for function \c n. */
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_1 fn);
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_2 fn);
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_3 fn);
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_4 fn);
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_5 fn);
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_6 fn);
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_7 fn);
environment declare_vm_builtin(environment const & env, name const & n, vm_cfunction_8 fn);
environment declare_vm_builtin(environment const & env, name const & n, unsigned arity, vm_cfunction_N fn);
/** \brief Reserve an index for the given function in the VM, the expression
\c e is the value of \c fn after preprocessing.
See library/compiler/pre_proprocess_rec.cpp for details. */