From a7027a1d00a248f0bfda3eab3a1197f81153c23b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 30 Nov 2013 00:14:33 -0800 Subject: [PATCH] feat(library/tactic): polish tactic API, and add new example showing how to implement tactics using Lua Signed-off-by: Leonardo de Moura --- examples/lean/tactic_in_lua.lean | 72 ++++++++++++++++++++++++++++ src/frontends/lean/parser.cpp | 36 +++++++++++--- src/library/kernel_bindings.cpp | 19 ++++++++ src/library/tactic/proof_builder.cpp | 6 ++- src/library/tactic/proof_state.cpp | 20 ++++++++ src/util/script_state.cpp | 13 +++++ 6 files changed, 158 insertions(+), 8 deletions(-) create mode 100644 examples/lean/tactic_in_lua.lean diff --git a/examples/lean/tactic_in_lua.lean b/examples/lean/tactic_in_lua.lean new file mode 100644 index 000000000..71974dc8e --- /dev/null +++ b/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. diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index fd0c1035d..093f7c408 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -157,6 +157,26 @@ class parser::imp { virtual void rethrow() const { throw *this; } }; + template + 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 + 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); }); } - lazy_list seq = t(m_frontend, m_frontend.get_state(), s); - auto r = seq.pull(); + proof_state_seq::maybe_pair r; + code_with_callbacks([&]() { + // t may have call-backs we should set ios in the script_state + lazy_list seq = t(m_frontend, m_frontend.get_state(), s); + 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()); }); } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index d720b6a08..b73c33cb3 100644 --- a/src/library/kernel_bindings.cpp +++ b/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}, {"is_eqp", safe_function}, {"hash", safe_function}, + {"is_not", safe_function}, + {"is_and", safe_function}, + {"is_or", safe_function}, + {"is_if", safe_function}, + {"is_iff", safe_function}, + {"is_implies", safe_function}, + {"is_forall", safe_function}, + {"is_exists", safe_function}, + {"is_home_eq", safe_function}, {0, 0} }; diff --git a/src/library/tactic/proof_builder.cpp b/src/library/tactic/proof_builder.cpp index 1e63e238e..50b999473 100644 --- a/src/library/tactic/proof_builder.cpp +++ b/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) { - return push_proof_map(L, proof_map()); + 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) { diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 96821bcc8..46408667a 100644 --- a/src/library/tactic/proof_state.cpp +++ b/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) { diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp index eaac79e34..3172b4e4c 100644 --- a/src/util/script_state.cpp +++ b/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"); }