max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/parser): do not skip command tokens after error recovery

Browse source
This commit is contained in:
Gabriel Ebner 2017-05-22 20:12:41 +02:00 • committed by Leonardo de Moura
parent 47629e9da3
commit ce44566c7d
3 changed files with 43 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/frontends/lean/parser.cpp
View file

@ -212,6 +212,11 @@ void parser::scan() {
check_break_before();
check_break_at_pos();
pos_info curr_pos = pos();
if (m_error_since_last_cmd && (curr_is_command() && !curr_is_token(get_end_tk()))) {
// If we're during error recovery, do not read past command tokens.
// `end` is not treated as a command token since it occurs in begin-end blocks.
return;
}
if (m_break_at_pos && m_break_at_pos->first == curr_pos.first && curr_is_identifier()) {
name curr_ident = get_name_val();
m_curr = m_scanner.scan(m_env);
@ -353,10 +358,13 @@ bool parser::curr_is_token_or_id(name const & tk) const {
return false;
}
void parser::check_token_next(name const & tk, char const * msg) {
if (!curr_is_token(tk))
return maybe_throw_error({msg, pos()});
bool parser::check_token_next(name const & tk, char const * msg) {
if (!curr_is_token(tk)) {
maybe_throw_error({msg, pos()});
return false;
}
next();
return true;
}
void parser::check_token_or_id_next(name const & tk, char const * msg) {
@ -2451,6 +2459,7 @@ void parser::get_imports(std::vector<module_name> & imports) {
bool parser::parse_command_like() {
init_scanner();
m_error_since_last_cmd = false;
// We disable hash-consing while parsing to make sure the pos-info are correct.
scoped_expr_caching disable(false);
@ -2559,6 +2568,7 @@ void parser::maybe_throw_error(parser_error && err) {
check_system("parser error recovery");
mk_message(ERROR).set_exception(err).report();
m_last_recovered_error_pos = err_pos;
m_error_since_last_cmd = true;
}
} else {
throw err;

5
src/frontends/lean/parser.h
View file

@ -70,6 +70,7 @@ class parser : public abstract_parser {
// error recovery
bool m_error_recovery = true;
bool m_error_since_last_cmd = false;
pos_info m_last_recovered_error_pos {0, 0};
// curr command token
@ -273,8 +274,8 @@ public:
virtual void next() override final { if (m_curr != token_kind::Eof) scan(); }
/** \brief Return true iff the current token is a keyword (or command keyword) named \c tk */
virtual bool curr_is_token(name const & tk) const override final;
/** \brief Check current token, and move to next characther, throw exception if current token is not \c tk. */
void check_token_next(name const & tk, char const * msg);
/** \brief Check current token, and move to next characther, throw exception if current token is not \c tk. Returns true if succesful. */
bool check_token_next(name const & tk, char const * msg);
void check_token_or_id_next(name const & tk, char const * msg);
/** \brief Check if the current token is an identifier, if it is return it and move to next token,
otherwise throw an exception. */

49
src/frontends/lean/tactic_notation.cpp
View file

@ -421,6 +421,17 @@ struct parse_begin_end_block_fn {
}
expr operator()(pos_info const & start_pos, name const & end_token) {
auto sync = [&] {
while (!m_p.curr_is_token(get_comma_tk()) && !m_p.curr_is_token(end_token) &&
!m_p.curr_is_token(get_semicolon_tk()) && !m_p.curr_is_token(get_orelse_tk())) {
auto pos0 = m_p.pos();
m_p.next();
if (m_p.pos() == pos0) break;
}
if (!m_p.curr_is_token(get_end_tk())) m_p.next();
m_p.maybe_throw_error({"sync", m_p.pos()});
};
m_p.next();
name new_tac_class = m_tac_class;
if (m_tac_class == get_tactic_name())
@ -435,30 +446,24 @@ struct parse_begin_end_block_fn {
m_tac_class = new_tac_class;
buffer<expr> to_concat;
to_concat.push_back(mk_tactic_save_info(m_p, start_pos, m_tac_class));
try {
while (!m_p.curr_is_token(end_token)) {
pos_info pos = m_p.pos();
try {
to_concat.push_back(parse_tactic());
if (!m_p.curr_is_token(end_token)) {
m_p.without_break_at_pos<void>([&]() {
m_p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected");
});
}
to_concat.push_back(mk_save_info());
} catch (break_at_pos_exception & ex) {
ex.report_goal_pos(pos);
throw;
}
if (m_p.pos() == pos) { // unsuccessful error recovery
consume_until_end_or_command(m_p);
break;
while (!m_p.curr_is_token(end_token)) {
pos_info pos = m_p.pos();
try {
to_concat.push_back(parse_tactic());
if (!m_p.curr_is_token(end_token)) {
m_p.without_break_at_pos<void>([&]() {
if (!m_p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected")) {
sync();
}
});
}
to_concat.push_back(mk_save_info());
} catch (break_at_pos_exception & ex) {
ex.report_goal_pos(pos);
throw;
}
} catch (exception & ex) {
if (end_token == get_end_tk())
consume_until_end_or_command(m_p);
throw;
if (m_p.pos() == pos) sync();
if (m_p.pos() == pos) break;
}
auto end_pos = m_p.pos();
expr r = concat(to_concat, start_pos);