fix(frontends/lean/decl_cmds): improve error message for invalid end of theorem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/decl_cmds.cpp

@@ -185,6 +185,11 @@ struct decl_modifiers {
     }
 };
 
+static void check_end_of_theorem(parser const & p) {
+    if (!p.curr_is_command_like())
+        throw parser_error("':=', '.', command, script, or end-of-file expected", p.pos());
+}
+
 environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
     auto n_pos = p.pos();
     unsigned start_line = n_pos.first;
@@ -216,6 +221,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
             auto pos = p.pos();
             type = p.parse_expr();
             if (is_theorem && !p.curr_is_token(g_assign)) {
+                check_end_of_theorem(p);
                 value = mk_expr_placeholder();
             } else {
                 p.check_token_next(g_assign, "invalid declaration, ':=' expected");
@@ -230,6 +236,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
                 p.next();
                 type = p.parse_scoped_expr(ps, *lenv);
                 if (is_theorem && !p.curr_is_token(g_assign)) {
+                    check_end_of_theorem(p);
                     value = p.save_pos(mk_expr_placeholder(), pos);
                 } else {
                     p.check_token_next(g_assign, "invalid declaration, ':=' expected");

src/frontends/lean/parser.cpp

@@ -1266,6 +1266,21 @@ bool parser::parse_commands() {
     return !m_found_errors;
 }
 
+bool parser::curr_is_command_like() const {
+    switch (curr()) {
+    case scanner::token_kind::CommandKeyword:
+        return true;
+    case scanner::token_kind::ScriptBlock:
+        return true;
+    case scanner::token_kind::Eof:
+        return true;
+    case scanner::token_kind::Keyword:
+        return curr_is_token(g_period);
+    default:
+        return false;
+    }
+}
+
 void parser::add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls, expr const & t, expr const & v) {
     m_theorem_queue.add(env, n, ls, get_local_level_decls(), t, v);
 }

src/frontends/lean/parser.h

@@ -239,8 +239,10 @@ public:
     bool curr_is_command() const { return curr() == scanner::token_kind::CommandKeyword; }
     /** \brief Return true iff the current token is a keyword */
     bool curr_is_quoted_symbol() const { return curr() == scanner::token_kind::QuotedSymbol; }
-    /** \brief Return true if the current token is a keyword named \c tk or an identifier named \c tk */
+    /** \brief Return true iff the current token is a keyword named \c tk or an identifier named \c tk */
     bool curr_is_token_or_id(name const & tk) const;
+    /** \brief Return true iff the current token is a command, EOF, period or script block */
+    bool curr_is_command_like() const;
     /** \brief Read the next token if the current one is not End-of-file. */
     void next() { if (m_curr != scanner::token_kind::Eof) scan(); }
     /** \brief Return true iff the current token is a keyword (or command keyword) named \c tk */

tests/lean/empty_thm.lean

@@ -0,0 +1,10 @@
+import logic tools.tactic
+using tactic
+
+definition simple := apply trivial
+
+tactic_hint simple
+
+theorem foo : true
+theorem foo2 (a : Prop) : a :
+theorem foo3 : true

tests/lean/empty_thm.lean.expected.out

@@ -0,0 +1 @@
+empty_thm.lean:9:28: error: ':=', '.', command, script, or end-of-file expected