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);