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

feat(library/vm/vm): add support for declaring builtin cfunctions

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-31 16:48:11 -07:00
parent 25903645a7
commit faf70ed58c
3 changed files with 65 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/vm_compiler.cpp
View file

@ -55,6 +55,8 @@ class vm_compiler_fn {
if (decl.get_arity() <= nargs) {
if (decl.is_builtin())
emit(mk_invoke_builtin_instr(decl.get_idx()));
else if (decl.is_cfun())
emit(mk_invoke_cfun_instr(decl.get_idx()));
else
emit(mk_invoke_global_instr(decl.get_idx()));
emit_apply_instr(nargs - decl.get_arity());

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

@ -575,6 +575,7 @@ void vm_decl_cell::dealloc() {
/** \brief VM builtin functions */
static name_map<pair<unsigned, vm_function>> * g_vm_builtins = nullptr;
static name_map<pair<unsigned, vm_cfunction>> * g_vm_cbuiltins = nullptr;
static bool g_may_update_vm_builtins = true;
void declare_vm_builtin(name const & n, unsigned arity, vm_function fn) {
@ -582,8 +583,53 @@ void declare_vm_builtin(name const & n, unsigned arity, vm_function fn) {
g_vm_builtins->insert(n, mk_pair(arity, fn));
}
void declare_vm_builtin(name const & n, vm_cfunction_1 fn) {
lean_assert(g_may_update_vm_builtins);
g_vm_cbuiltins->insert(n, mk_pair(1, fn));
}
void declare_vm_builtin(name const & n, vm_cfunction_2 fn) {
lean_assert(g_may_update_vm_builtins);
g_vm_cbuiltins->insert(n, mk_pair(2, reinterpret_cast<vm_cfunction>(fn)));
}
void declare_vm_builtin(name const & n, vm_cfunction_3 fn) {
lean_assert(g_may_update_vm_builtins);
g_vm_cbuiltins->insert(n, mk_pair(3, reinterpret_cast<vm_cfunction>(fn)));
}
void declare_vm_builtin(name const & n, vm_cfunction_4 fn) {
lean_assert(g_may_update_vm_builtins);
g_vm_cbuiltins->insert(n, mk_pair(4, reinterpret_cast<vm_cfunction>(fn)));
}
void declare_vm_builtin(name const & n, vm_cfunction_5 fn) {
lean_assert(g_may_update_vm_builtins);
g_vm_cbuiltins->insert(n, mk_pair(5, reinterpret_cast<vm_cfunction>(fn)));
}
void declare_vm_builtin(name const & n, vm_cfunction_6 fn) {
lean_assert(g_may_update_vm_builtins);
g_vm_cbuiltins->insert(n, mk_pair(6, reinterpret_cast<vm_cfunction>(fn)));
}
void declare_vm_builtin(name const & n, vm_cfunction_7 fn) {
lean_assert(g_may_update_vm_builtins);
g_vm_cbuiltins->insert(n, mk_pair(7, reinterpret_cast<vm_cfunction>(fn)));
}
void declare_vm_builtin(name const & n, vm_cfunction_8 fn) {
lean_assert(g_may_update_vm_builtins);
g_vm_cbuiltins->insert(n, mk_pair(8, reinterpret_cast<vm_cfunction>(fn)));
}
void declare_vm_builtin(name const & n, unsigned arity, vm_cfunction_N fn) {
lean_assert(g_may_update_vm_builtins);
g_vm_cbuiltins->insert(n, mk_pair(arity, reinterpret_cast<vm_cfunction>(fn)));
}
bool is_vm_builtin_function(name const & fn) {
return g_vm_builtins->contains(fn);
return g_vm_builtins->contains(fn) || g_vm_cbuiltins->contains(fn);
}
/** \brief VM function/constant declarations are stored in an environment extension. */
@ -595,6 +641,9 @@ struct vm_decls : public environment_extension {
g_vm_builtins->for_each([&](name const & n, pair<unsigned, vm_function> const & p) {
add(vm_decl(n, m_decls.size(), p.first, p.second));
});
g_vm_cbuiltins->for_each([&](name const & n, pair<unsigned, vm_cfunction> const & p) {
add(vm_decl(n, m_decls.size(), p.first, p.second));
});
}
void add(vm_decl const & d) {
@ -1810,6 +1859,7 @@ void display_vm_code(std::ostream & out, environment const & env, unsigned code_
void initialize_vm_core() {
g_vm_builtins = new name_map<pair<unsigned, vm_function>>();
g_vm_cbuiltins = new name_map<pair<unsigned, vm_cfunction>>();
g_may_update_vm_builtins = true;
DEBUG_CODE({
/* We only trace VM in debug mode because it produces a 10% performance penalty */
@ -1820,6 +1870,7 @@ void initialize_vm_core() {
void finalize_vm_core() {
delete g_vm_builtins;
delete g_vm_cbuiltins;
}
void initialize_vm() {

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

@ -530,8 +530,18 @@ public:
vm_obj invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args);
};
/** \brief Add builtin implementation for the function named \c n. */
/** \brief Add builtin implementation for the function named \c n.
All environment objects will contain this builtin. */
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);
void declare_vm_builtin(name const & n, vm_cfunction_3 fn);
void declare_vm_builtin(name const & n, vm_cfunction_4 fn);
void declare_vm_builtin(name const & n, vm_cfunction_5 fn);
void declare_vm_builtin(name const & n, vm_cfunction_6 fn);
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);
/** \brief Reserve an index for the given function in the VM, the expression
\c e is the value of \c fn after preprocessing.