michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/scope): bug when abstracting inductive declaration in the end of a section

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-02 13:46:16 -07:00
parent 2a101657c8
commit 9b6b162a7c
2 changed files with 38 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/scope.cpp
View file

@ -296,15 +296,13 @@ static expr update_inductive_type(expr const & t, unsigned old_num_params, level
expr T = get_app_args(t, args);
lean_assert(old_num_params <= args.size());
lean_assert(is_constant(T));
expr new_T = update_constant(T, append(const_levels(T), extra_ls));
expr new_T = update_constant(T, append(extra_ls, const_levels(T)));
buffer<expr> new_args;
for (unsigned i = 0; i < old_num_params; i++)
new_args.push_back(args[i]);
new_args.append(extra_params);
for (unsigned i = old_num_params; i < args.size(); i++)
new_args.push_back(args[i]);
new_args.append(args);
lean_assert(new_args.size() == args.size() + extra_params.size());
return mk_app(new_T, new_args);
expr r = mk_app(new_T, new_args);
return r;
}
// Add the extra universe levels and parameters to every occurrence in t of an inductive datatype in \c decls.
@ -347,7 +345,7 @@ environment add_inductive(environment env,
levels extra_lvls = map2<level>(extra_ls, [](name const & n) { return mk_param_univ(n); });
dependencies extra_ps = ctx.mk_var_deps();
unsigned new_num_params = num_params + extra_ps.size();
level_param_names new_ls = append(level_params, extra_ls);
level_param_names new_ls = append(extra_ls, level_params);
// create Pi(extra_ps, T) where T are the types in the declarations
buffer<inductive_decl> new_decls;
for (auto const & d : tmp_decls) {

33
tests/lua/sect9.lua Normal file
View file

@ -0,0 +1,33 @@
local env = environment()
env = env:begin_section_scope()
env = env:begin_section_scope()
local nat = Const("nat")
env = add_inductive(env,
"nat", Type,
"zero", nat,
"succ", mk_arrow(nat, nat))
local zero = Const("zero")
local succ = Const("succ")
local one = succ(zero)
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 l1 = mk_param_univ("l1")
local D = Const("D", {l1})
local n = Local("n", nat)
env = add_inductive(env,
"D", {l1}, 1, mk_arrow(nat, nat, mk_sort(max_univ(l1, l, 1))),
"mk1", Pi(n, mk_arrow(A, D(n, one))),
"mk0", Pi(n, mk_arrow(A, A, D(n, zero))))
print(env:find("D_rec"):type())
env = env:end_scope()
env = env:end_scope()
print(env:find("D_rec"):type())
local l = mk_param_univ("l")
local A = Local("A", mk_sort(l))
local D = Const("D", {l, l1})
print(env:find("mk1"):type())
assert(env:find("mk1"):type() == Pi({A, n}, mk_arrow(A, D(A, n, one))))