refactor(frontends/lean): create theorem_queue class

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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})

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<pos_info_table>()),
-    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(env, n, ls, get_local_level_decls(), t, v);
-    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));
-        });
 }
 
 bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions,

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<bool>          m_has_string;
     optional<bool>          m_has_tactic_decls;
     // We process theorems in parallel
-    worker_queue<certified_declaration> m_theorem_queue;
+    theorem_queue           m_theorem_queue;
 
     void display_error_pos(unsigned line, unsigned pos);
     void display_error_pos(pos_info p);

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 <vector>
+#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<certified_declaration> const & theorem_queue::join() { return m_queue.join(); }
+void theorem_queue::interrupt() { m_queue.interrupt(); }
+bool theorem_queue::done() const { return m_queue.done(); }
+}

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 <vector>
+#include "util/worker_queue.h"
+#include "kernel/environment.h"
+#include "frontends/lean/local_decls.h"
+
+namespace lean {
+class parser;
+typedef local_decls<level>  local_level_decls;
+class theorem_queue {
+    parser & m_parser;
+    worker_queue<certified_declaration> 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<certified_declaration> const & join();
+    void interrupt();
+    bool done() const;
+};
+}