feat(frontends/lean): add notation for orelse tactic, add show and now tactics

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/builtin_tactic_cmds.cpp

@@ -9,10 +9,13 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name g_comma(",");
+static name g_bar("|");
 static name g_rbracket("]");
 
 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_echo_tactic(parser & p) {
     if (!p.curr_is_string())
@@ -22,13 +25,31 @@ tactic parse_echo_tactic(parser & p) {
     return r;
 }
 tactic parse_tactic_seq(parser & p) {
+    buffer<tactic> choices;
     tactic r = p.parse_tactic();
-    while (p.curr_is_token(g_comma)) {
-        p.next();
-        r = then(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");
-    return r;
+    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); }
@@ -36,6 +57,8 @@ void add_tactic(tactic_cmd_table & t, tactic_cmd_info && info) { t.insert(info.g
 tactic_cmd_table get_builtin_tactic_cmds() {
     tactic_cmd_table t;
     add_tactic(t, tactic_cmd_info("fail", "always fail tactic", parse_fail_tactic));
+    add_tactic(t, tactic_cmd_info("show", "show goals tactic", parse_show_tactic));
+    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("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",

src/library/tactic/tactic.cpp

@@ -86,7 +86,7 @@ tactic trace_tactic(char const * msg) {
 
 tactic trace_state_tactic() {
     return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
-            diagnostic(env, ios) << s;
+            diagnostic(env, ios) << s << endl;
             ios.get_diagnostic_channel().get_stream().flush();
             return s;
         });

tests/lean/run/tactic3.lean

@@ -0,0 +1,6 @@
+import logic
+
+theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
+:= by [echo "first try",  show, now  |
+       echo "second try", fail       |
+       echo "third try", exact]