feat(frontends/lean): improve error handling inside match-with expressions

src/frontends/lean/builtin_exprs.cpp

@@ -242,17 +242,8 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const &
             }
         }
     } catch (exception & ex) {
-        if (end_token == get_end_tk()) {
+        if (end_token == get_end_tk())
-            // When the end_token is 'end', the default parser
+            consume_until_end(p);
-            // sync_command does not work well because it will
-            // interpret 'end' as a synchronization point because 'end' is also a command.
-            while (!p.curr_is_token(get_end_tk())) {
-                if (p.curr() == scanner::token_kind::Eof)
-                    ex.rethrow();
-                p.next();
-            }
-            p.next(); // consume 'end'
-        }
         ex.rethrow();
     }
     auto end_pos = p.pos();

src/frontends/lean/decl_cmds.cpp

@@ -698,47 +698,53 @@ expr parse_local_equations(parser & p, expr const & fn) {
 
 /** \brief Use equations compiler infrastructure to implement match-with */
 expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
-    expr t  = p.parse_expr();
     buffer<expr> eqns;
-    p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");
+    expr t;
-    expr fn = mk_local(p.mk_fresh_name(), "match", mk_expr_placeholder(), binder_info());
+    try {
-    if (p.curr_is_token(get_end_tk())) {
+        t  = p.parse_expr();
-        p.next();
+        p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");
-        // empty match-with
+        expr fn = mk_local(p.mk_fresh_name(), "match", mk_expr_placeholder(), binder_info());
-        eqns.push_back(Fun(fn, mk_no_equation()));
+        if (p.curr_is_token(get_end_tk())) {
-        expr f = p.save_pos(mk_equations(1, eqns.size(), eqns.data()), pos);
+            p.next();
-        return p.mk_app(f, t, pos);
+            // empty match-with
-    }
+            eqns.push_back(Fun(fn, mk_no_equation()));
-    if (is_eqn_prefix(p))
+            expr f = p.save_pos(mk_equations(1, eqns.size(), eqns.data()), pos);
-        p.next(); // optional '|' in the first case
+            return p.mk_app(f, t, pos);
-    while (true) {
+        }
-        expr lhs;
+        if (is_eqn_prefix(p))
-        unsigned prev_num_undef_ids = p.get_num_undef_ids();
+            p.next(); // optional '|' in the first case
-        buffer<expr> locals;
+        while (true) {
-        {
+            expr lhs;
-            parser::undef_id_to_local_scope scope2(p);
+            unsigned prev_num_undef_ids = p.get_num_undef_ids();
-            auto lhs_pos = p.pos();
+            buffer<expr> locals;
-            lhs = p.parse_expr();
+            {
-            lhs = p.mk_app(fn, lhs, lhs_pos);
+                parser::undef_id_to_local_scope scope2(p);
-            unsigned num_undef_ids = p.get_num_undef_ids();
+                auto lhs_pos = p.pos();
-            for (unsigned i = prev_num_undef_ids; i < num_undef_ids; i++) {
+                lhs = p.parse_expr();
-                locals.push_back(p.get_undef_id(i));
+                lhs = p.mk_app(fn, lhs, lhs_pos);
+                unsigned num_undef_ids = p.get_num_undef_ids();
+                for (unsigned i = prev_num_undef_ids; i < num_undef_ids; i++) {
+                    locals.push_back(p.get_undef_id(i));
+                }
             }
+            validate_equation_lhs(p, lhs, locals);
+            lhs = merge_equation_lhs_vars(lhs, locals);
+            auto assign_pos = p.pos();
+            p.check_token_next(get_assign_tk(), "invalid 'match' expression, ':=' expected");
+            {
+                parser::local_scope scope2(p);
+                for (expr const & local : locals)
+                    p.add_local(local);
+                expr rhs = p.parse_expr();
+                eqns.push_back(Fun(fn, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p)));
+            }
+            if (!is_eqn_prefix(p))
+                break;
+            p.next();
         }
-        validate_equation_lhs(p, lhs, locals);
+    } catch (exception & ex) {
-        lhs = merge_equation_lhs_vars(lhs, locals);
+        consume_until_end(p);
-        auto assign_pos = p.pos();
+        ex.rethrow();
-        p.check_token_next(get_assign_tk(), "invalid 'match' expression, ':=' expected");
-        {
-            parser::local_scope scope2(p);
-            for (expr const & local : locals)
-                p.add_local(local);
-            expr rhs = p.parse_expr();
-            eqns.push_back(Fun(fn, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p)));
-        }
-        if (!is_eqn_prefix(p))
-            break;
-        p.next();
     }
     p.check_token_next(get_end_tk(), "invalid 'match' expression, 'end' expected");
     expr f = p.save_pos(mk_equations(1, eqns.size(), eqns.data()), pos);

src/frontends/lean/util.cpp

@@ -22,6 +22,15 @@ Author: Leonardo de Moura
 #include "frontends/lean/tokens.h"
 
 namespace lean {
+void consume_until_end(parser & p) {
+    while (!p.curr_is_token(get_end_tk())) {
+        if (p.curr() == scanner::token_kind::Eof)
+            return;
+        p.next();
+    }
+    p.next();
+}
+
 bool parse_persistent(parser & p, bool & persistent) {
     if (p.curr_is_token_or_id(get_persistent_tk())) {
         p.next();

src/frontends/lean/util.h

@@ -14,6 +14,9 @@ Author: Leonardo de Moura
 
 namespace lean {
 class parser;
+/** \brief Consume tokes until 'end' token is consumed */
+void consume_until_end(parser & p);
+
 /** \brief Parse optional '[persistent]' modifier.
     return true if it is was found, and paremeter \c persistent to true.
 */

tests/lean/errors2.lean

@@ -0,0 +1,12 @@
+open nat
+
+namespace foo
+
+definition tst1 (a b : nat) : nat :=
+match a with
+| 0     := 1
+| (n+1) := foo
+end
+
+
+end foo

tests/lean/errors2.lean.expected.out

@@ -0,0 +1 @@
+errors2.lean:8:11: error: unknown identifier 'foo'