feat(library/tactic): polish tactic API, and add new example showing how to implement tactics using Lua

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

examples/lean/tactic_in_lua.lean

@@ -0,0 +1,72 @@
+(**
+ -- This example demonstrates how to create a new tactic using Lua.
+ -- The basic idea is to reimplement the tactic conj_tactic in Lua.
+
+ -- Tactic for splitting goals of the form
+ --      n : Hs |- A /\ B
+ -- into
+ --      n::1 : Hs |- A
+ --      n::2 : Hs |- B
+ function conj_fn(env, ios, s)
+    local gs = s:goals()
+    -- We store the information needed by the proof_builder in the
+    -- array proof_info.
+    -- proof_info has the format {{name_1, expr_1}, ... {name_k, expr_k}}
+    -- where name_i is a goal splitted by this tactic, and expr_i
+    -- is the conclusion of the theorem, that is, an expression of the form
+    --     A /\ B
+    local proof_info = {}
+    -- We store the new goals into the Lua array new_gs.
+    -- new_gs has the format {{name_1, goal_1}, ..., {name_n, goal_n}}
+    local new_gs     = {}
+    local found = false
+    for n, g in gs:pairs() do
+       yield() -- Give a chance to other tactics to run
+       local c = g:conclusion()
+       if c:is_and() then
+          -- Goal g is of the form Hs |- A /\ B
+          found = true -- The tactic managed to split at least one goal
+          local Hs = g:hypotheses()
+          local A  = c:arg(1)
+          local B  = c:arg(2)
+          proof_info[#proof_info + 1] = {n, c} -- Save information for implementing the proof builder
+          new_gs[#new_gs + 1]   = {name(n, 1), goal(Hs, A)} -- Add goal n::1 : Hs |- A
+          new_gs[#new_gs + 1]   = {name(n, 2), goal(Hs, B)} -- Add goal n::1 : Hs |- B
+       else
+          new_gs[#new_gs + 1]   = {n, g} -- Keep the goal
+       end
+    end
+    if not found then
+       return nil -- Tactic is not applicable
+    end
+    local pb     = s:proof_builder()
+    local new_pb =
+       function(m, a)
+          local Conj  = Const("Conj")
+          local new_m = proof_map(m) -- Copy proof map m
+          for _, p in ipairs(proof_info) do
+             local n = p[1]  -- n is the name of the goal splitted by this tactic
+             local c = p[2]  -- c is the conclusion of the goal splitted by this tactic
+             assert(c:is_and()) -- c is of the form A /\ B
+             -- The proof for goal n is
+             --      Conj(A, B, H1, H2)
+             -- where H1 and H2 are the proofs for goals n::1 and n::2
+             new_m:insert(n, Conj(c:arg(1), c:arg(2), m:find(name(n, 1)), m:find(name(n, 2))))
+             -- We don't need the proofs for n::1 and n::2 anymore
+             new_m:erase(name(n, 1))
+             new_m:erase(name(n, 2))
+          end
+          return pb(new_m, a) -- Apply the proof builder for the original state
+       end
+    return  proof_state(s, goals(new_gs), proof_builder(new_pb))
+ end
+ conj_in_lua = tactic(conj_fn) -- Create a new tactic object using the Lua function conj_fn
+ -- Now, the tactic conj_in_lua can be used when proving theorems in Lean.
+**)
+
+Theorem T (a b : Bool) : a => b => a /\ b := _.
+   apply (** REPEAT(ORELSE(imp_tactic, conj_in_lua)) .. assumption_tactic **)
+   done
+
+(* Show proof created using our script *)
+Show Environment 1.

src/frontends/lean/parser.cpp

@@ -157,6 +157,26 @@ class parser::imp {
         virtual void rethrow() const { throw *this; }
     };
 
+    template<typename F>
+    void using_script(F && f) {
+        m_script_state->apply([&](lua_State * L) {
+                set_io_state    set1(L, m_frontend.get_state());
+                set_environment set2(L, m_frontend.get_environment());
+                f(L);
+            });
+    }
+
+    template<typename F>
+    void code_with_callbacks(F && f) {
+        m_script_state->apply([&](lua_State * L) {
+                set_io_state    set1(L, m_frontend.get_state());
+                set_environment set2(L, m_frontend.get_environment());
+                m_script_state->exec_unprotected([&]() {
+                        f();
+                    });
+            });
+    }
+
     /**
         \brief Auxiliar struct for creating/destroying a new scope for
         local declarations.
@@ -1066,7 +1086,7 @@ class parser::imp {
                 tactic t;
                 if (curr() == scanner::token::ScriptBlock) {
                     parse_script_expr();
-                    m_script_state->apply([&](lua_State * L) {
+                    using_script([&](lua_State * L) {
                             if (is_tactic(L, -1))
                                 t = to_tactic(L, -1);
                             else
@@ -1074,7 +1094,7 @@ class parser::imp {
                         });
                 } else {
                     name tac_name = check_identifier_next("invalid apply command, identifier or 'script-block' expected");
-                    m_script_state->apply([&](lua_State * L) {
+                    using_script([&](lua_State * L) {
                             lua_getglobal(L, tac_name.to_string().c_str());
                             try {
                                 t = to_tactic_ext(L, -1);
@@ -1084,8 +1104,12 @@ class parser::imp {
                             lua_pop(L, 1);
                         });
                 }
+                proof_state_seq::maybe_pair r;
+                code_with_callbacks([&]() {
+                        // t may have call-backs we should set ios in the script_state
                         lazy_list<proof_state> seq = t(m_frontend, m_frontend.get_state(), s);
-                auto r = seq.pull();
+                        r = seq.pull();
+                    });
                 if (r) {
                     s = r->first;
                     stack.push_back(r->second);
@@ -1727,9 +1751,7 @@ class parser::imp {
             script_code = "return " + script_code;
         }
         next();
-        m_script_state->apply([&](lua_State * L) {
-                set_io_state    set1(L, m_frontend.get_state());
-                set_environment set2(L, m_frontend.get_environment());
+        using_script([&](lua_State * L) {
                 dostring(L, script_code.c_str());
             });
     }

src/library/kernel_bindings.cpp

@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/instantiate.h"
 #include "kernel/occurs.h"
+#include "kernel/builtin.h"
 #include "library/expr_lt.h"
 #include "library/kernel_bindings.h"
 #include "library/io_state.h"
@@ -453,6 +454,15 @@ EXPR_PRED(is_metavar)
 EXPR_PRED(has_free_vars)
 EXPR_PRED(closed)
 EXPR_PRED(has_metavar)
+EXPR_PRED(is_not)
+EXPR_PRED(is_and)
+EXPR_PRED(is_or)
+EXPR_PRED(is_if)
+EXPR_PRED(is_iff)
+EXPR_PRED(is_implies)
+EXPR_PRED(is_forall)
+EXPR_PRED(is_exists)
+EXPR_PRED(is_homo_eq)
 
 /**
    \brief Iterator (closure base function) for application args. See \c expr_args
@@ -637,6 +647,15 @@ static const struct luaL_Reg expr_m[] = {
     {"has_metavar",     safe_function<expr_has_metavar>},
     {"is_eqp",          safe_function<expr_is_eqp>},
     {"hash",            safe_function<expr_hash>},
+    {"is_not",          safe_function<expr_is_not>},
+    {"is_and",          safe_function<expr_is_and>},
+    {"is_or",           safe_function<expr_is_or>},
+    {"is_if",           safe_function<expr_is_if>},
+    {"is_iff",          safe_function<expr_is_iff>},
+    {"is_implies",      safe_function<expr_is_implies>},
+    {"is_forall",       safe_function<expr_is_forall>},
+    {"is_exists",       safe_function<expr_is_exists>},
+    {"is_home_eq",      safe_function<expr_is_homo_eq>},
     {0, 0}
 };
 

src/library/tactic/proof_builder.cpp

@@ -22,7 +22,11 @@ expr find(proof_map const & m, name const & n) {
 DECL_UDATA(proof_map)
 
 static int mk_proof_map(lua_State * L) {
+    int nargs = lua_gettop(L);
+    if (nargs == 0)
         return push_proof_map(L, proof_map());
+    else
+        return push_proof_map(L, to_proof_map(L, 1));
 }
 
 static int proof_map_len(lua_State * L) {

src/library/tactic/proof_state.cpp

@@ -88,6 +88,26 @@ static int mk_goals(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 0) {
         return push_goals(L, goals());
+    } else if (nargs == 1) {
+        // convert a Lua table of the form {{n_1, g_1}, ..., {n_n, g_n}} into a goal list
+        goals gs;
+        int len = objlen(L, 1);
+        for (int i = len; i >= 1; i--) {
+            lua_pushinteger(L, i);
+            lua_gettable(L, 1);  // now table {n_i, g_i} is on the top
+            if (!lua_istable(L, -1) || objlen(L, -1) != 2)
+                throw exception("arg #1 must be of the form '{{name, goal}, ...}'");
+            lua_pushinteger(L, 1);
+            lua_gettable(L, -2);
+            name n_i = to_name_ext(L, -1);
+            lua_pop(L, 1);  // remove n_i from the stack
+            lua_pushinteger(L, 2);
+            lua_gettable(L, -2);
+            goal g_i = to_goal(L, -1);
+            lua_pop(L, 2); // remove the g_i and table {n_i, g_i} from the stack
+            gs = goals(mk_pair(n_i, g_i), gs);
+        }
+        return push_goals(L, gs);
     } else if (nargs == 2) {
         return push_goals(L, goals(mk_pair(to_name_ext(L, 1), to_goal(L, 2)), goals()));
     } else if (nargs == 3) {

src/util/script_state.cpp

@@ -549,9 +549,22 @@ static int sleep(lua_State * L) {
     return 0;
 }
 
+static int yield(lua_State * L) {
+    check_interrupted();
+    int status = lua_pushthread(L);
+    lua_pop(L, 1);
+    if (status != 1) {
+        return lua_yield(L, 0);
+    } else {
+        // main thread cannot yield
+        return 0;
+    }
+}
+
 static void open_interrupt(lua_State * L) {
     SET_GLOBAL_FUN(check_interrupted, "check_interrupted");
     SET_GLOBAL_FUN(sleep,             "sleep");
+    SET_GLOBAL_FUN(yield,             "yield");
     SET_GLOBAL_FUN(channel_read,      "read");
     SET_GLOBAL_FUN(channel_write,     "write");
 }