From 98897b467d082ec7133c559df06e98cfd5cbce5d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Nov 2013 10:21:17 -0800
Subject: [PATCH] feat(frontends/lean/parser): add support for Lua expression
 code blocks

In expression code blocks, we do not have to write a "return".
After this commit, the argument of an apply command is a Lua expression instead of a Lua block of code. That is, we can now write

apply (** REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)

instead of

apply (** return REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp | 13 +++++++++++--
 tests/lean/tactic2.lean       |  2 +-
 tests/lean/tactic3.lean       |  2 +-
 3 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 0a51885589..8bf684e385 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1065,7 +1065,7 @@ class parser::imp {
                 auto tac_pos = pos();
                 optional<tactic> t;
                 if (curr() == scanner::token::ScriptBlock) {
-                    parse_script();
+                    parse_script_expr();
                     m_script_state->apply([&](lua_State * L) {
                             if (is_tactic(L, -1))
                                 t = to_tactic(L, -1);
@@ -1714,11 +1714,18 @@ class parser::imp {
             next();
     }
 
-    void parse_script() {
+    /**
+       \brief Parse a block of Lua code. If as_expr is true, then
+       it appends the string "return " in front of the script.
+    */
+    void parse_script(bool as_expr = false) {
         m_last_script_pos = mk_pair(m_scanner.get_script_block_line(), m_scanner.get_script_block_pos());
         if (!m_script_state)
             throw exception("failed to execute Lua script, parser does not have a Lua interpreter");
         std::string script_code = m_scanner.get_str_val();
+        if (as_expr) {
+            script_code = "return " + script_code;
+        }
         next();
         m_script_state->apply([&](lua_State * L) {
                 set_io_state    set1(L, m_frontend.get_state());
@@ -1727,6 +1734,8 @@ class parser::imp {
             });
     }
 
+    void parse_script_expr() { return parse_script(true); }
+
 public:
     imp(frontend & fe, std::istream & in, script_state * S, bool use_exceptions, bool interactive):
         m_frontend(fe),
diff --git a/tests/lean/tactic2.lean b/tests/lean/tactic2.lean
index 3bfbb6a162..8e8ead1563 100644
--- a/tests/lean/tactic2.lean
+++ b/tests/lean/tactic2.lean
@@ -23,7 +23,7 @@ Theorem T2 : p => q => p /\ q /\ p := _.
 Show Environment 1
 
 Theorem T3 : p => p /\ q => r => q /\ r /\ p := _.
-    apply (** return REPEAT(imp_tactic() ^ conj_tactic() ^ conj_hyp_tactic() ^ assumption_tactic()) **)
+    apply (** REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)
     done
 
 (* Display proof term generated by previous tactic *)
diff --git a/tests/lean/tactic3.lean b/tests/lean/tactic3.lean
index bb13c5857f..8d09e1efcb 100644
--- a/tests/lean/tactic3.lean
+++ b/tests/lean/tactic3.lean
@@ -1,7 +1,7 @@
 Variables p q r : Bool
 
 Theorem T1 : p => p /\ q => r => q /\ r /\ p := _.
-    apply (** return REPEAT(ORELSE(imp_tactic(), conj_tactic(), conj_hyp_tactic(), assumption_tactic())) **)
+    apply (** REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)
     done
 
 (* Display proof term generated by previous tactic *)