From 7ccb9a389c2262d84ea1ae1ec5d21af2a038740b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 12 Jul 2014 22:50:57 +0100 Subject: [PATCH] feat(frontends/lean): process theorems in parallel Signed-off-by: Leonardo de Moura --- src/frontends/lean/decl_cmds.cpp | 20 +++++++++++++++++--- src/frontends/lean/parser.cpp | 20 +++++++++++++++++++- src/frontends/lean/parser.h | 9 +++++++++ src/util/worker_queue.h | 2 ++ 4 files changed, 47 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 3a4fed330..7bae639b4 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -291,9 +291,23 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { env = add_decl_alias(env, n, mk_constant(real_n)); level_param_names new_ls; if (is_theorem) { - // TODO(Leo): delay theorems - std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value); - env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value))); + if (p.num_threads() > 1) { + // add as axiom, and create a task to prove the theorem + expr saved_type = type; + expr saved_value = value; + environment saved_env = env; + std::tie(type, new_ls) = p.elaborate_type(type); + env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type))); + p.add_delayed_theorem([=, &p]() { + level_param_names new_ls; + expr type, value; + std::tie(type, value, new_ls) = p.elaborate_definition_at(saved_env, n, saved_type, saved_value); + return check(saved_env, mk_theorem(real_n, append(ls, new_ls), type, value)); + }); + } else { + std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value); + env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value))); + } } else { std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value); env = module::add(env, check(env, mk_definition(env, real_n, append(ls, new_ls), type, value, modifiers.m_is_opaque))); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 93461496b..6ad3d6cd9 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -75,7 +75,7 @@ parser::parser(environment const & env, io_state const & ios, m_env(env), m_ios(ios), m_ngen(g_tmp_prefix), m_verbose(true), m_use_exceptions(use_exceptions), m_scanner(strm, strm_name), m_local_level_decls(lds), m_local_decls(eds), - m_pos_table(std::make_shared()) { + m_pos_table(std::make_shared()), m_theorem_queue(num_threads > 1 ? num_threads - 1 : 0) { m_scanner.set_line(line); m_num_threads = num_threads; m_no_undef_id_error = false; @@ -87,6 +87,15 @@ parser::parser(environment const & env, io_state const & ios, [&]() { sync_command(); }); } +parser::~parser() { + try { + if (!m_theorem_queue.done()) { + m_theorem_queue.interrupt(); + m_theorem_queue.join(); + } + } catch (...) {} +} + bool parser::has_tactic_decls() { if (!m_has_tactic_decls) m_has_tactic_decls = ::lean::has_tactic_decls(m_env); @@ -484,6 +493,12 @@ std::tuple parser::elaborate_definition(name cons return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, &pp); } +std::tuple parser::elaborate_definition_at(environment const & env, name const & n, expr const & t, + expr const & v) { + parser_pos_provider pp = get_pos_provider(); + return ::lean::elaborate(env, m_local_level_decls, m_ios, n, t, v, &pp); +} + [[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) { throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos); } @@ -1035,6 +1050,9 @@ bool parser::parse_commands() { [&]() { sync_command(); }); } } catch (interrupt_parser) {} + for (certified_declaration const & thm : m_theorem_queue.join()) { + m_env.replace(thm); + } return !m_found_errors; } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 16844eab8..b43cb71bd 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "util/exception.h" #include "util/thread_script_state.h" #include "util/script_exception.h" +#include "util/worker_queue.h" #include "util/name_generator.h" #include "kernel/environment.h" #include "kernel/expr_maps.h" @@ -63,6 +64,8 @@ class parser { optional m_has_num; optional m_has_string; optional m_has_tactic_decls; + // We process theorems in parallel + worker_queue m_theorem_queue; void display_error_pos(unsigned line, unsigned pos); void display_error_pos(pos_info p); @@ -130,6 +133,7 @@ public: local_level_decls const & lds = local_level_decls(), local_expr_decls const & eds = local_expr_decls(), unsigned line = 1); + ~parser(); environment const & env() const { return m_env; } io_state const & ios() const { return m_ios; } @@ -157,6 +161,9 @@ public: expr mk_app(expr fn, expr arg, pos_info const & p); expr mk_app(std::initializer_list const & args, pos_info const & p); + unsigned num_threads() const { return m_num_threads; } + void add_delayed_theorem(std::function const & fn) { m_theorem_queue.add(fn); } + /** \brief Read the next token. */ void scan() { m_curr = m_scanner.scan(m_env); } /** \brief Return the current token */ @@ -260,6 +267,8 @@ public: std::tuple elaborate(expr const & e) { return elaborate_at(m_env, e); } /** \brief Elaborate the definition n : t := v */ std::tuple elaborate_definition(name const & n, expr const & t, expr const & v); + /** \brief Elaborate the definition n : t := v in the given environment*/ + std::tuple elaborate_definition_at(environment const & env, name const & n, expr const & t, expr const & v); parser_pos_provider get_pos_provider() const { return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos); } diff --git a/src/util/worker_queue.h b/src/util/worker_queue.h index 542ed730c..eb5a99db6 100644 --- a/src/util/worker_queue.h +++ b/src/util/worker_queue.h @@ -115,5 +115,7 @@ public: for (auto & t : m_threads) t->request_interrupt(); } + + bool done() const { return m_done; } }; }