feat(frontends/lean/parser): error recovery in interactive tactics

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<notation::accepting> 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<expr> 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<optional<name>, expr> parser::parse_id_tk_expr(name const & tk, unsigned rbp) {
     if (curr_is_identifier()) {
         auto id_pos = pos();

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<name> const & extra_locals = list<name>());
 
+    /** 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<expr> maybe_parse_expr(unsigned rbp = 0);
     /** \brief Parse an (optionally) qualified expression.
         If the input is of the form <id> : <expr>, 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<expr> 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<bool> error_recovery_scope(bool enable_recovery) {
         return flet<bool>(m_error_recovery, enable_recovery);
     }

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);
     }
 }
 

src/library/vm/vm_parser.cpp

@@ -32,7 +32,7 @@ struct lean_parser_state {
 template struct interaction_monad<lean_parser_state>;
 typedef interaction_monad<lean_parser_state> 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;
 }