fix(frontends/lean/parser): segmentation fault after REPLACE, fixes #172

src/frontends/lean/parser.cpp

@@ -82,15 +82,19 @@ static name g_tmp_prefix = name::mk_internal_unique_name();
 parser::parser(environment const & env, io_state const & ios,
                std::istream & strm, char const * strm_name,
                bool use_exceptions, unsigned num_threads,
-               local_level_decls const & lds, local_expr_decls const & eds,
+               snapshot const * s, snapshot_vector * sv, info_manager * im):
-               unsigned line, snapshot_vector * sv, info_manager * im):
     m_env(env), m_ios(ios), m_ngen(g_tmp_prefix),
     m_verbose(true), m_use_exceptions(use_exceptions),
-    m_scanner(strm, strm_name, line), m_local_level_decls(lds), m_local_decls(eds),
+    m_scanner(strm, strm_name, s ? s->m_line : 1),
     m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0),
     m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) {
+    if (s) {
+        m_local_level_decls = s->m_lds;
+        m_local_decls       = s->m_eds;
+        m_options_stack     = s->m_options_stack;
+    }
     m_num_threads = num_threads;
-    m_no_undef_id_error    = false;
+    m_no_undef_id_error = false;
     m_found_errors = false;
     m_used_sorry = false;
     updt_options();
@@ -393,19 +397,20 @@ void parser::push_local_scope(bool save_options) {
     m_local_level_decls.push();
     m_local_decls.push();
     if (save_options)
-        m_options_stack.push_back(optional<options>(m_ios.get_options()));
+        m_options_stack = cons(optional<options>(m_ios.get_options()), m_options_stack);
     else
-        m_options_stack.push_back(optional<options>());
+        m_options_stack = cons(optional<options>(), m_options_stack);
 }
 
 void parser::pop_local_scope() {
     m_local_level_decls.pop();
     m_local_decls.pop();
-    if (auto const & it = m_options_stack.back()) {
+    lean_assert(!is_nil(m_options_stack));
+    if (auto const & it = head(m_options_stack)) {
         m_ios.set_options(*it);
         updt_options();
     }
-    m_options_stack.pop_back();
+    m_options_stack = tail(m_options_stack);
 }
 
 void parser::add_local_level(name const & n, level const & l) {
@@ -1316,7 +1321,8 @@ void parser::save_snapshot() {
     if (!m_snapshot_vector)
         return;
     if (m_snapshot_vector->empty() || static_cast<int>(m_snapshot_vector->back().m_line) != m_scanner.get_line())
-        m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls, m_ios.get_options(), m_scanner.get_line()));
+        m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls,
+                                              m_options_stack, m_ios.get_options(), m_scanner.get_line()));
 }
 
 void parser::save_pre_info_data() {

src/frontends/lean/parser.h

@@ -41,27 +41,29 @@ struct parser_error : public exception {
 };
 
 struct interrupt_parser {};
-typedef local_decls<expr>   local_expr_decls;
+typedef local_decls<expr>       local_expr_decls;
-typedef local_decls<level>  local_level_decls;
+typedef local_decls<level>      local_level_decls;
-typedef environment         local_environment;
+typedef list<optional<options>> options_stack;
+typedef environment             local_environment;
 
 /** \brief Snapshot of the state of the Lean parser */
 struct snapshot {
     environment       m_env;
     local_level_decls m_lds;
     local_expr_decls  m_eds;
+    options_stack     m_options_stack;
     options           m_options;
     unsigned          m_line;
     snapshot():m_line(0) {}
     snapshot(environment const & env, options const & o):m_env(env), m_options(o), m_line(1) {}
-    snapshot(environment const & env, local_level_decls const & lds, local_expr_decls const & eds, options const & opts, unsigned line):
+    snapshot(environment const & env, local_level_decls const & lds, local_expr_decls const & eds,
-        m_env(env), m_lds(lds), m_eds(eds), m_options(opts), m_line(line) {}
+             options_stack const & os, options const & opts, unsigned line):
+        m_env(env), m_lds(lds), m_eds(eds), m_options_stack(os), m_options(opts), m_line(line) {}
 };
 
 typedef std::vector<snapshot> snapshot_vector;
 
 class parser {
-    typedef std::vector<optional<options>> options_stack;
     environment             m_env;
     io_state                m_ios;
     name_generator          m_ngen;
@@ -183,9 +185,8 @@ public:
     parser(environment const & env, io_state const & ios,
            std::istream & strm, char const * str_name,
            bool use_exceptions = false, unsigned num_threads = 1,
-           local_level_decls const & lds = local_level_decls(),
+           snapshot const * s = nullptr, snapshot_vector * sv = nullptr,
-           local_expr_decls const & eds = local_expr_decls(), unsigned line = 1,
+           info_manager * im = nullptr);
-           snapshot_vector * sv = nullptr, info_manager * im = nullptr);
     ~parser();
 
     void set_cache(definition_cache * c) { m_cache = c; }

src/frontends/lean/server.cpp

@@ -202,7 +202,7 @@ server::worker::worker(environment const & env, io_state const & ios, definition
                     bool use_exceptions  = false;
                     unsigned num_threads = 1;
                     parser p(s.m_env, tmp_ios, strm, todo_file->m_fname.c_str(), use_exceptions, num_threads,
-                             s.m_lds, s.m_eds, s.m_line, &todo_file->m_snapshots, &todo_file->m_info);
+                             &s, &todo_file->m_snapshots, &todo_file->m_info);
                     p.set_cache(&m_cache);
                     p();
                 } catch (interrupted &) {

tests/lean/interactive/optstack.input

@@ -0,0 +1,5 @@
+LOAD whnfinst.lean
+WAIT
+REPLACE 14
+end
+WAIT

tests/lean/interactive/optstack.input.expected.out

@@ -0,0 +1,4 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINWAIT
+-- ENDWAIT

tests/lean/interactive/whnfinst.lean

@@ -0,0 +1,14 @@
+import logic
+open decidable
+
+abbreviation decidable_bin_rel {A : Type} (R : A → A → Prop) := Πx y, decidable (R x y)
+
+section
+  parameter {A : Type}
+  parameter (R : A → A → Prop)
+
+  theorem tst1 (H : Πx y, decidable (R x y)) (a b c : A) : decidable (R a b ∧ R b a)
+
+  theorem tst2 (H : decidable_bin_rel R) (a b c : A) : decidable (R a b ∧ R b a ∨ R b b) :=
+  _
+end