From 31c170117e508cc8bd12e5378ca5790f0bdaab30 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 19 Sep 2019 17:52:18 +0200 Subject: [PATCH] feat(frontends/lean/builtin_cmds,library/compiler/ir_interpreter): reimplement `#eval` --- src/frontends/lean/builtin_cmds.cpp | 58 ++++++++++ src/library/compiler/ir_interpreter.cpp | 135 +++++++++++++++--------- src/library/compiler/ir_interpreter.h | 2 + 3 files changed, 146 insertions(+), 49 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 447a12950a..b5ff53df60 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -40,6 +40,7 @@ Author: Leonardo de Moura #include "frontends/lean/parse_table.h" #include "frontends/lean/decl_attributes.h" #include "frontends/lean/typed_expr.h" +#include "library/compiler/ir_interpreter.h" namespace lean { environment section_cmd(parser & p) { @@ -315,6 +316,62 @@ environment hide_cmd(parser & p) { return new_env; } +static environment eval_cmd(parser & p) { + transient_cmd_scope cmd_scope(p); + auto pos = p.pos(); + expr e; names ls; + std::tie(e, ls) = parse_local_expr(p, "_eval", /* relaxed */ false); + if (has_synthetic_sorry(e)) + return p.env(); + + type_context_old tc(p.env(), transparency_mode::All); + auto type = tc.infer(e); + + bool has_eval = false; + + /* Check if resultant type has an instance of has_eval */ + try { + expr has_eval_type = mk_app(tc, "HasEval", type); + optional eval_instance = tc.mk_class_instance(has_eval_type); + if (eval_instance) { + /* Modify the 'program' to (has_eval.eval e) */ + e = mk_app(tc, {"HasEval", "eval"}, 3, type, *eval_instance, e); + type = tc.infer(e); + has_eval = true; + } + } catch (exception &) {} + + if (!has_eval) { + // NOTE: HasRepr implies HasEval + throw exception("result type does not have an instance of type class 'HasRepr' or 'HasEval'"); + } + + name fn_name = "_main"; + auto new_env = compile_expr(p.env(), p.get_options(), fn_name, ls, type, e, pos); + + auto out = p.mk_message(p.cmd_pos(), p.pos(), INFORMATION); + out.set_caption("eval result"); + scope_traces_as_messages scope_traces(p.get_stream_name(), p.cmd_pos()); + std::streambuf * saved_cout = std::cout.rdbuf(out.get_text_stream().get_stream().rdbuf()); + + // run `IO Unit` + object * args[] = { io_mk_world() }; + + if (p.profiling()) { + timeit timer(out.get_text_stream().get_stream(), "eval time"); + // NOTE: no need to free `()` + ir::run_boxed(new_env, fn_name, &args[0]); + } else { + ir::run_boxed(new_env, fn_name, &args[0]); + } + + std::cout.rdbuf(saved_cout); + out.report(); + return p.env(); +} + + + environment compact_tst_cmd(parser & p) { environment env = p.env(); unsigned num_copies = 0; @@ -410,6 +467,7 @@ void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("init_quot", "initialize `quot` type computational rules", init_quot_cmd)); add_cmd(r, cmd_info("import", "import module(s)", import_cmd)); add_cmd(r, cmd_info("hide", "hide aliases in the current scope", hide_cmd)); + add_cmd(r, cmd_info("#eval", "evaluate given expression using interpreter/precompiled code", eval_cmd)); register_decl_cmds(r); register_inductive_cmds(r); register_structure_cmd(r); diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index 7a2e2cd2ae..c89702987b 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -737,55 +737,6 @@ class interpreter { pop_frame(r, decl_type(e.m_decl)); return r; } -public: - explicit interpreter(environment const & env) : m_env(env) { - lean_assert(g_interpreter == nullptr); - g_interpreter = this; - } - ~interpreter() { - for_each(m_constant_cache, [](name const &, constant_cache_entry const & e) { - if (!e.m_is_scalar) { - dec(e.m_val.m_obj); - } - }); - lean_assert(g_interpreter == this); - g_interpreter = nullptr; - } - - uint32 run_main(int argc, char * argv[]) { - decl d = get_fdecl("main"); - array_ref const & params = decl_params(d); - if (params.size() == 2) { // List String -> IO UInt32 - lean_object * in = lean_box(0); - int i = argc; - while (i > 0) { - i--; - lean_object * n = lean_alloc_ctor(1, 2, 0); - lean_ctor_set(n, 0, lean_mk_string(argv[i])); - lean_ctor_set(n, 1, in); - in = n; - } - m_arg_stack.push_back(in); - } else { // IO UInt32 - lean_assert(params.size() == 1); - } - object * w = io_mk_world(); - m_arg_stack.push_back(w); - push_frame(d, 0); - w = eval_body(decl_fun_body(d)).m_obj; - pop_frame(w, type::Object); - if (io_result_is_ok(w)) { - // NOTE: in an awesome hack, `IO Unit` works just as well because `pure 0` and `pure ()` use the same - // representation - int ret = unbox(io_result_get_value(w)); - dec_ref(w); - return ret; - } else { - io_result_show_error(w); - dec_ref(w); - return 1; - } - } // closure stub object * stub_m(object ** args) { @@ -852,8 +803,94 @@ public: default: return reinterpret_cast(stub_m_aux); } } +public: + explicit interpreter(environment const & env) : m_env(env) { + lean_assert(g_interpreter == nullptr); + g_interpreter = this; + } + ~interpreter() { + for_each(m_constant_cache, [](name const &, constant_cache_entry const & e) { + if (!e.m_is_scalar) { + dec(e.m_val.m_obj); + } + }); + lean_assert(g_interpreter == this); + g_interpreter = nullptr; + } + + object * call_boxed(name const & fn, object ** args) { + symbol_cache_entry e = lookup_symbol(fn); + unsigned n = decl_params(e.m_decl).size(); + object * r; + if (e.m_addr) { + push_frame(e.m_decl, 0); + // 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 << "'"); + } + // 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]); + } + } + 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]); + } + } + } + pop_frame(r, decl_type(e.m_decl)); + return r; + } + + uint32 run_main(int argc, char * argv[]) { + decl d = get_fdecl("main"); + array_ref const & params = decl_params(d); + if (params.size() == 2) { // List String -> IO UInt32 + lean_object * in = lean_box(0); + int i = argc; + while (i > 0) { + i--; + lean_object * n = lean_alloc_ctor(1, 2, 0); + lean_ctor_set(n, 0, lean_mk_string(argv[i])); + lean_ctor_set(n, 1, in); + in = n; + } + m_arg_stack.push_back(in); + } else { // IO UInt32 + lean_assert(params.size() == 1); + } + object * w = io_mk_world(); + m_arg_stack.push_back(w); + push_frame(d, 0); + w = eval_body(decl_fun_body(d)).m_obj; + pop_frame(w, type::Object); + if (io_result_is_ok(w)) { + // NOTE: in an awesome hack, `IO Unit` works just as well because `pure 0` and `pure ()` use the same + // representation + int ret = unbox(io_result_get_value(w)); + dec_ref(w); + return ret; + } else { + io_result_show_error(w); + dec_ref(w); + return 1; + } + } }; +object * run_boxed(environment const & env, name const & fn, object ** args) { + return interpreter(env).call_boxed(fn, args); +} uint32 run_main(environment const & env, int argv, char * argc[]) { return interpreter(env).run_main(argv, argc); } diff --git a/src/library/compiler/ir_interpreter.h b/src/library/compiler/ir_interpreter.h index 93204ee415..331c5c797e 100644 --- a/src/library/compiler/ir_interpreter.h +++ b/src/library/compiler/ir_interpreter.h @@ -10,6 +10,8 @@ Author: Sebastian Ullrich namespace lean { namespace ir { +/** \brief Run `n` using the "boxed" ABI, i.e. with all-owned parameters. */ +object * run_boxed(environment const & env, name const & fn, object ** args); uint32 run_main(environment const & env, int argv, char * argc[]); } void initialize_ir_interpreter();