feat(library/private): preserve 'hidden/private name => user name' map when section is closed

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

src/library/private.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "util/hash.h"
 #include "library/private.h"
 #include "library/module.h"
+#include "library/scope.h"
 #include "library/kernel_bindings.h"
 
 namespace lean {
@@ -46,6 +47,15 @@ std::pair<environment, name> add_private_name(environment const & env, name cons
     ext.m_counter++;
     environment new_env = update(env, ext);
     new_env = module::add(new_env, g_prv_key, [=](serializer & s) { s << n << r; });
+    if (scope::has_open_sections(new_env)) {
+        new_env = scope::add(new_env, [=](scope::abstraction_context & ctx) {
+                environment env = ctx.env();
+                private_ext ext = get_extension(env);
+                ext.m_inv_map.insert(r, n);
+                ext.m_counter++;
+                ctx.update_env(update(env, ext));
+            });
+    }
     return mk_pair(new_env, r);
 }
 

src/library/scope.cpp

@@ -311,6 +311,10 @@ environment end(environment const & env) {
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
+bool has_open_sections(environment const & env) {
+    return !is_nil(get_extension(env).m_sections);
+}
+
 name const & get_namespace(environment const & env) {
     scope_ext const & ext = get_extension(env);
     if (is_nil(ext.m_namespaces))

src/library/scope.h

@@ -76,6 +76,9 @@ environment begin_namespace(environment const & env, char const * n);
 */
 environment end(environment const & env);
 
+/** \brief Return true iff the given environment has open sections. */
+bool has_open_sections(environment const & env);
+
 /**
    \brief Return the current namespace for \c env. The namespace is composed by the sequence
    of names provided to \c begin_namespace_scope.

tests/lua/sect3.lua

@@ -0,0 +1,26 @@
+local env = environment()
+env = env:begin_section_scope()
+env = env:add_global_level("l")
+local l = mk_global_univ("l")
+env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true))
+local A = Const("A")
+env = add_decl(env, mk_var_decl("R", mk_arrow(A, A, Bool)))
+local R = Const("R")
+local a = Local("a", A)
+env = add_decl(env, mk_definition("reflexive", Bool, Pi(a, R(a, a))))
+env, id_prv = add_private_name(env, "id")
+env = add_decl(env, mk_definition(id_prv, mk_arrow(A, A), Fun(a, a)))
+assert(user_to_hidden_name(env, "id") == id_prv)
+assert(hidden_to_user_name(env, id_prv) == name("id"))
+env = env:end_scope()
+local A1 = Local("A", mk_sort(mk_param_univ("l")))
+local R1 = Local("R", mk_arrow(A1, A1, Bool))
+local a1 = Local("a", A1)
+print(env:find("reflexive"):type())
+print(env:find("reflexive"):value())
+assert(env:find("reflexive"):type() == Pi({A1, R1}, Bool))
+assert(env:find("reflexive"):value() == Fun({A1, R1}, Pi(a1, R1(a1, a1))))
+assert(not user_to_hidden_name(env, "id"))
+assert(hidden_to_user_name(env, id_prv) == name("id"))
+print(env:find(id_prv):type())
+print(env:find(id_prv):value())