From 6ee272477ab26577d6b8d631884e9f670c69e878 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Jun 2014 11:32:14 -0700 Subject: [PATCH] fix(library/private): bug when preserving private names at end_section Signed-off-by: Leonardo de Moura --- src/library/private.cpp | 27 ++++++++++++++++---------- tests/lua/sect7.lua | 42 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 59 insertions(+), 10 deletions(-) create mode 100644 tests/lua/sect7.lua diff --git a/src/library/private.cpp b/src/library/private.cpp index 508c29f53..d85dbe985 100644 --- a/src/library/private.cpp +++ b/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 add_private_name(environment const & env, name const & n, optional const & extra_hash) { private_ext ext = get_extension(env); unsigned h = hash(n.hash(), ext.m_counter); @@ -46,16 +62,7 @@ std::pair 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; }); - 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)); - }); - } + new_env = preserve_private_data(new_env, r, n); return mk_pair(new_env, r); } diff --git a/tests/lua/sect7.lua b/tests/lua/sect7.lua new file mode 100644 index 000000000..356300ee8 --- /dev/null +++ b/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())