refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic

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

library/tools/tactic.lean

@@ -45,6 +45,15 @@ builtin : expr
 
 opaque definition apply  (e : expr) : tactic := builtin
 opaque definition rename (a b : expr) : tactic := builtin
+opaque definition intro (e : expr) : tactic := builtin
+
+inductive expr_list : Type :=
+nil  : expr_list,
+cons : expr → expr_list → expr_list
+
+opaque definition intro_list (es : expr_list) : tactic := builtin
+notation `intros`   := intro_list expr_list.nil
+notation `intros` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := intro_list l
 
 opaque definition unfold      {B : Type} (b : B) : tactic := builtin
 opaque definition exact       {B : Type} (b : B) : tactic := builtin

src/emacs/lean-syntax.el

@@ -117,8 +117,8 @@
                "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]")) . 'font-lock-doc-face)
      (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
      ;; tactics
-     (,(rx word-start
-           (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "rename" "intros"
+     (,(rx (not (any "\.")) word-start
+           (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "rename" "intro" "intros"
                "back" "beta" "done" "exact" "repeat")
            word-end)
       . 'font-lock-constant-face)

src/frontends/lean/builtin_tactics.cpp

@@ -6,28 +6,11 @@ Author: Leonardo de Moura
 */
 #include <limits>
 #include "library/explicit.h"
-#include "library/tactic/intros_tactic.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/parse_table.h"
 
-#define LEAN_APPLY_RBP 16 // it should be bigger than `;` (and_then) precedence
-
 namespace lean {
-using notation::transition;
-using notation::mk_ext_action;
-
-static expr parse_intros(parser & p, unsigned, expr const *, pos_info const & pos) {
-    buffer<name> ns;
-    while (p.curr_is_identifier()) {
-        ns.push_back(p.get_name_val());
-        p.next();
-    }
-    return p.save_pos(mk_intros_tactic_macro(ns), pos);
-}
-
 void init_nud_tactic_table(parse_table & r) {
-    expr x0 = mk_var(0);
-    r = r.add({transition("intros", mk_ext_action(parse_intros))}, x0);
 }
 
 void initialize_builtin_tactics() {

src/frontends/lean/token_table.cpp

@@ -76,7 +76,7 @@ void init_token_table(token_table & t) {
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"local", 0},
-         {"intros", 0}, {nullptr, 0}};
+         {nullptr, 0}};
 
     char const * commands[] =
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion",

src/library/tactic/expr_to_tactic.cpp

@@ -116,9 +116,45 @@ expr const & get_tactic_expr_expr(expr const & e) {
     return macro_arg(e, 0);
 }
 
-void check_tactic_expr(expr const & e, char const * msg) {
+void check_tactic_expr(expr const & e, char const * error_msg) {
     if (!is_tactic_expr(e))
-        throw expr_to_tactic_exception(e, msg);
+        throw expr_to_tactic_exception(e, error_msg);
+}
+
+name const & tactic_expr_to_id(expr e, char const * error_msg) {
+    if (is_tactic_expr(e))
+        e = get_tactic_expr_expr(e);
+    if (is_constant(e))
+        return const_name(e);
+    else if (is_local(e))
+        return local_pp_name(e);
+    else
+        throw expr_to_tactic_exception(e, error_msg);
+}
+
+static expr * g_expr_list_cons = nullptr;
+static expr * g_expr_list_nil  = nullptr;
+
+void get_tactic_expr_list_elements(expr l, buffer<expr> & r, char const * error_msg) {
+    while (true) {
+        if (l == *g_expr_list_nil)
+            return;
+        if (!is_app(l) ||
+            !is_app(app_fn(l)) ||
+            app_fn(app_fn(l)) != *g_expr_list_cons ||
+            !is_tactic_expr(app_arg(app_fn(l))))
+            throw expr_to_tactic_exception(l, error_msg);
+        r.push_back(get_tactic_expr_expr(app_arg(app_fn(l))));
+        l = app_arg(l);
+    }
+}
+
+void get_tactic_id_list_elements(expr l, buffer<name> & r, char const * error_msg) {
+    buffer<expr> es;
+    get_tactic_expr_list_elements(l, es, error_msg);
+    for (unsigned i = 0; i < es.size(); i++) {
+        r.push_back(tactic_expr_to_id(es[i], error_msg));
+    }
 }
 
 /** \brief We use macros to wrap some builtin tactics that would not type check otherwise.
@@ -359,6 +395,9 @@ void initialize_expr_to_tactic() {
                                     return mk_tactic_expr(args[0]);
                                 });
 
+    g_expr_list_cons = new expr(mk_constant(name({"tactic", "expr_list", "cons"})));
+    g_expr_list_nil  = new expr(mk_constant(name({"tactic", "expr_list", "nil"})));
+
     g_tactic_opcode     = new std::string("TAC");
 
     g_tactic_macros     = new tactic_macros();

src/library/tactic/expr_to_tactic.h

@@ -32,6 +32,10 @@ bool is_tactic_expr(expr const & e);
 expr const & get_tactic_expr_expr(expr const & e);
 void check_tactic_expr(expr const & e, char const * msg);
 
+name const & tactic_expr_to_id(expr e, char const * error_msg);
+void get_tactic_expr_list_elements(expr l, buffer<expr> & r, char const * error_msg);
+void get_tactic_id_list_elements(expr l, buffer<name> & r, char const * error_msg);
+
 /**
    \brief Create an expression `by t`, where \c t is an expression of type `tactic`.
    This kind of expression only affects the elaborator, the kernel will reject

src/library/tactic/intros_tactic.cpp

@@ -75,32 +75,20 @@ tactic intros_tactic(list<name> _ns, bool relax_main_opaque) {
     return tactic01(fn);
 }
 
-static name * g_intros_tactic_name = nullptr;
-
-expr mk_intros_tactic_macro(buffer<name> const & ns) {
-    buffer<expr> args;
-    for (name const & n : ns) {
-        args.push_back(Const(n));
-    }
-    return mk_tactic_macro(*g_intros_tactic_name, args.size(), args.data());
-}
-
 void initialize_intros_tactic() {
-    g_intros_tactic_name = new name({"tactic", "intros"});
-    auto fn = [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
-        buffer<name> ns;
-        for (unsigned i = 0; i < macro_num_args(e); i++) {
-            expr const & arg = macro_arg(e, i);
-            if (!is_constant(arg))
-                throw expr_to_tactic_exception(e, "invalid 'intros' tactic, arguments must be identifiers");
-            ns.push_back(const_name(arg));
-        }
-        return intros_tactic(to_list(ns.begin(), ns.end()));
-    };
-    register_tactic_macro(*g_intros_tactic_name, fn);
+    register_tac(name({"tactic", "intro"}),
+                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                     name const & id = tactic_expr_to_id(app_arg(e), "invalid 'intro' tactic, argument must be an identifier");
+                     return intros_tactic(to_list(id));
+                 });
+    register_tac(name({"tactic", "intro_list"}),
+                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                     buffer<name> ns;
+                     get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intros' tactic, arguments must be identifiers");
+                     return intros_tactic(to_list(ns.begin(), ns.end()));
+                 });
 }
 
 void finalize_intros_tactic() {
-    delete g_intros_tactic_name;
 }
 }

src/library/tactic/intros_tactic.h

@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic.h"
 namespace lean {
 tactic intros_tactic(list<name> ns, bool relax_main_opaque = true);
-expr mk_intros_tactic_macro(buffer<name> const & ns);
 void initialize_intros_tactic();
 void finalize_intros_tactic();
 }

src/library/tactic/rename_tactic.cpp

@@ -49,15 +49,8 @@ expr mk_rename_tactic_macro(name const & from, name const & to) {
     return mk_tactic_macro(*g_rename_tactic_name, 2, args);
 }
 
-static name const & get_rename_arg(expr const & _e) {
-    check_tactic_expr(_e, "invalid 'rename' tactic, arguments must be identifiers");
-    expr const & e = get_tactic_expr_expr(_e);
-    if (is_constant(e))
-        return const_name(e);
-    else if (is_local(e))
-        return local_pp_name(e);
-    else
-        throw expr_to_tactic_exception(e, "invalid 'rename' tactic, arguments must be identifiers");
+static name const & get_rename_arg(expr const & e) {
+    return tactic_expr_to_id(e, "invalid 'rename' tactic, arguments must be identifiers");
 }
 
 void initialize_rename_tactic() {

tests/lean/run/intros.lean

@@ -2,15 +2,15 @@ import logic tools.tactic
 open tactic
 
 theorem tst1 (a b : Prop) : a → b → b :=
-by intros Ha; intros Hb; apply Hb
+by intro Ha; intro Hb; apply Hb
 
 theorem tst2 (a b : Prop) : a → b → a ∧ b :=
-by intros Ha; intros Hb; apply and.intro; apply Hb; apply Ha
+by intro Ha; intro Hb; apply and.intro; apply Hb; apply Ha
 
 theorem tst3 (a b : Prop) : a → b → a ∧ b :=
 begin
- intros Ha,
- intros Hb,
+ intro Ha,
+ intro Hb,
  apply and.intro,
  apply Hb,
  apply Ha
@@ -18,7 +18,7 @@ end
 
 theorem tst4 (a b : Prop) : a → b → a ∧ b :=
 begin
-  intros Ha Hb,
+  intros (Ha, Hb),
   apply and.intro,
   apply Hb,
   apply Ha