From 60f32fa709193fca555a3ff7f8b39eed58ee8d6a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Oct 2014 17:12:25 -0700 Subject: [PATCH] fix(frontends/lean): `begin-end` automatic tactic notation bug, fixes #262 --- src/frontends/lean/builtin_exprs.cpp | 13 ++++++++----- src/frontends/lean/parse_table.cpp | 11 ++++++++++- src/frontends/lean/parse_table.h | 2 ++ src/frontends/lean/parser.cpp | 8 +++++++- tests/lean/run/tactic_notation.lean | 11 +++++++++++ 5 files changed, 38 insertions(+), 7 deletions(-) create mode 100644 tests/lean/run/tactic_notation.lean diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 8cdb62577..765d677e6 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -128,9 +128,12 @@ static environment open_tactic_namespace(parser & p) { } static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) { - parser::undef_id_to_local_scope scope(p); environment env = open_tactic_namespace(p); - expr t = p.parse_scoped_expr(0, nullptr, env); + parser::undef_id_to_local_scope scope(p); + parser::local_scope scope2(p, env); + parser::undef_id_to_local_scope scope1(p); + p.next(); + expr t = p.parse_expr(); return p.mk_by(t, pos); } @@ -140,6 +143,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) { environment env = open_tactic_namespace(p); parser::local_scope scope2(p, env); parser::undef_id_to_local_scope scope1(p); + p.next(); optional pre_tac = get_begin_end_pre_tactic(env); buffer tacs; bool first = true; @@ -209,7 +213,6 @@ static expr parse_proof(parser & p, expr const & prop) { return parse_proof_qed_core(p, pos); } else if (p.curr_is_token(get_begin_tk())) { auto pos = p.pos(); - p.next(); return parse_begin_end_core(p, pos); } else if (p.curr_is_token(get_by_tk())) { // parse: 'by' tactic @@ -420,7 +423,7 @@ parse_table init_nud_table() { expr x0 = mk_var(0); parse_table r; r = r.add({transition("_", mk_ext_action(parse_placeholder))}, x0); - r = r.add({transition("by", mk_ext_action(parse_by))}, x0); + r = r.add({transition("by", mk_ext_action_core(parse_by))}, x0); r = r.add({transition("have", mk_ext_action(parse_have))}, x0); r = r.add({transition("show", mk_ext_action(parse_show))}, x0); r = r.add({transition("obtain", mk_ext_action(parse_obtain))}, x0); @@ -433,7 +436,7 @@ parse_table init_nud_table() { r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0); r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0); r = r.add({transition("!", mk_ext_action(parse_consume_args_expr))}, x0); - r = r.add({transition("begin", mk_ext_action(parse_begin_end))}, x0); + r = r.add({transition("begin", mk_ext_action_core(parse_begin_end))}, x0); r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, x0); r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0); return r; diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp index 0aad72210..d6a93949e 100644 --- a/src/frontends/lean/parse_table.cpp +++ b/src/frontends/lean/parse_table.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "library/kernel_bindings.h" #include "frontends/lean/parse_table.h" +#include "frontends/lean/parser.h" #include "frontends/lean/no_info.h" namespace lean { @@ -251,7 +252,15 @@ action mk_scoped_expr_action(expr const & rec, unsigned rb, bool lambda) { expr new_rec = annotate_macro_subterms(rec); return action(new scoped_expr_action_cell(new_rec, rb, lambda)); } -action mk_ext_action(parse_fn const & fn) { return action(new ext_action_cell(fn)); } +action mk_ext_action_core(parse_fn const & fn) { return action(new ext_action_cell(fn)); } +action mk_ext_action(parse_fn const & fn) { + auto new_fn = [=](parser & p, unsigned num, expr const * args, pos_info const & pos) -> expr { + p.next(); + return fn(p, num, args, pos); + }; + return action(new ext_action_cell(new_fn)); +} + action mk_ext_lua_action(char const * fn) { return action(new ext_lua_action_cell(fn)); } action replace(action const & a, std::function const & f) { diff --git a/src/frontends/lean/parse_table.h b/src/frontends/lean/parse_table.h index c7d04f04d..ffe210dd7 100644 --- a/src/frontends/lean/parse_table.h +++ b/src/frontends/lean/parse_table.h @@ -63,6 +63,7 @@ public: friend action mk_exprs_action(name const & sep, expr const & rec, expr const & ini, optional const & terminator, bool right, unsigned rbp); friend action mk_scoped_expr_action(expr const & rec, unsigned rbp, bool lambda); + friend action mk_ext_action_core(parse_fn const & fn); friend action mk_ext_action(parse_fn const & fn); friend action mk_ext_lua_action(char const * lua_fn); @@ -93,6 +94,7 @@ action mk_exprs_action(name const & sep, expr const & rec, expr const & ini, opt action mk_binder_action(); action mk_binders_action(); action mk_scoped_expr_action(expr const & rec, unsigned rbp = 0, bool lambda = true); +action mk_ext_action_core(parse_fn const & fn); action mk_ext_action(parse_fn const & fn); action mk_ext_lua_action(char const * lua_fn); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 315a263f6..6c8ce0331 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -869,15 +869,17 @@ expr parser::parse_notation(parse_table t, expr * left) { auto r = t.find(get_token_info().value()); if (!r) break; - next(); notation::action const & a = r->first; switch (a.kind()) { case notation::action_kind::Skip: + next(); break; case notation::action_kind::Expr: + next(); args.push_back(parse_expr(a.rbp())); break; case notation::action_kind::Exprs: { + next(); buffer r_args; auto terminator = a.get_terminator(); if (!terminator || !curr_is_token(*terminator)) { @@ -917,14 +919,17 @@ expr parser::parse_notation(parse_table t, expr * left) { break; } case notation::action_kind::Binder: + next(); binder_pos = pos(); ps.push_back(parse_binder()); break; case notation::action_kind::Binders: + next(); binder_pos = pos(); lenv = parse_binders(ps); break; case notation::action_kind::ScopedExpr: { + next(); expr r = parse_scoped_expr(ps, lenv, a.rbp()); bool no_cache = false; if (is_var(a.get_rec(), 0)) { @@ -953,6 +958,7 @@ expr parser::parse_notation(parse_table t, expr * left) { break; } case notation::action_kind::LuaExt: + next(); m_last_script_pos = p; using_script([&](lua_State * L) { scoped_set_parser scope(L, *this); diff --git a/tests/lean/run/tactic_notation.lean b/tests/lean/run/tactic_notation.lean new file mode 100644 index 000000000..df3caa566 --- /dev/null +++ b/tests/lean/run/tactic_notation.lean @@ -0,0 +1,11 @@ +import logic + +theorem tst1 (a b c : Prop) : a → b → a ∧ b := +begin + intros, + apply and.intro, + assumption +end + +theorem tst2 (a b c : Prop) : a → b → a ∧ b := +by intros; apply and.intro; assumption