From 9516cd9ee3533293ff87fc30b2504ff637d6d0a9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Nov 2014 14:59:35 -0800 Subject: [PATCH] feat(library/tactic): 'exact' tactic report unsolved placeholders in nested expression Actually, the elaborator is the one reporting the unassigned placeholders. The 'exact' tactic just makes the request. To implement this feature we had to extend the elaboration interface expected by the tactic framework. --- src/frontends/lean/elaborator.cpp | 8 +++++--- src/frontends/lean/elaborator.h | 2 +- src/frontends/lean/info_tactic.cpp | 2 +- src/library/tactic/apply_tactic.cpp | 2 +- src/library/tactic/elaborate.cpp | 5 +++-- src/library/tactic/elaborate.h | 10 ++++++++-- src/library/tactic/exact_tactic.cpp | 3 ++- 7 files changed, 21 insertions(+), 11 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index fac4e17cd8..ffe13fa3df 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -961,12 +961,12 @@ optional elaborator::get_pre_tactic_for(expr const & mvar) { 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) { + auto fn = [=](goal const & g, name_generator const & ngen, expr const & e, 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(), e, relax, use_tactic_hints); + return aux_elaborator.elaborate_nested(g.to_context(), e, relax, use_tactic_hints, report_unassigned); }; return optional(expr_to_tactic(env(), fn, pre_tac, pip())); } catch (expr_to_tactic_exception & ex) { @@ -1274,7 +1274,7 @@ 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, expr const & n, - bool relax, bool use_tactic_hints) { + bool relax, bool use_tactic_hints, bool report_unassigned) { if (infom()) { if (auto ps = get_info_tactic_proof_state()) { save_proof_state_info(*ps, n); @@ -1295,6 +1295,8 @@ pair elaborator::elaborate_nested(list const & ctx, exp r = s.instantiate_all(r); r = solve_unassigned_mvars(s, r); copy_info_to_manager(s); + if (report_unassigned) + display_unassigned_mvars(r, s); return mk_pair(r, rcs); } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index f797a61a9c..4cf4724140 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -150,7 +150,7 @@ class elaborator : public coercion_info_manager { 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 & g, expr const & e, - bool relax, bool use_tactic_hints); + bool relax, bool use_tactic_hints, bool report_unassigned); public: elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names = false); std::tuple operator()(list const & ctx, expr const & e, bool _ensure_type, diff --git a/src/frontends/lean/info_tactic.cpp b/src/frontends/lean/info_tactic.cpp index a3a884bfb0..28b76e8448 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); + fn(goal(), name_generator("dummy"), dummy, false); return ps; }); } diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index cbe26953da..7f22415b17 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -158,7 +158,7 @@ tactic apply_tactic(elaborate_fn const & elab, expr const & e, bool rev) { name_generator ngen = s.get_ngen(); expr new_e; buffer cs; - auto ecs = elab(g, ngen.mk_child(), e); + auto ecs = elab(g, ngen.mk_child(), e, false); new_e = ecs.first; to_buffer(ecs.second, cs); to_buffer(s.get_postponed(), cs); diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp index 52439f628c..e6eeb99f78 100644 --- a/src/library/tactic/elaborate.cpp +++ b/src/library/tactic/elaborate.cpp @@ -30,13 +30,14 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat } optional elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab, - proof_state & s, expr const & e, optional const & expected_type) { + proof_state & s, expr const & e, optional const & expected_type, + bool report_unassigned) { name_generator ngen = s.get_ngen(); substitution subst = s.get_subst(); goals const & gs = s.get_goals(); if (empty(gs)) return none_expr(); - auto ecs = elab(head(gs), ngen.mk_child(), e); + auto ecs = elab(head(gs), ngen.mk_child(), e, report_unassigned); expr new_e = ecs.first; buffer cs; to_buffer(ecs.second, cs); diff --git a/src/library/tactic/elaborate.h b/src/library/tactic/elaborate.h index 1ed8c74520..cb49bb808f 100644 --- a/src/library/tactic/elaborate.h +++ b/src/library/tactic/elaborate.h @@ -12,8 +12,13 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat /** \brief Function for elaborating expressions nested in tactics. Some tactics contain nested expression (aka pre-terms) that need to be elaborated. + The arguments are: + 1- goal that will provide the context where the expression will be elaborated + 2- name generator + 3- expression to be elaborated + 4- a flag indicating whether the elaborator should report unassigned/unsolved placeholders */ -typedef std::function(goal const &, name_generator const &, expr const &)> elaborate_fn; +typedef std::function(goal const &, name_generator const &, expr 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 @@ -26,5 +31,6 @@ typedef std::function(goal const &, name_generator const is not modified. */ optional elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab, - proof_state & s, expr const & e, optional const & expected_type = optional()); + proof_state & s, expr const & e, optional const & expected_type = optional(), + bool report_unassigned = false); } diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp index d6c7c38b0e..e1972cb34a 100644 --- a/src/library/tactic/exact_tactic.cpp +++ b/src/library/tactic/exact_tactic.cpp @@ -17,7 +17,8 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e) { if (!gs) return none_proof_state(); expr t = head(gs).get_type(); - if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t))) { + bool report_unassigned = true; + if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t), report_unassigned)) { goals const & gs = new_s.get_goals(); goal const & g = head(gs); expr new_p = g.abstract(*new_e);