From 55c8627f2ce29ce6a789abc2659ca4e95aeeabce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Jun 2017 22:10:51 -0700 Subject: [PATCH] feat(frontends/lean): {! ... !} takes a list of pre-terms --- library/init/meta/hole_command.lean | 14 +++++------ src/frontends/lean/builtin_exprs.cpp | 33 +++++++++++++++++++++----- src/frontends/lean/builtin_exprs.h | 2 ++ src/frontends/lean/elaborator.cpp | 7 +++++- src/frontends/lean/tactic_notation.cpp | 10 -------- src/frontends/lean/util.cpp | 25 +++++++++++++++++++ src/frontends/lean/util.h | 3 +++ tests/lean/run/hole1.lean | 2 +- 8 files changed, 71 insertions(+), 25 deletions(-) diff --git a/library/init/meta/hole_command.lean b/library/init/meta/hole_command.lean index 17712cb487..d585e53d8d 100644 --- a/library/init/meta/hole_command.lean +++ b/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, diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 7d46a2a855..a8b042348c 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/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, optional> get_hole_info(expr const & e) { + lean_assert(is_hole(e)); + optional 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 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; } diff --git a/src/frontends/lean/builtin_exprs.h b/src/frontends/lean/builtin_exprs.h index dceef830b0..6ad24732a2 100644 --- a/src/frontends/lean/builtin_exprs.h +++ b/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, optional> 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(); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 97b3dd4a70..8a5e485052 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2055,8 +2055,13 @@ expr elaborator::visit_by(expr const & e, optional const & expected_type) expr elaborator::visit_hole(expr const & e, optional const & expected_type) { lean_assert(is_hole(e)); expr const & ref = e; + expr args; optional 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; } diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index 20155f870c..57299fd2da 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/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 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())); } diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 4568516979..c70a7ada8e 100644 --- a/src/frontends/lean/util.cpp +++ b/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 const & pos) { + if (pos) + return p->save_pos(e, *pos); + else + return e; +} + +static expr mk_lean_list(parser * p, buffer const & es, optional 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 const & es, pos_info const & pos) { + return mk_lean_list(&p, es, optional(pos)); +} + +expr mk_lean_list(buffer const & es) { + return mk_lean_list(nullptr, es, optional()); +} + void finalize_frontend_lean_util() { delete g_auto_param_check_exists; delete g_no_info; diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index b985030fde..1cc9d5552b 100644 --- a/src/frontends/lean/util.h +++ b/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 const & es, pos_info const & pos); +expr mk_lean_list(buffer const & es); + void initialize_frontend_lean_util(); void finalize_frontend_lean_util(); } diff --git a/tests/lean/run/hole1.lean b/tests/lean/run/hole1.lean index c65cf3609c..0cbe0acdfd 100644 --- a/tests/lean/run/hole1.lean +++ b/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