fix(library/private): bug when preserving private names at end_section

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

src/library/private.cpp

@@ -36,6 +36,22 @@ static environment update(environment const & env, private_ext const & ext) {
 static name g_private("private");
 static std::string g_prv_key("prv");
 
+// Make sure the mapping "hidden-name r ==> user-name n" is preserved when we close sections and
+// export .olean files.
+static environment preserve_private_data(environment const & env, name const & r, name const & n) {
+    if (scope::has_open_sections(env)) {
+        return scope::add(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(preserve_private_data(update(env, ext), r, n));
+            });
+    } else {
+        return module::add(env, g_prv_key, [=](serializer & s) { s << n << r; });
+    }
+}
+
 std::pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
     private_ext ext = get_extension(env);
     unsigned h      = hash(n.hash(), ext.m_counter);
@@ -46,16 +62,7 @@ std::pair<environment, name> add_private_name(environment const & env, name cons
     ext.m_inv_map.insert(r, n);
     ext.m_counter++;
     environment new_env = update(env, ext);
-    new_env = module::add(new_env, g_prv_key, [=](serializer & s) { s << n << r; });
+    new_env = preserve_private_data(new_env, r, n);
-    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);
 }
 

tests/lua/sect7.lua

@@ -0,0 +1,42 @@
+local env = environment()
+env = env:begin_section_scope()
+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())
+env = env:end_scope()
+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())
+env:export("sect7_mod.olean")
+local env2 = import_modules("sect7_mod")
+assert(hidden_to_user_name(env2, id_prv) == name("id"))
+print(env2:find(id_prv):type())
+assert(env2:find(id_prv):type() == env:find(id_prv):type())
+assert(env2:find(id_prv):value() == env:find(id_prv):value())