From 4ea323a2b26d3150299ccf98e79c702941c4a299 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Mar 2015 14:13:01 -0700 Subject: [PATCH] refactor(library/tactic): cleanup common pattern --- src/kernel/metavar.cpp | 5 ++ src/kernel/metavar.h | 3 ++ src/library/definitional/equations.cpp | 2 +- src/library/tactic/apply_tactic.cpp | 4 +- src/library/tactic/assert_tactic.cpp | 3 +- src/library/tactic/change_tactic.cpp | 3 +- src/library/tactic/clear_tactic.cpp | 3 +- src/library/tactic/exact_tactic.cpp | 4 +- src/library/tactic/generalize_tactic.cpp | 3 +- src/library/tactic/goal.cpp | 6 +++ src/library/tactic/goal.h | 2 + src/library/tactic/inversion_tactic.cpp | 68 +++++++++++------------- src/library/tactic/revert_tactic.cpp | 3 +- src/library/tactic/rewrite_tactic.cpp | 16 +++--- src/library/tactic/tactic.cpp | 8 +-- 15 files changed, 66 insertions(+), 67 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 1724ba7a5..61d052116 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "kernel/level.h" #include "kernel/cache_stack.h" #include "kernel/expr_cache.h" +#include "kernel/abstract.h" #ifndef LEAN_INSTANTIATE_METAVARS_CACHE_CAPACITY #define LEAN_INSTANTIATE_METAVARS_CACHE_CAPACITY 1024*8 @@ -58,6 +59,10 @@ optional substitution::get_level(name const & m) const { return it ? some_level(*it) : none_level(); } +void substitution::assign(expr const & mvar, buffer const & locals, expr const & v, justification const & j) { + assign(mlocal_name(mvar), Fun(locals, v), j); +} + void substitution::assign(name const & m, expr const & t, justification const & j) { lean_assert(closed(t)); m_expr_subst.insert(m, t); diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index 2be50bef4..619e5b3bb 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -60,6 +60,9 @@ public: bool is_expr_assigned(name const & m) const; bool is_level_assigned(name const & m) const; + void assign(expr const & mvar, buffer const & locals, expr const & v, justification const & j); + void assign(expr const & mvar, buffer const & locals, expr const & v) { return assign(mvar, locals, v, justification()); } + void assign(name const & m, expr const & t, justification const & j); void assign(name const & m, expr const & t) { assign(m, t, justification()); } void assign(expr const & m, expr const & t, justification const & j) { assign(mlocal_name(m), t, j); } diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp index 69299fbb2..6de41e83a 100644 --- a/src/library/definitional/equations.cpp +++ b/src/library/definitional/equations.cpp @@ -925,7 +925,7 @@ class equation_compiler_fn { imps_list = tail(imps_list); rn_maps = tail(rn_maps); expr t = compile_core(new_p); - subst.assign(new_g.get_name(), new_g.abstract(t)); + assign(subst, new_g, t); } expr t = subst.instantiate_all(g.get_meta()); return some_expr(t); diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 5a92c1c6f..88ecb3bdd 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -146,9 +146,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const name_generator new_ngen(ngen); substitution new_subst = subst; expr new_e = new_subst.instantiate_all(e); - expr new_p = g.abstract(new_e); - check_has_no_local(new_p, _e, "apply"); - new_subst.assign(g.get_name(), new_p); + assign(new_subst, g, new_e); goals new_gs = tail_gs; if (subgoals_action != IgnoreSubgoals) { buffer metas; diff --git a/src/library/tactic/assert_tactic.cpp b/src/library/tactic/assert_tactic.cpp index 4d9195e4b..e52332eaf 100644 --- a/src/library/tactic/assert_tactic.cpp +++ b/src/library/tactic/assert_tactic.cpp @@ -46,9 +46,8 @@ tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e) expr new_meta2_core = mk_app(new_mvar2, hyps); expr new_meta2 = mk_app(new_meta2_core, new_local); goal new_goal2(new_meta2, g.get_type()); - expr val = g.abstract(mk_app(new_meta2_core, new_meta1)); substitution new_subst = new_s.get_subst(); - new_subst.assign(g.get_name(), val); + assign(new_subst, g, mk_app(new_meta2_core, new_meta1)); return some_proof_state(proof_state(new_s, cons(new_goal1, cons(new_goal2, tail(gs))), new_subst, ngen)); } return none_proof_state(); diff --git a/src/library/tactic/change_tactic.cpp b/src/library/tactic/change_tactic.cpp index 1a463cfd3..387241322 100644 --- a/src/library/tactic/change_tactic.cpp +++ b/src/library/tactic/change_tactic.cpp @@ -32,8 +32,7 @@ tactic change_goal_tactic(elaborate_fn const & elab, expr const & e) { if (tc->is_def_eq(t, *new_e, justification(), cs) && !cs) { expr M = g.mk_meta(ngen.next(), *new_e); goal new_g(M, *new_e); - expr val = g.abstract(M); - subst.assign(g.get_name(), val); + assign(subst, g, M); return some(proof_state(new_s, cons(new_g, tail(gs)), subst, ngen)); } else { // generate error diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp index d0288a57c..f5dfaafac 100644 --- a/src/library/tactic/clear_tactic.cpp +++ b/src/library/tactic/clear_tactic.cpp @@ -30,9 +30,8 @@ tactic clear_tactic(name const & n) { expr new_type = g.get_type(); expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); - expr val = g.abstract(new_meta); substitution new_subst = s.get_subst(); - new_subst.assign(g.get_name(), val); + assign(new_subst, g, new_meta); proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen); return some_proof_state(new_s); } else { diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp index 4e80d43b6..93e8710ad 100644 --- a/src/library/tactic/exact_tactic.cpp +++ b/src/library/tactic/exact_tactic.cpp @@ -25,10 +25,8 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type report_unassigned, enforce_type_during_elaboration)) { goals const & gs = new_s.get_goals(); goal const & g = head(gs); - expr new_p = g.abstract(*new_e); substitution subst = new_s.get_subst(); - check_has_no_local(new_p, e, "exact"); - subst.assign(g.get_name(), new_p); + assign(subst, g, *new_e); return some(proof_state(new_s, tail(gs), subst)); } return none_proof_state(); diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp index 3dd13f5f1..1543877e4 100644 --- a/src/library/tactic/generalize_tactic.cpp +++ b/src/library/tactic/generalize_tactic.cpp @@ -38,7 +38,6 @@ tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const & n = x; expr new_t = mk_pi(n, e_t, abstract(t, *new_e)); expr new_m = g.mk_meta(ngen.next(), new_t); - expr new_v = g.abstract(mk_app(new_m, *new_e)); try { tc->check_ignore_levels(g.abstract(new_t)); } catch (kernel_exception const & ex) { @@ -52,7 +51,7 @@ tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const & return none_proof_state(); } - subst.assign(g.get_name(), new_v); + assign(subst, g, mk_app(new_m, *new_e)); goal new_g(new_m, new_t); return some(proof_state(new_s, goals(new_g, tail(gs)), subst, ngen)); } diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index b71d30874..51742915c 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -172,6 +172,12 @@ void goal::get_hyps(buffer & r) const { get_app_args(m_meta, r); } +void assign(substitution & s, goal const & g, expr const & v) { + buffer hyps; + expr const & mvar = get_app_args(g.get_meta(), hyps); + s.assign(mvar, hyps, v); +} + static bool uses_name(name const & n, buffer const & locals) { for (expr const & local : locals) { if (is_local(local) && local_pp_name(local) == n) diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index 9ace3db44..f96962307 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -103,6 +103,8 @@ public: format pp(formatter const & fmt) const; }; +void assign(substitution & s, goal const & g, expr const & v); + name get_unused_name(name const & prefix, unsigned & idx, buffer const & locals); name get_unused_name(name const & prefix, buffer const & locals); name get_unused_name(name const & prefix, unsigned & idx, expr const & meta); diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 936247fb3..037a30102 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -162,8 +162,8 @@ class inversion_tac { } } - void assign(name const & n, expr const & val) { - m_subst.assign(n, val); + void assign(goal const & g, expr const & val) { + ::lean::assign(m_subst, g, val); } /** \brief We say h has independent indices IF @@ -286,9 +286,9 @@ class inversion_tac { expr new_type = Pi(eqs, g.get_type()); expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); - expr val = g.abstract(mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h), - refls)); - assign(g.get_name(), val); + expr val = mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h), + refls); + assign(g, val); return new_g; } else { // proof relevant version @@ -316,9 +316,9 @@ class inversion_tac { expr new_type = Pi(eqs, g.get_type()); expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); - expr val = g.abstract(mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h), - refls)); - assign(g.get_name(), val); + expr val = mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h), + refls); + assign(g, val); return new_g; } } @@ -340,8 +340,8 @@ class inversion_tac { expr new_type = Pi(deps, g.get_type()); expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)), new_hyps); goal new_g(new_meta, new_type); - expr val = g.abstract(mk_app(new_meta, deps)); - assign(g.get_name(), val); + expr val = mk_app(new_meta, deps); + assign(g, val); return new_g; } @@ -420,8 +420,7 @@ class inversion_tac { name const & intro_name = intro_names[i]; new_imps.push_back(filter(imps, [&](implementation_ptr const & imp) { return imp->get_constructor_name() == intro_name; })); } - expr val = g.abstract(cases_on); - assign(g.get_name(), val); + assign(g, cases_on); return mk_pair(to_list(new_goals), to_list(new_imps)); } @@ -484,8 +483,8 @@ class inversion_tac { expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, g_type)), new_hyps); goal new_g(new_meta, g_type); new_gs.push_back(new_g); - expr val = g.abstract(Fun(nargs, new_hyps.end() - nargs, new_meta)); - assign(g.get_name(), val); + expr val = Fun(nargs, new_hyps.end() - nargs, new_meta); + assign(g, val); gs = tail(gs); } return mk_pair(to_list(new_gs), to_list(new_args)); @@ -566,8 +565,8 @@ class inversion_tac { // aux_eq : a = eq.rec A s C a s p expr trans_eq = mk_app({mk_constant(get_eq_trans_name(), {lvl}), A, reduced_lhs, lhs, rhs, *aux_eq, old_eq}); // trans_eq : a = b - expr val = g.abstract(Fun(old_eq, mk_app(new_meta, trans_eq))); - assign(g.get_name(), val); + expr val = Fun(old_eq, mk_app(new_meta, trans_eq)); + assign(g, val); return intro_next_eq(new_g); } @@ -598,8 +597,8 @@ class inversion_tac { hyps.pop_back(); expr H = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info()); expr to_eq = mk_app(mk_constant(get_heq_to_eq_name(), const_levels(heq_fn)), args[0], args[1], args[3], H); - expr val = g.abstract(Fun(H, mk_app(mk_app(new_mvar, hyps), to_eq))); - assign(g.get_name(), val); + expr val = Fun(H, mk_app(mk_app(new_mvar, hyps), to_eq)); + assign(g, val); return new_g; } else { if (m_throw_tactic_exception) { @@ -626,8 +625,8 @@ class inversion_tac { hyps.push_back(new_hyp); expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); - expr val = g.abstract(Fun(new_hyp, new_meta)); - assign(g.get_name(), val); + expr val = Fun(new_hyp, new_meta); + assign(g, val); return new_g; } @@ -722,8 +721,7 @@ class inversion_tac { expr new_type = g.get_type(); expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); - expr val = g.abstract(new_meta); - assign(g.get_name(), val); + assign(g, new_meta); return unify_eqs(new_g, neqs-1); } buffer lhs_args, rhs_args; @@ -755,15 +753,15 @@ class inversion_tac { expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type)); expr new_meta = mk_app(new_mvar, hyps); goal new_g(new_meta, new_type); - expr val = g.abstract(lift_down(mk_app(no_confusion, new_meta))); - assign(g.get_name(), val); + expr val = lift_down(mk_app(no_confusion, new_meta)); + assign(g, val); unsigned A_nparams = *inductive::get_num_params(m_env, const_name(A_fn)); lean_assert(lhs_args.size() >= A_nparams); return unify_eqs(new_g, neqs - 1 + lhs_args.size() - A_nparams); } else { // conflict transition, eq is of the form c_1 ... = c_2 ..., where c_1 and c_2 are different constructors/intro rules. - expr val = g.abstract(lift_down(no_confusion)); - assign(g.get_name(), val); + expr val = lift_down(no_confusion); + assign(g, val); return optional(); // goal has been solved } } @@ -798,8 +796,7 @@ class inversion_tac { expr new_mvar = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)); expr new_meta = mk_app(new_mvar, new_hyps); goal new_g(new_meta, new_type); - expr val = g.abstract(new_meta); - assign(g.get_name(), val); + assign(g, new_meta); return unify_eqs(new_g, neqs-1); } else { expr deps_g_type = Pi(deps, g_type); @@ -837,8 +834,8 @@ class inversion_tac { goal new_g(new_meta, new_type); expr eq_rec_minor = mk_app(new_mvar, non_deps); eq_rec = mk_app(eq_rec, eq_rec_minor, rhs, eq); - expr val = g.abstract(mk_app(eq_rec, deps)); - assign(g.get_name(), val); + expr val = mk_app(eq_rec, deps); + assign(g, val); return unify_eqs(new_g, neqs-1); } } else if (is_local(lhs)) { @@ -853,8 +850,8 @@ class inversion_tac { level eq_symm_lvl = sort_level(m_tc.ensure_type(A).first); expr symm_pr = mk_constant(get_eq_symm_name(), {eq_symm_lvl}); symm_pr = mk_app(symm_pr, A, lhs, rhs, eq); - expr val = g.abstract(mk_app(new_meta, symm_pr)); - assign(g.get_name(), val); + expr val = mk_app(new_meta, symm_pr); + assign(g, val); return unify_eqs(new_g, neqs); } if (m_throw_tactic_exception) { @@ -912,8 +909,8 @@ class inversion_tac { expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, g_type)), new_hyps); goal new_g(new_meta, g_type); unsigned ndeps = deps.size(); - expr val = g.abstract(Fun(ndeps, new_hyps.end() - ndeps, new_meta)); - assign(g.get_name(), val); + expr val = Fun(ndeps, new_hyps.end() - ndeps, new_meta); + assign(g, val); return mk_pair(new_g, rs); } @@ -941,8 +938,7 @@ class inversion_tac { expr new_type = g.get_type(); expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); - expr val = g.abstract(new_meta); - assign(g.get_name(), val); + assign(g, new_meta); return new_g; } else { return g; diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/tactic/revert_tactic.cpp index 6d22a7acb..a5b85c723 100644 --- a/src/library/tactic/revert_tactic.cpp +++ b/src/library/tactic/revert_tactic.cpp @@ -35,9 +35,8 @@ tactic revert_tactic(name const & n) { expr new_type = Pi(h, g.get_type()); expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); - expr val = g.abstract(mk_app(new_meta, h)); substitution new_subst = s.get_subst(); - new_subst.assign(g.get_name(), val); + assign(new_subst, g, mk_app(new_meta, h)); proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen); return some_proof_state(new_s); } else { diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index ddbea68b7..a688a4d3b 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -511,8 +511,7 @@ class rewrite_fn { void replace_goal(expr const & new_type) { expr M = m_g.mk_meta(m_ngen.next(), new_type); goal new_g(M, new_type); - expr val = m_g.abstract(M); - m_subst.assign(m_g.get_name(), val); + assign(m_subst, m_g, M); update_goal(new_g); } @@ -540,8 +539,7 @@ class rewrite_fn { expr new_mvar = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)); expr new_meta = mk_app(new_mvar, new_hyps); goal new_g(new_meta, new_type); - expr val = m_g.abstract(new_meta); - m_subst.assign(m_g.get_name(), val); + assign(m_subst, m_g, new_meta); update_goal(new_g); } @@ -968,8 +966,7 @@ class rewrite_fn { expr new_mvar = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)); expr new_meta = mk_app(new_mvar, new_hyps); goal new_g(new_meta, new_type); - expr val = m_g.abstract(mk_app(new_mvar, args)); - m_subst.assign(m_g.get_name(), val); + assign(m_subst, m_g, mk_app(new_mvar, args)); update_goal(new_g); return true; } @@ -1003,8 +1000,7 @@ class rewrite_fn { } goal new_g(M, Pb); - expr val = m_g.abstract(H); - m_subst.assign(m_g.get_name(), val); + assign(m_subst, m_g, H); update_goal(new_g); // regular(m_env, m_ios) << "FOUND\n" << a << "\n==>\n" << b << "\nWITH\n" << Heq << "\n"; // regular(m_env, m_ios) << H << "\n"; @@ -1116,13 +1112,13 @@ class rewrite_fn { expr rhs = app_arg(type); if (m_unifier_tc->is_def_eq(lhs, rhs, justification(), cs) && !cs) { expr H = is_eq(type) ? mk_refl(*m_tc, lhs) : mk_iff_refl(lhs); - m_subst.assign(m_g.get_name(), m_g.abstract(H)); + assign(m_subst, m_g, H); return true; } else { return false; } } else if (type == mk_true()) { - m_subst.assign(m_g.get_name(), mk_constant(get_eq_intro_name())); + assign(m_subst, m_g, mk_constant(get_eq_intro_name())); return true; } else { return false; diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index e0cb733df..2bb4edb04 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -227,16 +227,16 @@ tactic assumption_tactic() { goals new_gs = map_goals(s, [&](goal const & g) -> optional { expr const & t = g.get_type(); optional h; - buffer locals; - get_app_args(g.get_meta(), locals); - for (auto const & l : locals) { + buffer hyps; + g.get_hyps(hyps); + for (auto const & l : hyps) { if (mlocal_type(l) == t) { h = l; break; } } if (h) { - subst.assign(g.get_mvar(), g.abstract(*h), justification()); + assign(subst, g, *h); solved = true; return optional(); } else {