fix(frontends/lean/parser): fixes #584

src/frontends/lean/parser.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "library/aliases.h"
 #include "library/constants.h"
 #include "library/private.h"
+#include "library/locals.h"
 #include "library/protected.h"
 #include "library/choice.h"
 #include "library/placeholder.h"
@@ -521,9 +522,39 @@ void parser::add_parameter(name const & n, expr const & p) {
 
 bool parser::update_local_binder_info(name const & n, binder_info const & bi) {
     auto it = get_local(n);
-    if (!it) return false;
-    if (!is_local(*it)) return false;
-    m_local_decls.update(n, update_local(*it, bi));
+    if (!it || !is_local(*it)) return false;
+
+    buffer<pair<name, expr>> entries;
+    to_buffer(m_local_decls.get_entries(), entries);
+    std::reverse(entries.begin(), entries.end());
+    unsigned idx = m_local_decls.find_idx(n);
+    lean_assert(idx > 0);
+    lean_assert_eq(entries[idx-1].second, *it);
+
+    buffer<expr> old_locals;
+    buffer<expr> new_locals;
+    old_locals.push_back(*it);
+    expr new_l = update_local(*it, bi);
+    m_local_decls.update(n, 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); })) {
+            r  = instantiate_rev(abstract_locals(r, old_locals.size(), old_locals.data()),
+                                 new_locals.size(), new_locals.data());
+            if (is_local(curr_e)) {
+                expr new_e = update_mlocal(curr_e, r);
+                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);
+            }
+        }
+    }
     return true;
 }
 

tests/lean/584a.lean

@@ -0,0 +1,18 @@
+variables (A : Type) [H : inhabited A] (x : A)
+include H
+
+definition foo := x
+check foo  -- A and x are explicit
+
+variables {A x}
+definition foo' := x
+check @foo' -- A is explicit, x is implicit
+
+open nat
+
+check foo nat 10
+
+definition test : foo' = 10 := rfl
+
+set_option pp.implicit true
+print test

tests/lean/584a.lean.expected.out

@@ -0,0 +1,5 @@
+foo : Π (A : Type) [H : inhabited A], A → A
+foo' : Π {A : Type} [H : inhabited A] {x : A}, A
+foo ℕ 10 : ℕ
+definition test : ∀ {A : Type} [H : inhabited A], @foo' num num.is_inhabited 10 = 10
+λ (A : Type) (H : inhabited A), @rfl num (@foo' num num.is_inhabited 10)

tests/lean/584b.lean

@@ -0,0 +1,27 @@
+section
+  variable (A : Type)
+
+  section
+    variables (a b : A)
+    variable  (H : a = b)
+
+    definition tst₁ := a
+
+    check @tst₁
+
+    variable {A}
+
+    definition tst₂ := a
+
+    check @tst₂ -- A is implicit
+
+    lemma symm₂ : b = a := eq.symm H
+
+    check @symm₂
+  end
+
+  variable (a : A)
+  definition tst₃ := a
+
+  check @tst₃  -- A is explicit again
+end

tests/lean/584b.lean.expected.out

@@ -0,0 +1,4 @@
+tst₁ : Π (A : Type), A → A
+tst₂ : Π {A : Type}, A → A
+symm₂ : ∀ {A : Type} (a b : A), a = b → b = a
+tst₃ : Π (A : Type), A → A

tests/lean/584c.lean

@@ -0,0 +1,29 @@
+section
+  parameter (A : Type)
+
+  section
+    parameters (a b : A)
+    parameter  (H : a = b)
+
+    definition tst₁ := a
+
+    parameter {A}
+
+    definition tst₂ := a
+
+    lemma symm₂ : b = a := eq.symm H
+
+    parameters {a b}
+    lemma foo (c : A) (h₂ : c = b) : c = a :=
+    eq.trans h₂ symm₂
+  end
+
+  parameter (a : A)
+  definition tst₃ := a
+end
+
+check @tst₁
+check @tst₂ -- A is implicit
+check @symm₂
+check @tst₃  -- A is explicit again
+check @foo

tests/lean/584c.lean.expected.out

@@ -0,0 +1,5 @@
+tst₁ : Π (A : Type), A → A
+tst₂ : Π {A : Type}, A → A
+symm₂ : ∀ {A : Type} (a b : A), a = b → b = a
+tst₃ : Π (A : Type), A → A
+foo : ∀ {A : Type} {a b : A}, a = b → (∀ (c : A), c = b → c = a)