fix(frontends/lean): fixes #652

src/frontends/lean/builtin_cmds.cpp

@@ -513,14 +513,18 @@ static environment redeclare_aliases(environment env, parser & p,
         return env;
     list<pair<name, expr>> new_entries = p.get_local_entries();
     buffer<pair<name, expr>> to_redeclare;
+    unsigned new_len = length(new_entries);
+    unsigned old_len = length(old_entries);
+    lean_assert(old_len >= new_len);
     name_set popped_locals;
-    while (!is_eqp(old_entries, new_entries)) {
+    while (old_len > new_len) {
         pair<name, expr> entry = head(old_entries);
         if (is_local_ref(entry.second))
             to_redeclare.push_back(entry);
         else if (is_local(entry.second))
             popped_locals.insert(mlocal_name(entry.second));
         old_entries = tail(old_entries);
+        old_len--;
     }
     name_set popped_levels;
     list<pair<name, level>> new_level_entries = p.get_local_level_entries();

src/frontends/lean/local_decls.h

@@ -38,13 +38,24 @@ public:
         lean_assert(m_counter > 0);
         return m_counter - 1;
     }
-    void update(name const & k, V const & v) {
-        if (auto it = m_map.find(k)) {
-            m_map.insert(k, mk_pair(v, it->second));
-        } else {
-            lean_unreachable();
+    void update_entries(entries const & new_entries) {
+        lean_assert(length(new_entries) == length(m_entries));
+        auto it1 = m_entries;
+        auto it2 = new_entries;
+        unsigned i = length(new_entries);
+        while (it1.raw() != it2.raw()) {
+            name const & k = head(it2).first;
+            V const & v    = head(it2).second;
+            lean_assert(m_map.find(k));
+            lean_assert_eq(m_map.find(k)->second, i);
+            m_map.insert(k, mk_pair(v, i));
+            it1 = tail(it1);
+            it2 = tail(it2);
+            --i;
         }
+        m_entries = new_entries;
     }
+
     V const * find(name const & k) const { auto it = m_map.find(k); return it ? &(it->first) : nullptr; }
     unsigned find_idx(name const & k) const { auto it = m_map.find(k); return it ? it->second : 0; }
     bool contains(name const & k) const { return m_map.contains(k); }

src/frontends/lean/parser.cpp

@@ -542,11 +542,10 @@ bool parser::update_local_binder_info(name const & n, binder_info const & bi) {
     buffer<expr> new_locals;
     old_locals.push_back(*it);
     expr new_l = update_local(*it, bi);
-    m_local_decls.update(n, new_l);
+    entries[idx-1].second = new_l;
     new_locals.push_back(new_l);
 
     for (unsigned i = idx; i < entries.size(); i++) {
-        name const & curr_n = entries[i].first;
         expr const & curr_e = entries[i].second;
         expr r = is_local(curr_e) ? mlocal_type(curr_e) : curr_e;
         if (std::any_of(old_locals.begin(), old_locals.end(), [&](expr const & l) { return depends_on(r, l); })) {
@@ -554,14 +553,21 @@ bool parser::update_local_binder_info(name const & n, binder_info const & bi) {
                                  new_locals.size(), new_locals.data());
             if (is_local(curr_e)) {
                 expr new_e = update_mlocal(curr_e, r);
+                entries[i].second = new_e;
                 old_locals.push_back(curr_e);
                 new_locals.push_back(new_e);
-                m_local_decls.update(curr_n, new_e);
             } else {
-                m_local_decls.update(curr_n, r);
+                entries[i].second = r;
             }
         }
     }
+    auto new_entries = m_local_decls.get_entries();
+    unsigned sz_to_updt = entries.size() - idx + 1;
+    for (unsigned i = 0; i < sz_to_updt; i++)
+        new_entries = tail(new_entries); // remove entries that will be updated
+    for (unsigned i = idx-1; i < entries.size(); i++)
+        new_entries = cons(entries[i], new_entries);
+    m_local_decls.update_entries(new_entries);
     return true;
 }
 

tests/lean/652.lean

@@ -0,0 +1,25 @@
+section
+  parameters {b c : bool}
+
+  definition R : Prop := (b = c)
+
+  parameters (b c)
+  definition R2 := R
+  parameter (c)
+  parameter (b)
+  definition R3 := R
+  parameter {c}
+  parameter (b)
+  definition R4 := R
+  parameters {c b}
+  definition R5 := R
+  parameters (c)
+  definition R6 := R
+end
+
+check @R
+check @R2
+check @R3
+check @R4
+check @R5
+check @R6

tests/lean/652.lean.expected.out

@@ -0,0 +1,6 @@
+R : Π {b c : bool}, Prop
+R2 : bool → bool → Prop
+R3 : bool → bool → Prop
+R4 : bool → (Π {c : bool}, Prop)
+R5 : Π {b c : bool}, Prop
+R6 : Π {b : bool}, bool → Prop