From 345cd1bc2a8753cf98bbaa1d054c821cea33427c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 19 May 2017 18:00:26 +0200 Subject: [PATCH] feat(frontends/lean/parser): error recovery in interactive tactics --- src/frontends/lean/parser.cpp | 35 ++++++++++++++++++++------ src/frontends/lean/parser.h | 5 ++++ src/frontends/lean/tactic_notation.cpp | 30 +++++++++++++--------- src/library/vm/vm_parser.cpp | 10 +++++--- 4 files changed, 57 insertions(+), 23 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index c0013901ac..a91a3857cf 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -373,7 +373,7 @@ name parser::check_id_next(char const * msg, break_at_pos_exception::token_conte if (!curr_is_identifier()) { auto _ = no_error_recovery_scope_if(curr_is_command()); maybe_throw_error({msg, pos()}); - r = get_token_info().value(); + return "_"; } else { r = get_name_val(); } @@ -1361,16 +1361,15 @@ expr parser::parse_notation(parse_table t, expr * left) { } list const & as = t.is_accepting(); if (is_nil(as)) { + if (!left && p == pos() && has_error_recovery()) { + // Empty input + return mk_sorry(pos(), true); + } // TODO(gabriel): search children of t for accepting states sstream msg; msg << "invalid expression"; if (p != pos()) { msg << "starting at " << p.first << ":" << p.second; - } else if (!curr_is_command()) { - next(); // consume input - } else { - // nothing consumed, but we're at a command token now, so abort, abort, abort - throw parser_error(msg, pos()); } return parser_error_or_expr({msg, pos()}); } @@ -2161,14 +2160,34 @@ unsigned parser::curr_lbp() const { lean_unreachable(); // LCOV_EXCL_LINE } -expr parser::parse_expr(unsigned rbp) { - expr left = parse_nud(); +expr parser::parse_led_loop(expr left, unsigned rbp) { while (rbp < curr_lbp()) { + auto pos0 = pos(); left = parse_led(left); + + if (pos() == pos0) { + // We did not consume any input, this can happen if we fail inside parse_notation. + break; + } } return left; } +optional parser::maybe_parse_expr(unsigned rbp) { + auto pos0 = pos(); + auto res = parse_expr(rbp); + if (pos() == pos0) { + return none_expr(); + } else { + return some_expr(res); + } +} + +expr parser::parse_expr(unsigned rbp) { + expr left = parse_nud(); + return parse_led_loop(left, rbp); +} + pair, expr> parser::parse_id_tk_expr(name const & tk, unsigned rbp) { if (curr_is_identifier()) { auto id_pos = pos(); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index a2cc786e6a..c5e1cb6bd3 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -361,7 +361,10 @@ public: expr id_to_expr(name const & id, pos_info const & p, bool resolve_only = false, bool allow_field_notation = true, list const & extra_locals = list()); + /** Always parses an expression. Returns a synthetic sorry even if no input is consumed. */ expr parse_expr(unsigned rbp = 0); + /** Tries to parse an expression, or else consumes no input. */ + optional maybe_parse_expr(unsigned rbp = 0); /** \brief Parse an (optionally) qualified expression. If the input is of the form : , then return the pair (some(id), expr). Otherwise, parse the next expression and return (none, expr). */ @@ -389,6 +392,7 @@ public: expr parse_id(bool allow_field_notation = true); expr parse_led(expr left); + expr parse_led_loop(expr left, unsigned rbp); expr parse_scoped_expr(unsigned num_params, expr const * ps, local_environment const & lenv, unsigned rbp = 0); expr parse_scoped_expr(buffer const & ps, local_environment const & lenv, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), lenv, rbp); @@ -458,6 +462,7 @@ public: expr parser_error_or_expr(parser_error && err); void throw_invalid_open_binder(pos_info const & pos); + bool has_error_recovery() const { return m_error_recovery; } flet error_recovery_scope(bool enable_recovery) { return flet(m_error_recovery, enable_recovery); } diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index e5c553d4d3..833aa5d93e 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -138,18 +138,24 @@ static expr parse_nested_interactive_tactic(parser & p, name const & tac_class, } static expr parse_interactive_param(parser & p, expr const & ty, expr const & quote_inst, expr const & lean_parser) { - vm_obj vm_parsed = run_parser(p, lean_parser); - type_context ctx(p.env()); - name n("_quote_inst"); - tactic_evaluator eval(ctx, p.get_options(), ty); - auto env = eval.compile(n, quote_inst); - vm_state S(env, p.get_options()); - auto vm_res = S.invoke(n, vm_parsed); - expr r = to_expr(vm_res); - if (is_app_of(r, get_expr_subst_name())) { - return r; // HACK - } else { - return mk_as_is(r); + try { + vm_obj vm_parsed = run_parser(p, lean_parser); + type_context ctx(p.env()); + name n("_quote_inst"); + tactic_evaluator eval(ctx, p.get_options(), ty); + auto env = eval.compile(n, quote_inst); + vm_state S(env, p.get_options()); + auto vm_res = S.invoke(n, vm_parsed); + expr r = to_expr(vm_res); + if (is_app_of(r, get_expr_subst_name())) { + return r; // HACK + } else { + return mk_as_is(r); + } + } catch (exception & ex) { + if (!p.has_error_recovery()) throw; + p.mk_message(ERROR).set_exception(ex).report(); + return p.mk_sorry(p.pos(), true); } } diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp index 70ba36a0a0..80040756cd 100644 --- a/src/library/vm/vm_parser.cpp +++ b/src/library/vm/vm_parser.cpp @@ -32,7 +32,7 @@ struct lean_parser_state { template struct interaction_monad; typedef interaction_monad lean_parser; -#define TRY try { auto _ = s.m_p->no_error_recovery_scope(); +#define TRY try { #define CATCH } catch (break_at_pos_exception const & ex) { throw; }\ catch (exception const & ex) { return lean_parser::mk_exception(ex, s); } @@ -49,6 +49,7 @@ vm_obj vm_parser_state_cur_pos(vm_obj const & o) { vm_obj vm_parser_ident(vm_obj const & o) { auto const & s = lean_parser::to_state(o); TRY; + auto _ = s.m_p->no_error_recovery_scope(); name ident = s.m_p->check_id_next("identifier expected"); return lean_parser::mk_success(to_obj(ident), s); CATCH; @@ -70,8 +71,11 @@ vm_obj vm_parser_qexpr(vm_obj const & vm_rbp, vm_obj const & o) { TRY; auto rbp = to_unsigned(vm_rbp); parser::quote_scope scope(*s.m_p, true); - expr e = s.m_p->parse_expr(rbp); - return lean_parser::mk_success(to_obj(e), s); + if (auto e = s.m_p->maybe_parse_expr(rbp)) { + return lean_parser::mk_success(to_obj(*e), s); + } else { + throw parser_error(sstream() << "expression expected", s.m_p->pos()); + } CATCH; }