feat(frontends/parser): improve error message when an apply tactic refers a local constant that is not marked as [fact]

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/elaborator.cpp

@@ -665,18 +665,24 @@ public:
                 expr type = m_tc.infer(*meta);
                 proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child());
                 if (optional<tactic> t = get_tactic_for(subst, mvar)) {
-                    proof_state_seq seq = (*t)(m_env, m_ios, ps);
-                    if (auto r = seq.pull()) {
-                        subst = r->first.get_subst();
-                        expr v = subst.instantiate_metavars_wo_jst(mvar);
-                        if (has_metavar(v)) {
-                            display_unsolved_proof_state(mvar, r->first, "unsolved subgoals");
+                    try {
+                        proof_state_seq seq = (*t)(m_env, m_ios, ps);
+                        if (auto r = seq.pull()) {
+                            subst = r->first.get_subst();
+                            expr v = subst.instantiate_metavars_wo_jst(mvar);
+                            if (has_metavar(v)) {
+                                display_unsolved_proof_state(mvar, r->first, "unsolved subgoals");
+                            } else {
+                                subst = subst.assign(mlocal_name(mvar), v);
+                            }
                         } else {
-                            subst = subst.assign(mlocal_name(mvar), v);
+                            // tactic failed to produce any result
+                            display_unsolved_proof_state(mvar, ps, "tactic failed");
                         }
-                    } else {
-                        // tactic failed to produce any result
-                        display_unsolved_proof_state(mvar, ps, "tactic failed");
+                    } catch (tactic_exception & ex) {
+                        regular out(m_env, m_ios);
+                        display_error_pos(out, m_pos_provider, ex.get_expr());
+                        out << " tactic failed: " << ex.what() << "\n";
                     }
                 }
             }

src/library/tactic/apply_tactic.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <utility>
 #include "util/lazy_list_fn.h"
+#include "util/sstream.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
@@ -59,6 +60,18 @@ void collect_simple_meta(expr const & e, buffer<expr> & metas) {
         });
 }
 
+/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */
+void check_has_no_local(expr const & v, expr const & e) {
+    if (has_local(v)) {
+        for_each(v, [&](expr const & l, unsigned) {
+                if (is_local(l))
+                    throw tactic_exception(e, sstream() << "apply tactic contains reference to local '" << local_pp_name(l)
+                                           << "' which is not marked as [fact], so it is not visible to tactics");
+                return has_local(l);
+            });
+    }
+}
+
 tactic apply_tactic(expr const & _e) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();
@@ -86,7 +99,9 @@ tactic apply_tactic(expr const & _e) {
                     name_generator new_ngen(ngen);
                     type_checker tc(env, new_ngen.mk_child());
                     expr new_e = subst.instantiate_metavars_wo_jst(e);
-                    substitution new_subst = subst.assign(g.get_name(), g.abstract(new_e));
+                    expr new_p = g.abstract(new_e);
+                    check_has_no_local(new_p, _e);
+                    substitution new_subst = subst.assign(g.get_name(), new_p);
                     buffer<expr> metas;
                     collect_simple_meta(new_e, metas);
                     goals new_gs = tail_gs;

src/library/tactic/expr_to_tactic.h

@@ -9,11 +9,8 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic.h"
 
 namespace lean {
-class expr_to_tactic_exception : public exception {
-    expr m_expr;
-public:
-    expr_to_tactic_exception(expr const & e, char const * msg):exception(msg), m_expr(e) {}
-    expr const & get_expr() const { return m_expr; }
+class expr_to_tactic_exception : public tactic_exception {
+public: expr_to_tactic_exception(expr const & e, char const * msg):tactic_exception(e, msg) {}
 };
 
 typedef std::function<tactic(type_checker & tc, expr const & e, pos_info_provider const *)> expr_to_tactic_fn;

src/library/tactic/tactic.cpp

@@ -19,6 +19,9 @@ Author: Leonardo de Moura
 #include "library/io_state_stream.h"
 
 namespace lean {
+tactic_exception::tactic_exception(expr const & e, char const * msg):exception(msg), m_expr(e) {}
+tactic_exception::tactic_exception(expr const & e, sstream const & strm):exception(strm), m_expr(e) {}
+
 tactic tactic01(std::function<optional<proof_state>(environment const &, io_state const & ios, proof_state const &)> f) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             return mk_proof_state_seq([=]() {

src/library/tactic/tactic.h

@@ -14,6 +14,14 @@ Author: Leonardo de Moura
 #include "library/tactic/proof_state.h"
 
 namespace lean {
+class tactic_exception : public exception {
+    expr m_expr;
+public:
+    tactic_exception(expr const & e, char const * msg);
+    tactic_exception(expr const & e, sstream const & strm);
+    expr const & get_expr() const { return m_expr; }
+};
+
 typedef lazy_list<proof_state> proof_state_seq;
 
 typedef std::function<proof_state_seq(environment const &, io_state const & ios, proof_state const &)> tactic;

tests/lean/run/tactic11.lean

@@ -1,8 +1,9 @@
-import logic
+import standard
+using tactic
 
-exit -- TODO
 theorem tst (a b : Bool) (H : a ↔ b) : b ↔ a
-:= have H1 [fact] : a → b, from iff_elim_left H,
-   by (apply iff_intro,
-       assume Hb, iff_mp_right H Hb,
-       assume Ha, H1 Ha)
+:= have H1 [fact] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics
+   from iff_elim_left H,
+   by ⟦ iff_intro ⟧;
+      ⟦ assume Hb, iff_mp_right H Hb ⟧;
+      ⟦ assume Ha, H1 Ha ⟧