From e6fb6f7d1eb558463dd1724ef2d20b7a598a7fdc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Dec 2013 20:08:36 -0800
Subject: [PATCH] feat(frontends/lean/parser): add assumption command, and
 allow Lean expressions (proof terms) to be used with apply tactic command

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

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 9865545279..be2228de29 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -98,7 +98,8 @@ static name g_apply("apply");
 static name g_done("done");
 static name g_back("back");
 static name g_abort("abort");
-static list<name> g_tactic_cmds = { g_apply, g_done, g_back, g_abort };
+static name g_assumption("assumption");
+static list<name> g_tactic_cmds = { g_apply, g_done, g_back, g_abort, g_assumption };
 /** \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,
@@ -1260,6 +1261,21 @@ class parser::imp {
         throw tactic_cmd_error("failed to backtrack", p, s);
     }
 
+    void tactic_apply(proof_state_seq_stack & stack, proof_state & s, tactic const & t, pos_info const & tac_pos) {
+        proof_state_seq::maybe_pair r;
+        code_with_callbacks([&]() {
+                // t may have call-backs we should set ios in the script_state
+                proof_state_seq seq = t(m_frontend, m_frontend.get_state(), s);
+                r = seq.pull();
+            });
+        if (r) {
+            s = r->first;
+            stack.push_back(r->second);
+        } else {
+            throw tactic_cmd_error("tactic failed", tac_pos, s);
+        }
+    }
+
     void tactic_apply(proof_state_seq_stack & stack, proof_state & s) {
         auto tac_pos = pos();
         next();
@@ -1267,13 +1283,20 @@ class parser::imp {
         if (curr() == scanner::token::ScriptBlock) {
             parse_script_expr();
             using_script([&](lua_State * L) {
-                    if (is_tactic(L, -1))
-                        t = to_tactic(L, -1);
-                    else
+                    try {
+                        t = to_tactic_ext(L, -1);
+                    } catch (...) {
                         throw tactic_cmd_error(sstream() << "invalid script-block, it must return a tactic", tac_pos, s);
+                    }
                 });
+        } else if (curr_is_lparen()) {
+            next();
+            expr pr      = parse_expr();
+            check_rparen_next("invalid apply command, ')' expected");
+            expr pr_type = m_type_inferer(pr);
+            t = apply_tactic(pr, pr_type);
         } else {
-            name n = check_identifier_next("invalid apply command, identifier or 'script-block' expected");
+           name n = check_identifier_next("invalid apply command, identifier, '(' expr ')', or 'script-block' expected");
             object const & o = m_frontend.find_object(n);
             if (o && (o.is_theorem() || o.is_axiom())) {
                 t = apply_tactic(n);
@@ -1289,18 +1312,13 @@ class parser::imp {
                     });
             }
         }
-        proof_state_seq::maybe_pair r;
-        code_with_callbacks([&]() {
-                // t may have call-backs we should set ios in the script_state
-                proof_state_seq seq = t(m_frontend, m_frontend.get_state(), s);
-                r = seq.pull();
-            });
-        if (r) {
-            s = r->first;
-            stack.push_back(r->second);
-        } else {
-            throw tactic_cmd_error("tactic failed", tac_pos, s);
-        }
+        tactic_apply(stack, s, t, tac_pos);
+    }
+
+    void tactic_assumption(proof_state_seq_stack & stack, proof_state & s) {
+        auto tac_pos = pos();
+        next();
+        tactic_apply(stack, s, assumption_tactic(), tac_pos);
     }
 
     expr tactic_done(proof_state const & s) {
@@ -1370,6 +1388,8 @@ class parser::imp {
                         } else if (id == g_abort) {
                             next();
                             st = status::Abort;
+                        } else if (id == g_assumption) {
+                            tactic_assumption(stack, s);
                         } else {
                             next();
                             throw tactic_cmd_error(sstream() << "invalid tactic command '" << id << "'", p, s);
diff --git a/tests/lean/interactive/t7.lean b/tests/lean/interactive/t7.lean
new file mode 100644
index 0000000000..094dbbb4b3
--- /dev/null
+++ b/tests/lean/interactive/t7.lean
@@ -0,0 +1,9 @@
+Variable q : Int -> Int -> Bool.
+Variable p : Int -> Bool.
+Axiom Ax (a b : Int) (H : q a b) : p b.
+Variable a : Int.
+Theorem T (x : Int) : (q a x) => (p x).
+    apply imp_tac.
+    apply (Ax a).
+    assumption.
+    done.
diff --git a/tests/lean/interactive/t7.lean.expected.out b/tests/lean/interactive/t7.lean.expected.out
new file mode 100644
index 0000000000..0be1633c5e
--- /dev/null
+++ b/tests/lean/interactive/t7.lean.expected.out
@@ -0,0 +1,17 @@
+Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
+#   Set: pp::colors
+  Set: pp::unicode
+  Assumed: q
+#   Assumed: p
+#   Assumed: Ax
+#   Assumed: a
+# Proof state:
+x : ℤ ⊢ (q a x) ⇒ (p x)
+## Proof state:
+H : q a x, x : ℤ ⊢ p x
+## Proof state:
+H : q a x, x : ℤ ⊢ q a x
+## Proof state:
+no goals
+##   Proved: T
+# 
\ No newline at end of file