From b6d2328c1d49da43fcba6320b520e82033547de4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Jun 2014 14:06:27 -0700 Subject: [PATCH] fix(library/scope): make sure local levels are added in the beginning of the universe parameter list The idea is to make sure it is consistent with the behavior used for regular local parameters. Signed-off-by: Leonardo de Moura --- src/library/scope.cpp | 4 ++-- tests/lua/sect1b.lua | 12 ++++++++++++ 2 files changed, 14 insertions(+), 2 deletions(-) create mode 100644 tests/lua/sect1b.lua diff --git a/src/library/scope.cpp b/src/library/scope.cpp index dcbc92b96..73b9fb4c3 100644 --- a/src/library/scope.cpp +++ b/src/library/scope.cpp @@ -90,7 +90,7 @@ public: if (info.m_local) { return some_expr(update_constant(e, levels())); } else { - return some_expr(mk_app(update_constant(e, append(const_levels(e), info.m_levels)), info.m_var_deps)); + return some_expr(mk_app(update_constant(e, append(info.m_levels, const_levels(e))), info.m_var_deps)); } } else { levels new_ls = map(const_levels(e), [&](level const & l) { return convert(l); }); @@ -176,7 +176,7 @@ public: expr new_type = convert(d.get_type()); expr new_value = convert(d.get_value()); level_param_names level_deps = mk_level_deps(); - level_param_names new_ls = append(d.get_params(), level_deps); + level_param_names new_ls = append(level_deps, d.get_params()); dependencies var_deps = mk_var_deps(); new_type = Pi(new_type, var_deps); new_value = Fun(new_value, var_deps); diff --git a/tests/lua/sect1b.lua b/tests/lua/sect1b.lua new file mode 100644 index 000000000..68d6f8c9e --- /dev/null +++ b/tests/lua/sect1b.lua @@ -0,0 +1,12 @@ +local env = environment() +env = env:begin_section_scope() +env = env:add_global_level("l") +local l = mk_global_univ("l") +local l1 = mk_param_univ("l1") +env = add_decl(env, mk_definition("A", {l1}, mk_sort(max_univ(l, l1)+1), mk_sort(max_univ(l, l1)))) +env = env:end_scope() +local ls = env:find("A"):univ_params() +assert(#ls == 2) +print(ls:head()) +assert(ls:head() == name("l")) +assert(ls:tail():head() == name("l1"))