From 014271da8b59af65d6f7cea3ac352b60177369a1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Feb 2015 14:36:21 -0800 Subject: [PATCH] feat(frontends/lean): better error messages for ill-terminated declarations --- src/frontends/lean/decl_cmds.cpp | 3 +++ src/frontends/lean/parser.h | 2 ++ src/frontends/lean/util.cpp | 14 ++++++++++++++ src/frontends/lean/util.h | 4 ++++ tests/lean/natsucc.lean | 14 ++++++++++++++ tests/lean/natsucc.lean.expected.out | 1 + tests/lean/varcomma.lean | 15 +++++++++++++++ tests/lean/varcomma.lean.expected.out | 3 +++ 8 files changed, 56 insertions(+) create mode 100644 tests/lean/natsucc.lean create mode 100644 tests/lean/natsucc.lean.expected.out create mode 100644 tests/lean/varcomma.lean create mode 100644 tests/lean/varcomma.lean.expected.out diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index efe5f78b9..f1f9f23c9 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/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(); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index b7f49d7a2..ecf5bfe03 100644 --- a/src/frontends/lean/parser.h +++ b/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 */ diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 9907b4e59..d73d640c2 100644 --- a/src/frontends/lean/util.cpp +++ b/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"); diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index ebcdd89d6..f946b63bb 100644 --- a/src/frontends/lean/util.h +++ b/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); diff --git a/tests/lean/natsucc.lean b/tests/lean/natsucc.lean new file mode 100644 index 000000000..26808c5ab --- /dev/null +++ b/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) diff --git a/tests/lean/natsucc.lean.expected.out b/tests/lean/natsucc.lean.expected.out new file mode 100644 index 000000000..e37060733 --- /dev/null +++ b/tests/lean/natsucc.lean.expected.out @@ -0,0 +1 @@ +natsucc.lean:6:40: error: unexpected token, '.', command, Lua script, or end-of-file expected diff --git a/tests/lean/varcomma.lean b/tests/lean/varcomma.lean new file mode 100644 index 000000000..9a333e49a --- /dev/null +++ b/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 + +(* + +*) diff --git a/tests/lean/varcomma.lean.expected.out b/tests/lean/varcomma.lean.expected.out new file mode 100644 index 000000000..cc99870fd --- /dev/null +++ b/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