From e2fa36342301d4bd26249ec801cf9e4e5eeb5be9 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 7 Apr 2017 14:16:00 +0200 Subject: [PATCH] feat(library/system/io,shell/lean): add --run switch --- library/system/io.lean | 4 + src/frontends/lean/builtin_cmds.cpp | 132 +++++++++----------- src/library/CMakeLists.txt | 1 + src/library/eval_helper.cpp | 89 +++++++++++++ src/library/eval_helper.h | 53 ++++++++ src/library/vm/vm_io.cpp | 33 +++-- src/library/vm/vm_io.h | 2 + src/shell/lean.cpp | 70 ++++++++--- tests/lean/char_lits.lean.expected.out | 4 - tests/lean/io_bug1.lean.expected.out | 3 - tests/lean/io_bug2.lean.expected.out | 1 - tests/lean/let_elim_issue.lean.expected.out | 1 - 12 files changed, 284 insertions(+), 109 deletions(-) create mode 100644 src/library/eval_helper.cpp create mode 100644 src/library/eval_helper.h diff --git a/library/system/io.lean b/library/system/io.lean index a9b0a38c37..a887616f01 100644 --- a/library/system/io.lean +++ b/library/system/io.lean @@ -13,6 +13,7 @@ inductive io.error structure io.terminal (m : Type → Type → Type) := (put_str : string → m io.error unit) (get_line : m io.error string) +(cmdline_args : list string) inductive io.mode | read | write | read_write | append @@ -77,6 +78,9 @@ put_str s >> put_str "\n" def get_line : io string := interface.term.get_line +def cmdline_args : io (list string) := +return interface.term.cmdline_args + def print {α} [has_to_string α] (s : α) : io unit := put_str ∘ to_string $ s diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 1800f636c2..482355ac1e 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include +#include "library/eval_helper.h" #include "util/timeit.h" #include "util/sstream.h" #include "util/sexpr/option_declarations.h" @@ -423,34 +424,6 @@ static environment compile_expr(environment const & env, name const & n, level_p return vm_compile(new_env, new_env.get(n)); } -static void eval_core(vm_state & s, name const & main, bool is_io) { - vm_decl d = *s.get_decl(main); - if (!is_io && d.get_arity() > 0) - throw exception("eval result is a function"); - if (is_io) { - s.push(mk_vm_simple(0)); // "world state" - s.push(mk_io_interface()); - } - s.invoke_fn(main); - if (is_io) { - if (d.get_arity() == 1) { - /* main returned a closure, it did not process initial_state yet. - So, we force the execution. */ - s.apply(); - } - vm_obj r = s.top(); - if (optional error = is_io_error(r)) { - std::string msg = io_error_to_string(*error); - throw exception(msg); - } - } -} - -static optional find_io_interface_local(expr const & e) { - return find(e, [&](expr const & e, unsigned) { - return is_local(e) && is_constant(mlocal_type(e), get_io_interface_name()); - }); -} static environment eval_cmd(parser & p) { auto pos = p.pos(); @@ -458,60 +431,69 @@ static environment eval_cmd(parser & p) { std::tie(e, ls) = parse_local_expr(p, "_eval"); if (has_metavar(e)) throw parser_error("invalid eval command, expression contains metavariables", pos); + type_context tc(p.env(), transparency_mode::All); - expr type0 = tc.infer(e); - expr type = type0; // TODO(Leo): tc.whnf(type0); - bool is_io = is_constant(get_app_fn(type), get_io_name()); - bool is_string = false; - if (optional io_interface = find_io_interface_local(e)) { - if (!is_io) - throw parser_error("invalid eval command, it depends on io.interface local variable, but it is not an io action", pos); - e = Fun(*io_interface, e); - type = Pi(*io_interface, type); - } else if (is_io) { - throw parser_error("invalid eval command, failed to locate io.interface local variable", pos); + auto type = tc.infer(e); + + /* Check if resultant type has an instance of has_to_string */ + try { + expr has_to_string_type = mk_app(tc, get_has_to_string_name(), type); + optional to_string_instance = tc.mk_class_instance(has_to_string_type); + if (to_string_instance) { + /* Modify the 'program' to (to_string e) */ + e = mk_app(tc, get_to_string_name(), type, *to_string_instance, e); + type = tc.infer(e); + } + } catch (exception &) {} + + // Close under locals + collected_locals locals; + collect_locals(e, locals); + for (auto & l : locals.get_collected()) { + e = Fun(l, e); + type = Pi(l, type); } - if (!is_io) { - /* Check if resultant type has an instance of has_to_string */ - try { - expr has_to_string_type = mk_app(tc, get_has_to_string_name(), type0); - optional to_string_instance = tc.mk_class_instance(has_to_string_type); - if (to_string_instance) { - /* Modify the 'program' to (to_string e) */ - e = mk_app(tc, get_to_string_name(), type0, *to_string_instance, e); - type = tc.infer(e); - is_string = true; - } - } catch (exception &) {} - } - name main("_main"); - environment new_env = compile_expr(p.env(), main, ls, type, e, pos); - vm_state s(new_env, p.get_options()); + + name fn_name = "_main"; + auto new_env = compile_expr(p.env(), fn_name, ls, type, e, pos); + auto out = p.mk_message(p.cmd_pos(), INFORMATION); - out.set_caption("eval result"); - vm_state::profiler prof(s, p.get_options()); - // TODO(gabriel): capture output + scope_traces_as_messages scope_traces(p.get_stream_name(), p.cmd_pos()); + bool should_report = false; + + auto run = [&] { + eval_helper fn(new_env, p.get_options(), fn_name); + fn.dependency_injection(); + try { + if (!fn.try_exec()) { + auto r = fn.invoke_fn(); + should_report = true; + if (is_constant(fn.get_type(), get_string_name())) { + out << to_string(r); + } else { + display(out.get_text_stream().get_stream(), r); + } + } + } catch (throwable & t) { + p.mk_message(p.cmd_pos(), ERROR).set_exception(t).report(); + } + if (fn.get_profiler().enabled()) { + out << "\n"; + fn.get_profiler().get_snapshots().display(out.get_text_stream().get_stream()); + should_report = true; + } + }; + if (p.profiling()) { timeit timer(out.get_text_stream().get_stream(), "eval time"); - eval_core(s, main, is_io); + run(); + should_report = true; } else { - eval_core(s, main, is_io); + run(); } - if (is_io) { - // do not print anything - } else if (is_string) { - vm_obj r = s.get(0); - out << to_string(r); - } else { - /* if it is not IO nor a string, then display object on top of the stack using vm_obj display method */ - vm_obj r = s.get(0); - display(out.get_text_stream().get_stream(), r); - } - if (prof.enabled()) { - out << "\n"; - prof.get_snapshots().display(out.get_text_stream().get_stream()); - } - out.report(); + + if (should_report) out.report(); + return p.env(); } diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index e42ba97a02..98caeb8455 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -18,6 +18,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp locals.cpp normalize.cpp discr_tree.cpp mt_task_queue.cpp st_task_queue.cpp library_task_builder.cpp + eval_helper.cpp messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp documentation.cpp check.cpp arith_instance.cpp parray.cpp process.cpp pipe.cpp handle.cpp) diff --git a/src/library/eval_helper.cpp b/src/library/eval_helper.cpp new file mode 100644 index 0000000000..e3c43d08b7 --- /dev/null +++ b/src/library/eval_helper.cpp @@ -0,0 +1,89 @@ +/* +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Gabriel Ebner +*/ +#include "library/eval_helper.h" +#include "library/tactic/tactic_state.h" + +namespace lean { + +eval_helper::eval_helper(environment const & env, options const & opts, name const & fn) : + m_env(env), m_opts(opts), m_tc(env, opts, transparency_mode::None), + m_vms(env, opts), m_prof(m_vms, opts), m_fn(fn) { + auto d = env.get(m_fn); + m_ty = m_tc.whnf(d.get_type()); + + if (auto vm_decl = m_vms.get_decl(m_fn)) { + m_arity = vm_decl->get_arity(); + } else { + throw exception(sstream() << "no vm declaration found for " << m_fn); + } + + m_io_iface = m_tc.push_local( + "_vm_io_iface", mk_constant(get_io_interface_name(), {}), + mk_inst_implicit_binder_info()); +} + +void eval_helper::dependency_injection() { + while (is_pi(m_ty)) { + auto arg_ty = m_tc.whnf(binding_domain(m_ty)); + optional arg; + + if (is_constant(get_app_fn(arg_ty), get_io_interface_name())) { + m_args.push_back(mk_io_interface(m_cmdline_args)); + arg = m_io_iface; + } + + if (arg) { + m_ty = m_tc.whnf(instantiate(binding_body(m_ty), *arg)); + } else { + break; + } + } +} + +vm_obj eval_helper::invoke_fn() { + std::reverse(m_args.begin(), m_args.end()); + return m_vms.invoke(m_fn, m_args.size(), m_args.data()); +} + +optional eval_helper::try_exec_io() { + if (is_constant(get_app_fn(m_ty), get_io_name()) && app_arg(app_fn(m_ty)) == m_io_iface) { + m_args.push_back(mk_vm_simple(0)); // "world state" + auto r = invoke_fn(); + if (auto error = is_io_error(r)) { + throw exception(io_error_to_string(*error)); + } else if (auto result = is_io_result(r)) { + return result; + } else { + throw exception("unexpected vm result of io expression"); + } + } + return optional(); +} + +optional eval_helper::try_exec_tac() { + if (is_constant(get_app_fn(m_ty), get_tactic_name())) { + auto tac_st = mk_tactic_state_for(m_env, m_opts, m_fn, m_tc.mctx(), m_tc.lctx(), mk_true()); + m_vms.push(tactic::to_obj(tac_st)); + auto r = invoke_fn(); + if (tactic::is_result_success(r)) { + return optional(tactic::get_result_value(r)); + } else if (auto ex = tactic::is_exception(m_vms, r)) { + throw formatted_exception(std::get<1>(*ex), std::get<0>(*ex)); + } else { + throw exception("tactic failed"); + } + } + return optional(); +} + +optional eval_helper::try_exec() { + if (auto res = try_exec_io()) return res; + if (auto res = try_exec_tac()) return res; + return optional(); +} + +} diff --git a/src/library/eval_helper.h b/src/library/eval_helper.h new file mode 100644 index 0000000000..40c408aff5 --- /dev/null +++ b/src/library/eval_helper.h @@ -0,0 +1,53 @@ +/* +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Gabriel Ebner +*/ +#pragma once +#include "library/vm/vm_io.h" +#include "library/type_context.h" +#include "library/vm/vm.h" +#include "library/constants.h" +#include +#include + +namespace lean { + +class eval_helper { + environment m_env; + options m_opts; + + type_context m_tc; + + std::vector m_cmdline_args; + + buffer m_args; + vm_state m_vms; + vm_state::profiler m_prof; + + name m_fn; + expr m_ty; + unsigned m_arity; + + expr m_io_iface; + +public: + eval_helper(environment const & env, options const & opts, name const & fn); + + void set_cmdline_args(std::vector const & cmdline_args) { + m_cmdline_args = cmdline_args; + } + + void dependency_injection(); + vm_obj invoke_fn(); + + expr const & get_type() const { return m_ty; } + vm_state::profiler & get_profiler() { return m_prof; } + + optional try_exec_io(); + optional try_exec_tac(); + optional try_exec(); +}; + +} diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp index 8418bfd879..09fe8d6428 100644 --- a/src/library/vm/vm_io.cpp +++ b/src/library/vm/vm_io.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include #include #include #include "util/sstream.h" @@ -47,17 +48,26 @@ static vm_obj io_get_line(vm_obj const &) { return mk_io_result(to_obj(str)); } +static vm_obj cmdline_args_to_obj(std::vector const & ss) { + buffer objs; + for (auto & s : ss) objs.push_back(to_obj(s)); + return to_obj(objs); +} + /* structure io.terminal (m : Type → Type → Type) := (put_str : string → m io.error unit) (get_line : m io.error string) +(cmdline_args : list string) */ -static vm_obj mk_terminal() { - vm_obj fields[2] = { +static vm_obj mk_terminal(std::vector const & cmdline_args) { + constexpr size_t num_fields = 3; + vm_obj fields[num_fields] = { mk_native_closure(io_put_str), - mk_native_closure(io_get_line) + mk_native_closure(io_get_line), + cmdline_args_to_obj(cmdline_args), }; - return mk_vm_constructor(0, 2, fields); + return mk_vm_constructor(0, num_fields, fields); } struct vm_handle : public vm_external { @@ -397,18 +407,23 @@ class io.interface := (fs : io.file_system handle m) (process : io.process io.error handle m) */ -vm_obj mk_io_interface() { - vm_obj fields[8] = { +vm_obj mk_io_interface(std::vector const & cmdline_args) { + constexpr size_t num_fields = 8; + vm_obj fields[num_fields] = { mk_native_closure(io_m), /* TODO(Leo): delete after we improve code generator */ mk_native_closure(io_monad), mk_native_closure(io_catch), mk_native_closure(io_fail), mk_native_closure(io_iterate), - mk_terminal(), + mk_terminal(cmdline_args), mk_fs(), - mk_process() + mk_process(), }; - return mk_vm_constructor(0, 8, fields); + return mk_vm_constructor(0, num_fields, fields); +} + +vm_obj mk_io_interface() { + return mk_io_interface({}); } optional is_io_result(vm_obj const & o) { diff --git a/src/library/vm/vm_io.h b/src/library/vm/vm_io.h index ad58fcf22f..07a487dfbb 100644 --- a/src/library/vm/vm_io.h +++ b/src/library/vm/vm_io.h @@ -6,12 +6,14 @@ Author: Leonardo de Moura */ #pragma once #include +#include #include "library/vm/vm.h" #include "library/handle.h" namespace lean { vm_obj mk_io_result(vm_obj const & r); vm_obj mk_io_interface(); +vm_obj mk_io_interface(std::vector const & cmdline_args); /* The io monad produces a result object, or an error. If `o` is a result, then we return the result value. */ optional is_io_result(vm_obj const & o); diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 52a0a5786a..0a8232099c 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include #include #include +#include "library/eval_helper.h" #include "util/timer.h" #include "util/task_builder.h" #include "util/realpath.h" @@ -95,6 +96,7 @@ static void display_help(std::ostream & out) { std::cout << " --help -h display this message\n"; std::cout << " --version -v display version number\n"; std::cout << " --githash display the git commit hash number used to build this binary\n"; + std::cout << " --run executes the 'main' definition\n"; std::cout << " --path display the path used for finding Lean libraries and extensions\n"; std::cout << " --doc=file -r generate module documentation based on module doc strings\n"; std::cout << " --make create olean files\n"; @@ -129,6 +131,7 @@ static void display_help(std::ostream & out) { static struct option g_long_options[] = { {"version", no_argument, 0, 'v'}, {"help", no_argument, 0, 'h'}, + {"run", required_argument, 0, 'a'}, {"smt2", no_argument, 0, 'Y'}, {"path", no_argument, 0, 'p'}, {"githash", no_argument, 0, 'g'}, @@ -350,6 +353,7 @@ int main(int argc, char ** argv) { optional export_txt; optional doc; optional server_in; + optional run_arg; std::string native_output; while (true) { int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL); @@ -368,6 +372,9 @@ int main(int argc, char ** argv) { case 'h': display_help(std::cout); return 0; + case 'a': + run_arg = optarg; + break; case 'Y': smt2 = true; break; @@ -449,6 +456,10 @@ int main(int argc, char ** argv) { display_help(std::cerr); return 1; } + if (run_arg) { + // treat run_arg as the last arg + break; + } } if (auto max_memory = opts.get_unsigned(get_max_memory_opt_name(), @@ -516,6 +527,49 @@ int main(int argc, char ** argv) { } try { + std::shared_ptr tq; +#if defined(LEAN_MULTI_THREAD) + if (num_threads == 0) { + tq = std::make_shared(); + } else { + tq = std::make_shared(num_threads); + } +#else + tq = std::make_shared(); +#endif + set_task_queue(tq.get()); + + fs_module_vfs vfs; + module_mgr mod_mgr(&vfs, lt.get_root(), env, ios); + + if (run_arg) { + auto mod = mod_mgr.get_module(lrealpath(run_arg->c_str())); + if (!mod) throw exception(sstream() << "could not load " << *run_arg); + + auto main_env = get(get(mod->m_result).m_loaded_module->m_env); + auto main_opts = get(mod->m_result).m_opts; + eval_helper fn(main_env, main_opts, "main"); + fn.set_cmdline_args({argv + optind, argv + argc}); + + type_context tc(main_env, main_opts); + scope_trace_env scope2(main_env, main_opts, tc); + + try { + fn.dependency_injection(); + if (fn.try_exec()) { + return 0; + } else { + throw exception(sstream() << *run_arg << ": cannot execute main function with type " + << ios.get_formatter_factory()(main_env, main_opts, tc)(fn.get_type())); + } + } catch (std::exception & ex) { + std::cerr << ex.what() << std::endl; + return 1; + } + } + + mod_mgr.set_save_olean(make_mode); + std::vector args(argv + optind, argv + argc); if (recursive) { if (args.empty()) args.push_back("."); @@ -538,27 +592,11 @@ int main(int argc, char ** argv) { std::vector module_args; for (auto & f : args) module_args.push_back(lrealpath(f.c_str())); - std::shared_ptr tq; -#if defined(LEAN_MULTI_THREAD) - if (num_threads == 0) { - tq = std::make_shared(); - } else { - tq = std::make_shared(num_threads); - } -#else - tq = std::make_shared(); -#endif - set_task_queue(tq.get()); - - fs_module_vfs vfs; if (!recursive) { for (auto & mod_id : module_args) vfs.m_modules_to_load_from_source.insert(mod_id); } - module_mgr mod_mgr(&vfs, lt.get_root(), env, ios); - mod_mgr.set_save_olean(make_mode); - bool ok = true; if (only_deps) { diff --git a/tests/lean/char_lits.lean.expected.out b/tests/lean/char_lits.lean.expected.out index 84038f4945..ccf7bf9e8e 100644 --- a/tests/lean/char_lits.lean.expected.out +++ b/tests/lean/char_lits.lean.expected.out @@ -2,11 +2,7 @@ #"a" #"\n" #"\\" - aaa\ - - - aaa' diff --git a/tests/lean/io_bug1.lean.expected.out b/tests/lean/io_bug1.lean.expected.out index 4172ab7fab..9ae65df1c5 100644 --- a/tests/lean/io_bug1.lean.expected.out +++ b/tests/lean/io_bug1.lean.expected.out @@ -1,7 +1,5 @@ - onetwothree --------- - in in in @@ -10,7 +8,6 @@ out out out --------- - in in in diff --git a/tests/lean/io_bug2.lean.expected.out b/tests/lean/io_bug2.lean.expected.out index 420bee977e..81f183a9bb 100644 --- a/tests/lean/io_bug2.lean.expected.out +++ b/tests/lean/io_bug2.lean.expected.out @@ -1,3 +1,2 @@ - "t1" "t2" diff --git a/tests/lean/let_elim_issue.lean.expected.out b/tests/lean/let_elim_issue.lean.expected.out index 50dc7b331c..8cd25748ff 100644 --- a/tests/lean/let_elim_issue.lean.expected.out +++ b/tests/lean/let_elim_issue.lean.expected.out @@ -1,4 +1,3 @@ - hello world from Lean