refactor(library/tactic): add namespace 'tactic', improve expr_to_tactic failure error message

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

library/standard/tactic.lean

@@ -3,6 +3,7 @@
 -- Author: Leonardo de Moura
 import logic
 
+namespace tactic
 -- This is just a trick to embed the 'tactic language' as a
 -- Lean expression. We should view 'tactic' as automation
 -- that when execute produces a term.
@@ -14,19 +15,19 @@ inductive tactic : Type :=
 -- uses them when converting Lean expressions into actual tactic objects.
 -- The bultin 'by' construct triggers the process of converting a
 -- a term of type 'tactic' into a tactic that sythesizes a term
-definition then_tac   (t1 t2 : tactic) : tactic := tactic_value
-definition orelse_tac (t1 t2 : tactic) : tactic := tactic_value
-definition repeat_tac (t : tactic) : tactic := tactic_value
-definition now_tac    : tactic := tactic_value
-definition exact_tac  : tactic := tactic_value
-definition state_tac  : tactic := tactic_value
-definition fail_tac   : tactic := tactic_value
-definition id_tac     : tactic := tactic_value
-definition beta_tac   : tactic := tactic_value
+definition and_then   (t1 t2 : tactic) : tactic := tactic_value
+definition or_else    (t1 t2 : tactic) : tactic := tactic_value
+definition repeat     (t : tactic) : tactic := tactic_value
+definition now        : tactic := tactic_value
+definition exact      : tactic := tactic_value
+definition state      : tactic := tactic_value
+definition fail       : tactic := tactic_value
+definition id         : tactic := tactic_value
+definition beta       : tactic := tactic_value
 definition apply      {B : Type} (b : B) : tactic := tactic_value
-definition unfold_tac {B : Type} (b : B) : tactic := tactic_value
-
-infixl `;`:200         := then_tac
-infixl `|`:100         := orelse_tac
-notation `!`:max t:max := repeat_tac t
+definition unfold     {B : Type} (b : B) : tactic := tactic_value
 
+infixl `;`:200         := and_then
+infixl `|`:100         := or_else
+notation `!`:max t:max := repeat t
+end

src/frontends/lean/elaborator.cpp

@@ -623,10 +623,22 @@ public:
             });
     }
 
+    format pp_indent_expr(expr const & e) {
+        return ::lean::pp_indent_expr(m_ios.get_formatter(), m_env, m_ios.get_options(), e);
+    }
+
     optional<tactic> get_tactic_for(substitution const & substitution, expr const & mvar) {
         if (auto it = m_tactic_hints.find(mlocal_name(mvar))) {
             expr pre_tac = substitution.instantiate_metavars_wo_jst(*it);
-            return optional<tactic>(expr_to_tactic(m_env, pre_tac, m_pos_provider));
+            try {
+                return optional<tactic>(expr_to_tactic(m_env, pre_tac, m_pos_provider));
+            } catch (expr_to_tactic_exception & ex) {
+                regular out(m_env, m_ios);
+                display_error_pos(out, m_pos_provider, mvar);
+                out << " " << ex.what();
+                out << pp_indent_expr(pre_tac) << endl << "failed at:" << pp_indent_expr(ex.get_expr()) << endl;
+                return optional<tactic>();
+            }
         } else {
             // TODO(Leo): m_env tactic hints
             return optional<tactic>();
@@ -689,9 +701,9 @@ public:
     static format pp_type_mismatch(formatter const & fmt, environment const & env, options const & opts,
                             expr const & expected_type, expr const & given_type) {
         format r("type mismatch, expected type");
-        r += pp_indent_expr(fmt, env, opts, expected_type);
+        r += ::lean::pp_indent_expr(fmt, env, opts, expected_type);
         r += compose(line(), format("given type:"));
-        r += pp_indent_expr(fmt, env, opts, given_type);
+        r += ::lean::pp_indent_expr(fmt, env, opts, given_type);
         return r;
     }
 

src/library/tactic/expr_to_tactic.cpp

@@ -38,20 +38,20 @@ tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider
                 return expr_to_tactic(env, v, p);
             }
         }
-        throw exception("failed to convert expression into tactic");
+        throw expr_to_tactic_exception(e, "failed to convert expression into tactic");
     } else if (is_lambda(f)) {
         buffer<expr> locals;
         get_app_rev_args(e, locals);
         return expr_to_tactic(env, apply_beta(f, locals.size(), locals.data()), p);
     } else {
-        throw exception("failed to convert expression into tactic");
+        throw expr_to_tactic_exception(e, "failed to convert expression into tactic");
     }
 }
 
 register_simple_tac::register_simple_tac(name const & n, std::function<tactic()> f) {
     register_expr_to_tactic(n, [=](environment const &, expr const & e, pos_info_provider const *) {
             if (!is_constant(e))
-                throw exception("invalid constant tactic");
+                throw expr_to_tactic_exception(e, "invalid constant tactic");
             return f();
         });
 }
@@ -61,7 +61,7 @@ register_bin_tac::register_bin_tac(name const & n, std::function<tactic(tactic c
             buffer<expr> args;
             get_app_args(e, args);
             if (args.size() != 2)
-                throw exception("invalid binary tactic, it must have two arguments");
+                throw expr_to_tactic_exception(e, "invalid binary tactic, it must have two arguments");
             return f(expr_to_tactic(env, args[0], p),
                      expr_to_tactic(env, args[1], p));
         });
@@ -72,29 +72,30 @@ register_unary_tac::register_unary_tac(name const & n, std::function<tactic(tact
             buffer<expr> args;
             get_app_args(e, args);
             if (args.size() != 1)
-                throw exception("invalid unary tactic, it must have one argument");
+                throw expr_to_tactic_exception(e, "invalid unary tactic, it must have one argument");
             return f(expr_to_tactic(env, args[0], p));
         });
 }
 
-static register_simple_tac reg_id(name("id_tac"), []() { return id_tactic(); });
-static register_simple_tac reg_now(name("now_tac"), []() { return now_tactic(); });
-static register_simple_tac reg_exact(name("exact_tac"), []() { return assumption_tactic(); });
-static register_simple_tac reg_fail(name("fail_tac"), []() { return fail_tactic(); });
-static register_simple_tac reg_beta(name("beta_tac"), []() { return beta_tactic(); });
-static register_bin_tac reg_then(name("then_tac"), [](tactic const & t1, tactic const & t2) { return then(t1, t2); });
-static register_bin_tac reg_orelse(name("orelse_tac"), [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
-static register_unary_tac reg_repeat(name("repeat_tac"), [](tactic const & t1) { return repeat(t1); });
-static register_tac reg_state(name("state_tac"), [](environment const &, expr const & e, pos_info_provider const * p) {
+static name g_tac("tactic");
+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_exact(name(g_tac, "exact"), []() { return assumption_tactic(); });
+static register_simple_tac reg_fail(name(g_tac, "fail"), []() { return fail_tactic(); });
+static register_simple_tac reg_beta(name(g_tac, "beta"), []() { return beta_tactic(); });
+static register_bin_tac reg_then(name(g_tac, "and_then"), [](tactic const & t1, tactic const & t2) { return then(t1, t2); });
+static register_bin_tac reg_orelse(name(g_tac, "or_else"), [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
+static register_unary_tac reg_repeat(name(g_tac, "repeat"), [](tactic const & t1) { return repeat(t1); });
+static register_tac reg_state(name(g_tac, "state"), [](environment const &, expr const & e, pos_info_provider const * p) {
         if (p)
             return trace_state_tactic(std::string(p->get_file_name()), p->get_pos_info(e));
         else
             return trace_state_tactic("unknown", mk_pair(0, 0));
     });
-static register_tac reg_apply(name("apply"), [](environment const &, expr const & e, pos_info_provider const *) {
+static register_tac reg_apply(name(g_tac, "apply"), [](environment const &, expr const & e, pos_info_provider const *) {
         return apply_tactic(app_arg(e));
     });
-static register_tac reg_unfold(name("unfold_tac"), [](environment const &, expr const & e, pos_info_provider const *) {
+static register_tac reg_unfold(name(g_tac, "unfold"), [](environment const &, expr const & e, pos_info_provider const *) {
         expr id = get_app_fn(app_arg(e));
         if (!is_constant(id))
             return fail_tactic();

src/library/tactic/expr_to_tactic.h

@@ -9,6 +9,13 @@ 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; }
+};
+
 typedef std::function<tactic(environment const & env, expr const & e, pos_info_provider const *)> expr_to_tactic_fn;
 void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn);
 struct register_tac {

tests/lean/run/have5.lean

@@ -1,11 +1,12 @@
 import standard
+using tactic
 variables a b c d : Bool
 axiom Ha : a
 axiom Hb : b
 axiom Hc : c
 print raw
-  have H1 : a, by exact_tac,
-  then have H2 : b, by exact_tac,
-  have H3 : c, by exact_tac,
-  then have H4 : d, by exact_tac,
+  have H1 : a, by exact,
+  then have H2 : b, by exact,
+  have H3 : c, by exact,
+  then have H4 : d, by exact,
   H4

tests/lean/run/t8.lean

@@ -1,2 +1,3 @@
 import standard
-print raw (by exact_tac)
+using tactic
+print raw (by exact)

tests/lean/run/tactic1.lean

@@ -1,5 +1,5 @@
-import logic
-import tactic
+import standard
+using tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
-:= by exact_tac
+:= by exact

tests/lean/run/tactic2.lean

@@ -1,7 +1,7 @@
-import logic
-import tactic
+import standard
+using tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
-:= by state_tac; exact_tac
+:= by state; exact
 
 check tst

tests/lean/run/tactic3.lean

@@ -1,10 +1,9 @@
-import logic
-import tactic
+import standard
 using tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
-:= by state_tac; now_tac  |
-      state_tac; fail_tac |
-      exact_tac
+:= by state; now  |
+      state; fail |
+      exact
 
 check tst

tests/lean/run/tactic4.lean

@@ -1,11 +1,12 @@
 import standard
+using tactic (renaming id->id_tac)
 
 definition id {A : Type} (a : A) := a
 
-definition simple_tac {A : Bool} : tactic
-:= unfold_tac @id.{1}; exact_tac
+definition simple {A : Bool} : tactic
+:= unfold @id.{1}; exact
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by simple_tac
+:= by simple
 
 check tst

tests/lean/run/tactic5.lean

@@ -1,8 +1,9 @@
 import standard
+using tactic (renaming id->id_tac)
 
 definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by !(unfold_tac @id; state_tac); exact_tac
+:= by !(unfold @id; state); exact
 
 check tst

tests/lean/run/tactic6.lean

@@ -1,8 +1,9 @@
 import standard
+using tactic (renaming id->id_tac)
 
 definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by unfold_tac id; exact_tac
+:= by unfold id; exact
 
 check tst