From e0856284b0711d96de82434afe603b016cb366aa Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Mar 2017 17:16:25 +0100 Subject: [PATCH] feat(frontends/lean,emacs): tactic info before elaboration, fix many edge cases --- src/emacs/lean-type.el | 4 +- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/interactive.cpp | 18 +++-- src/frontends/lean/parser.cpp | 3 +- src/frontends/lean/parser_state.h | 4 +- src/frontends/lean/tactic_notation.cpp | 81 +++++++++++-------- src/frontends/lean/tactic_notation.h | 3 +- src/library/vm/vm_parser.cpp | 3 +- tests/lean/interactive/info_tactic.lean | 11 +++ .../interactive/info_tactic.lean.expected.out | 6 ++ 10 files changed, 88 insertions(+), 47 deletions(-) create mode 100644 tests/lean/interactive/info_tactic.lean create mode 100644 tests/lean/interactive/info_tactic.lean.expected.out diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index 4a53c3387c..efb4f508c1 100644 --- a/src/emacs/lean-type.el +++ b/src/emacs/lean-type.el @@ -40,14 +40,14 @@ (cl-defun lean-info-record-to-string (info-record) "Given typeinfo, overload, and sym-name, compose information as a string." - (destructuring-bind (&key type tactic_params tactic_param_idx doc overloads synth coercion proofstate full-id symbol extra &allow-other-keys) info-record + (destructuring-bind (&key type tactic_params tactic_param_idx text doc overloads synth coercion proofstate full-id symbol extra &allow-other-keys) info-record (let (name-str type-str coercion-str extra-str proofstate-str overload-str stale-str str) (setq name-str (cond (synth synth) ((and full-id symbol) (format "[%s] %s" symbol full-id)) - (t (or full-id symbol)))) + (t (or full-id text symbol)))) (when coercion (destructuring-bind (&key expr type) coercion (setq coercion-str diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index e21ac5a7cb..78a0a2f354 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -964,7 +964,7 @@ parse_table init_nud_table() { r = r.add({transition("`(", mk_ext_action(parse_lazy_quoted_pexpr))}, x0); r = r.add({transition("``(", mk_ext_action(parse_quoted_pexpr))}, x0); r = r.add({transition("```(", mk_ext_action(parse_quoted_expr))}, x0); - r = r.add({transition("`[", mk_ext_action(parse_auto_quote_tactic_block))}, x0); + r = r.add({transition("`[", mk_ext_action(parse_interactive_tactic_block))}, x0); r = r.add({transition("`", mk_ext_action(parse_quoted_name))}, x0); r = r.add({transition("%%", mk_ext_action(parse_antiquote_expr))}, x0); r = r.add({transition("(:", Expr), transition(":)", mk_ext_action(parse_pattern))}, x0); diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp index 8f0f94a79b..0959d45e01 100644 --- a/src/frontends/lean/interactive.cpp +++ b/src/frontends/lean/interactive.cpp @@ -11,7 +11,9 @@ Author: Sebastian Ullrich #include "library/module_mgr.h" #include "library/versioned_msg_buf.h" #include "library/attribute_manager.h" +#include "frontends/lean/interactive.h" #include "frontends/lean/pp.h" +#include "frontends/lean/tactic_notation.h" #include "shell/completion.h" namespace lean { @@ -96,6 +98,17 @@ void report_info(environment const & env, options const & opts, io_state const & g_context = e.m_token_info.m_context; json record; + if (e.m_token_info.m_context == break_at_pos_exception::token_context::interactive_tactic && + e.m_token_info.m_token.size()) { + record = serialize_decl(e.m_token_info.m_token, + get_interactive_tactic_full_name(e.m_token_info.m_tac_class, e.m_token_info.m_token), + env, opts); + if (auto idx = e.m_token_info.m_tac_param_idx) + record["tactic_param_idx"] = *idx; + j["record"] = record; + return; + } + // info data not dependent on elaboration/info_manager auto const & tk = e.m_token_info.m_token; if (tk.size()) { @@ -124,11 +137,6 @@ void report_info(environment const & env, options const & opts, io_state const & } } - if (e.m_token_info.m_context == break_at_pos_exception::token_context::interactive_tactic) { - if (auto idx = e.m_token_info.m_tac_param_idx) - record["tactic_param_idx"] = *idx; - } - for (auto & infom : info_managers) { if (infom.get_file_name() == m_mod_info.m_mod) { if (e.m_goal_pos) { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index ffa1f1699e..2a222ac00f 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -424,7 +424,8 @@ void parser::check_token_or_id_next(name const & tk, char const * msg) { name parser::check_id_next(char const * msg, break_at_pos_exception::token_context ctxt) { // initiate empty completion even if following token is not an identifier - check_break_before(ctxt); + if (get_complete()) + check_break_before(ctxt); if (!curr_is_identifier()) throw parser_error(msg, pos()); name r = get_name_val(); diff --git a/src/frontends/lean/parser_state.h b/src/frontends/lean/parser_state.h index c7445457b5..e081e8fdca 100644 --- a/src/frontends/lean/parser_state.h +++ b/src/frontends/lean/parser_state.h @@ -58,8 +58,8 @@ public: optional m_goal_pos; break_at_pos_exception(pos_info const & token_pos, name token = "", - token_context ctxt = break_at_pos_exception::token_context::none, name tac_class = {}): - m_token_info(token_info {token_pos, token, ctxt, tac_class, {}, name()}) {} + token_context ctxt = break_at_pos_exception::token_context::none): + m_token_info(token_info {token_pos, token, ctxt, {}, {}, {}}) {} void report_goal_pos(pos_info goal_pos); }; diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index f4e6858897..b7157f9530 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -117,9 +117,13 @@ static expr concat(parser & p, expr const & tac1, expr const & tac2, pos_info co return p.save_pos(mk_app(mk_constant(get_has_bind_seq_name()), tac1, tac2), pos); } -static optional is_auto_quote_tactic(parser & p, name const & tac_class) { +name get_interactive_tactic_full_name(name const & tac_class, name const & tac) { + return name(tac_class, "interactive") + tac; +} + +static optional is_interactive_tactic(parser & p, name const & tac_class) { if (!p.curr_is_identifier()) return optional(); - name id = tac_class + name("interactive") + p.get_name_val(); + name id = get_interactive_tactic_full_name(tac_class, p.get_name_val()); if (p.env().find(id)) return optional(id); else @@ -134,7 +138,7 @@ static void info_tweak(parser & p) { static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep, bool report_error); -static expr parse_nested_auto_quote_tactic(parser & p, name const & tac_class, bool use_rstep, bool report_error) { +static expr parse_nested_interactive_tactic(parser & p, name const & tac_class, bool use_rstep, bool report_error) { auto pos = p.pos(); if (p.curr_is_token(get_lcurly_tk())) { return parse_begin_end_block(p, pos, get_rcurly_tk(), tac_class, use_rstep, report_error); @@ -156,35 +160,43 @@ static expr parse_interactive_param(parser & p, expr const & ty, expr const & qu return to_expr(vm_res); } -static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name const & tac_class, bool use_rstep, bool report_error) { +static expr parse_interactive_tactic(parser & p, name const & decl_name, name const & tac_class, bool use_rstep, bool report_error) { auto pos = p.pos(); - p.next(); - expr type = p.env().get(decl_name).get_type(); - name itactic(name(tac_class, "interactive"), "itactic"); - name irtactic(name(tac_class, "interactive"), "irtactic"); + expr type = p.env().get(decl_name).get_type(); + name itactic = get_interactive_tactic_full_name(tac_class, "itactic"); + name irtactic = get_interactive_tactic_full_name(tac_class, "irtactic"); buffer args; try { - while (is_pi(type)) { - if (is_explicit(binding_info(type))) { - expr arg_type = binding_domain(type); - if (is_app_of(arg_type, get_interactive_parse_name())) { - buffer arg_args; - get_app_args(arg_type, arg_args); - lean_assert(arg_args.size() == 3); - args.push_back(parse_interactive_param(p, arg_args[0], arg_args[1], arg_args[2])); - } else if (is_constant(arg_type, itactic)) { - bool report_error = false; - args.push_back(parse_nested_auto_quote_tactic(p, tac_class, use_rstep, report_error)); - } else if (is_constant(arg_type, irtactic)) { - args.push_back(parse_nested_auto_quote_tactic(p, tac_class, use_rstep, report_error)); - } else { - break; + try { + p.next(); + while (is_pi(type)) { + p.check_break_before(); + if (is_explicit(binding_info(type))) { + expr arg_type = binding_domain(type); + if (is_app_of(arg_type, get_interactive_parse_name())) { + buffer arg_args; + get_app_args(arg_type, arg_args); + lean_assert(arg_args.size() == 3); + args.push_back(parse_interactive_param(p, arg_args[0], arg_args[1], arg_args[2])); + } else if (is_constant(arg_type, itactic)) { + bool report_error = false; + args.push_back(parse_nested_interactive_tactic(p, tac_class, use_rstep, report_error)); + } else if (is_constant(arg_type, irtactic)) { + args.push_back(parse_nested_interactive_tactic(p, tac_class, use_rstep, report_error)); + } else { + break; + } } + type = binding_body(type); } - type = binding_body(type); - } - while (p.curr_lbp() >= get_max_prec()) { - args.push_back(p.parse_expr(get_max_prec())); + while (p.curr_lbp() >= get_max_prec()) { + p.check_break_before(); + args.push_back(p.parse_expr(get_max_prec())); + } + p.check_break_before(); + } catch (...) { + p.check_break_before(); + throw; } } catch (break_at_pos_exception & e) { e.m_token_info.m_tac_param_idx = args.size(); @@ -237,26 +249,27 @@ struct parse_tactic_fn { if (m_p.curr_is_identifier()) m_p.check_break_at_pos(); } catch (break_at_pos_exception & e) { - e.m_token_info.m_context = break_at_pos_exception::token_context::interactive_tactic; + e.m_token_info.m_context = break_at_pos_exception::token_context::interactive_tactic; e.m_token_info.m_tac_class = m_tac_class; throw; } expr r; auto pos = m_p.pos(); - if (auto dname = is_auto_quote_tactic(m_p, m_tac_class)) { + if (auto dname = is_interactive_tactic(m_p, m_tac_class)) { try { - r = parse_auto_quote_tactic(m_p, *dname, m_tac_class, m_use_rstep, m_report_error); + r = parse_interactive_tactic(m_p, *dname, m_tac_class, m_use_rstep, m_report_error); } catch (break_at_pos_exception & e) { if (!m_p.get_complete() && e.m_token_info.m_context == break_at_pos_exception::token_context::none) { - e.m_token_info.m_pos = pos; - e.m_token_info.m_context = break_at_pos_exception::token_context::interactive_tactic; + e.m_token_info.m_pos = pos; + e.m_token_info.m_token = dname->get_string(); + e.m_token_info.m_context = break_at_pos_exception::token_context::interactive_tactic; e.m_token_info.m_tac_class = m_tac_class; } throw; } } else if (is_curr_exact_shortcut(m_p)) { expr arg = parse_qexpr(); - r = m_p.mk_app(m_p.save_pos(mk_constant(m_tac_class + name({"interactive", "exact"})), pos), arg, pos); + r = m_p.mk_app(m_p.save_pos(mk_constant(get_interactive_tactic_full_name(m_tac_class, "exact")), pos), arg, pos); if (m_use_rstep) r = mk_tactic_rstep(m_p, r, pos, m_tac_class, m_report_error); } else { r = m_p.parse_expr(); @@ -530,7 +543,7 @@ static void erase_quoted_terms_pos_info(parser & p, expr const & e) { }); } -expr parse_auto_quote_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos) { +expr parse_interactive_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos) { name const & tac_class = get_tactic_name(); bool use_rstep = false; bool report_error = false; diff --git a/src/frontends/lean/tactic_notation.h b/src/frontends/lean/tactic_notation.h index 614173852d..b7cefa0f5a 100644 --- a/src/frontends/lean/tactic_notation.h +++ b/src/frontends/lean/tactic_notation.h @@ -7,11 +7,12 @@ Author: Leonardo de Moura #pragma once #include "frontends/lean/parser.h" namespace lean { +name get_interactive_tactic_full_name(name const & tac_class, name const & tac); expr parse_begin_end_expr(parser & p, pos_info const & pos); expr parse_curly_begin_end_expr(parser & p, pos_info const & pos); expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos); expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos); -expr parse_auto_quote_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos); +expr parse_interactive_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos); void initialize_tactic_notation(); void finalize_tactic_notation(); } diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp index 289055f025..896cd3c8e9 100644 --- a/src/library/vm/vm_parser.cpp +++ b/src/library/vm/vm_parser.cpp @@ -34,7 +34,8 @@ template struct interaction_monad; typedef interaction_monad lean_parser; #define TRY try { -#define CATCH } catch (exception const & ex) { return lean_parser::mk_exception(ex, s); } +#define CATCH } catch (break_at_pos_exception const & ex) { throw; }\ + catch (exception const & ex) { return lean_parser::mk_exception(ex, s); } vm_obj run_parser(parser & p, expr const & spec) { type_context ctx(p.env(), p.get_options()); diff --git a/tests/lean/interactive/info_tactic.lean b/tests/lean/interactive/info_tactic.lean new file mode 100644 index 0000000000..0f9ac8603a --- /dev/null +++ b/tests/lean/interactive/info_tactic.lean @@ -0,0 +1,11 @@ +example : false := +begin + simp, + --^ "command": "info" + simp , + --^ "command": "info" + simp [ ], + --^ "command": "info" + simp [d] , + --^ "command": "info" +end diff --git a/tests/lean/interactive/info_tactic.lean.expected.out b/tests/lean/interactive/info_tactic.lean.expected.out new file mode 100644 index 0000000000..d2243286d0 --- /dev/null +++ b/tests/lean/interactive/info_tactic.lean.expected.out @@ -0,0 +1,6 @@ +{"msg":{"caption":"","file_name":"f","pos_col":2,"pos_line":3,"severity":"error","text":"simplify tactic failed to simplify\nstate:\n⊢ false"},"response":"additional_message"} +{"message":"file invalidated","response":"ok","seq_num":0} +{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_params":["([ expr, ... ])?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default} → tactic unit"},"response":"ok","seq_num":4} +{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["([ expr, ... ])?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default} → tactic unit"},"response":"ok","seq_num":6} +{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["([ expr, ... ])?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default} → tactic unit"},"response":"ok","seq_num":8} +{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":1,"tactic_params":["([ expr, ... ])?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default} → tactic unit"},"response":"ok","seq_num":10}