feat(frontends/lean): {! ... !} takes a list of pre-terms

library/init/meta/hole_command.lean

@@ -8,21 +8,21 @@ import init.meta.tactic
 
 /--
 The front-end (e.g., Emacs, VS Code) can invoke commands for holes {! ... !} in
-a declaration. A command is a tactic that takes the optional pre-term in the
+a declaration. A command is a tactic that takes zero or more pre-terms in the
 hole, and returns a list of expressions. The Lean server converts the list
-into a list of strings using the pretty printer, and return it to the front-end.
+into a list of strings using the pretty printer, and returns it to the front-end.
 Each string represents a different way to fill the hole.
-The front-end is responsible for replacing the hole with the user selected alternative.
+The front-end is responsible for replacing the hole with the string/alternative selected by the user.
 
 This infra-structure can be use to implement auto-fill and/or refine commands.
 
 An action may return an empty list. This is useful for actions that just return
-information such as the type of an expression, its normal form, etc.
+information such as: the type of an expression, its normal form, etc.
 -/
 meta structure hole_command :=
 (name   : string)
 (descr  : string)
-(action : option pexpr → tactic (list expr))
+(action : list pexpr → tactic (list expr))
 
 open tactic
 
@@ -30,8 +30,8 @@ open tactic
 meta def infer_type_cmd : hole_command :=
 { name   := "Infer",
   descr  := "Infer type of the expression in the hole",
-  action := λ o, do
-    some p ← return o | fail "Infer command, hole does not contain a term",
+  action := λ ps, do
+    [p] ← return ps | fail "Infer command failed, the hole must contain a single term",
     e ← to_expr p,
     t ← infer_type e,
     trace t,

src/frontends/lean/builtin_exprs.cpp

@@ -988,23 +988,44 @@ expr mk_hole(parser & p, expr const & e, pos_info const & begin_pos, pos_info co
     return mk_annotation_with_pos(p, *g_begin_hole, mk_annotation_with_pos(p, *g_end_hole, e, end_pos), begin_pos);
 }
 
-bool is_hole(expr const & e) { return is_annotation(e, *g_begin_hole); }
+bool is_hole(expr const & e) {
+    return is_annotation(e, *g_begin_hole);
+}
+
+std::tuple<expr, optional<pos_info>, optional<pos_info>> get_hole_info(expr const & e) {
+    lean_assert(is_hole(e));
+    optional<pos_info> begin_pos, end_pos;
+    if (get_pos_info_provider()) {
+        begin_pos = get_pos_info_provider()->get_pos_info(e);
+        end_pos   = get_pos_info_provider()->get_pos_info(get_annotation_arg(e));
+    }
+    expr args = get_annotation_arg(get_annotation_arg(e));
+    return std::make_tuple(args, begin_pos, end_pos);
+}
+
+expr update_hole_args(expr const & e, expr const & new_args) {
+    lean_assert(is_hole(e));
+    return copy_annotations(e, new_args);
+}
 
 static expr parse_hole(parser_state & p, unsigned, expr const *, pos_info const & begin_pos) {
-    expr e;
-    if (!p.curr_is_token(get_rcurlybang_tk())) {
+    buffer<expr> ps;
+    while (!p.curr_is_token(get_rcurlybang_tk())) {
+        expr e;
         if (p.in_quote()) {
             e = p.parse_expr();
         } else {
             parser_state::quote_scope scope(p, false);
             e = p.parse_expr();
         }
-    } else {
-        e = p.save_pos(mk_expr_placeholder(), begin_pos);;
+        ps.push_back(copy_tag(e, mk_pexpr_quote(e)));
+        if (!p.curr_is_token(get_comma_tk()))
+            break;
+        p.next();
     }
     auto end_pos = p.pos();
     p.check_token_next(get_rcurlybang_tk(), "invalid hole, `!}` expected");
-    expr r = mk_hole(p, e, begin_pos, end_pos);
+    expr r = mk_hole(p, mk_lean_list(ps), begin_pos, end_pos);
     return r;
 }
 

src/frontends/lean/builtin_exprs.h

@@ -21,6 +21,8 @@ parse_table get_builtin_led_table();
 bool is_infix_function(expr const & e);
 
 bool is_hole(expr const & e);
+std::tuple<expr, optional<pos_info>, optional<pos_info>> get_hole_info(expr const & e);
+expr update_hole_args(expr const & e, expr const & new_args);
 
 void initialize_builtin_exprs();
 void finalize_builtin_exprs();

src/frontends/lean/elaborator.cpp

@@ -2055,8 +2055,13 @@ expr elaborator::visit_by(expr const & e, optional<expr> const & expected_type)
 expr elaborator::visit_hole(expr const & e, optional<expr> const & expected_type) {
     lean_assert(is_hole(e));
     expr const & ref = e;
+    expr args; optional<pos_info> begin_pos, end_pos;
+    std::tie(args, begin_pos, end_pos) = get_hole_info(e);
+    expr args_type   = mk_app(mk_constant(get_list_name(), {mk_level_zero()}),
+                              mk_app(mk_constant(get_expr_name()), mk_constant(get_bool_ff_name())));
+    expr new_args    = ground_uvars(strict_visit(args, some_expr(args_type)));
     expr mvar        = mk_metavar(expected_type, ref);
-    m_holes          = cons(mk_pair(mvar, e), m_holes);
+    m_holes          = cons(mk_pair(mvar, update_hole_args(e, new_args)), m_holes);
     return mvar;
 }
 

src/frontends/lean/tactic_notation.cpp

@@ -186,16 +186,6 @@ static bool is_curr_exact_shortcut(parser & p) {
         p.curr_is_token(get_suppose_tk());
 }
 
-static expr mk_lean_list(parser & p, buffer<expr> const & es, pos_info const & pos) {
-    expr r = p.save_pos(mk_constant(get_list_nil_name()), pos);
-    unsigned i = es.size();
-    while (i > 0) {
-        --i;
-        r = p.save_pos(mk_app(p.save_pos(mk_constant(get_list_cons_name()), pos), es[i], r), pos);
-    }
-    return r;
-}
-
 static expr mk_tactic_unit(name const & tac_class) {
     return mk_app(mk_constant(tac_class), mk_constant(get_unit_name()));
 }

src/frontends/lean/util.cpp

@@ -531,6 +531,31 @@ vm_obj eval_closed_expr(environment const & env, name const & n, expr const & ty
     return vm.invoke(n, 0, nullptr);
 }
 
+static expr save_pos(parser * p, expr const & e, optional<pos_info> const & pos) {
+    if (pos)
+        return p->save_pos(e, *pos);
+    else
+        return e;
+}
+
+static expr mk_lean_list(parser * p, buffer<expr> const & es, optional<pos_info> const & pos) {
+    expr r = save_pos(p, mk_constant(get_list_nil_name()), pos);
+    unsigned i = es.size();
+    while (i > 0) {
+        --i;
+        r = save_pos(p, mk_app(save_pos(p, mk_constant(get_list_cons_name()), pos), es[i], r), pos);
+    }
+    return r;
+}
+
+expr mk_lean_list(parser & p, buffer<expr> const & es, pos_info const & pos) {
+    return mk_lean_list(&p, es, optional<pos_info>(pos));
+}
+
+expr mk_lean_list(buffer<expr> const & es) {
+    return mk_lean_list(nullptr, es, optional<pos_info>());
+}
+
 void finalize_frontend_lean_util() {
     delete g_auto_param_check_exists;
     delete g_no_info;

src/frontends/lean/util.h

@@ -141,6 +141,9 @@ unsigned get_field_notation_field_idx(expr const & e);
 environment compile_expr(environment const & env, name const & n, level_param_names const & ls, expr const & type, expr const & e, pos_info const & pos);
 vm_obj eval_closed_expr(environment const & env, name const & n, expr const & type, expr const & e, pos_info const & pos);
 
+expr mk_lean_list(parser & p, buffer<expr> const & es, pos_info const & pos);
+expr mk_lean_list(buffer<expr> const & es);
+
 void initialize_frontend_lean_util();
 void finalize_frontend_lean_util();
 }

tests/lean/run/hole1.lean

@@ -4,5 +4,5 @@ example : ∀ a b : nat, a + b = b + a :=
 example : ∀ a b : nat, a + b = b + a :=
 begin
   intros h,
-  exact  λ x, {! _+_ !}
+  exact  λ x, {! _+_, "lt" !}
 end