From e069ce640bc8b87c434abc2de1b2145858c143f5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Dec 2013 17:15:19 -0800
Subject: [PATCH] feat(frontends/lean/parser): add tactic abort command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp               | 24 +++++++++++++--------
 tests/lean/interactive/t2.lean              |  9 ++++++++
 tests/lean/interactive/t2.lean.expected.out | 21 ++++++++++++++++++
 3 files changed, 45 insertions(+), 9 deletions(-)
 create mode 100644 tests/lean/interactive/t2.lean
 create mode 100644 tests/lean/interactive/t2.lean.expected.out

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index ecd4863b2..b1a05500c 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -96,7 +96,8 @@ static name g_exit_kwd("Exit");
 static name g_apply("apply");
 static name g_done("done");
 static name g_back("back");
-static list<name> g_tactic_cmds = { g_apply, g_done, g_back };
+static name g_abort("abort");
+static list<name> g_tactic_cmds = { g_apply, g_done, g_back, g_abort };
 /** \brief Table/List with all builtin command keywords */
 static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd,
                                         g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_echo_kwd,
@@ -1333,8 +1334,9 @@ class parser::imp {
         proof_state ini = s;
         proof_state_seq_stack stack;
         expr pr;
-        bool done = false;
-        while (!done) {
+        enum class status { Continue, Done, Eof, Abort };
+        status st = status::Continue;
+        while (st == status::Continue) {
             protected_call(
                 [&]() {
                     auto p = pos();
@@ -1347,7 +1349,7 @@ class parser::imp {
                         next();
                         break;
                     case scanner::token::Eof:
-                        done = true;
+                        st = status::Eof;
                         break;
                     case scanner::token::Id:
                         id = curr_name();
@@ -1358,7 +1360,10 @@ class parser::imp {
                         } else if (id == g_done) {
                             pr = tactic_done(s);
                             if (pr)
-                                done = true;
+                                st = status::Done;
+                        } else if (id == g_abort) {
+                            next();
+                            st = status::Abort;
                         } else {
                             next();
                             throw tactic_cmd_error(sstream() << "invalid tactic command '" << id << "'", p, s);
@@ -1379,10 +1384,11 @@ class parser::imp {
                         next();
                 });
         }
-        if (pr) {
-            return pr;
-        } else {
-            throw parser_error("invalid tactic command, unexpected end of file", pos());
+        switch (st) {
+        case status::Done:  return pr;
+        case status::Eof:   throw parser_error("invalid tactic command, unexpected end of file", pos());
+        case status::Abort: throw parser_error("failed to prove theorem, proof has been aborted", pos());
+        default: lean_unreachable(); // LCOV_EXCL_LINE
         }
     }
 
diff --git a/tests/lean/interactive/t2.lean b/tests/lean/interactive/t2.lean
new file mode 100644
index 000000000..412e2cacc
--- /dev/null
+++ b/tests/lean/interactive/t2.lean
@@ -0,0 +1,9 @@
+Theorem T2 (a b : Bool) : a => b => a /\ b.
+apply imp_tactic.
+apply imp_tactic2.
+foo.
+apply imp_tactic.
+abort.
+
+Variables a b : Bool.
+Show Environment 2.
diff --git a/tests/lean/interactive/t2.lean.expected.out b/tests/lean/interactive/t2.lean.expected.out
new file mode 100644
index 000000000..04d5a349f
--- /dev/null
+++ b/tests/lean/interactive/t2.lean.expected.out
@@ -0,0 +1,21 @@
+Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
+#   Set: pp::colors
+  Set: pp::unicode
+Proof state:
+a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
+## Proof state:
+H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
+## Error (line: 6, pos: 0) unknown tactic 'imp_tactic2'
+Proof state:
+H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
+## Error (line: 7, pos: 0) invalid tactic command 'foo'
+Proof state:
+H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
+## Proof state:
+H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
+## Error (line: 9, pos: 5) failed to prove theorem, proof has been aborted
+# #   Assumed: a
+  Assumed: b
+# Variable a : Bool
+Variable b : Bool
+# 
\ No newline at end of file