fix(frontends/lean): name clash inside section, fixes #181

library/data/sigma.lean

@@ -14,7 +14,7 @@ section
   parameters {A : Type} {B : A → Type}
 
   abbreviation dpr1 (p : Σ x, B x) : A := rec (λ a b, a) p
-  abbreviation dpr2 {A : Type} {B : A → Type} (p : Σ x, B x) : B (dpr1 p) := rec (λ a b, b) p
+  abbreviation dpr2 (p : Σ x, B x) : B (dpr1 p) := rec (λ a b, b) p
 
   theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := rfl
   theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := rfl

src/frontends/lean/builtin_exprs.cpp

@@ -349,7 +349,7 @@ static expr parse_including_expr(parser & p, unsigned, expr const *, pos_info co
     buffer<expr> new_locals;
     for (auto old_l : locals) {
         binder_info bi = mk_contextual_info(true);
-        expr new_l     = p.save_pos(mk_local(local_pp_name(old_l), mk_as_is(mlocal_type(old_l)), bi), pos);
+        expr new_l     = p.save_pos(mk_local(p.mk_fresh_name(), local_pp_name(old_l), mk_as_is(mlocal_type(old_l)), bi), pos);
         p.add_local(new_l);
         new_locals.push_back(new_l);
     }

src/frontends/lean/decl_cmds.cpp

@@ -81,7 +81,9 @@ static environment declare_var(parser & p, environment env,
     binder_info bi;
     if (_bi) bi = *_bi;
     if (in_section_or_context(p.env())) {
-        p.add_local(p.save_pos(mk_local(n, type, bi), pos));
+        name u = p.mk_fresh_name();
+        expr l = p.save_pos(mk_local(u, n, type, bi), pos);
+        p.add_local_expr(n, l);
         return env;
     } else {
         name const & ns = get_namespace(env);

src/frontends/lean/elaborator.cpp

@@ -936,7 +936,8 @@ public:
     }
 
     std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n, bool is_opaque) {
-        lean_assert(!has_local(t)); lean_assert(!has_local(v));
+        lean_assert(!has_local(t));
+        lean_assert(!has_local(v));
         constraint_seq t_cs;
         expr r_t      = ensure_type(visit(t, t_cs), t_cs);
         // Opaque definitions in the main module may treat other opaque definitions (in the main module) as transparent.

src/frontends/lean/local_decls.h

@@ -28,7 +28,11 @@ class local_decls {
 public:
     local_decls():m_counter(1) {}
     local_decls(local_decls const & d):m_map(d.m_map), m_counter(d.m_counter), m_scopes(d.m_scopes) {}
-    void insert(name const & k, V const & v) { m_map.insert(k, mk_pair(v, m_counter)); m_counter++; m_values = cons(v, m_values); }
+    void insert(name const & k, V const & v) {
+        m_map.insert(k, mk_pair(v, m_counter));
+        m_counter++;
+        m_values = cons(v, m_values);
+    }
     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/util.cpp

@@ -38,7 +38,7 @@ void sort_section_params(expr_struct_set const & locals, parser const & p, buffe
     for (expr const & l : locals)
         section_ps.push_back(l);
     std::sort(section_ps.begin(), section_ps.end(), [&](expr const & p1, expr const & p2) {
-            return p.get_local_index(mlocal_name(p1)) < p.get_local_index(mlocal_name(p2));
+            return p.get_local_index(local_pp_name(p1)) < p.get_local_index(local_pp_name(p2));
         });
 }
 

tests/lean/run/section3.lean

@@ -0,0 +1,6 @@
+section
+  parameter (A : Type)
+  definition foo := A
+  theorem bar {X : Type} {A : X} : foo :=
+  sorry
+end