diff --git a/src/library/compiler/inliner.cpp b/src/library/compiler/inliner.cpp index e387429a6b..acc98fcb50 100644 --- a/src/library/compiler/inliner.cpp +++ b/src/library/compiler/inliner.cpp @@ -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); } diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp index 145f2c0fa5..600e407b38 100644 --- a/src/library/compiler/preprocess.cpp +++ b/src/library/compiler/preprocess.cpp @@ -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)); diff --git a/tests/lean/run/inliner_bug.lean b/tests/lean/run/inliner_bug.lean new file mode 100644 index 0000000000..e939a2132b --- /dev/null +++ b/tests/lean/run/inliner_bug.lean @@ -0,0 +1,4 @@ +@[inline] def g (n : nat) : nat := +nat.rec_on n 0 (λ m r, r + 2) + +vm_eval g 10