feat(frontends/lean): better error messages for ill-terminated declarations

src/frontends/lean/decl_cmds.cpp

@@ -197,6 +197,7 @@ static environment variable_cmd_core(parser & p, variable_kind k) {
         type = p.parse_expr();
     }
     p.parse_close_binder_info(bi);
+    check_command_period_or_eof(p);
     level_param_names ls;
     if (ls_buffer.empty()) {
         ls = to_level_param_names(collect_univ_params(type));
@@ -248,6 +249,7 @@ static environment variables_cmd_core(parser & p, variable_kind k) {
             // Alternative: elaborate once and copy types replacing universes in new_ls.
             level_param_names new_ls;
             expr new_type;
+            check_command_period_open_binder_or_eof(p);
             std::tie(new_type, new_ls) = p.elaborate_type(type, ctx);
             if (k == variable_kind::Variable || k == variable_kind::Parameter)
                 update_local_levels(p, new_ls, k == variable_kind::Variable);
@@ -710,6 +712,7 @@ class definition_cmd_fn {
     void parse() {
         parse_name();
         parse_type_value();
+        check_command_period_or_eof(m_p);
         if (m_p.used_sorry())
             m_p.declare_sorry();
         m_env = m_p.env();

src/frontends/lean/parser.h

@@ -290,6 +290,8 @@ public:
     bool curr_is_keyword() const { return curr() == scanner::token_kind::Keyword; }
     /** \brief Return true iff the current token is a keyword */
     bool curr_is_command() const { return curr() == scanner::token_kind::CommandKeyword; }
+    /** \brief Return true iff the current token is a Lua script block */
+    bool curr_is_script_block() const { return curr() == scanner::token_kind::ScriptBlock; }
     /** \brief Return true iff the current token is EOF */
     bool curr_is_eof() const { return curr() == scanner::token_kind::Eof; }
     /** \brief Return true iff the current token is a keyword */

src/frontends/lean/util.cpp

@@ -31,6 +31,20 @@ bool parse_persistent(parser & p, bool & persistent) {
     }
 }
 
+void check_command_period_or_eof(parser const & p) {
+    if (!p.curr_is_command() && !p.curr_is_eof() && !p.curr_is_token(get_period_tk()) &&
+        !p.curr_is_script_block())
+        throw parser_error("unexpected token, '.', command, Lua script, or end-of-file expected", p.pos());
+}
+
+void check_command_period_open_binder_or_eof(parser const & p) {
+    if (!p.curr_is_command() && !p.curr_is_eof() && !p.curr_is_token(get_period_tk()) &&
+        !p.curr_is_script_block() &&
+        !p.curr_is_token(get_lparen_tk()) && !p.curr_is_token(get_lbracket_tk()) &&
+        !p.curr_is_token(get_lcurly_tk()) && !p.curr_is_token(get_ldcurly_tk()))
+        throw parser_error("unexpected token, '(', '{', '[', '⦃', '.', command, Lua script, or end-of-file expected", p.pos());
+}
+
 void check_atomic(name const & n) {
     if (!n.is_atomic())
         throw exception(sstream() << "invalid declaration name '" << n << "', identifier must be atomic");

src/frontends/lean/util.h

@@ -19,6 +19,10 @@ class parser;
 */
 bool parse_persistent(parser & p, bool & persistent);
 
+/** \brief Throw and error if the current token is not a command, nor a '.', nor an end-of-file. */
+void check_command_period_or_eof(parser const & p);
+/** \brief Throw and error if the current token is not a command, nor an open binder, nor a '.', nor an end-of-file. */
+void check_command_period_open_binder_or_eof(parser const & p);
 void check_atomic(name const & n);
 void check_in_context(parser const & p);
 void check_in_context_or_section(parser const & p);

tests/lean/natsucc.lean

@@ -0,0 +1,14 @@
+import data.nat
+open nat
+
+theorem add_assoc (m n k : nat) : m + n + k = m + (n + k) :=
+nat.induction_on k
+(show m + n + 0 = m + (n + 0), from rfl),
+(take k,
+   assume IH : m + n + k = m + (n + k),
+   show m + n + mysucc k = m + (n + mysucc k), from
+     calc
+       m + n + mysucc k = mysucc (m + n + k) : rfl
+       ... = mysucc (m + (n + k)) : IH
+       ... = m + mysucc (n + k) : rfl
+       ... = m + (n + mysucc k) : rfl)

tests/lean/natsucc.lean.expected.out

@@ -0,0 +1 @@
+natsucc.lean:6:40: error: unexpected token, '.', command, Lua script, or end-of-file expected

tests/lean/varcomma.lean

@@ -0,0 +1,15 @@
+variable {A : Type},
+variables {A : Type},
+variables {A : Type} {B : Type} in
+
+variables {C : Type} {D : Type}
+
+(*
+
+*)
+
+theorem a : true := trivial
+
+(*
+
+*)

tests/lean/varcomma.lean.expected.out

@@ -0,0 +1,3 @@
+varcomma.lean:1:19: error: unexpected token, '.', command, Lua script, or end-of-file expected
+varcomma.lean:2:20: error: unexpected token, '(', '{', '[', '⦃', '.', command, Lua script, or end-of-file expected
+varcomma.lean:3:32: error: unexpected token, '(', '{', '[', '⦃', '.', command, Lua script, or end-of-file expected