max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/compiler/elim_recursors): it was assuming that recursive arguments occur after non recursive ones

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-14 20:59:49 -08:00
parent 70b7a35cfe
commit fc00275636
3 changed files with 25 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/compiler/elim_recursors.cpp
View file

@ -178,9 +178,8 @@ protected:
type_context::tmp_locals minor_locals(m_ctx);
buffer<expr> minor_recs; /* "recursive calls" */
lean_assert(carity >= nparams);
unsigned num_recursive = get_num_inductive_hypotheses_for(env(), cnames[i]);
lean_assert(num_recursive <= carity - nparams);
unsigned num_nonrecursive = carity - nparams - num_recursive;
buffer<bool> rec_mask;
get_constructor_rec_arg_mask(env(), cnames[i], rec_mask);
for (unsigned j = 0; j < carity - nparams; j++) {
minor = ctx().whnf(minor);
lean_assert(is_lambda(minor));
@ -194,7 +193,7 @@ protected:
expr aux_local = aux_locals.push_local_from_binding(minor_local_type);
minor_local_type = ctx().whnf(instantiate(binding_body(minor_local_type), aux_local));
}
if (j >= num_nonrecursive) {
if (rec_mask[nparams + j]) {
/* Recursive data, we must update minor_recs */
buffer<expr> I_args;
get_app_args(minor_local_type, I_args);

16
src/library/util.cpp
View file

@ -285,8 +285,9 @@ unsigned get_constructor_idx(environment const & env, name const & n) {
lean_unreachable();
}
unsigned get_num_inductive_hypotheses_for(environment const & env, name const & n) {
unsigned get_num_inductive_hypotheses_for(environment const & env, name const & n, buffer<bool> & rec_mask) {
lean_assert(inductive::is_intro_rule(env, n));
lean_assert(rec_mask.empty());
name I_name = *inductive::is_intro_rule(env, n);
inductive::inductive_decl decl = *inductive::is_inductive_decl(env, I_name);
expr type = env.get(n).get_type();
@ -300,13 +301,26 @@ unsigned get_num_inductive_hypotheses_for(environment const & env, name const &
}
return false;
})) {
r++;
rec_mask.push_back(true);
} else {
rec_mask.push_back(false);
}
type = binding_body(type);
}
return r;
}
unsigned get_num_inductive_hypotheses_for(environment const & env, name const & n) {
buffer<bool> rec_mask;
return get_num_inductive_hypotheses_for(env, n, rec_mask);
}
void get_constructor_rec_arg_mask(environment const & env, name const & n, buffer<bool> & rec_mask) {
get_num_inductive_hypotheses_for(env, n, rec_mask);
}
expr instantiate_univ_param (expr const & e, name const & p, level const & l) {
return instantiate_univ_params(e, to_list(p), to_list(l));
}

7
src/library/util.h
View file

@ -96,6 +96,13 @@ unsigned get_constructor_idx(environment const & env, name const & n);
hypotheses. This function return then number of inductive hypotheses for the minor premise associated with
the constructor named \c n. */
unsigned get_num_inductive_hypotheses_for(environment const & env, name const & n);
/** Given a constructor \c n, store in the bitmask rec_mask[i] = true iff the i-th argument
of \c n is recursive.
\pre is_intro_rule(n) && rec_mask.empty() */
void get_constructor_rec_arg_mask(environment const & env, name const & n, buffer<bool> & rec_mask);
/** Combines get_num_inductive_hypotheses_for and get_constructor_rec_arg_mask */
unsigned get_num_inductive_hypotheses_for(environment const & env, name const & n, buffer<bool> & rec_mask);
/* Store in `rec_args` the recursive arguments of constructor application \c `e`.
The result is false if `e` is not a constructor application.