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

fix(library/compiler): move inliner to the beginning

Browse source 
Reason: the inliner may introduce recursors, non eta-expanded terms,
etc. Before this commit, it was "undoing" previous compilation steps.
This commit is contained in:
Leonardo de Moura 2016-11-08 16:14:01 -08:00
parent c6558f8af5
commit 6ce00a9b45
3 changed files with 9 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/compiler/inliner.cpp
View file

@ -90,6 +90,8 @@ class inline_simple_definitions_fn : public compiler_step_visitor {
} else {
major_idx = *inductive::get_elim_major_idx(env(), rec_name);
}
if (major_idx >= args.size())
return e;
expr major = beta_reduce(args[major_idx]);
if (is_constructor_app(env(), major)) {
/* Major premise became a constructor. So, we should reduce. */
@ -138,15 +140,9 @@ class inline_simple_definitions_fn : public compiler_step_visitor {
return visit(*r);
}
/*
TODO(Leo): this is not safe here.
Reason: we may put recursors have have been eliminated in previous steps.
We need to move this code to a different place, or make sure
that we can recursors will be eliminated later
if (auto r = ctx().reduce_projection(e)) {
return visit(*r);
}
*/
return default_visit_app(e);
}

8
src/library/compiler/preprocess.cpp
View file

@ -174,6 +174,9 @@ public:
expr v = d.get_value();
lean_trace(name({"compiler", "input"}), tout() << "\n" << v << "\n";);
v = fix_tactic_eval_expr(v);
v = inline_simple_definitions(m_env, v);
lean_cond_assert("compiler", check(d, v));
lean_trace(name({"compiler", "inline"}), tout() << "\n" << v << "\n";);
v = expand_aux(m_env, v);
lean_cond_assert("compiler", check(d, v));
lean_trace(name({"compiler", "expand_aux"}), tout() << "\n" << v << "\n";);
@ -187,11 +190,6 @@ public:
v = simp_pr1_rec(m_env, v);
lean_cond_assert("compiler", check(d, v));
lean_trace(name({"compiler", "simplify_pr1"}), tout() << "\n" << v << "\n";);
v = inline_simple_definitions(m_env, v);
lean_cond_assert("compiler", check(d, v));
lean_trace(name({"compiler", "inline"}), tout() << "\n" << v << "\n";);
v = mark_comp_irrelevant_subterms(m_env, v);
lean_cond_assert("compiler", check(d, v));
v = elim_recursors(m_env, d.get_name(), v, procs);
procs.emplace_back(d.get_name(), v);
lean_cond_assert("compiler", check(d, procs.back().second));

4
tests/lean/run/inliner_bug.lean Normal file
View file

@ -0,0 +1,4 @@
@[inline] def g (n : nat) : nat :=
nat.rec_on n 0 (λ m r, r + 2)
vm_eval g 10