From 441f1f9fe2a9251c4ff74c830a8aed4ac27e147c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 May 2015 18:57:58 -0700 Subject: [PATCH] feat(frontends/lean): import error message for "unknown" tactics when parsing --- src/frontends/lean/builtin_exprs.cpp | 14 ++++++-------- src/frontends/lean/builtin_tactics.cpp | 4 ++-- src/frontends/lean/parse_rewrite_tactic.cpp | 16 ++++++++-------- src/frontends/lean/parser.cpp | 14 ++++++++++++-- src/frontends/lean/parser.h | 2 ++ tests/lean/tactic_error_msg.lean | 5 +++++ tests/lean/tactic_error_msg.lean.expected.out | 1 + 7 files changed, 36 insertions(+), 20 deletions(-) create mode 100644 tests/lean/tactic_error_msg.lean create mode 100644 tests/lean/tactic_error_msg.lean.expected.out diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index a142a18bf..692c87ce7 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -124,7 +124,6 @@ static expr parse_placeholder(parser & p, unsigned, expr const *, pos_info const } static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) { - parser::undef_id_to_local_scope scope(p); p.next(); expr t = p.parse_tactic(); return p.mk_by(t, pos); @@ -133,7 +132,6 @@ static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) { static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & end_token, bool nested = false) { if (!p.has_tactic_decls()) throw parser_error("invalid 'begin-end' expression, tactic module has not been imported", pos); - parser::undef_id_to_local_scope scope1(p); p.next(); optional pre_tac = get_begin_end_pre_tactic(p.env()); buffer tacs; @@ -171,7 +169,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & p.next(); name id = p.check_id_next("invalid 'assert' tactic, identifier expected"); p.check_token_next(get_colon_tk(), "invalid 'assert' tactic, ':' expected"); - expr A = p.parse_expr(); + expr A = p.parse_tactic_expr_arg(); expr assert_tac = p.save_pos(mk_assert_tactic_expr(id, A), pos); tacs.push_back(mk_begin_end_element_annotation(assert_tac)); } else if (p.curr_is_token(get_have_tk())) { @@ -180,7 +178,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & auto id_pos = p.pos(); name id = p.check_id_next("invalid 'have' tactic, identifier expected"); p.check_token_next(get_colon_tk(), "invalid 'have' tactic, ':' expected"); - expr A = p.parse_expr(); + expr A = p.parse_tactic_expr_arg(); expr assert_tac = p.save_pos(mk_assert_tactic_expr(id, A), pos); tacs.push_back(mk_begin_end_element_annotation(assert_tac)); if (p.curr_is_token(get_bar_tk())) { @@ -196,7 +194,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & // parse: 'from' expr p.next(); auto pos = p.pos(); - expr t = p.parse_expr(); + expr t = p.parse_tactic_expr_arg(); t = p.mk_app(get_rexact_tac_fn(), t, pos); t = p.save_pos(mk_begin_end_element_annotation(t), pos); t = p.save_pos(mk_begin_end_annotation(t), pos); @@ -204,7 +202,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & } else if (p.curr_is_token(get_proof_tk())) { auto pos = p.pos(); p.next(); - expr t = p.parse_expr(); + expr t = p.parse_tactic_expr_arg(); p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected"); t = p.mk_app(get_rexact_tac_fn(), t, pos); t = p.save_pos(mk_begin_end_element_annotation(t), pos); @@ -225,13 +223,13 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & } } else if (p.curr_is_token(get_show_tk())) { auto pos = p.pos(); - expr t = p.parse_expr(); + expr t = p.parse_tactic_expr_arg(); t = p.mk_app(get_rexact_tac_fn(), t, pos); add_tac(t, pos); } else if (p.curr_is_token(get_match_tk()) || p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) || p.curr_is_token(get_fun_tk())) { auto pos = p.pos(); - expr t = p.parse_expr(); + expr t = p.parse_tactic_expr_arg(); t = p.mk_app(get_exact_tac_fn(), t, pos); add_tac(t, pos); } else { diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp index becbbc170..bf1809998 100644 --- a/src/frontends/lean/builtin_tactics.cpp +++ b/src/frontends/lean/builtin_tactics.cpp @@ -35,12 +35,12 @@ static expr parse_rparen(parser &, unsigned, expr const * args, pos_info const & static expr parse_let_tactic(parser & p, unsigned, expr const *, pos_info const & pos) { name id = p.check_atomic_id_next("invalid 'let' tactic, identifier expected"); p.check_token_next(get_assign_tk(), "invalid 'let' tactic, ':=' expected"); - expr value = p.parse_expr(); + expr value = p.parse_tactic_expr_arg(); return p.save_pos(mk_let_tactic_expr(id, value), pos); } static expr parse_generalize_tactic(parser & p, unsigned, expr const *, pos_info const & pos) { - expr e = p.parse_expr(); + expr e = p.parse_tactic_expr_arg(); name id; if (p.curr_is_token(get_as_tk())) { p.next(); diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp index 7059e85ab..677b90d14 100644 --- a/src/frontends/lean/parse_rewrite_tactic.cpp +++ b/src/frontends/lean/parse_rewrite_tactic.cpp @@ -13,7 +13,7 @@ namespace lean { static optional parse_pattern(parser & p) { if (p.curr_is_token(get_lcurly_tk())) { p.next(); - expr r = p.parse_expr(); + expr r = p.parse_tactic_expr_arg(); p.check_token_next(get_rcurly_tk(), "invalid rewrite pattern, '}' expected"); return some_expr(r); } else { @@ -25,14 +25,14 @@ static expr parse_rule(parser & p, bool use_paren) { if (use_paren) { if (p.curr_is_token(get_lparen_tk())) { p.next(); - expr r = p.parse_expr(); + expr r = p.parse_tactic_expr_arg(); p.check_token_next(get_rparen_tk(), "invalid rewrite pattern, ')' expected"); return r; } else { - return p.parse_id(); + return p.parse_tactic_id_arg(); } } else { - return p.parse_expr(); + return p.parse_tactic_expr_arg(); } } @@ -66,7 +66,7 @@ static expr parse_rewrite_element(parser & p, bool use_paren) { return parse_rewrite_unfold(p); if (p.curr_is_token(get_down_tk())) { p.next(); - expr e = p.parse_expr(); + expr e = p.parse_tactic_expr_arg(); location loc = parse_tactic_location(p); return mk_rewrite_fold(e, loc); } @@ -108,7 +108,7 @@ static expr parse_rewrite_element(parser & p, bool use_paren) { location loc = parse_tactic_location(p); return mk_rewrite_reduce(loc); } else { - expr e = p.parse_expr(); + expr e = p.parse_tactic_expr_arg(); location loc = parse_tactic_location(p); return mk_rewrite_reduce_to(e, loc); } @@ -175,7 +175,7 @@ expr parse_fold_tactic(parser & p) { p.next(); while (true) { auto pos = p.pos(); - expr e = p.parse_expr(); + expr e = p.parse_tactic_expr_arg(); location loc = parse_tactic_location(p); elems.push_back(p.save_pos(mk_rewrite_fold(e, loc), pos)); if (!p.curr_is_token(get_comma_tk())) @@ -184,7 +184,7 @@ expr parse_fold_tactic(parser & p) { } p.check_token_next(get_rbracket_tk(), "invalid 'fold' tactic, ',' or ']' expected"); } else { - expr e = p.parse_expr(); + expr e = p.parse_tactic_expr_arg(); location loc = parse_tactic_location(p); elems.push_back(p.save_pos(mk_rewrite_fold(e, loc), pos));; } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 94cab6ca4..c1a503ad0 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1383,6 +1383,16 @@ static bool is_tactic_command_type(expr e) { return is_tactic_type(e); } +expr parser::parse_tactic_expr_arg(unsigned rbp) { + parser::undef_id_to_local_scope scope1(*this); + return parse_expr(rbp); +} + +expr parser::parse_tactic_id_arg() { + parser::undef_id_to_local_scope scope1(*this); + return parse_id(); +} + optional parser::is_tactic_command(name & id) { if (id.is_atomic()) id = get_tactic_name() + id; @@ -1410,7 +1420,7 @@ expr parser::parse_tactic_expr_list() { check_token_next(get_lbracket_tk(), "invalid tactic, '[' expected"); buffer args; while (true) { - args.push_back(parse_expr()); + args.push_back(parse_tactic_expr_arg()); if (!curr_is_token(get_comma_tk())) break; next(); @@ -1510,7 +1520,7 @@ expr parser::parse_tactic_nud() { rbp = 0; else rbp = get_max_prec(); - r = mk_app(r, parse_expr(rbp), id_pos); + r = mk_app(r, parse_tactic_expr_arg(rbp), id_pos); } } return r; diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 4d461ed0e..257e58b14 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -404,6 +404,8 @@ public: expr parse_scoped_expr(buffer const & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); } expr parse_tactic(unsigned rbp = 0); + expr parse_tactic_expr_arg(unsigned rbp = 0); + expr parse_tactic_id_arg(); struct local_scope { parser & m_p; environment m_env; local_scope(parser & p, bool save_options = false); diff --git a/tests/lean/tactic_error_msg.lean b/tests/lean/tactic_error_msg.lean new file mode 100644 index 000000000..6ed2b700d --- /dev/null +++ b/tests/lean/tactic_error_msg.lean @@ -0,0 +1,5 @@ +example (a b : Prop) : a → b → a ∧ b := +begin + intros, + splits +end diff --git a/tests/lean/tactic_error_msg.lean.expected.out b/tests/lean/tactic_error_msg.lean.expected.out new file mode 100644 index 000000000..a53193607 --- /dev/null +++ b/tests/lean/tactic_error_msg.lean.expected.out @@ -0,0 +1 @@ +tactic_error_msg.lean:4:2: error: unknown identifier 'splits'