From b317d4bc58b75b2666bcd0c652c96fbecb5df1b9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Aug 2016 08:19:05 -0700 Subject: [PATCH] refactor(library/tactic): add hsubstitution module --- src/library/equations_compiler/elim_match.cpp | 34 +++++------ src/library/tactic/CMakeLists.txt | 3 +- src/library/tactic/cases_tactic.cpp | 59 ++++++++++--------- src/library/tactic/cases_tactic.h | 3 +- src/library/tactic/hsubstitution.cpp | 47 +++++++++++++++ src/library/tactic/hsubstitution.h | 30 ++++++++++ src/library/tactic/induction_tactic.cpp | 14 ++--- src/library/tactic/induction_tactic.h | 6 +- src/library/tactic/subst_tactic.cpp | 49 ++------------- src/library/tactic/subst_tactic.h | 16 +---- 10 files changed, 145 insertions(+), 116 deletions(-) create mode 100644 src/library/tactic/hsubstitution.cpp create mode 100644 src/library/tactic/hsubstitution.h diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 44d18f0d24..091376a25c 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -54,7 +54,7 @@ struct elim_match_fn { list m_patterns; expr m_rhs; /* m_renames map variables in this->m_lctx to problem local context */ - substitutions m_substs; + hsubstitution m_subst; expr m_ref; /* for producing error messages */ unsigned m_eqn_idx; /* for producing error message */ }; @@ -72,7 +72,7 @@ struct elim_match_fn { list m_hs; list m_args; expr m_rhs; - substitutions m_substs; + hsubstitution m_subst; unsigned m_eqn_idx; }; @@ -108,7 +108,7 @@ struct elim_match_fn { bool check_equation(problem const & P, equation const & eqn) { lean_assert(length(eqn.m_patterns) == length(P.m_var_stack)); local_context const & lctx = get_local_context(P); - eqn.m_substs.for_each([&](name const & n, expr const & e) { + eqn.m_subst.for_each([&](name const & n, expr const & e) { lean_assert(eqn.m_lctx.get_local_decl(n)); lean_assert(check_locals_decl_at(e, lctx)); }); @@ -430,11 +430,11 @@ struct elim_match_fn { lean_unreachable(); } - substitutions add_subst(substitutions substs, expr const & src, expr const & target) { + hsubstitution add_subst(hsubstitution subst, expr const & src, expr const & target) { lean_assert(is_local(src)); - if (!substs.contains(mlocal_name(src))) - substs.insert(mlocal_name(src), target); - return substs; + if (!subst.contains(mlocal_name(src))) + subst.insert(mlocal_name(src), target); + return subst; } /* Variable and Inaccessible transition are very similar, this method implements both. */ @@ -450,7 +450,7 @@ struct elim_match_fn { equation new_eqn = eqn; new_eqn.m_patterns = tail(eqn.m_patterns); if (is_var_transition) { - new_eqn.m_substs = add_subst(eqn.m_substs, head(eqn.m_patterns), head(P.m_var_stack)); + new_eqn.m_subst = add_subst(eqn.m_subst, head(eqn.m_patterns), head(P.m_var_stack)); } new_eqns.push_back(new_eqn); } @@ -505,26 +505,26 @@ struct elim_match_fn { /* Append `ilist` and `var_stack`. Due to dependent pattern matching, ilist may contain terms that are not local constants. */ - list update_var_stack(list const & ilist, list const & var_stack, substitutions const & substs) { + list update_var_stack(list const & ilist, list const & var_stack, hsubstitution const & subst) { buffer new_var_stack; for (expr const & e : ilist) { new_var_stack.push_back(e); } for (expr const & v : var_stack) { - new_var_stack.push_back(apply_substitutions(v, substs)); + new_var_stack.push_back(apply(v, subst)); } return to_list(new_var_stack); } /* eqns is the data-structured returned by distribute_constructor_equations. This method selects the ones such that eqns[i].first == C. - It also updates eqns[i].second.m_substs using \c new_substs. + It also updates eqns[i].second.m_subst using \c new_subst. It also "replaces" the next pattern (a constructor) with its fields. - The map \c new_substs is produced by the `cases` tactic. + The map \c new_subst is produced by the `cases` tactic. It is needed because the `cases` tactic may revert and reintroduce hypothesis that depend on the hypothesis being destructed. */ - list get_equations_for(name const & C, unsigned nparams, substitutions const & new_substs, + list get_equations_for(name const & C, unsigned nparams, hsubstitution const & new_subst, local_context const & lctx, list const & eqns) { buffer R; for (equation const & eqn : eqns) { @@ -533,7 +533,7 @@ struct elim_match_fn { expr const & C2 = get_app_args(pattern, pattern_args); if (!is_constant(C2, C)) continue; equation new_eqn = eqn; - new_eqn.m_substs = apply_substitutions(eqn.m_substs, new_substs); + new_eqn.m_subst = apply(eqn.m_subst, new_subst); /* Update patterns */ type_context ctx = mk_type_context(eqn.m_lctx); new_eqn.m_patterns = to_list(pattern_args.begin() + nparams, pattern_args.end(), tail(eqn.m_patterns)); @@ -579,7 +579,7 @@ struct elim_match_fn { name I_name = const_name(get_app_fn(x_type)); unsigned I_nparams = get_inductive_num_params(I_name); intros_list ilist; - substitutions_list slist; + hsubstitution_list slist; list new_goals; list new_goal_cnames; try { @@ -711,7 +711,7 @@ struct elim_match_fn { new_var_stack.push_back(C_args[i]); to_buffer(tail(P.m_var_stack), new_var_stack); new_P.m_var_stack = to_list(new_var_stack); - new_P.m_equations = get_equations_for(const_name(C), I_nparams, substitutions(), + new_P.m_equations = get_equations_for(const_name(C), I_nparams, hsubstitution(), get_local_context(P.m_goal), eqns); list Ls = process(new_P); buffer new_Ls; @@ -728,7 +728,7 @@ struct elim_match_fn { } equation const & eqn = head(P.m_equations); m_used_eqns[eqn.m_eqn_idx] = true; - expr rhs = apply_substitutions(eqn.m_rhs, eqn.m_substs); + expr rhs = apply(eqn.m_rhs, eqn.m_subst); m_mctx.assign(P.m_goal, rhs); if (m_lemmas) { lemma L; diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 4a18edff7f..f7bae22c27 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -5,4 +5,5 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp fun_info_tactics.cpp congr_lemma_tactics.cpp match_tactic.cpp ac_tactics.cpp induction_tactic.cpp cases_tactic.cpp generalize_tactic.cpp rewrite_tactic.cpp unfold_tactic.cpp - gexpr.cpp elaborate.cpp init_module.cpp simp_result.cpp user_attribute.cpp) + hsubstitution.cpp gexpr.cpp elaborate.cpp init_module.cpp + simp_result.cpp user_attribute.cpp) diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 2ca8beaacb..2c2153c437 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -237,15 +237,15 @@ struct cases_tactic_fn { return tmp.pp_goal(mvar); } - list elim_aux_indices(list const & goals, buffer const & aux_indices_H, substitutions_list & slist) { + list elim_aux_indices(list const & goals, buffer const & aux_indices_H, hsubstitution_list & slist) { lean_assert(!slist || length(goals) == length(slist)); buffer new_goals; - buffer new_slist; + buffer new_slist; list it1 = goals; - substitutions_list it2 = slist; + hsubstitution_list it2 = slist; while (it1 && it2) { expr mvar = head(it1); - substitutions substs = head(it2); + hsubstitution subst = head(it2); name_set removed; lean_assert(aux_indices_H.size() > 1); unsigned i = aux_indices_H.size() - 1; /* last element is the auxiliary major premise */ @@ -253,23 +253,23 @@ struct cases_tactic_fn { --i; name idx_name = aux_indices_H[i]; removed.insert(idx_name); - if (auto ridx = substs.find(idx_name)) { + if (auto ridx = subst.find(idx_name)) { lean_assert(is_local(*ridx)); name new_name = mlocal_name(*ridx); - substs.erase(idx_name); + subst.erase(idx_name); idx_name = new_name; } expr H_idx = m_mctx.get_hypothesis_of(mvar, idx_name)->mk_ref(); mvar = clear(m_mctx, mvar, H_idx); } - substitutions new_substs; - substs.for_each([&](name const & from, expr const & to) { + hsubstitution new_subst; + subst.for_each([&](name const & from, expr const & to) { lean_assert(is_local(to)); if (!removed.contains(mlocal_name(to))) - new_substs.insert(from, to); + new_subst.insert(from, to); }); new_goals.push_back(mvar); - new_slist.push_back(new_substs); + new_slist.push_back(new_subst); it1 = tail(it1); it2 = tail(it2); } @@ -278,7 +278,7 @@ struct cases_tactic_fn { } optional unify_eqs(expr mvar, unsigned num_eqs, bool updating, - list & new_intros, substitutions & substs) { + list & new_intros, hsubstitution & subst) { if (num_eqs == 0) { lean_cases_trace(mvar, tout() << "solved equalities\n" << pp_goal(mvar) << "\n";); return some_expr(mvar); @@ -322,17 +322,17 @@ 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, new_intros, substs); + return unify_eqs(mvar2, num_eqs, updating, new_intros, subst); } else if (is_eq(H_type, A, lhs, rhs)) { if (is_local(rhs) || is_local(lhs)) { lean_cases_trace(mvar, tout() << "substitute\n";); - substitutions extra_substs; + hsubstitution extra_subst; bool symm = !is_local(lhs) && is_local(rhs); - expr mvar2 = subst(m_env, m_opts, m_mode, m_mctx, *mvar1, H, symm, - updating ? &extra_substs : nullptr); - new_intros = apply_substitutions(new_intros, extra_substs); - substs = merge(apply_substitutions(substs, extra_substs), extra_substs); - return unify_eqs(mvar2, num_eqs - 1, updating, new_intros, substs); + expr mvar2 = ::lean::subst(m_env, m_opts, m_mode, m_mctx, *mvar1, H, symm, + updating ? &extra_subst : nullptr); + new_intros = apply(new_intros, extra_subst); + subst = merge(apply(subst, extra_subst), extra_subst); + return unify_eqs(mvar2, num_eqs - 1, updating, new_intros, subst); } else { optional c1 = is_constructor_app(m_env, lhs); optional c2 = is_constructor_app(m_env, rhs); @@ -360,7 +360,7 @@ struct cases_tactic_fn { 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, new_intros, substs); + updating, new_intros, subst); } else { /* conflict, closes the goal */ lean_cases_trace(*mvar1, tout() << "conflicting equality detected, " @@ -377,25 +377,25 @@ struct cases_tactic_fn { } pair, list> unify_eqs(list const & mvars, list const & cnames, unsigned num_eqs, - intros_list * ilist, substitutions_list * slist) { + intros_list * ilist, hsubstitution_list * slist) { lean_assert((ilist == nullptr) == (slist == nullptr)); buffer new_goals; buffer> new_ilist; - buffer new_slist; + buffer new_slist; buffer new_cnames; list it1 = mvars; list itn = cnames; intros_list const * it2 = ilist; - substitutions_list const * it3 = slist; + hsubstitution_list const * it3 = slist; while (it1) { list new_intros; - substitutions substs; + hsubstitution subst; if (ilist) { new_intros = head(*it2); - substs = head(*it3); + subst = head(*it3); } bool updating = ilist != nullptr; - optional new_mvar = unify_eqs(head(it1), num_eqs, updating, new_intros, substs); + optional new_mvar = unify_eqs(head(it1), num_eqs, updating, new_intros, subst); if (new_mvar) { new_goals.push_back(*new_mvar); new_cnames.push_back(head(itn)); @@ -407,7 +407,7 @@ struct cases_tactic_fn { it3 = &tail(*it3); if (new_mvar) { new_ilist.push_back(new_intros); - new_slist.push_back(substs); + new_slist.push_back(subst); } } } @@ -427,7 +427,8 @@ struct cases_tactic_fn { m_ids(ids){ } - pair, list> operator()(expr const & mvar, expr const & H, intros_list * ilist, substitutions_list * slist) { + pair, list> operator()(expr const & mvar, expr const & H, + intros_list * ilist, hsubstitution_list * slist) { lean_assert((ilist != nullptr) == (slist != nullptr)); lean_assert(is_metavar(mvar)); lean_assert(m_mctx.get_metavar_decl(mvar)); @@ -454,7 +455,7 @@ struct cases_tactic_fn { lean_cases_trace(mvar1, tout() << "after generalize_indices:\n" << pp_goal(mvar1) << "\n";); expr H1 = m_mctx.get_metavar_decl(mvar1)->get_context().get_last_local_decl()->mk_ref(); intros_list tmp_ilist; - substitutions_list tmp_slist; + hsubstitution_list tmp_slist; 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_slist); lean_cases_trace(mvar1, tout() << "after applying cases_on:"; @@ -474,7 +475,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, intros_list * ilist, substitutions_list * slist) { + expr const & mvar, expr const & H, list & ids, intros_list * ilist, hsubstitution_list * slist) { auto r = cases_tactic_fn(env, opts, m, mctx, ids)(mvar, H, ilist, slist); 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 cfde3758a1..6468dfdbb4 100644 --- a/src/library/tactic/cases_tactic.h +++ b/src/library/tactic/cases_tactic.h @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #pragma once #include "library/tactic/induction_tactic.h" -#include "library/tactic/subst_tactic.h" namespace lean { /** \brief Similar to induction, but applies 'cases_on' and has bettern support for dependent types. Failures are reported using exceptions. @@ -29,7 +28,7 @@ namespace lean { 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, intros_list * ilist, substitutions_list * slist); + expr const & mvar, expr const & H, list & ids, intros_list * ilist, hsubstitution_list * slist); void initialize_cases_tactic(); void finalize_cases_tactic(); diff --git a/src/library/tactic/hsubstitution.cpp b/src/library/tactic/hsubstitution.cpp new file mode 100644 index 0000000000..053046a67d --- /dev/null +++ b/src/library/tactic/hsubstitution.cpp @@ -0,0 +1,47 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/replace_fn.h" +#include "library/tactic/hsubstitution.h" + +namespace lean { +expr apply(expr const & e, hsubstitution const & s) { + if (s.empty()) return e; + if (!has_local(e)) return e; + return replace(e, [&](expr const & e, unsigned) { + if (!has_local(e)) return some_expr(e); + if (is_local(e)) { + if (auto r = s.find(mlocal_name(e))) + return some_expr(*r); + } + return none_expr(); + }); +} + +list apply(list const & es, hsubstitution const & s) { + if (s.empty()) return es; + return map(es, [&](expr const & e) { return apply(e, s); }); +} + +hsubstitution apply(hsubstitution const & s1, hsubstitution const & s2) { + if (s2.empty()) return s1; + hsubstitution R; + s1.for_each([&](name const & x, expr const & e) { + R.insert(x, apply(e, s2)); + }); + return R; +} + +hsubstitution merge(hsubstitution const & s1, hsubstitution const & s2) { + if (s1.empty()) return s2; + if (s2.empty()) return s1; + hsubstitution R = s1; + s2.for_each([&](name const & x, expr const & e) { + R.insert(x, e); + }); + return R; +} +} diff --git a/src/library/tactic/hsubstitution.h b/src/library/tactic/hsubstitution.h new file mode 100644 index 0000000000..0b6f340e2e --- /dev/null +++ b/src/library/tactic/hsubstitution.h @@ -0,0 +1,30 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/name_map.h" +#include "kernel/expr.h" + +namespace lean { +/* Some tactics substitute hypotheses with new ones and/or terms. + We track these substitutions using hsubstitution datastructure. + It is just a mapping from the hypothesis original (internal) name + to an expression. The new expression should be well-formed with + respect to the new goal. */ +typedef name_map hsubstitution; + +/* \brief Given `e`, for each (x := v) in `s` replace `x` with `v` in `e` */ +expr apply(expr const & e, hsubstitution const & s); +/* \brief (map es apply) */ +list apply(list const & es, hsubstitution const & s); +/* \brief Return a new hsubstitution containing (x := apply(v, s2)) for + each (x := v) in `s1`. */ +hsubstitution apply(hsubstitution const & s1, hsubstitution const & s2); + +/* \brief Return a new hsubstitution containing the entries of `s1` and `s2`. + \remark the entries in `s2` have precedence over the ones in `s1`. */ +hsubstitution merge(hsubstitution const & s1, hsubstitution const & s2); +} diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index 29851defb2..7e9c2b4210 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -63,7 +63,7 @@ static unsigned get_expr_arity(expr type) { list induction(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, expr const & mvar, expr const & H, name const & rec_name, list & ns, - intros_list * ilist, substitutions_list * slist) { + intros_list * ilist, hsubstitution_list * slist) { lean_assert(is_metavar(mvar)); lean_assert(is_local(H)); lean_assert((ilist == nullptr) == (slist == nullptr)); @@ -128,12 +128,12 @@ list induction(environment const & env, options const & opts, transparency optional mvar2 = intron(env, opts, mctx, mvar1, indices.size() + 1, indices_H); if (!mvar2) throw exception("induction tactic failed, failed to reintroduce major premise"); - substitutions base_substs; /* substitutions for all branches */ + hsubstitution base_subst; /* substitutions for all branches */ if (slist) { local_context lctx = mctx.get_metavar_decl(*mvar2)->get_context(); /* store old index name -> new index name */ for (unsigned i = 0; i < indices.size(); i++) { - base_substs.insert(mlocal_name(indices[i]), lctx.get_local_decl(indices_H[i])->mk_ref()); + base_subst.insert(mlocal_name(indices[i]), lctx.get_local_decl(indices_H[i])->mk_ref()); } } optional g2 = mctx.get_metavar_decl(*mvar2); @@ -205,7 +205,7 @@ list induction(environment const & env, options const & opts, transparency bool consumed_major = false; buffer new_goals; buffer> params_buffer; - buffer substs_buffer; + buffer subst_buffer; list produce_motive = rec_info.get_produce_motive(); while (is_pi(rec_type) && curr_pos < rec_info.get_num_args()) { if (first_idx_pos == curr_pos) { @@ -257,12 +257,12 @@ list induction(environment const & env, options const & opts, transparency } if (slist) { /* Save renaming for hypothesis that depend on indices and/or major premise. */ - substitutions S = base_substs; + hsubstitution S = base_subst; lean_assert(extra_names.size() == nextra); for (unsigned i = indices.size() + 1, j = 0; i < to_revert.size(); i++, j++) { S.insert(mlocal_name(to_revert[i]), aux_M_lctx.get_local_decl(extra_names[j])->mk_ref()); } - substs_buffer.push_back(S); + subst_buffer.push_back(S); } /* Clear hypothesis in the new goal. */ set_clear(aux_M, ctx2, aux_M, H2); @@ -283,7 +283,7 @@ list induction(environment const & env, options const & opts, transparency if (ilist) { lean_assert(slist); *ilist = to_list(params_buffer); - *slist = to_list(substs_buffer); + *slist = to_list(subst_buffer); } return to_list(new_goals); } diff --git a/src/library/tactic/induction_tactic.h b/src/library/tactic/induction_tactic.h index a983ac487a..6f3c92e1c8 100644 --- a/src/library/tactic/induction_tactic.h +++ b/src/library/tactic/induction_tactic.h @@ -6,11 +6,11 @@ Author: Leonardo de Moura */ #pragma once #include "library/tactic/tactic_state.h" -#include "library/tactic/subst_tactic.h" +#include "library/tactic/hsubstitution.h" namespace lean { typedef list> intros_list; -typedef list substitutions_list; +typedef list hsubstitution_list; /** \brief Apply the induction lemma \c rec_name on the hypothesis \c H at goal \c mvar. The tactic uses ns (if available) to name parameters associated with minor premises. @@ -28,7 +28,7 @@ typedef list substitutions_list; \post slist != nullptr ==> length(*slist) == length(result) */ list induction(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, expr const & mvar, expr const & H, name const & rec_name, list & ns, - intros_list * ilist, substitutions_list * slist); + intros_list * ilist, hsubstitution_list * slist); void initialize_induction_tactic(); void finalize_induction_tactic(); diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index 7f5ff22ec6..e7cf82dc6a 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -21,43 +21,6 @@ Author: Leonardo de Moura #include "library/tactic/app_builder_tactics.h" namespace lean { -expr apply_substitutions(expr const & e, substitutions const & s) { - if (s.empty()) return e; - if (!has_local(e)) return e; - return replace(e, [&](expr const & e, unsigned) { - if (!has_local(e)) return some_expr(e); - if (is_local(e)) { - if (auto r = s.find(mlocal_name(e))) - return some_expr(*r); - } - return none_expr(); - }); -} - -list apply_substitutions(list const & es, substitutions const & s) { - if (s.empty()) return es; - return map(es, [&](expr const & e) { return apply_substitutions(e, s); }); -} - -substitutions apply_substitutions(substitutions const & s1, substitutions const & s2) { - if (s2.empty()) return s1; - substitutions R; - s1.for_each([&](name const & x, expr const & e) { - R.insert(x, apply_substitutions(e, s2)); - }); - return R; -} - -substitutions merge(substitutions const & s1, substitutions const & s2) { - if (s1.empty()) return s2; - if (s2.empty()) return s1; - substitutions R = s1; - s2.for_each([&](name const & x, expr const & e) { - R.insert(x, e); - }); - return R; -} - /* For debugging purposes, make sure H is in the local context for mvar */ bool check_hypothesis_in_context(metavar_context const & mctx, expr const & mvar, name const & H) { local_context lctx = mctx.get_metavar_decl(mvar)->get_context(); @@ -69,7 +32,7 @@ bool check_hypothesis_in_context(metavar_context const & mctx, expr const & mvar } expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, - expr const & mvar, expr const & H, bool symm, substitutions * substs) { + expr const & mvar, expr const & H, bool symm, hsubstitution * subst) { #define lean_subst_trace(CODE) lean_trace(name({"tactic", "subst"}), CODE) #define lean_subst_trace_state(MVAR, MSG) lean_trace(name({"tactic", "subst"}), tactic_state S(env, opts, mctx, to_list(MVAR), MVAR); type_context TMP_CTX = mk_type_context_for(S, m); scope_trace_env _scope1(env, TMP_CTX); tout() << MSG << S.pp() << "\n";) @@ -125,16 +88,16 @@ expr subst(environment const & env, options const & opts, transparency_mode cons optional mvar6 = intron(env, opts, mctx, mvar5, to_revert.size() - 2, new_Hnames); if (!mvar6) throw exception("subst tactic failed, unexpected failure when re-introducing dependencies"); lean_assert(new_Hnames.size() == to_revert.size() - 2); - if (substs) { + if (subst) { local_context lctx = mctx.get_metavar_decl(*mvar6)->get_context(); - substitutions new_substs; + hsubstitution new_subst; for (unsigned i = 0; i < to_revert.size() - 2; i++) { lean_assert(check_hypothesis_in_context(mctx, mvar, mlocal_name(to_revert[i+2]))); lean_assert(check_hypothesis_in_context(mctx, *mvar6, new_Hnames[i])); - new_substs.insert(mlocal_name(to_revert[i+2]), lctx.get_local_decl(new_Hnames[i])->mk_ref()); + new_subst.insert(mlocal_name(to_revert[i+2]), lctx.get_local_decl(new_Hnames[i])->mk_ref()); } - new_substs.insert(mlocal_name(init_lhs), apply_substitutions(rhs, new_substs)); - *substs = new_substs; + new_subst.insert(mlocal_name(init_lhs), apply(rhs, new_subst)); + *subst = new_subst; } lean_subst_trace_state(*mvar6, "after intro remaining reverted hypotheses:\n"); return *mvar6; diff --git a/src/library/tactic/subst_tactic.h b/src/library/tactic/subst_tactic.h index 1cd0577c50..5afd4149b3 100644 --- a/src/library/tactic/subst_tactic.h +++ b/src/library/tactic/subst_tactic.h @@ -6,21 +6,9 @@ Author: Leonardo de Moura */ #pragma once #include "library/tactic/tactic_state.h" +#include "library/tactic/hsubstitution.h" namespace lean { -typedef name_map substitutions; - -/* \brief Given `e`, for each (x := v) in `s` replace `x` with `v` in `e` */ -expr apply_substitutions(expr const & e, substitutions const & s); -list apply_substitutions(list const & es, substitutions const & s); - -/* \brief Return a new set of substitutions containing (x := apply_substitutions(v, s2)) for - each (x := v) in `s1`. */ -substitutions apply_substitutions(substitutions const & s1, substitutions const & s2); - -/* \brief Return a new set of substitutions containing the entries of `s1` and `s2`. */ -substitutions merge(substitutions const & s1, substitutions const & s2); - /** \brief Given (H : lhs = rhs), replace lhs with rhs in the goal \c mvar. If symm == true, then replace rhs with lhs. The replaced term must be a local constant. If substs is not nullptr, then hypotheses renamed by revert/intro are stored in \c substs, and the actual substitution. @@ -32,7 +20,7 @@ substitutions merge(substitutions const & s1, substitutions const & s2); \pre symm == false ==> is_local(lhs(typeof(H))) \pre symm == false ==> is_local(rhs(typeof(H))) */ expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, - expr const & mvar, expr const & H, bool symm, substitutions * substs); + expr const & mvar, expr const & H, bool symm, hsubstitution * substs); void initialize_subst_tactic(); void finalize_subst_tactic();