From 6d09d82a7c65840d653de1d9a845a135e7d34e10 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Jun 2014 11:39:05 -0700
Subject: [PATCH] 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 | 31 +++++++++++++++++++---
 src/library/tactic/tactic.cpp              |  2 +-
 tests/lean/run/tactic3.lean                |  6 +++++
 3 files changed, 34 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/tactic3.lean

diff --git a/src/frontends/lean/builtin_tactic_cmds.cpp b/src/frontends/lean/builtin_tactic_cmds.cpp
index 9dfc89ccf..add8c1653 100644
--- a/src/frontends/lean/builtin_tactic_cmds.cpp
+++ b/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",
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 0e82d7373..1bf698861 100644
--- a/src/library/tactic/tactic.cpp
+++ b/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;
         });
diff --git a/tests/lean/run/tactic3.lean b/tests/lean/run/tactic3.lean
new file mode 100644
index 000000000..519a41b27
--- /dev/null
+++ b/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]