feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics

library/tools/tactic.lean

@@ -36,6 +36,15 @@ opaque definition state       : tactic := builtin
 opaque definition fail        : tactic := builtin
 opaque definition id          : tactic := builtin
 opaque definition beta        : tactic := builtin
+
+-- This is just a trick to embed expressions into tactics.
+-- The nested expressions are "raw". They tactic should
+-- elaborate them when it is executed.
+inductive expr : Type :=
+builtin : expr
+
+opaque definition apply (e : expr) : tactic := builtin
+
 opaque definition unfold      {B : Type} (b : B) : tactic := builtin
 opaque definition exact       {B : Type} (b : B) : tactic := builtin
 opaque definition trace       (s : string) : tactic := builtin

src/frontends/lean/builtin_exprs.cpp

@@ -115,6 +115,7 @@ static expr parse_placeholder(parser & p, unsigned, expr const *, pos_info const
 }
 
 static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
+    parser::no_undef_id_error_scope scope(p);
     expr t = p.parse_expr();
     return p.mk_by(t, pos);
 }
@@ -125,6 +126,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
     optional<expr> pre_tac = get_begin_end_pre_tactic(p.env());
     buffer<expr> tacs;
     bool first = true;
+    parser::no_undef_id_error_scope scope(p);
     while (!p.curr_is_token(get_end_tk())) {
         if (first)
             first = false;

src/frontends/lean/builtin_tactics.cpp

@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #include <limits>
 #include "library/explicit.h"
-#include "library/tactic/apply_tactic.h"
 #include "library/tactic/rename_tactic.h"
 #include "library/tactic/intros_tactic.h"
 #include "frontends/lean/parser.h"
@@ -18,12 +17,6 @@ namespace lean {
 using notation::transition;
 using notation::mk_ext_action;
 
-static expr parse_apply(parser & p, unsigned, expr const *, pos_info const & pos) {
-    parser::no_undef_id_error_scope scope(p);
-    expr e = p.parse_expr(LEAN_APPLY_RBP);
-    return p.save_pos(mk_apply_tactic_macro(e), pos);
-}
-
 static expr parse_rename(parser & p, unsigned, expr const *, pos_info const & pos) {
     name from = p.check_id_next("invalid 'rename' tactic, identifier expected");
     name to   = p.check_id_next("invalid 'rename' tactic, identifier expected");
@@ -41,7 +34,6 @@ static expr parse_intros(parser & p, unsigned, expr const *, pos_info const & po
 
 void init_nud_tactic_table(parse_table & r) {
     expr x0 = mk_var(0);
-    r = r.add({transition("apply",  mk_ext_action(parse_apply))}, x0);
     r = r.add({transition("rename", mk_ext_action(parse_rename))}, x0);
     r = r.add({transition("intros", mk_ext_action(parse_intros))}, x0);
 }

src/frontends/lean/elaborator.cpp

@@ -553,15 +553,20 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
     }
     constraint_seq a_cs;
     expr d_type = binding_domain(f_type);
-    expr a      = visit_expecting_type_of(app_arg(e), d_type, a_cs);
-    expr a_type = infer_type(a, a_cs);
-    expr r      = mk_app(f, a, e.get_tag());
-
-    justification j = mk_app_justification(r, a, d_type, a_type);
-    auto new_a_cs   = ensure_has_type(a, a_type, d_type, j, m_relax_main_opaque);
-    expr new_a      = new_a_cs.first;
-    cs += f_cs + new_a_cs.second + a_cs;
-    return update_app(r, app_fn(r), new_a);
+    if (d_type == get_tactic_expr_type()) {
+        expr r = mk_app(f, mk_tactic_expr(app_arg(e)), e.get_tag());
+        cs += f_cs + a_cs;
+        return r;
+    } else {
+        expr a          = visit_expecting_type_of(app_arg(e), d_type, a_cs);
+        expr a_type     = infer_type(a, a_cs);
+        expr r          = mk_app(f, a, e.get_tag());
+        justification j = mk_app_justification(r, a, d_type, a_type);
+        auto new_a_cs   = ensure_has_type(a, a_type, d_type, j, m_relax_main_opaque);
+        expr new_a      = new_a_cs.first;
+        cs += f_cs + new_a_cs.second + a_cs;
+        return update_app(r, app_fn(r), new_a);
+    }
 }
 
 expr elaborator::visit_placeholder(expr const & e, constraint_seq & cs) {

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},
-         {"apply", 0}, {"rename", 0}, {"intros", 0}, {nullptr, 0}};
+         {"rename", 0}, {"intros", 0}, {nullptr, 0}};
 
     char const * commands[] =
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion",

src/library/tactic/apply_tactic.cpp

@@ -139,11 +139,11 @@ expr mk_apply_tactic_macro(expr const & e) {
 
 void initialize_apply_tactic() {
     g_apply_tactic_name = new name({"tactic", "apply"});
-    auto fn = [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
-        check_macro_args(e, 1, "invalid 'apply' tactic, it must have one argument");
-        return apply_tactic(fn, macro_arg(e, 0));
-    };
-    register_tactic_macro(*g_apply_tactic_name, fn);
+    register_tac(*g_apply_tactic_name,
+                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                     check_tactic_expr(app_arg(e), "invalid 'apply' tactic, invalid argument");
+                     return apply_tactic(fn, get_tactic_expr_expr(app_arg(e)));
+                 });
 
     register_simple_tac(name({"tactic", "eassumption"}),
                         []() { return eassumption_tactic(); });

src/library/tactic/expr_to_tactic.cpp

@@ -57,14 +57,70 @@ bool has_tactic_decls(environment const & env) {
     }
 }
 
+static expr * g_tactic_expr_type = nullptr;
+static expr * g_tactic_expr_builtin = nullptr;
+
+expr const & get_tactic_expr_type() { return *g_tactic_expr_type; }
+expr const & get_tactic_expr_builtin() { return *g_tactic_expr_builtin; }
+
+static name * g_tactic_expr_name = nullptr;
+static std::string * g_tactic_expr_opcode = nullptr;
+
 static name * g_tactic_name = nullptr;
 static std::string * g_tactic_opcode = nullptr;
 
+name const & get_tactic_expr_name() { return *g_tactic_expr_name; }
+std::string const & get_tactic_expr_opcode() { return *g_tactic_expr_opcode; }
+
 name const & get_tactic_name() { return *g_tactic_name; }
 std::string const & get_tactic_opcode() { return *g_tactic_opcode; }
 
 LEAN_THREAD_VALUE(bool, g_unfold_tactic_macros, true);
 
+class tactic_expr_macro_definition_cell : public macro_definition_cell {
+public:
+    tactic_expr_macro_definition_cell() {}
+    virtual name get_name() const { return get_tactic_expr_name(); }
+    virtual pair<expr, constraint_seq> get_type(expr const &, extension_context &) const {
+        return mk_pair(get_tactic_expr_type(), constraint_seq());
+    }
+    virtual optional<expr> expand(expr const &, extension_context &) const {
+        // Remark: small hack for conditionally expanding tactic expr macros.
+        // When type checking a macro definition, we want to unfold it,
+        // otherwise the kernel will not accept it.
+        // When converting it to a tactic object, we don't want to unfold it.
+        // The procedure expr_to_tactic temporarily sets g_unfold_tactic_macros to false.
+        // This is a thread local storage. So, there is no danger.
+        if (g_unfold_tactic_macros)
+            return some_expr(get_tactic_expr_builtin());
+        else
+            return none_expr();
+    }
+    virtual void write(serializer & s) const {
+        s.write_string(get_tactic_expr_opcode());
+    }
+};
+
+static macro_definition * g_tactic_expr_macro = nullptr;
+
+expr mk_tactic_expr(expr const & e) {
+    return mk_macro(*g_tactic_expr_macro, 1, &e, e.get_tag());
+}
+
+bool is_tactic_expr(expr const & e) {
+    return is_macro(e) && macro_def(e).get_name() == get_tactic_expr_name();
+}
+
+expr const & get_tactic_expr_expr(expr const & e) {
+    lean_assert(is_tactic_expr(e));
+    return macro_arg(e, 0);
+}
+
+void check_tactic_expr(expr const & e, char const * msg) {
+    if (!is_tactic_expr(e))
+        throw expr_to_tactic_exception(e, msg);
+}
+
 /** \brief We use macros to wrap some builtin tactics that would not type check otherwise.
     Example: in the tactic `apply t`, `t` is a pre-term (i.e., a term before elaboration).
     Moreover its context depends on the goal it is applied to.
@@ -289,6 +345,20 @@ void initialize_expr_to_tactic() {
     g_map               = new expr_to_tactic_map();
 
     g_tactic_name       = new name("tactic");
+
+    g_tactic_expr_type    = new expr(mk_constant(name(*g_tactic_name, "expr")));
+    g_tactic_expr_builtin = new expr(mk_constant(name(const_name(*g_tactic_expr_type), "builtin")));
+    g_tactic_expr_name   = new name("tactic-expr");
+    g_tactic_expr_opcode = new std::string("TACE");
+    g_tactic_expr_macro  = new macro_definition(new tactic_expr_macro_definition_cell());
+
+    register_macro_deserializer(*g_tactic_expr_opcode,
+                                [](deserializer &, unsigned num, expr const * args) {
+                                    if (num != 1)
+                                        throw corrupted_stream_exception();
+                                    return mk_tactic_expr(args[0]);
+                                });
+
     g_tactic_opcode     = new std::string("TAC");
 
     g_tactic_macros     = new tactic_macros();
@@ -364,6 +434,11 @@ void initialize_expr_to_tactic() {
 }
 
 void finalize_expr_to_tactic() {
+    delete g_tactic_expr_type;
+    delete g_tactic_expr_builtin;
+    delete g_tactic_expr_name;
+    delete g_tactic_expr_opcode;
+    delete g_tactic_expr_macro;
     delete g_fixpoint_tac;
     delete g_builtin_tac;
     delete g_tac_type;

src/library/tactic/expr_to_tactic.h

@@ -26,6 +26,12 @@ bool has_tactic_decls(environment const & env);
 */
 tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p);
 
+expr const & get_tactic_expr_type();
+expr mk_tactic_expr(expr const & e);
+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);
+
 /**
    \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

tests/lean/run/beginend2.lean

@@ -6,7 +6,7 @@ open path (induction_on)
 definition concat_whisker2 {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') :
   (whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') :=
 begin
-  apply induction_on b,
-  apply induction_on a,
-  apply (concat_1p _)⁻¹,
+  apply (induction_on b),
+  apply (induction_on a),
+  apply ((concat_1p _)⁻¹),
 end