From 936ca80b9bdf9052c99845aa9513f837ccf65e58 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Jun 2014 11:04:34 -0700 Subject: [PATCH] fix(library/scope): bug in add_definition Signed-off-by: Leonardo de Moura --- src/library/scope.cpp | 4 ++-- tests/lua/sect6.lua | 27 +++++++++++++++++++++++++++ 2 files changed, 29 insertions(+), 2 deletions(-) create mode 100644 tests/lua/sect6.lua diff --git a/src/library/scope.cpp b/src/library/scope.cpp index b4602b891..f5242ed30 100644 --- a/src/library/scope.cpp +++ b/src/library/scope.cpp @@ -184,10 +184,10 @@ public: if (d.is_definition()) { declaration new_d = mk_definition(d.get_name(), new_ls, new_type, new_value, d.is_opaque(), d.get_weight(), d.get_module_idx(), d.use_conv_opt()); - m_env = module::add(m_env, check(m_env, new_d)); + m_env = add(m_env, check(m_env, new_d)); } else { declaration new_d = mk_theorem(d.get_name(), new_ls, new_type, new_value); - m_env = module::add(m_env, check(m_env, new_d)); + m_env = add(m_env, check(m_env, new_d)); } } }; diff --git a/tests/lua/sect6.lua b/tests/lua/sect6.lua new file mode 100644 index 000000000..83b1cf29c --- /dev/null +++ b/tests/lua/sect6.lua @@ -0,0 +1,27 @@ +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 = add_decl(env, mk_definition("id", mk_arrow(A, A), Fun(a, a))) +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)))) +print(env:find("id"):type()) +print(env:find("id"):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))))