From 138267b53a79b95932a728d8b51cf908d6c54e80 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Jul 2014 18:58:32 -0700
Subject: [PATCH] feat(frontends/lean/elaborator) add trick for improving error
 messages when mixing tactics, elaboration and exact tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/elaborator.cpp     | 15 +++++++++++++++
 src/library/tactic/expr_to_tactic.cpp |  4 +++-
 src/library/tactic/expr_to_tactic.h   |  2 ++
 3 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index eafc4faa7..fdce77793 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -640,10 +640,25 @@ public:
         }
     }
 
+    // For each occurrence of \c exact_tac in \c pre_tac, display its unassigned metavariables.
+    // This is a trick to improve the quality of the error messages.
+    void check_exact_tacs(expr const & pre_tac, substitution const & s) {
+        for_each(pre_tac, [&](expr const & e, unsigned) {
+                expr const & f = get_app_fn(e);
+                if (is_constant(f) && const_name(f) == get_exact_tac_name()) {
+                    display_unassigned_mvars(e, s);
+                    return false;
+                } else {
+                    return true;
+                }
+            });
+    }
+
     optional<expr> get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited) {
         if (auto it = m_tactic_hints.find(mlocal_name(mvar))) {
             expr pre_tac = subst.instantiate(*it);
             pre_tac = solve_unassigned_mvars(subst, pre_tac, visited);
+            check_exact_tacs(pre_tac, subst);
             return some_expr(pre_tac);
         } else {
             // TODO(Leo): m_env tactic hints
diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp
index fce79abd1..1ea3c841c 100644
--- a/src/library/tactic/expr_to_tactic.cpp
+++ b/src/library/tactic/expr_to_tactic.cpp
@@ -81,6 +81,8 @@ register_unary_tac::register_unary_tac(name const & n, std::function<tactic(tact
 }
 
 static name g_tac("tactic");
+static name g_exact_tac_name(g_tac, "exact");
+name const & get_exact_tac_name() { return g_exact_tac_name; }
 static register_simple_tac reg_id(name(g_tac, "id"), []() { return id_tactic(); });
 static register_simple_tac reg_now(name(g_tac, "now"), []() { return now_tactic(); });
 static register_simple_tac reg_assumption(name(g_tac, "assumption"), []() { return assumption_tactic(); });
@@ -110,7 +112,7 @@ static register_tac reg_trace(name(g_tac, "trace"), [](type_checker & tc, expr c
 static register_tac reg_apply(name(g_tac, "apply"), [](type_checker &, expr const & e, pos_info_provider const *) {
         return apply_tactic(app_arg(e));
     });
-static register_tac reg_exact(name(g_tac, "exact"), [](type_checker &, expr const & e, pos_info_provider const *) {
+static register_tac reg_exact(g_exact_tac_name, [](type_checker &, expr const & e, pos_info_provider const *) {
         return exact_tactic(app_arg(e));
     });
 static register_tac reg_unfold(name(g_tac, "unfold"), [](type_checker &, expr const & e, pos_info_provider const *) {
diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h
index 447896454..8099baaeb 100644
--- a/src/library/tactic/expr_to_tactic.h
+++ b/src/library/tactic/expr_to_tactic.h
@@ -28,6 +28,8 @@ struct register_unary_tac {
     register_unary_tac(name const & n, std::function<tactic(tactic const &)> f);
 };
 
+name const & get_exact_tac_name();
+
 tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const *p);
 expr mk_by(expr const & e);
 bool is_by(expr const & e);