From 9d4c073618840d4703eea04c0c87c442b22a4ccb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 10 Aug 2014 11:04:16 -0700 Subject: [PATCH] feat(frontends/lean): add option --cache Signed-off-by: Leonardo de Moura --- src/frontends/lean/decl_cmds.cpp | 44 +++++++++++++++++++++------- src/frontends/lean/parser.cpp | 23 ++++++++++++--- src/frontends/lean/parser.h | 16 ++++++++-- src/frontends/lean/theorem_queue.cpp | 5 +++- src/library/definitions_cache.cpp | 21 ++++++++++--- src/library/definitions_cache.h | 7 ++++- src/shell/lean.cpp | 30 ++++++++++++++++--- 7 files changed, 120 insertions(+), 26 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 0a9505644..4eebbb44a 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -269,21 +269,45 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { expr ref = mk_implicit(mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps)); p.add_local_expr(n, ref); } + expr pre_type = type; + expr pre_value = value; level_param_names new_ls; - if (is_theorem) { - if (p.num_threads() > 1) { - // add as axiom, and create a task to prove the theorem - p.add_delayed_theorem(env, real_n, ls, type, value); - std::tie(type, new_ls) = p.elaborate_type(type); - env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type))); + bool found_cached = false; + if (auto it = p.find_cached_definition(real_n, pre_type, pre_value)) { + optional cd; + try { + level_param_names c_ls; expr c_type, c_value; + std::tie(c_ls, c_type, c_value) = *it; + if (is_theorem) + cd = check(env, mk_theorem(real_n, c_ls, c_type, c_value)); + else + cd = check(env, mk_definition(env, real_n, c_ls, c_type, c_value, modifiers.m_is_opaque)); + env = module::add(env, *cd); + found_cached = true; + } catch (exception&) {} + } + + if (!found_cached) { + if (is_theorem) { + if (p.num_threads() > 1) { + // add as axiom, and create a task to prove the theorem + p.add_delayed_theorem(env, real_n, ls, type, value); + std::tie(type, new_ls) = p.elaborate_type(type); + env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type))); + } else { + std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque); + new_ls = append(ls, new_ls); + env = module::add(env, check(env, mk_theorem(real_n, new_ls, type, value))); + p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value); + } } else { std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque); - env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value))); + new_ls = append(ls, new_ls); + env = module::add(env, check(env, mk_definition(env, real_n, new_ls, type, value, modifiers.m_is_opaque))); + p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value); } - } else { - std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque); - env = module::add(env, check(env, mk_definition(env, real_n, append(ls, new_ls), type, value, modifiers.m_is_opaque))); } + if (real_n != n) env = add_expr_alias_rec(env, n, real_n); if (modifiers.m_is_instance) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 01367857a..d41c6e7f4 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -88,7 +88,7 @@ parser::parser(environment const & env, io_state const & ios, m_scanner(strm, strm_name, line), m_local_level_decls(lds), m_local_decls(eds), m_pos_table(std::make_shared()), m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0), - m_snapshot_vector(sv), m_info_manager(im) { + m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr) { m_num_threads = num_threads; m_no_undef_id_error = false; m_found_errors = false; @@ -109,6 +109,19 @@ parser::~parser() { } catch (...) {} } +void parser::cache_definition(name const & n, expr const & pre_type, expr const & pre_value, + level_param_names const & ls, expr const & type, expr const & value) { + if (m_cache) + m_cache->add(n, pre_type, pre_value, ls, type, value); +} + +optional> parser::find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value) { + if (m_cache) + return m_cache->find(n, pre_type, pre_value); + else + return optional>(); +} + expr parser::mk_sorry(pos_info const & p) { m_used_sorry = true; { @@ -1252,18 +1265,20 @@ void parser::save_type_info(expr const & e) { } bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, - unsigned num_threads) { + unsigned num_threads, definitions_cache * cache) { parser p(env, ios, in, strm_name, use_exceptions, num_threads); + p.set_cache(cache); bool r = p(); ios = p.ios(); env = p.env(); return r; } -bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads) { +bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads, + definitions_cache * cache) { std::ifstream in(fname); if (in.bad() || in.fail()) throw exception(sstream() << "failed to open file '" << fname << "'"); - return parse_commands(env, ios, in, fname, use_exceptions, num_threads); + return parse_commands(env, ios, in, fname, use_exceptions, num_threads, cache); } } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index f2dfd9f3a..e079dee7f 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -20,6 +20,7 @@ Author: Leonardo de Moura #include "library/io_state.h" #include "library/io_state_stream.h" #include "library/kernel_bindings.h" +#include "library/definitions_cache.h" #include "frontends/lean/scanner.h" #include "frontends/lean/local_decls.h" #include "frontends/lean/parser_config.h" @@ -90,6 +91,9 @@ class parser { info_manager * m_info_manager; std::vector m_pre_info_data; // type information before elaboration + // cache support + definitions_cache * m_cache; + void display_warning_pos(unsigned line, unsigned pos); void display_warning_pos(pos_info p); void display_error_pos(unsigned line, unsigned pos); @@ -167,6 +171,12 @@ public: snapshot_vector * sv = nullptr, info_manager * im = nullptr); ~parser(); + void set_cache(definitions_cache * c) { m_cache = c; } + void cache_definition(name const & n, expr const & pre_type, expr const & pre_value, + level_param_names const & ls, expr const & type, expr const & value); + /** \brief Try to find an elaborated definition for (n, pre_type, pre_value) in the cache */ + optional> find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value); + environment const & env() const { return m_env; } io_state const & ios() const { return m_ios; } local_level_decls const & get_local_level_decls() const { return m_local_level_decls; } @@ -309,6 +319,8 @@ public: bool operator()() { return parse_commands(); } }; -bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, unsigned num_threads); -bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads); +bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, unsigned num_threads, + definitions_cache * cache = nullptr); +bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads, + definitions_cache * cache = nullptr); } diff --git a/src/frontends/lean/theorem_queue.cpp b/src/frontends/lean/theorem_queue.cpp index 08c3fff91..94c022f86 100644 --- a/src/frontends/lean/theorem_queue.cpp +++ b/src/frontends/lean/theorem_queue.cpp @@ -18,7 +18,10 @@ void theorem_queue::add(environment const & env, name const & n, level_param_nam expr type, value; bool is_opaque = true; // theorems are always opaque std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v, is_opaque); - return check(env, mk_theorem(n, append(ls, new_ls), type, value)); + new_ls = append(ls, new_ls); + auto r = check(env, mk_theorem(n, new_ls, type, value)); + m_parser.cache_definition(n, t, v, new_ls, type, value); + return r; }); } std::vector const & theorem_queue::join() { return m_queue.join(); } diff --git a/src/library/definitions_cache.cpp b/src/library/definitions_cache.cpp index b22b0f5cd..d03ed8cef 100644 --- a/src/library/definitions_cache.cpp +++ b/src/library/definitions_cache.cpp @@ -120,7 +120,8 @@ public: definitions_cache::definitions_cache() {} -definitions_cache::definitions_cache(std::istream & in) { +void definitions_cache::load(std::istream & in) { + lock_guard lc(m_mutex); deserializer d(in); unsigned num; d >> num; @@ -129,17 +130,28 @@ definitions_cache::definitions_cache(std::istream & in) { level_param_names ls; expr pre_type, pre_value, type, value; d >> n >> pre_type >> pre_value >> ls >> type >> value; - add(n, pre_type, pre_value, ls, type, value); + add_core(n, pre_type, pre_value, ls, type, value); } } +void definitions_cache::add_core(name const & n, expr const & pre_type, expr const & pre_value, + level_param_names const & ls, expr const & type, expr const & value) { + m_definitions.insert(n, entry(pre_type, pre_value, ls, type, value)); +} + void definitions_cache::add(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value) { - m_definitions.insert(n, entry(pre_type, pre_value, ls, type, value)); + lock_guard lc(m_mutex); + add_core(n, pre_type, pre_value, ls, type, value); } optional> definitions_cache::find(name const & n, expr const & pre_type, expr const & pre_value) { - if (auto it = m_definitions.find(n)) { + entry const * it; + { + lock_guard lc(m_mutex); + it = m_definitions.find(n); + } + if (it) { level_param_names ls; expr c_pre_type, c_pre_value, type, value; std::tie(c_pre_type, c_pre_value, ls, type, value) = *it; @@ -151,6 +163,7 @@ optional> definitions_cache::find(name } void definitions_cache::save(std::ostream & out) { + lock_guard lc(m_mutex); serializer s(out); s << m_definitions.size(); m_definitions.for_each([&](name const & n, entry const & e) { diff --git a/src/library/definitions_cache.h b/src/library/definitions_cache.h index c573413e3..96a2fee03 100644 --- a/src/library/definitions_cache.h +++ b/src/library/definitions_cache.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "util/thread.h" #include "util/name_map.h" #include "util/optional.h" #include "kernel/expr.h" @@ -15,10 +16,12 @@ namespace lean { */ class definitions_cache { typedef std::tuple entry; + mutex m_mutex; name_map m_definitions; + void add_core(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, + expr const & type, expr const & value); public: definitions_cache(); - definitions_cache(std::istream & in); /** \brief Add the cache entry (n, pre_type, pre_value) -> (ls, type, value) */ void add(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value); /** \brief Return (if available) elaborated (level_names, type, value) for (n, pre_type, pre_value). @@ -29,5 +32,7 @@ public: optional> find(name const & n, expr const & pre_type, expr const & pre_value); /** \brief Store the cache content into the given stream */ void save(std::ostream & out); + /** \brief Load the cache content from the given stream */ + void load(std::istream & in); }; } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index b18891641..0033cffba 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -24,6 +24,7 @@ Author: Leonardo de Moura #include "library/hott_kernel.h" #include "library/module.h" #include "library/io_state_stream.h" +#include "library/definitions_cache.h" #include "library/error_handling/error_handling.h" #include "frontends/lean/parser.h" #include "frontends/lean/pp.h" @@ -43,6 +44,7 @@ using lean::mk_environment; using lean::mk_hott_environment; using lean::set_environment; using lean::set_io_state; +using lean::definitions_cache; enum class input_kind { Unspecified, Lean, Lua }; @@ -76,6 +78,7 @@ static void display_help(std::ostream & out) { std::cout << " --threads=num -j number of threads used to process lean files\n"; std::cout << " --deps just print dependencies of a Lean input\n"; std::cout << " --flycheck print structured error message for flycheck\n"; + std::cout << " --cache=file -c load/save cached definitions from/to the given file\n"; #if defined(LEAN_USE_BOOST) std::cout << " --tstack=num -s thread stack size in Kb\n"; #endif @@ -109,6 +112,7 @@ static struct option g_long_options[] = { {"quiet", no_argument, 0, 'q'}, {"hott", no_argument, 0, 'H'}, {"threads", required_argument, 0, 'j'}, + {"cache", required_argument, 0, 'c'}, {"deps", no_argument, 0, 'D'}, {"flycheck", no_argument, 0, 'F'}, #if defined(LEAN_USE_BOOST) @@ -118,9 +122,9 @@ static struct option g_long_options[] = { }; #if defined(LEAN_USE_BOOST) -static char const * g_opt_str = "FDHSqlupgvhj:012k:012s:012t:012o:"; +static char const * g_opt_str = "FDHSqlupgvhj:012k:012s:012t:012o:c:"; #else -static char const * g_opt_str = "FDHSqlupgvhj:012k:012t:012o:"; +static char const * g_opt_str = "FDHSqlupgvhj:012k:012t:012o:c:"; #endif enum class lean_mode { Standard, HoTT }; @@ -136,7 +140,9 @@ int main(int argc, char ** argv) { bool flycheck = false; lean_mode mode = lean_mode::Standard; unsigned num_threads = 1; + bool use_cache = false; std::string output; + std::string cache_name; input_kind default_k = input_kind::Lean; // default while (true) { int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL); @@ -178,9 +184,13 @@ int main(int argc, char ** argv) { lean::set_thread_stack_size(atoi(optarg)*1024); break; case 'o': - output = optarg; + output = optarg; export_objects = true; break; + case 'c': + cache_name = optarg; + use_cache = true; + break; case 't': trust_lvl = atoi(optarg); break; @@ -209,6 +219,14 @@ int main(int argc, char ** argv) { script_state S = lean::get_thread_script_state(); set_environment set1(S, env); set_io_state set2(S, ios); + definitions_cache cache; + definitions_cache * cache_ptr = nullptr; + if (use_cache) { + cache_ptr = &cache; + std::ifstream in(cache_name); + if (!in.bad() && !in.fail()) + cache.load(in); + } try { bool ok = true; @@ -225,7 +243,7 @@ int main(int argc, char ** argv) { if (k == input_kind::Lean) { if (only_deps) { display_deps(env, std::cout, argv[i]); - } else if (!parse_commands(env, ios, argv[i], false, num_threads)) { + } else if (!parse_commands(env, ios, argv[i], false, num_threads, cache_ptr)) { ok = false; } } else if (k == input_kind::Lua) { @@ -245,6 +263,10 @@ int main(int argc, char ** argv) { if (!Sv(std::cin)) ok = false; } + if (use_cache) { + std::ofstream out(cache_name, std::ofstream::binary); + cache.save(out); + } if (export_objects && ok) { std::ofstream out(output, std::ofstream::binary); export_module(out, env);