diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 44078360e..c2469bcff 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -4,6 +4,6 @@ parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp interactive.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp -class.cpp pp_options.cpp tactic_hint.cpp pp.cpp) +class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 67882a72d..1adbae19a 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -17,7 +17,6 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" -#include "kernel/type_checker.h" #include "library/parser_nested_exception.h" #include "library/aliases.h" #include "library/private.h" @@ -84,7 +83,7 @@ parser::parser(environment const & env, io_state const & ios, 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_theorem_queue(num_threads > 1 ? num_threads - 1 : 0, []() { enable_expr_caching(false); }) { + m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0) { m_scanner.set_line(line); m_num_threads = num_threads; m_no_undef_id_error = false; @@ -1079,13 +1078,7 @@ bool parser::parse_commands() { } void parser::add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls, expr const & t, expr const & v) { - local_level_decls saved_lls = get_local_level_decls(); - m_theorem_queue.add([=]() { - level_param_names new_ls; - expr type, value; - std::tie(type, value, new_ls) = elaborate_definition_at(env, saved_lls, n, t, v); - return check(env, mk_theorem(n, append(ls, new_ls), type, value)); - }); + m_theorem_queue.add(env, n, ls, get_local_level_decls(), t, v); } bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 28ba2dca9..861aacc00 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -24,6 +24,7 @@ Author: Leonardo de Moura #include "frontends/lean/local_decls.h" #include "frontends/lean/parser_config.h" #include "frontends/lean/parser_pos_provider.h" +#include "frontends/lean/theorem_queue.h" namespace lean { /** \brief Exception used to track parsing erros, it does not leak outside of this class. */ @@ -65,7 +66,7 @@ class parser { optional m_has_string; optional m_has_tactic_decls; // We process theorems in parallel - worker_queue m_theorem_queue; + theorem_queue m_theorem_queue; void display_error_pos(unsigned line, unsigned pos); void display_error_pos(pos_info p); diff --git a/src/frontends/lean/theorem_queue.cpp b/src/frontends/lean/theorem_queue.cpp new file mode 100644 index 000000000..b0e0e37e7 --- /dev/null +++ b/src/frontends/lean/theorem_queue.cpp @@ -0,0 +1,26 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "kernel/type_checker.h" +#include "frontends/lean/theorem_queue.h" +#include "frontends/lean/parser.h" + +namespace lean { +theorem_queue::theorem_queue(parser & p, unsigned num_threads):m_parser(p), m_queue(num_threads, []() { enable_expr_caching(false); }) {} +void theorem_queue::add(environment const & env, name const & n, level_param_names const & ls, local_level_decls const & lls, + expr const & t, expr const & v) { + m_queue.add([=]() { + level_param_names new_ls; + expr type, value; + std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v); + return check(env, mk_theorem(n, append(ls, new_ls), type, value)); + }); +} +std::vector const & theorem_queue::join() { return m_queue.join(); } +void theorem_queue::interrupt() { m_queue.interrupt(); } +bool theorem_queue::done() const { return m_queue.done(); } +} diff --git a/src/frontends/lean/theorem_queue.h b/src/frontends/lean/theorem_queue.h new file mode 100644 index 000000000..6a69a3191 --- /dev/null +++ b/src/frontends/lean/theorem_queue.h @@ -0,0 +1,27 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "util/worker_queue.h" +#include "kernel/environment.h" +#include "frontends/lean/local_decls.h" + +namespace lean { +class parser; +typedef local_decls local_level_decls; +class theorem_queue { + parser & m_parser; + worker_queue m_queue; +public: + theorem_queue(parser & p, unsigned num_threads); + void add(environment const & env, name const & n, level_param_names const & ls, local_level_decls const & lls, + expr const & t, expr const & v); + std::vector const & join(); + void interrupt(); + bool done() const; +}; +}