From 0b57f7d00a37c641c18c36d7080e33de14071659 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 May 2015 18:02:51 -0700 Subject: [PATCH] refactor(library/tactic): refine interface between tactic and proof-term modes Some constraints were being lost with the previous interface. This is why we had a workaround in fintype.lean. We can also remove some hacks we have used in the past. --- hott/algebra/category/functor.hlean | 2 +- library/data/fintype.lean | 8 +---- src/frontends/lean/elaborator.cpp | 33 ++++++++++--------- src/frontends/lean/elaborator.h | 7 +++-- src/frontends/lean/info_tactic.cpp | 2 +- src/library/tactic/apply_tactic.cpp | 10 +++--- src/library/tactic/check_expr_tactic.cpp | 2 +- src/library/tactic/elaborate.cpp | 11 ++++--- src/library/tactic/elaborate.h | 12 +++++-- src/library/tactic/let_tactic.cpp | 9 +++--- src/library/tactic/proof_state.h | 9 +++++- src/library/tactic/rewrite_tactic.cpp | 40 ++++++++++++++++++------ 12 files changed, 89 insertions(+), 56 deletions(-) diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean index a70f3099ef..4fe26039ec 100644 --- a/hott/algebra/category/functor.hlean +++ b/hott/algebra/category/functor.hlean @@ -74,7 +74,7 @@ namespace functor apply (apd10' c'), apply concat, rotate_left 1, esimp, exact (pi_transport_constant (eq_of_homotopy pF) H₁ c), - reflexivity + esimp end)))) definition functor_eq {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ ∼ to_fun_ob F₂), diff --git a/library/data/fintype.lean b/library/data/fintype.lean index 893ec1a571..622570b3b5 100644 --- a/library/data/fintype.lean +++ b/library/data/fintype.lean @@ -136,13 +136,7 @@ match h₁ with match check_pred (λ a, ¬ p a) e with | tt := λ h : check_pred (λ a, ¬ p a) e = tt, inr (λ ex : (∃ x, p x), obtain x px, from ex, - begin - -- TODO(Leo): remove the following hack. This hack is needed to workaround a problem in - -- the method elaborator::elaborate_nested - apply absurd px, - apply all_of_check_pred_eq_tt h, - apply c x, - end) + absurd px (all_of_check_pred_eq_tt h (c x))) | ff := λ h : check_pred (λ a, ¬ p a) e = ff, inl ( assert aux₁ : ∃ x, ¬¬p x, from ex_of_check_pred_eq_ff h, obtain x nnpx, from aux₁, exists.intro x (not_not_elim nnpx)) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index d05f30b35c..5fe75ec88a 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1640,13 +1640,13 @@ optional elaborator::pre_tactic_to_tactic(expr const & pre_tac) { try { bool relax = m_relax_main_opaque; auto fn = [=](goal const & g, name_generator const & ngen, expr const & e, optional const & expected_type, - bool report_unassigned) { + substitution const & subst, bool report_unassigned) { elaborator aux_elaborator(m_ctx, ngen); // Disable tactic hints when processing expressions nested in tactics. // We must do it otherwise, it is easy to make the system loop. bool use_tactic_hints = false; return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e, - relax, use_tactic_hints, report_unassigned); + relax, use_tactic_hints, subst, report_unassigned); }; return optional(expr_to_tactic(env(), fn, pre_tac, pip())); } catch (expr_to_tactic_exception & ex) { @@ -2067,9 +2067,9 @@ static expr translate(environment const & env, list const & ctx, expr cons } /** \brief Elaborate expression \c e in context \c ctx. */ -pair elaborator::elaborate_nested(list const & ctx, optional const & expected_type, - expr const & n, bool relax, bool use_tactic_hints, - bool report_unassigned) { +elaborate_result elaborator::elaborate_nested(list const & ctx, optional const & expected_type, + expr const & n, bool relax, bool use_tactic_hints, + substitution const & subst, bool report_unassigned) { if (infom()) { if (auto ps = get_info_tactic_proof_state()) { save_proof_state_info(*ps, n); @@ -2089,21 +2089,24 @@ pair elaborator::elaborate_nested(list const & ctx, opt flet set_use_hints(m_use_tactic_hints, use_tactic_hints); constraint_seq cs; expr r = visit(e, cs); - auto p = solve(cs).pull(); + + buffer tmp; + cs.linearize(tmp); + auto p = unify(env(), tmp.size(), tmp.data(), m_ngen.mk_child(), subst, m_unifier_config).pull(); lean_assert(p); - substitution s = p->first.first; - constraints rcs = p->first.second; - r = s.instantiate_all(r); - r = solve_unassigned_mvars(s, r); - rcs = map(rcs, [&](constraint const & c) { return instantiate_metavars(c, s); }); - copy_info_to_manager(s); + substitution new_subst = p->first.first; + constraints rcs = p->first.second; + r = new_subst.instantiate_all(r); + r = solve_unassigned_mvars(new_subst, r); + rcs = map(rcs, [&](constraint const & c) { return instantiate_metavars(c, new_subst); }); + copy_info_to_manager(new_subst); if (report_unassigned) - display_unassigned_mvars(r, s); + display_unassigned_mvars(r, new_subst); if (expected_type) { justification j; - rcs = append(rcs, cls.mk_constraints(s, j, relax)); + rcs = append(rcs, cls.mk_constraints(new_subst, j, relax)); } - return mk_pair(r, rcs); + return elaborate_result(r, new_subst, rcs); } static name * g_tmp_prefix = nullptr; diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 7a0ec4f955..64a27f21bd 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -12,8 +12,9 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "library/expr_lt.h" #include "library/unifier.h" -#include "library/tactic/tactic.h" #include "library/local_context.h" +#include "library/tactic/tactic.h" +#include "library/tactic/elaborate.h" #include "frontends/lean/elaborator_context.h" #include "frontends/lean/coercion_elaborator.h" #include "frontends/lean/util.h" @@ -165,8 +166,8 @@ class elaborator : public coercion_info_manager { void check_sort_assignments(substitution const & s); expr apply(substitution & s, expr const & e, name_set & univ_params, buffer & new_params); std::tuple apply(substitution & s, expr const & e); - pair elaborate_nested(list const & ctx, optional const & expected_type, expr const & e, - bool relax, bool use_tactic_hints, bool report_unassigned); + elaborate_result elaborate_nested(list const & ctx, optional const & expected_type, expr const & e, + bool relax, bool use_tactic_hints, substitution const &, bool report_unassigned); expr const & get_equation_fn(expr const & eq) const; expr visit_equations(expr const & eqns, constraint_seq & cs); diff --git a/src/frontends/lean/info_tactic.cpp b/src/frontends/lean/info_tactic.cpp index fd5bae7d55..4bbedf0b95 100644 --- a/src/frontends/lean/info_tactic.cpp +++ b/src/frontends/lean/info_tactic.cpp @@ -36,7 +36,7 @@ tactic mk_info_tactic(elaborate_fn const & fn, expr const & e) { // create dummy variable just to communicate position to the elaborator expr dummy = mk_sort(mk_level_zero(), e.get_tag()); scoped_info_tactic_proof_state scope(ps); - fn(goal(), name_generator("dummy"), dummy, none_expr(), false); + fn(goal(), name_generator("dummy"), dummy, none_expr(), substitution(), false); return ps; }); } diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 2db78982de..db749151da 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -234,13 +234,13 @@ tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, add_meta_kin } goal const & g = head(gs); name_generator ngen = s.get_ngen(); - expr new_e; + expr new_e; substitution new_subst; constraints cs_; + auto ecs = elab(g, ngen.mk_child(), e, none_expr(), s.get_subst(), false); + std::tie(new_e, new_subst, cs_) = ecs; buffer cs; - auto ecs = elab(g, ngen.mk_child(), e, none_expr(), false); - new_e = ecs.first; - to_buffer(ecs.second, cs); + to_buffer(cs_, cs); to_buffer(s.get_postponed(), cs); - proof_state new_s(s, ngen, constraints()); + proof_state new_s(s, new_subst, ngen, constraints()); return apply_tactic_core(env, ios, new_s, new_e, cs, add_meta, k); }); } diff --git a/src/library/tactic/check_expr_tactic.cpp b/src/library/tactic/check_expr_tactic.cpp index 016f2ab805..d2fc96c307 100644 --- a/src/library/tactic/check_expr_tactic.cpp +++ b/src/library/tactic/check_expr_tactic.cpp @@ -21,7 +21,7 @@ tactic check_expr_tactic(elaborate_fn const & elab, expr const & e, } goal const & g = head(gs); name_generator ngen = s.get_ngen(); - expr new_e = elab(g, ngen.mk_child(), e, none_expr(), false).first; + expr new_e = std::get<0>(elab(g, ngen.mk_child(), e, none_expr(), s.get_subst(), false)); auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque()); expr new_t = tc->infer(new_e).first; auto out = regular(env, ios); diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp index 212bd373f6..503cadf0f5 100644 --- a/src/library/tactic/elaborate.cpp +++ b/src/library/tactic/elaborate.cpp @@ -44,13 +44,14 @@ optional elaborate_with_respect_to(environment const & env, io_state const optional elab_expected_type; if (enforce_type_during_elaboration) elab_expected_type = expected_type; - auto ecs = elab(head(gs), ngen.mk_child(), e, elab_expected_type, report_unassigned); - expr new_e = ecs.first; + auto esc = elab(head(gs), ngen.mk_child(), e, elab_expected_type, subst, report_unassigned); + expr new_e; substitution new_subst; constraints cs_; + std::tie(new_e, new_subst, cs_) = esc; buffer cs; - to_buffer(ecs.second, cs); + to_buffer(cs_, cs); if (cs.empty() && (!expected_type || enforce_type_during_elaboration)) { // easy case: no constraints to be solved - s = proof_state(s, ngen); + s = proof_state(s, new_subst, ngen); return some_expr(new_e); } else { to_buffer(s.get_postponed(), cs); @@ -75,7 +76,7 @@ optional elaborate_with_respect_to(environment const & env, io_state const d_cs.second.linearize(cs); } unifier_config cfg(ios.get_options()); - unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), subst, cfg); + unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), new_subst, cfg); if (auto p = rseq.pull()) { substitution new_subst = p->first.first; constraints new_postponed = p->first.second; diff --git a/src/library/tactic/elaborate.h b/src/library/tactic/elaborate.h index 9de211678a..7ffe85d329 100644 --- a/src/library/tactic/elaborate.h +++ b/src/library/tactic/elaborate.h @@ -17,10 +17,16 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat 2- name generator 3- expression to be elaborated 4- expected type - 5- a flag indicating whether the elaborator should report unassigned/unsolved placeholders + 5- substitution associated with the proof state + 6- a flag indicating whether the elaborator should report unassigned/unsolved placeholders + The results are + 1- elaborated expression + 2- updated substitution + 3- postponed constraints */ -typedef std::function(goal const &, name_generator const &, expr const &, - optional const &, bool)> elaborate_fn; +typedef std::tuple elaborate_result; +typedef std::function const &, substitution const &, bool)> elaborate_fn; /** \brief Try to elaborate expression \c e using the elaboration function \c elab. The elaboration is performed with respect to (local context of) the first goal in \c s. The constraints generated during elaboration diff --git a/src/library/tactic/let_tactic.cpp b/src/library/tactic/let_tactic.cpp index 8fb457cfe4..14b1e51c71 100644 --- a/src/library/tactic/let_tactic.cpp +++ b/src/library/tactic/let_tactic.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "library/constants.h" #include "library/reducible.h" +#include "library/unifier.h" #include "library/tactic/tactic.h" #include "library/tactic/elaborate.h" #include "library/tactic/expr_to_tactic.h" @@ -28,10 +29,11 @@ tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) { goal const & g = head(gs); name_generator ngen = s.get_ngen(); bool report_unassigned = true; - auto ecs = elab(g, ngen.mk_child(), e, none_expr(), report_unassigned); - if (ecs.second) + elaborate_result esc = elab(g, ngen.mk_child(), e, none_expr(), new_s.get_subst(), report_unassigned); + expr new_e; substitution new_subst; constraints cs; + std::tie(new_e, new_subst, cs) = esc; + if (cs) throw_tactic_exception_if_enabled(s, "invalid 'let' tactic, fail to resolve generated constraints"); - expr new_e = ecs.first; auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque()); expr new_e_type = tc->infer(new_e).first; expr new_local = mk_local(ngen.next(), id, new_e_type, binder_info()); @@ -43,7 +45,6 @@ tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) { expr new_meta_core = mk_app(new_mvar, hyps); expr new_meta = mk_app(new_meta_core, new_local); goal new_goal(new_meta, g.get_type()); - substitution new_subst = new_s.get_subst(); assign(new_subst, g, mk_app(new_meta_core, new_e)); return some_proof_state(proof_state(s, cons(new_goal, tail(gs)), new_subst, ngen)); }); diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 2e6be3ef9c..8b3f15ff57 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -40,10 +40,17 @@ public: proof_state(s, gs, s.m_subst, ngen) {} proof_state(proof_state const & s, goals const & gs): proof_state(s, gs, s.m_subst) {} + proof_state(proof_state const & s, substitution const & subst, name_generator const & ngen, + constraints const & postponed): + proof_state(s.m_goals, subst, ngen, postponed, s.relax_main_opaque(), s.report_failure()) {} proof_state(proof_state const & s, name_generator const & ngen, constraints const & postponed): - proof_state(s.m_goals, s.m_subst, ngen, postponed, s.relax_main_opaque(), s.report_failure()) {} + proof_state(s, s.m_goals, s.m_subst, ngen, postponed) {} + proof_state(proof_state const & s, substitution const & subst, name_generator const & ngen): + proof_state(s, s.m_goals, subst, ngen, s.m_postponed) {} proof_state(proof_state const & s, name_generator const & ngen): proof_state(s, ngen, s.m_postponed) {} + proof_state(proof_state const & s, substitution const & subst): + proof_state(s, subst, s.m_ngen) {} proof_state update_report_failure(bool f) const { return m_report_failure == f ? *this : proof_state(m_goals, m_subst, m_ngen, m_postponed, m_relax_main_opaque, f); diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index f016bf57df..95765baa4c 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -677,11 +677,31 @@ class rewrite_fn { return process_reduce_step(info.get_names(), info.get_location()); } + optional> elaborate_core(expr const & e, bool fail_if_cnstrs) { + expr new_expr; substitution new_subst; constraints cs; + std::tie(new_expr, new_subst, cs) = m_elab(m_g, m_ngen.mk_child(), e, none_expr(), m_ps.get_subst(), false); + if (fail_if_cnstrs && cs) + return optional>(); + m_ps = proof_state(m_ps, new_subst); + return optional>(new_expr, cs); + } + + optional elaborate_if_no_cnstr(expr const & e) { + if (auto r = elaborate_core(e, true)) + return some_expr(r->first); + else + return none_expr(); + } + + pair elaborate(expr const & e) { + return *elaborate_core(e, false); + } + optional fold(expr const & type, expr const & e, occurrence const & occ) { - auto ecs = m_elab(m_g, m_ngen.mk_child(), e, none_expr(), false); - expr new_e = ecs.first; - if (ecs.second) - return none_expr(); // contain constraints... + auto oe = elaborate_if_no_cnstr(e); + if (!oe) + return none_expr(); + expr new_e = *oe; optional unfolded_e = unfold_app(m_env, new_e); if (!unfolded_e) return none_expr(); @@ -750,7 +770,7 @@ class rewrite_fn { } optional unify_with(expr const & t, expr const & e) { - auto ecs = m_elab(m_g, m_ngen.mk_child(), e, none_expr(), false); + auto ecs = elaborate(e); expr new_e = ecs.first; buffer cs; to_buffer(ecs.second, cs); @@ -1074,7 +1094,7 @@ class rewrite_fn { unify_result unify_target(expr const & t, expr const & orig_elem, bool is_goal) { try { expr rule = get_rewrite_rule(orig_elem); - auto rcs = m_elab(m_g, m_ngen.mk_child(), rule, none_expr(), false); + auto rcs = elaborate(rule); rule = rcs.first; buffer cs; to_buffer(rcs.second, cs); @@ -1376,11 +1396,11 @@ class rewrite_fn { expr rule = get_rewrite_rule(elem); expr new_elem; if (has_rewrite_pattern(elem)) { - expr pattern = m_elab(m_g, m_ngen.mk_child(), get_rewrite_pattern(elem), none_expr(), false).first; + expr pattern = elaborate(get_rewrite_pattern(elem)).first; expr new_args[2] = { rule, pattern }; new_elem = mk_macro(macro_def(elem), 2, new_args); } else { - rule = m_elab(m_g, m_ngen.mk_child(), rule, none_expr(), false).first; + rule = elaborate(rule).first; new_elem = mk_macro(macro_def(elem), 1, &rule); } return process_rewrite_step(new_elem, elem); @@ -1504,8 +1524,8 @@ tactic mk_simple_rewrite_tactic(buffer const & rw_elems) { auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { // dummy elaborator auto elab = [](goal const &, name_generator const &, expr const & H, - optional const &, bool) -> pair { - return mk_pair(H, constraints()); + optional const &, substitution const & s, bool) -> elaborate_result { + return elaborate_result(H, s, constraints()); }; return rewrite_fn(env, ios, elab, s)(rw_elems); };