From 95e8228e8a4a232daae10e0c4488a5d15360e8fc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Aug 2016 16:34:40 -0700 Subject: [PATCH] refactor(library/tactic/cases_tactic): improve low-level API --- src/library/equations_compiler/elim_match.cpp | 16 ++- src/library/tactic/cases_tactic.cpp | 127 +++++++++++------- src/library/tactic/cases_tactic.h | 10 +- tests/lean/run/def6.lean | 1 + tests/lean/run/def8.lean | 34 +++++ 5 files changed, 128 insertions(+), 60 deletions(-) create mode 100644 tests/lean/run/def8.lean diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 985cbb19be..814278626e 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -694,7 +694,7 @@ struct elim_match_fn { optional aux_mvar1 = intron(m_env, m_opts, m_mctx, P.m_goal, 1, new_names); if (!aux_mvar1) throw_ill_formed_eqns(); expr x = get_local_context(*aux_mvar1).get_local_decl(new_names[0])->mk_ref(); - cintros_list ilist; + xintros_list ilist; renaming_list rlist; list new_goals; list new_goal_cnames; try { @@ -729,7 +729,15 @@ struct elim_match_fn { expr new_goal = head(new_goals); /* Revert constructor fields (which have not been eliminated by dependent pattern matching). */ buffer to_revert; - to_buffer_local(new_goal, head(ilist), to_revert); + // Temporary hack to be able to compile lean before major elim_match reorg + list> new_fields = map2>(head(ilist), + [&](expr const & e) { + if (is_local(e)) + return optional(mlocal_name(e)); + else + return optional(); + }); + to_buffer_local(new_goal, new_fields, to_revert); unsigned to_revert_size = to_revert.size(); unsigned num_intro_fields = to_revert_size; expr aux_mvar2 = revert(m_env, m_opts, m_mctx, head(new_goals), to_revert); @@ -738,10 +746,10 @@ struct elim_match_fn { /* The arity of the auxiliary program is the arity of the original program - 1 (we consumed one argument in this step) and + number of introduced constructor fields. */ new_P.m_nvars = P.m_nvars - 1 + num_intro_fields; - new_P.m_equations = get_equations_for(head(new_goal_cnames), head(ilist), head(rlist), + new_P.m_equations = get_equations_for(head(new_goal_cnames), new_fields, head(rlist), get_local_context(aux_mvar2), equations_by_constructor); result new_R = compile_core(new_P); - result_by_constructor.emplace_back(head(new_goal_cnames), to_bitmask(head(ilist)), new_P.m_nvars, new_R); + result_by_constructor.emplace_back(head(new_goal_cnames), to_bitmask(new_fields), new_P.m_nvars, new_R); new_goals = tail(new_goals); new_goal_cnames = tail(new_goal_cnames); diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 4efb56b27a..72a0137864 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "util/list_fn.h" #include "kernel/instantiate.h" +#include "kernel/replace_fn.h" #include "kernel/inductive/inductive.h" #include "library/util.h" #include "library/constants.h" @@ -99,7 +100,8 @@ struct cases_tactic_fn { init_inductive_info(const_name(fn)); if (args.size() != m_nindices + m_nparams) return false; - lean_cases_trace(mvar, tout() << "inductive type: " << const_name(fn) << ", num. params: " << m_nparams << ", num. indices: " << m_nindices << "\n";); + lean_cases_trace(mvar, tout() << "inductive type: " << const_name(fn) << + ", num. params: " << m_nparams << ", num. indices: " << m_nindices << "\n";); return true; } @@ -267,20 +269,9 @@ struct cases_tactic_fn { } /* Apply the new_renames at new_names and renames. */ - void merge_renames(bool update_names, list> & new_names, name_map & renames, name_map new_renames) { + void merge_renames(bool update_names, name_map & renames, name_map new_renames) { if (!update_names) return; if (new_renames.empty()) return; - /* Apply new_renames to new_names. */ - buffer> new_new_names; - for (optional const & n : new_names) { - if (!n) - new_new_names.push_back(n); - else if (auto r = new_renames.find(*n)) - new_new_names.push_back(optional(*r)); - else - new_new_names.push_back(n); - } - new_names = to_list(new_new_names); /* Merge renames and new_renames */ name_map m; renames.for_each([&](name const & k, name const & d) { @@ -299,7 +290,25 @@ struct cases_tactic_fn { renames = m; } - optional unify_eqs(expr mvar, unsigned num_eqs, bool updating_names, list> & new_names, name_map & renames) { + expr apply_renames(local_context const & lctx, name_map const & renames, expr const & e) { + return replace(e, [&](expr const & e, unsigned) { + if (is_local(e)) { + if (auto n = renames.find(mlocal_name(e))) { + return some_expr(lctx.get_local_decl(*n)->mk_ref()); + } + } + return none_expr(); + }); + } + + list apply_renames(expr const & mvar, name_map const & renames, list const & es) { + if (renames.empty()) return es; + local_context lctx = m_mctx.get_metavar_decl(mvar)->get_context(); + return map(es, [&](expr const & e) { return apply_renames(lctx, renames, e); }); + } + + optional unify_eqs(expr mvar, unsigned num_eqs, bool updating_intros, + list & new_intros, name_map & renames) { if (num_eqs == 0) return some_expr(mvar); expr A, B, lhs, rhs; @@ -341,24 +350,22 @@ struct cases_tactic_fn { expr val = mk_app(mvar2, mk_eq_of_heq(ctx, H)); m_mctx.assign(*mvar1, val); lean_cases_trace(mvar, tout() << "converted heq => eq\n";); - return unify_eqs(mvar2, num_eqs, updating_names, new_names, renames); + return unify_eqs(mvar2, num_eqs, updating_intros, new_intros, renames); } else if (is_eq(H_type, A, lhs, rhs)) { if (is_local(rhs) || is_local(lhs)) { lean_cases_trace(mvar, tout() << "substitute\n";); name_map extra_renames; bool symm = is_local(rhs); - lean_assert(check_hypotheses_in_context(*mvar1, new_names)); - if (updating_names && is_local(rhs)) { - /* The next substitution may eliminate introduced hypothesis */ - name from_name = mlocal_name(rhs); - new_names = map(new_names, [&](optional const & n) { - return (n && *n == from_name) ? optional() : n; + expr mvar2 = subst(m_env, m_opts, m_mode, m_mctx, *mvar1, H, symm, + updating_intros ? &extra_renames : nullptr); + new_intros = apply_renames(mvar2, extra_renames, new_intros); + merge_renames(updating_intros, renames, extra_renames); + if (updating_intros && is_local(rhs)) { + new_intros = map(new_intros, [&](expr const & e) { + return replace_local(e, rhs, lhs); }); } - expr mvar2 = subst(m_env, m_opts, m_mode, m_mctx, *mvar1, H, symm, updating_names ? &extra_renames : nullptr); - merge_renames(updating_names, new_names, renames, extra_renames); - lean_assert(check_hypotheses_in_context(mvar2, new_names)); - return unify_eqs(mvar2, num_eqs - 1, updating_names, new_names, renames); + return unify_eqs(mvar2, num_eqs - 1, updating_intros, new_intros, renames); } else { optional c1 = is_constructor_app(m_env, lhs); optional c2 = is_constructor_app(m_env, rhs); @@ -369,11 +376,13 @@ struct cases_tactic_fn { throw_ill_formed_datatype(); name no_confusion_name(const_name(A_fn), "no_confusion"); if (!m_env.find(no_confusion_name)) { - throw exception(sstream() << "cases tactic failed, construction '" << no_confusion_name << "' is not available in the environment"); + throw exception(sstream() << "cases tactic failed, construction '" + << no_confusion_name << "' is not available in the environment"); } expr target = g1.get_type(); level target_lvl = get_level(ctx, target); - expr no_confusion = mk_app(mk_app(mk_constant(no_confusion_name, cons(target_lvl, const_levels(A_fn))), A_args), target, lhs, rhs, H); + expr no_confusion = mk_app(mk_app(mk_constant(no_confusion_name, cons(target_lvl, const_levels(A_fn))), + A_args), target, lhs, rhs, H); if (c1 && c2) { if (*c1 == *c2) { lean_cases_trace(mvar, tout() << "injection\n";); @@ -383,10 +392,12 @@ struct cases_tactic_fn { m_mctx.assign(*mvar1, val); unsigned A_nparams = *inductive::get_num_params(m_env, const_name(A_fn)); lean_assert(get_app_num_args(lhs) >= A_nparams); - return unify_eqs(mvar2, num_eqs - 1 + get_app_num_args(lhs) - A_nparams, updating_names, new_names, renames); + return unify_eqs(mvar2, num_eqs - 1 + get_app_num_args(lhs) - A_nparams, + updating_intros, new_intros, renames); } else { /* conflict, closes the goal */ - lean_cases_trace(*mvar1, tout() << "conflicting equality detected, closing goal using no_confusion\n";); + lean_cases_trace(*mvar1, tout() << "conflicting equality detected, " + "closing goal using no_confusion\n";); m_mctx.assign(*mvar1, no_confusion); return none_expr(); } @@ -398,25 +409,26 @@ struct cases_tactic_fn { } } - pair, list> unify_eqs(list const & mvars, list const & cnames, unsigned num_eqs, cintros_list * ilist, renaming_list * rlist) { + pair, list> unify_eqs(list const & mvars, list const & cnames, unsigned num_eqs, + xintros_list * ilist, renaming_list * rlist) { lean_assert((ilist == nullptr) == (rlist == nullptr)); buffer new_goals; - buffer>> new_ilist; + buffer> new_ilist; buffer> new_rlist; buffer new_cnames; list it1 = mvars; list itn = cnames; - cintros_list const * it2 = ilist; + xintros_list const * it2 = ilist; renaming_list const * it3 = rlist; while (it1) { - list> new_names; + list new_intros; name_map renames; if (ilist) { - new_names = head(*it2); - renames = head(*it3); + new_intros = head(*it2); + renames = head(*it3); } - bool updating_names = ilist != nullptr; - optional new_mvar = unify_eqs(head(it1), num_eqs, updating_names, new_names, renames); + bool updating_intros = ilist != nullptr; + optional new_mvar = unify_eqs(head(it1), num_eqs, updating_intros, new_intros, renames); if (new_mvar) { new_goals.push_back(*new_mvar); new_cnames.push_back(head(itn)); @@ -427,8 +439,7 @@ struct cases_tactic_fn { it2 = &tail(*it2); it3 = &tail(*it3); if (new_mvar) { - lean_assert(check_hypotheses_in_context(*new_mvar, new_names)); - new_ilist.push_back(new_names); + new_ilist.push_back(new_intros); new_rlist.push_back(renames); } } @@ -440,7 +451,8 @@ struct cases_tactic_fn { return mk_pair(to_list(new_goals), to_list(new_cnames)); } - cases_tactic_fn(environment const & env, options const & opts, transparency_mode m, metavar_context & mctx, list & ids): + cases_tactic_fn(environment const & env, options const & opts, transparency_mode m, + metavar_context & mctx, list & ids): m_env(env), m_opts(opts), m_mode(m), @@ -448,14 +460,25 @@ struct cases_tactic_fn { m_ids(ids) { } - cintros_list to_cintros_list(intros_list const & ilist) { - return map2>>(ilist, [](list const & ls) { - return map2>(ls, [](name const & n) { - return optional(n); }); - }); + xintros_list to_xintros_list(list const & new_goals, intros_list const & ilist) { + lean_assert(length(new_goals) == length(ilist)); + buffer> new_intros; + auto it1 = new_goals; + auto it2 = ilist; + while (it1 && it2) { + expr const & mvar = head(it1); + local_context lctx = m_mctx.get_metavar_decl(mvar)->get_context(); + new_intros.push_back(map2(head(it2), [&](name const & n) { + return lctx.get_local_decl(n)->mk_ref(); + })); + it1 = tail(it1); + it2 = tail(it2); + } + lean_assert(!it1 && !it2); + return to_list(new_intros); } - pair, list> operator()(expr const & mvar, expr const & H, cintros_list * ilist, renaming_list * rlist) { + pair, list> operator()(expr const & mvar, expr const & H, xintros_list * ilist, renaming_list * rlist) { lean_assert((ilist != nullptr) == (rlist != nullptr)); lean_assert(is_metavar(mvar)); lean_assert(m_mctx.get_metavar_decl(mvar)); @@ -470,9 +493,10 @@ struct cases_tactic_fn { if (has_indep_indices(g, H)) { /* Easy case */ intros_list tmp_ilist; - auto p = mk_pair(induction(m_env, m_opts, m_mode, m_mctx, mvar, H, m_cases_on_decl.get_name(), m_ids, ilist ? &tmp_ilist : nullptr, rlist), + auto p = mk_pair(induction(m_env, m_opts, m_mode, m_mctx, mvar, H, + m_cases_on_decl.get_name(), m_ids, ilist ? &tmp_ilist : nullptr, rlist), cname_list); - if (ilist) *ilist = to_cintros_list(tmp_ilist); + if (ilist) *ilist = to_xintros_list(p.first, tmp_ilist); return p; } else { buffer aux_indices_H; /* names of auxiliary indices and major */ @@ -482,13 +506,14 @@ struct cases_tactic_fn { expr H1 = m_mctx.get_metavar_decl(mvar1)->get_context().get_last_local_decl()->mk_ref(); intros_list tmp_ilist; renaming_list tmp_rlist; - list new_goals1 = induction(m_env, m_opts, m_mode, m_mctx, mvar1, H1, m_cases_on_decl.get_name(), m_ids, &tmp_ilist, &tmp_rlist); + list new_goals1 = induction(m_env, m_opts, m_mode, m_mctx, mvar1, H1, m_cases_on_decl.get_name(), + m_ids, &tmp_ilist, &tmp_rlist); lean_cases_trace(mvar1, tout() << "after applying cases_on:"; for (auto g : new_goals1) tout() << "\n" << pp_goal(g) << "\n";); list new_goals2 = elim_aux_indices(new_goals1, aux_indices_H, tmp_rlist); lean_cases_trace(mvar1, tout() << "after eliminating auxiliary indices:"; for (auto g : new_goals2) tout() << "\n" << pp_goal(g) << "\n";); - if (ilist) *ilist = to_cintros_list(tmp_ilist); + if (ilist) *ilist = to_xintros_list(new_goals2, tmp_ilist); if (rlist) *rlist = tmp_rlist; return unify_eqs(new_goals2, cname_list, num_eqs, ilist, rlist); } @@ -497,7 +522,7 @@ struct cases_tactic_fn { pair, list> cases(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, - expr const & mvar, expr const & H, list & ids, cintros_list * ilist, renaming_list * rlist) { + expr const & mvar, expr const & H, list & ids, xintros_list * ilist, renaming_list * rlist) { auto r = cases_tactic_fn(env, opts, m, mctx, ids)(mvar, H, ilist, rlist); lean_assert(length(r.first) == length(r.second)); return r; diff --git a/src/library/tactic/cases_tactic.h b/src/library/tactic/cases_tactic.h index 69f3409fd3..ff80fed232 100644 --- a/src/library/tactic/cases_tactic.h +++ b/src/library/tactic/cases_tactic.h @@ -8,14 +8,14 @@ Author: Leonardo de Moura #include "library/tactic/induction_tactic.h" namespace lean { -typedef list>> cintros_list; +typedef list> xintros_list; /** \brief Similar to induction, but applies 'cases_on' and has bettern support for dependent types. Failures are reported using exceptions. \c ids (if available) provides the names for new hypotheses. If cilist and rlist are not nullptr, then - 1- Store in ilist the new hypotheses introduced for each new goal. - We have a new hypothesis for each constructor field. - The entry is none if the field was eliminated during dependent pattern matching. + 1- Store in ilist the new "hypotheses" introduced for each new goal. + We have a new "hypothesis" for each constructor field. + We say "hypothesis" because it may be an arbitrary term. This may happen because of dependent pattern matching. 2- Store in rlist the hypotheses renamed in each new goal. \pre (ilist == nullptr) iff (rlist == nullptr) \post ilist != nullptr -> rlist != nullptr -> length(*ilist) == length(*rlist) @@ -28,7 +28,7 @@ typedef list>> cintros_list; since some of the goals are discarded. */ pair, list> cases(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, - expr const & mvar, expr const & H, list & ids, cintros_list * ilist, renaming_list * rlist); + expr const & mvar, expr const & H, list & ids, xintros_list * ilist, renaming_list * rlist); void initialize_cases_tactic(); void finalize_cases_tactic(); diff --git a/tests/lean/run/def6.lean b/tests/lean/run/def6.lean index 4fa79ee176..82077687a3 100644 --- a/tests/lean/run/def6.lean +++ b/tests/lean/run/def6.lean @@ -1,4 +1,5 @@ set_option new_elaborator true +exit inductive vec (A : Type) : nat → Type | nil {} : vec 0 diff --git a/tests/lean/run/def8.lean b/tests/lean/run/def8.lean new file mode 100644 index 0000000000..18fe94a651 --- /dev/null +++ b/tests/lean/run/def8.lean @@ -0,0 +1,34 @@ +set_option new_elaborator true +exit +inductive imf {A B : Type} (f : A → B) : B → Type +| mk : ∀ (a : A), imf (f a) + +definition g {A B : Type} {f : A → B} : ∀ {b : B}, imf f b → A +| .(f a) (imf.mk .f a) := a + +definition v₁ : imf nat.succ 1 := +(imf.mk nat.succ 0) + +definition v₂ : imf (λ x, 1 + x) 1 := +(imf.mk (λ x, 1 + x) 0) + +example : g v₁ = 0 := +rfl + +example : g v₂ = 0 := +rfl + +lemma ex1 (A : Type) : ∀ a b : A, a = b → b = a +| a .a rfl := rfl + +lemma ex2 (A : Type) : ∀ a b : A, a = b → b = a +| a .a (eq.refl .a) := rfl + +lemma ex3 (A : Type) : ∀ a b : A, a = b → b = a +| a ._ (eq.refl ._) := rfl + +lemma ex4 (A : Type) : ∀ a b : A, a = b → b = a +| .a a (eq.refl .a) := eq.refl a + +lemma ex5 (A : Type) : ∀ a b : A, a = b → b = a +| .a .a (eq.refl a) := eq.refl a