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

refactor: call generated boxed wrapper instead of reinventing it in the interpreter

Browse source
This commit is contained in:
Sebastian Ullrich 2019-12-05 10:27:10 +01:00
parent e3e50b7940
commit 44ce73ced9
1 changed files with 10 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/library/compiler/ir_interpreter.cpp
View file

@ -172,6 +172,7 @@ option_ref<decl> find_ir_decl(environment const & env, name const & n) {
}
static string_ref * g_mangle_prefix = nullptr;
static string_ref * g_boxed_suffix = nullptr;
static string_ref * g_boxed_mangled_suffix = nullptr;
// reuse the compiler's name mangling to compute native symbol names
@ -826,6 +827,7 @@ public:
}
object * call_boxed(name const & fn, object ** args) {
/** Like `call`, but taking (owned) `object *`s instead of `arg`s. */
symbol_cache_entry e = lookup_symbol(fn);
unsigned n = decl_params(e.m_decl).size();
object * r;
@ -834,26 +836,17 @@ public:
// directly call boxed function, nothing more to do
r = curry(e.m_addr, n, args);
} else {
// equivalent code to boxed stubs generated by the compiler: unbox args, box result, decrement borrowed args
if (decl_tag(e.m_decl) == decl_kind::Extern) {
throw exception(sstream() << "unexpected external declaration '" << fn << "'");
decl d = e.m_decl;
if (option_ref<decl> d_boxed = find_ir_decl(m_env, fn + *g_boxed_suffix)) {
d = *d_boxed.get();
}
// `d` now has a boxed signature
// evaluate args in old stack frame
for (unsigned i = 0; i < n; i++) {
type t = param_type(decl_params(e.m_decl)[i]);
m_arg_stack.push_back(unbox_t(args[i], t));
if (type_is_scalar(t)) {
dec(args[i]);
}
m_arg_stack.push_back(args[i]);
}
push_frame(e.m_decl, 0);
r = box_t(eval_body(decl_fun_body(e.m_decl)), decl_type(e.m_decl));
for (size_t i = 0; i < n; i++) {
if (param_borrow(decl_params(e.m_decl)[i])) {
dec(args[i]);
}
}
r = eval_body(decl_fun_body(e.m_decl)).m_obj;
}
pop_frame(r, decl_type(e.m_decl));
return r;
@ -905,6 +898,7 @@ uint32 run_main(environment const & env, int argv, char * argc[]) {
void initialize_ir_interpreter() {
ir::g_mangle_prefix = new string_ref("l_");
ir::g_boxed_suffix = new string_ref("_boxed");
ir::g_boxed_mangled_suffix = new string_ref("___boxed");
DEBUG_CODE({
register_trace_class({"interpreter"});
@ -915,6 +909,7 @@ void initialize_ir_interpreter() {
void finalize_ir_interpreter() {
delete ir::g_boxed_mangled_suffix;
delete ir::g_boxed_suffix;
delete ir::g_mangle_prefix;
}
}