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

fix(compiler/simp_pr1_rec): make sure simplification support reflexive datatypes

Browse source 
Example:

inductive tree (A : Type) :=
| leaf : A → tree A
| node : (nat → tree A) → tree A

definition tree_fn : tree nat → nat
| (tree.leaf a) := a
| (tree.node f) := tree_fn (f 0)
This commit is contained in:
Leonardo de Moura 2016-05-03 18:22:12 -07:00
parent 19c87dd711
commit 3dac0f6bb6
1 changed files with 20 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/compiler/simp_pr1_rec.cpp
View file

@ -30,11 +30,17 @@ class simp_pr1_rec_fn : public compiler_step_visitor {
}
bool is_rec_arg(expr const & e) {
if (!is_local(e))
buffer<expr> e_args;
expr const & fn = get_app_args(e, e_args);
if (!is_local(fn))
return false;
for (unsigned i = 0; i < minor_ctx.size(); i++) {
if (minor_is_rec_arg[i] && mlocal_name(minor_ctx[i]) == mlocal_name(e))
if (minor_is_rec_arg[i] && mlocal_name(minor_ctx[i]) == mlocal_name(fn)) {
/* make sure arguments contain only valid occurrences */
for (expr const & e_arg : e_args)
visit(e_arg);
return true;
}
}
return false;
}
@ -54,8 +60,9 @@ class simp_pr1_rec_fn : public compiler_step_visitor {
}
virtual expr visit_local(expr const & e) {
if (is_rec_arg(e))
if (is_rec_arg(e)) {
throw failed();
}
return replace_visitor::visit_local(e);
}
};
@ -125,19 +132,27 @@ class simp_pr1_rec_fn : public compiler_step_visitor {
for (unsigned k = 0; k < minor_ctx.size(); k++) {
if (minor_is_rec_arg[k]) {
expr type = ctx().whnf(ctx().infer(minor_ctx[k]));
type_context::tmp_locals locals(ctx());
while (is_pi(type)) {
expr l = locals.push_local(binding_name(type), binding_domain(type), binding_info(type));
type = instantiate(binding_body(type), l);
type = ctx().whnf(type);
}
buffer<expr> type_args;
expr type_fn = get_app_args(type, type_args);
if (!is_constant(type_fn) || const_name(type_fn) != get_prod_name() || type_args.size() != 2) {
return none_expr();
}
minor_ctx[k] = update_mlocal(minor_ctx[k], type_args[0]);
minor_ctx[k] = update_mlocal(minor_ctx[k], locals.mk_pi(type_args[0]));
}
}
// Step 2
buffer<expr> minor_body_args;
expr minor_body_fn = get_app_args(minor_body, minor_body_args);
if (!is_constant(minor_body_fn) || const_name(minor_body_fn) != get_prod_mk_name() || minor_body_args.size() != 4) {
if (!is_constant(minor_body_fn) ||
const_name(minor_body_fn) != get_prod_mk_name() ||
minor_body_args.size() != 4) {
return none_expr();
}
minor_body = minor_body_args[2];