From 6645fdeae075afa204b308b74d49808fbbd3ceb2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Jun 2014 12:24:13 -0700 Subject: [PATCH] feat(frontends/lean): add repeat tactic command, refactor tactic sequence notation Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_tactic_cmds.cpp | 46 +++++++--------------- src/frontends/lean/parser.cpp | 36 +++++++++++++++-- src/frontends/lean/token_table.cpp | 2 +- tests/lean/run/tactic5.lean | 6 +++ tests/lean/run/tactic6.lean | 9 +++++ 5 files changed, 62 insertions(+), 37 deletions(-) create mode 100644 tests/lean/run/tactic5.lean create mode 100644 tests/lean/run/tactic6.lean diff --git a/src/frontends/lean/builtin_tactic_cmds.cpp b/src/frontends/lean/builtin_tactic_cmds.cpp index 4099e0cbc8..3e56ba3d78 100644 --- a/src/frontends/lean/builtin_tactic_cmds.cpp +++ b/src/frontends/lean/builtin_tactic_cmds.cpp @@ -8,15 +8,14 @@ Author: Leonardo de Moura #include "frontends/lean/parser.h" namespace lean { -static name g_comma(","); -static name g_bar("|"); -static name g_rbracket("]"); +static name g_bang("!"); tactic parse_fail_tactic(parser &) { return fail_tactic(); } tactic parse_id_tactic(parser &) { return id_tactic(); } tactic parse_now_tactic(parser &) { return now_tactic(); } tactic parse_show_tactic(parser &) { return trace_state_tactic(); } tactic parse_assumption_tactic(parser &) { return assumption_tactic(); } + tactic parse_unfold_tactic(parser & p) { auto pos = p.pos(); expr id = p.parse_expr(); @@ -25,6 +24,16 @@ tactic parse_unfold_tactic(parser & p) { return unfold_tactic(const_name(id)); } +tactic parse_repeat_tactic(parser & p) { + tactic t = p.parse_tactic(); + if (p.curr_is_numeral()) { + unsigned n = p.parse_small_nat(); + return repeat_at_most(t, n); + } else { + return repeat(t); + } +} + tactic parse_echo_tactic(parser & p) { if (!p.curr_is_string()) throw parser_error("invalid 'echo' tactic, string expected", p.pos()); @@ -32,33 +41,6 @@ tactic parse_echo_tactic(parser & p) { p.next(); return r; } -tactic parse_tactic_seq(parser & p) { - buffer choices; - tactic r = p.parse_tactic(); - while (true) { - if (p.curr_is_token(g_comma)) { - p.next(); - r = then(r, p.parse_tactic()); - } else if (p.curr_is_token(g_bar)) { - p.next(); - choices.push_back(r); - r = p.parse_tactic(); - } else { - break; - } - } - p.check_token_next(g_rbracket, "invalid tactic sequence, ']' expected"); - if (choices.empty()) { - return r; - } else { - choices.push_back(r); - r = choices[0]; - for (unsigned i = 1; i < choices.size(); i++) { - r = orelse(r, choices[i]); - } - return r; - } -} void add_tactic(tactic_cmd_table & t, tactic_cmd_info && info) { t.insert(info.get_name(), info); } @@ -69,13 +51,13 @@ tactic_cmd_table get_builtin_tactic_cmds() { add_tactic(t, tactic_cmd_info("now", "succeeds only if all goals have been solved", parse_now_tactic)); add_tactic(t, tactic_cmd_info("echo", "trace tactic: display message", parse_echo_tactic)); add_tactic(t, tactic_cmd_info("unfold", "unfold definition", parse_unfold_tactic)); + add_tactic(t, tactic_cmd_info("repeat", "repeat tactic", parse_repeat_tactic)); + add_tactic(t, tactic_cmd_info("!", "repeat tactic", parse_repeat_tactic)); add_tactic(t, tactic_cmd_info("id", "do nothing tactic", parse_id_tactic)); add_tactic(t, tactic_cmd_info("assumption", "solve goal if there is an assumption that is identical to the conclusion", parse_assumption_tactic)); add_tactic(t, tactic_cmd_info("exact", "solve goal if there is an assumption that is identical to the conclusion", parse_assumption_tactic)); - add_tactic(t, tactic_cmd_info("[", "tactic command sequence", - parse_tactic_seq)); return t; } } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index a7a40da125..ad48da8dc7 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -400,6 +400,8 @@ static name g_ldcurly("⦃"); static name g_rdcurly("⦄"); static name g_lbracket("["); static name g_rbracket("]"); +static name g_bar("|"); +static name g_comma(","); static name g_add("+"); static name g_max("max"); static name g_imax("imax"); @@ -956,11 +958,37 @@ expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e, } tactic parser::parse_tactic(unsigned /* rbp */) { - if (curr_is_token(g_lparen)) { + if (curr_is_token(g_lparen) || curr_is_token(g_lbracket)) { + bool paren = curr_is_token(g_lparen); next(); - auto r = parse_tactic(); - check_token_next(g_rparen, "invalid tactic, ')' expected"); - return r; + buffer choices; + tactic r = parse_tactic(); + while (true) { + if (curr_is_token(g_comma)) { + next(); + r = then(r, parse_tactic()); + } else if (curr_is_token(g_bar)) { + next(); + choices.push_back(r); + r = parse_tactic(); + } else { + break; + } + } + if (paren) + check_token_next(g_rparen, "invalid tactic sequence, ')' expected"); + else + check_token_next(g_rbracket, "invalid tactic sequence, ']' expected"); + if (choices.empty()) { + return r; + } else { + choices.push_back(r); + r = choices[0]; + for (unsigned i = 1; i < choices.size(); i++) { + r = orelse(r, choices[i]); + } + return r; + } } else { name id; auto p = pos(); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 4e4c95743c..e0c5566e8f 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -57,7 +57,7 @@ token_table init_token_table() { std::pair builtin[] = {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0}, {"then", 0}, {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, - {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"with", 0}, + {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", 0}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; diff --git a/tests/lean/run/tactic5.lean b/tests/lean/run/tactic5.lean new file mode 100644 index 0000000000..668df0a932 --- /dev/null +++ b/tests/lean/run/tactic5.lean @@ -0,0 +1,6 @@ +import logic + +definition id {A : Type} (a : A) := a + +theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A +:= by [!(unfold id, show), exact] diff --git a/tests/lean/run/tactic6.lean b/tests/lean/run/tactic6.lean new file mode 100644 index 0000000000..49daf7e73c --- /dev/null +++ b/tests/lean/run/tactic6.lean @@ -0,0 +1,9 @@ +import logic + +definition id {A : Type} (a : A) := a + +theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A +:= by [!echo "message" 5, unfold id, exact] + +theorem tst2 {A B : Bool} (H1 : A) (H2 : B) : id A +:= by [repeat echo "message" 5, unfold id, exact] \ No newline at end of file