From a964ceb0e29fa3a2f8e060108bedc3f54cf69d30 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Jun 2014 16:37:46 -0700 Subject: [PATCH] feat(frontends/lean): add 'import' command, add command line option for setting number of threads Signed-off-by: Leonardo de Moura --- src/frontends/lean/interactive.cpp | 6 ++-- src/frontends/lean/interactive.h | 2 ++ src/frontends/lean/parser.cpp | 55 ++++++++++++++++++++++++++---- src/frontends/lean/parser.h | 7 ++-- src/shell/lean.cpp | 24 ++++++++----- src/util/lean_path.cpp | 8 +++++ src/util/lean_path.h | 4 ++- src/util/script_state.cpp | 2 +- 8 files changed, 86 insertions(+), 22 deletions(-) diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp index 9c0d37b6f..3f35033f6 100644 --- a/src/frontends/lean/interactive.cpp +++ b/src/frontends/lean/interactive.cpp @@ -12,9 +12,9 @@ Author: Leonardo de Moura #include "frontends/lean/interactive.h" namespace lean { -interactive::interactive(environment const & env, io_state const & ios, script_state const & ss, +interactive::interactive(environment const & env, io_state const & ios, script_state const & ss, unsigned num_threads, char const * ack_cmd, char const * snapshot_cmd, char const * restore_cmd, char const * restart_cmd): - m_env(env), m_ios(ios), m_ss(ss), m_line(1), + m_env(env), m_ios(ios), m_ss(ss), m_num_threads(num_threads), m_line(1), m_ack_cmd(ack_cmd), m_snapshot_cmd(snapshot_cmd), m_restore_cmd(restore_cmd), m_restart_cmd(restart_cmd) { save_snapshot(); } @@ -22,7 +22,7 @@ interactive::interactive(environment const & env, io_state const & ios, script_s void interactive::parse_block(std::string const & str, char const * strm_name) { if (str.size() > 0) { std::istringstream block(str); - parser p(m_env, m_ios, block, strm_name, &m_ss, false, m_lds, m_eds, m_line); + parser p(m_env, m_ios, block, strm_name, &m_ss, false, m_num_threads, m_lds, m_eds, m_line); p(); m_env = p.env(); m_ios = p.ios(); diff --git a/src/frontends/lean/interactive.h b/src/frontends/lean/interactive.h index e4281fa63..cda5a9e65 100644 --- a/src/frontends/lean/interactive.h +++ b/src/frontends/lean/interactive.h @@ -35,6 +35,7 @@ class interactive { environment m_env; io_state m_ios; script_state m_ss; + unsigned m_num_threads; local_level_decls m_lds; local_expr_decls m_eds; unsigned m_line; @@ -47,6 +48,7 @@ class interactive { void restore(unsigned new_line, std::string & block); public: interactive(environment const & env, io_state const & ios, script_state const & ss, + unsigned num_threads = 1, char const * ack_cmd = "#ACK", char const * snapshot_cmd = "#SNAPSHOT", char const * res_cmd = "#RESTORE", char const * restart_cmd = "#RESTART"); environment const & env() const { return m_env; } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 4be0fcfa0..a0d550b1c 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "util/script_exception.h" #include "util/sstream.h" #include "util/flet.h" +#include "util/lean_path.h" #include "kernel/for_each_fn.h" #include "kernel/replace_fn.h" #include "kernel/abstract.h" @@ -21,6 +22,7 @@ Author: Leonardo de Moura #include "library/choice.h" #include "library/placeholder.h" #include "library/deep_copy.h" +#include "library/module.h" #include "library/error_handling/error_handling.h" #include "frontends/lean/parser.h" #include "frontends/lean/notation_cmd.h" @@ -58,7 +60,7 @@ parser::param_universe_scope::~param_universe_scope() { parser::parser(environment const & env, io_state const & ios, std::istream & strm, char const * strm_name, - script_state * ss, bool use_exceptions, + script_state * ss, bool use_exceptions, unsigned num_threads, local_level_decls const & lds, local_expr_decls const & eds, unsigned line): m_env(env), m_ios(ios), m_ss(ss), @@ -66,6 +68,7 @@ parser::parser(environment const & env, io_state const & ios, m_scanner(strm, strm_name), m_local_level_decls(lds), m_local_decls(eds), m_pos_table(std::make_shared()) { m_scanner.set_line(line); + m_num_threads = num_threads; m_type_use_placeholder = true; m_found_errors = false; updt_options(); @@ -340,7 +343,8 @@ static name g_infix("infix"); static name g_infixl("infixl"); static name g_infixr("infixr"); static name g_postfix("postfix"); -static name g_notation("postfix"); +static name g_notation("notation"); +static name g_import("import"); static unsigned g_level_add_prec = 10; static unsigned g_level_cup_prec = 5; @@ -890,11 +894,49 @@ void parser::parse_script(bool as_expr) { }); } +static optional find_file(name const & f, char const * ext) { + try { + return optional(find_file(f, {ext})); + } catch (...) { + return optional(); + } +} + +void parser::parse_imports() { + buffer olean_files; + buffer lua_files; + while (curr_is_token(g_import)) { + m_last_cmd_pos = pos(); + next(); + while (curr_is_identifier()) { + name f = get_name_val(); + if (auto it = find_file(f, ".lua")) { + if (!m_ss) + throw parser_error("invalid import, Lua interpreter is not available", pos()); + lua_files.push_back(*it); + } else if (auto it = find_file(f, ".olean")) { + olean_files.push_back(*it); + } else { + throw parser_error(sstream() << "invalid import, unknow module '" << f << "'", pos()); + } + next(); + } + } + m_env = import_modules(m_env, olean_files.size(), olean_files.data(), m_num_threads, true, m_ios); + using_script([&](lua_State *) { + m_ss->exec_unprotected([&]() { + for (auto const & f : lua_files) { + m_ss->import_explicit(f.c_str()); + }}); + }); +} + bool parser::parse_commands() { // We disable hash-consing while parsing to make sure the pos-info are correct. scoped_expr_caching disable(false); try { bool done = false; + parse_imports(); while (!done) { protected_call([&]() { check_interrupted(); @@ -924,18 +966,19 @@ bool parser::parse_commands() { } -bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions) { - parser p(env, ios, in, strm_name, S, use_exceptions); +bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions, + unsigned num_threads) { + parser p(env, ios, in, strm_name, S, use_exceptions, num_threads); bool r = p(); ios = p.ios(); env = p.env(); return r; } -bool parse_commands(environment & env, io_state & ios, char const * fname, script_state * S, bool use_exceptions) { +bool parse_commands(environment & env, io_state & ios, char const * fname, script_state * S, bool use_exceptions, unsigned num_threads) { std::ifstream in(fname); if (in.bad() || in.fail()) throw exception(sstream() << "failed to open file '" << fname << "'"); - return parse_commands(env, ios, in, fname, S, use_exceptions); + return parse_commands(env, ios, in, fname, S, use_exceptions, num_threads); } } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index e62e16b90..975d5400d 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -53,6 +53,7 @@ class parser { bool m_verbose; bool m_use_exceptions; bool m_show_errors; + unsigned m_num_threads; scanner m_scanner; scanner::token_kind m_curr; @@ -105,6 +106,7 @@ class parser { level parse_level_nud(); level parse_level_led(level left); + void parse_imports(); void parse_command(); void parse_script(bool as_expr = false); bool parse_commands(); @@ -133,6 +135,7 @@ public: parser(environment const & env, io_state const & ios, std::istream & strm, char const * str_name, script_state * ss = nullptr, bool use_exceptions = false, + unsigned num_threads = 1, local_level_decls const & lds = local_level_decls(), local_expr_decls const & eds = local_expr_decls(), unsigned line = 1); @@ -246,7 +249,7 @@ public: }; bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, - script_state * S, bool use_exceptions); + script_state * S, bool use_exceptions, unsigned num_threads); bool parse_commands(environment & env, io_state & ios, char const * fname, script_state * S, - bool use_exceptions); + bool use_exceptions, unsigned num_threads); } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 59d06c7c9..84439a72e 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -68,6 +68,7 @@ static void display_help(std::ostream & out) { std::cout << " --quiet -q do not print verbose messages\n"; std::cout << " --interactive -i read blocks of commands from the input stream\n"; std::cout << " --hott use Homotopy Type Theory kernel and libraries\n"; + std::cout << " --threads=num -r number of threads used to process lean files\n"; #if defined(LEAN_USE_BOOST) std::cout << " --tstack=num -s thread stack size in Kb\n"; #endif @@ -100,6 +101,7 @@ static struct option g_long_options[] = { {"interactive", no_argument, 0, 'i'}, {"quiet", no_argument, 0, 'q'}, {"hott", no_argument, 0, 'H'}, + {"threads", required_argument, 0, 'r'}, #if defined(LEAN_USE_BOOST) {"tstack", required_argument, 0, 's'}, #endif @@ -107,9 +109,9 @@ static struct option g_long_options[] = { }; #if defined(LEAN_USE_BOOST) -static char const * g_opt_str = "Hiqlupgvhc:012s:012t:012o:"; +static char const * g_opt_str = "Hiqlupgvhr:012c:012s:012t:012o:"; #else -static char const * g_opt_str = "Hiqlupgvhc:012t:012o:"; +static char const * g_opt_str = "Hiqlupgvhr:012c:012t:012o:"; #endif enum class lean_mode { Standard, HoTT }; @@ -117,11 +119,12 @@ enum class lean_mode { Standard, HoTT }; int main(int argc, char ** argv) { lean::save_stack_info(); lean::register_modules(); - bool export_objects = false; - unsigned trust_lvl = 0; - bool quiet = false; - bool interactive = false; - lean_mode mode = lean_mode::Standard; + bool export_objects = false; + unsigned trust_lvl = 0; + bool quiet = false; + bool interactive = false; + lean_mode mode = lean_mode::Standard; + unsigned num_threads = 1; std::string output; input_kind default_k = input_kind::Lean; // default while (true) { @@ -129,6 +132,9 @@ int main(int argc, char ** argv) { if (c == -1) break; // end of command line switch (c) { + case 'r': + num_threads = atoi(optarg); + break; case 'H': mode = lean_mode::HoTT; lean::init_lean_path("hott"); @@ -201,7 +207,7 @@ int main(int argc, char ** argv) { } } if (k == input_kind::Lean) { - if (!parse_commands(env, ios, argv[i], &S, false)) + if (!parse_commands(env, ios, argv[i], &S, false, num_threads)) ok = false; } else if (k == input_kind::Lua) { try { @@ -216,7 +222,7 @@ int main(int argc, char ** argv) { } if (ok && interactive && default_k == input_kind::Lean) { signal(SIGINT, on_ctrl_c); - lean::interactive in(env, ios, S); + lean::interactive in(env, ios, S, num_threads); in(std::cin, "[stdin]"); } if (export_objects) { diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp index 9783263ad..11005afa5 100644 --- a/src/util/lean_path.cpp +++ b/src/util/lean_path.cpp @@ -218,6 +218,14 @@ std::string find_file(std::string fname) { return find_file(fname, {".olean", ".lean", ".lua"}); } +std::string find_file(name const & fname) { + return find_file(fname.to_string(g_sep_str.c_str())); +} + +std::string find_file(name const & fname, std::initializer_list const & exts) { + return find_file(fname.to_string(g_sep_str.c_str()), exts); +} + char const * get_lean_path() { return g_lean_path.c_str(); } diff --git a/src/util/lean_path.h b/src/util/lean_path.h index cf5c5f100..5549e3126 100644 --- a/src/util/lean_path.h +++ b/src/util/lean_path.h @@ -17,9 +17,11 @@ char const * get_lean_path(); exception if the file was not found. */ std::string find_file(std::string fname); - std::string find_file(std::string fname, std::initializer_list const & exts); +/** \brief Hierarchical names are converted into paths using the path separator. Example: foo.bar is converted into foo/bar */ +std::string find_file(name const & fname); +std::string find_file(name const & fname, std::initializer_list const & exts); /** \brief Return true iff fname ends with ".lean" */ bool is_lean_file(std::string const & fname); diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp index 1c9033df2..a6a5a3be2 100644 --- a/src/util/script_state.cpp +++ b/src/util/script_state.cpp @@ -128,7 +128,7 @@ struct script_state::imp { } bool import(char const * fname) { - return import_explicit(find_file(fname)); + return import_explicit(find_file(std::string(fname))); } };