From e56307f006db6ed59d1905558531629bb5742d9f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Jun 2014 10:43:28 -0700 Subject: [PATCH] fix(library/scope): bug in end_scope procedure Signed-off-by: Leonardo de Moura --- src/library/scope.cpp | 3 +-- tests/lua/sect5.lua | 26 ++++++++++++++++++++++++++ 2 files changed, 27 insertions(+), 2 deletions(-) create mode 100644 tests/lua/sect5.lua diff --git a/src/library/scope.cpp b/src/library/scope.cpp index 8cde445b3..b4602b891 100644 --- a/src/library/scope.cpp +++ b/src/library/scope.cpp @@ -413,8 +413,7 @@ environment end(environment const & env) { (*p)(ctx); ctx.clear_deps(); } - ext.m_sections = tail(ext.m_sections); - return update(ctx.env(), ext); + return ctx.env(); }} lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/tests/lua/sect5.lua b/tests/lua/sect5.lua new file mode 100644 index 000000000..28869005b --- /dev/null +++ b/tests/lua/sect5.lua @@ -0,0 +1,26 @@ +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)) +env = env:add(check(env, mk_var_decl("B", mk_sort(l))), binder_info(true)) +local A = Const("A") +local list = Const("list") +env = add_inductive(env, + "list", mk_sort(max_univ(l, 1)), + "nil", list, + "cons", mk_arrow(A, list, list)) +print(env:find("list_rec"):type()) +assert(env:find("cons"):type() == mk_arrow(A, list, list)) +env = env:end_scope() +print(env:find("list_rec"):type()) +print(env:find("cons"):type()) +local l = mk_param_univ("l") +local A = Local("A", mk_sort(l)) +local list = Const("list", {l}) +assert(env:find("cons"):type() == Pi({A}, mk_arrow(A, list(A), list(A)))) +env = env:end_scope() + +print(env:find("list_rec"):type()) +print(env:find("cons"):type())