michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/tactic): simplify tactic framework, no more proof builders

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-01 16:11:19 -07:00
parent d4b29cd132
commit 4cb5f97038
16 changed files with 240 additions and 578 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/frontends/lean/elaborator.cpp
View file

@ -610,21 +610,16 @@ public:
collect_metavars(e, mvars); collect_metavars(e, mvars);
for (auto mvar : mvars) { for (auto mvar : mvars) {
mvar = update_mlocal(mvar, subst.instantiate_metavars_wo_jst(mlocal_type(mvar))); mvar = update_mlocal(mvar, subst.instantiate_metavars_wo_jst(mlocal_type(mvar)));
proof_state ps = to_proof_state(m_env, mvar, m_ngen.mk_child(), m_ios.get_options()); proof_state ps = to_proof_state(mvar, m_ngen.mk_child());
if (optional<tactic> t = get_tactic_for(mvar)) { if (optional<tactic> t = get_tactic_for(mvar)) {
proof_state_seq seq = (*t)(m_env, m_ios, ps); proof_state_seq seq = (*t)(m_env, m_ios, ps);
if (auto r = seq.pull()) { if (auto r = seq.pull()) {
try { substitution s = r->first.get_subst();
if (auto pr = to_proof(r->first)) { expr v = s.instantiate_metavars_wo_jst(mvar);
subst = subst.assign(mlocal_name(mvar), *pr, justification()); if (has_metavar(v)) {
} else { display_unsolved_proof_state(mvar, r->first, "unsolved subgoals");
display_unsolved_proof_state(mvar, r->first, "unsolved subgoals"); } else {
} subst = subst.assign(mlocal_name(mvar), v);
} catch (exception & ex) {
regular out(m_env, m_ios);
display_error_pos(out, m_pos_provider, mvar);
out << " proof generation failed\n >> ";
display_error(out, nullptr, ex);
} }
} else { } else {
// tactic failed to produce any result // tactic failed to produce any result

8
src/frontends/lean/parser.cpp
View file

@ -945,6 +945,9 @@ static list<expr> collect_contextual_parameters(local_expr_decls const & local_d
} }
tactic parser::parse_exact_apply() { tactic parser::parse_exact_apply() {
parse_expr();
return id_tactic();
#if 0
auto p = pos(); auto p = pos();
expr e = parse_expr(); expr e = parse_expr();
check_only_contextual_locals(e, m_local_decls, p); check_only_contextual_locals(e, m_local_decls, p);
@ -979,9 +982,13 @@ tactic parser::parse_exact_apply() {
proof_builder new_pb = add_proof(s.get_pb(), gname, new_e); proof_builder new_pb = add_proof(s.get_pb(), gname, new_e);
return some_proof_state(proof_state(s, new_gs, new_pb, ngen)); return some_proof_state(proof_state(s, new_gs, new_pb, ngen));
}); });
#endif
} }
tactic parser::parse_apply() { tactic parser::parse_apply() {
parse_expr();
return id_tactic();
#if 0
auto p = pos(); auto p = pos();
expr e = parse_expr(); expr e = parse_expr();
check_only_contextual_locals(e, m_local_decls, p); check_only_contextual_locals(e, m_local_decls, p);
@ -1000,6 +1007,7 @@ tactic parser::parse_apply() {
new_e = instantiate(new_e, l); new_e = instantiate(new_e, l);
return apply_tactic(new_e)(env, ios, new_s); return apply_tactic(new_e)(env, ios, new_s);
}); });
#endif
} }
tactic parser::parse_tactic(unsigned /* rbp */) { tactic parser::parse_tactic(unsigned /* rbp */) {

1
src/kernel/expr.h
View file

@ -217,6 +217,7 @@ public:
bool is_cast() const { return m_cast; } bool is_cast() const { return m_cast; }
bool is_contextual() const { return m_contextual; } bool is_contextual() const { return m_contextual; }
bool is_strict_implicit() const { return m_strict_implicit; } bool is_strict_implicit() const { return m_strict_implicit; }
binder_info update_contextual(bool f) const { return binder_info(m_implicit, m_cast, f, m_strict_implicit); }
}; };
inline binder_info mk_implicit_binder_info() { return binder_info(true); } inline binder_info mk_implicit_binder_info() { return binder_info(true); }

3
src/library/tactic/CMakeLists.txt
View file

@ -1,5 +1,4 @@
add_library(tactic goal.cpp proof_builder.cpp proof_state.cpp add_library(tactic goal.cpp proof_state.cpp tactic.cpp apply_tactic.cpp)
tactic.cpp apply_tactic.cpp)
# simplify_tactic.cpp) # simplify_tactic.cpp)

7
src/library/tactic/apply_tactic.cpp
View file

@ -37,8 +37,10 @@ bool collect_simple_metas(expr const & e, buffer<expr> & result) {
return !failed; return !failed;
} }
tactic apply_tactic(expr const & e) { tactic apply_tactic(expr const & /* e */) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { return tactic([=](environment const &, io_state const &, proof_state const & s) {
return s;
#if 0
if (s.is_final_state()) { if (s.is_final_state()) {
return proof_state_seq(); return proof_state_seq();
} }
@ -111,6 +113,7 @@ tactic apply_tactic(expr const & e) {
}); });
return proof_state(s, new_gs, new_pb, new_ngen); return proof_state(s, new_gs, new_pb, new_ngen);
}); });
#endif
}); });
} }

225
src/library/tactic/goal.cpp
View file

@ -10,17 +10,18 @@ Author: Leonardo de Moura
#include "kernel/replace_fn.h" #include "kernel/replace_fn.h"
#include "kernel/for_each_fn.h" #include "kernel/for_each_fn.h"
#include "kernel/abstract.h" #include "kernel/abstract.h"
#include "kernel/type_checker.h"
#include "library/kernel_bindings.h" #include "library/kernel_bindings.h"
#include "library/tactic/goal.h" #include "library/tactic/goal.h"
namespace lean { namespace lean {
goal::goal(hypotheses const & hs, expr const & c):m_hypotheses(hs), m_conclusion(c) {} static bool is_used_pp_name(expr const * begin, expr const * end, name const & n) {
return std::any_of(begin, end, [&](expr const & h) {
static bool is_used_pp_name(hypothesis const * begin, hypothesis const * end, name const & n) { return local_pp_name(h) == n;
return std::any_of(begin, end, [&](hypothesis const & h) { return local_pp_name(h.first) == n; }); });
} }
static expr pick_unused_pp_name(hypothesis const * begin, hypothesis const * end, expr const & l) { static expr pick_unused_pp_name(expr const * begin, expr const * end, expr const & l) {
expr r = l; expr r = l;
unsigned i = 1; unsigned i = 1;
while (is_used_pp_name(begin, end, local_pp_name(r))) { while (is_used_pp_name(begin, end, local_pp_name(r))) {
@ -42,10 +43,10 @@ static void update_local(expr & t, expr const & old_local, expr const & new_loca
}); });
} }
static void update_local(hypothesis * begin, hypothesis * end, expr & conclusion, static void update_local(expr * begin, expr * end, expr & conclusion,
expr const & old_local, expr const & new_local) { expr const & old_local, expr const & new_local) {
for (auto it = begin; it != end; ++it) for (auto it = begin; it != end; ++it)
update_local(it->first, old_local, new_local); update_local(*it, old_local, new_local);
update_local(conclusion, old_local, new_local); update_local(conclusion, old_local, new_local);
} }
@ -53,16 +54,15 @@ format goal::pp(environment const & env, formatter const & fmt, options const &
unsigned indent = get_pp_indent(opts); unsigned indent = get_pp_indent(opts);
bool unicode = get_pp_unicode(opts); bool unicode = get_pp_unicode(opts);
format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-");
expr conclusion = m_conclusion; expr conclusion = m_type;
buffer<hypothesis> tmp; buffer<expr> tmp;
to_buffer(m_hypotheses, tmp); get_app_args(m_meta, tmp);
std::reverse(tmp.begin(), tmp.end());
bool first = true; bool first = true;
format r; format r;
auto end = tmp.end(); auto end = tmp.end();
for (auto it = tmp.begin(); it != end; ++it) { for (auto it = tmp.begin(); it != end; ++it) {
if (first) first = false; else r += compose(comma(), line()); if (first) first = false; else r += compose(comma(), line());
expr l = it->first; expr l = *it;
expr new_l = pick_unused_pp_name(tmp.begin(), it, l); expr new_l = pick_unused_pp_name(tmp.begin(), it, l);
if (!is_eqp(l, new_l)) if (!is_eqp(l, new_l))
update_local(it+1, end, conclusion, l, new_l); update_local(it+1, end, conclusion, l, new_l);
@ -73,59 +73,36 @@ format goal::pp(environment const & env, formatter const & fmt, options const &
return group(r); return group(r);
} }
expr goal::mk_meta(name const & n, expr const & type) const { expr goal::abstract(expr const & v) const {
if (has_local(type)) { buffer<expr> locals;
bool failed = false; get_app_args(m_meta, locals);
name missing; return Fun(locals, v);
for_each(type, [&](expr const & e, unsigned) { }
if (!has_local(e) || failed) return false;
if (is_local(e)) { expr goal::mk_meta(name const & n, expr const & type, bool only_contextual) const {
bool found = false; buffer<expr> locals;
for (hypothesis const & h : m_hypotheses) { get_app_args(m_meta, locals);
if (mlocal_name(h.first) == mlocal_name(e)) { if (only_contextual) {
found = true; auto new_end = std::remove_if(locals.begin(), locals.end(),
break; [](expr const & l) { return !local_info(l).is_contextual(); });
} locals.shrink(locals.size() - (locals.end() - new_end));
}
if (!found) {
failed = true;
missing = local_pp_name(e);
return false;
}
}
return true;
});
if (failed) {
throw exception(sstream() << "invalid metavariable for goal, metavariable type contains local constant '"
<< missing << "' which is not a hypothesis for this goal");
}
} }
expr t = type; expr mvar = mk_metavar(n, Pi(locals, type));
buffer<expr> args; return mk_app(mvar, locals);
for (hypothesis const & h : m_hypotheses) {
if (h.second) {
t = Pi(h.first, t);
args.push_back(h.first);
}
}
std::reverse(args.begin(), args.end());
return mk_app(mk_metavar(n, t), args);
} }
goal goal::instantiate_metavars(substitution const & s) const { goal goal::instantiate_metavars(substitution const & s) const {
hypotheses hs = map(m_hypotheses, [&](hypothesis const & h) { return goal(s.instantiate_metavars_wo_jst(m_meta),
return mk_pair(s.instantiate_metavars_wo_jst(h.first), h.second); s.instantiate_metavars_wo_jst(m_type));
});
expr c = s.instantiate_metavars_wo_jst(m_conclusion);
return goal(hs, c);
} }
static bool validate(expr const & r, hypotheses const & hs) { static bool validate_locals(expr const & r, unsigned num_locals, expr const * locals) {
bool failed = false; bool failed = false;
for_each(r, [&](expr const & e, unsigned) { for_each(r, [&](expr const & e, unsigned) {
if (!has_local(e) || failed) return false; if (!has_local(e) || failed) return false;
if (is_local(e) && if (is_local(e) &&
!std::any_of(hs.begin(), hs.end(), [&](hypothesis const & h) { return h.first == e; })) { !std::any_of(locals, locals + num_locals,
[&](expr const & l) { return mlocal_name(l) == mlocal_name(e); })) {
failed = true; failed = true;
return false; return false;
} }
@ -134,111 +111,34 @@ static bool validate(expr const & r, hypotheses const & hs) {
return !failed; return !failed;
} }
bool goal::validate() const { bool goal::validate_locals() const {
if (!::lean::validate(m_conclusion, m_hypotheses)) buffer<expr> locals;
get_app_args(m_meta, locals);
if (!::lean::validate_locals(m_type, locals.size(), locals.data()))
return false; return false;
hypotheses const * h = &m_hypotheses; unsigned i = locals.size();
while (!is_nil(*h)) { while (i > 0) {
if (!::lean::validate(mlocal_type(head(*h).first), tail(*h))) --i;
if (!::lean::validate_locals(mlocal_type(locals[i]), i, locals.data()))
return false; return false;
h = &tail(*h);
} }
return true; return true;
} }
DECL_UDATA(hypotheses) bool goal::validate(environment const & env) const {
if (validate_locals()) {
static int mk_hypotheses(lua_State * L) { type_checker tc(env);
int i = lua_gettop(L); return tc.is_def_eq(tc.check(m_meta), m_type);
hypotheses r;
if (i > 0 && is_hypotheses(L, i)) {
r = to_hypotheses(L, i);
i--;
}
while (i > 0) {
if (is_expr(L, i)) {
expr const & l = to_expr(L, i);
if (!is_local(l))
throw exception(sstream() << "arg #" << i << " must be a local constant or a pair");
r = hypotheses(hypothesis(l, true), r);
} else {
lua_rawgeti(L, i, 1);
lua_rawgeti(L, i, 2);
if (!is_expr(L, -2) || !is_local(to_expr(L, -2)) || !lua_isboolean(L, -1))
throw exception(sstream() << "arg #" << i << " must be a pair: local constant, Boolean");
r = hypotheses(hypothesis(to_expr(L, -2), lua_toboolean(L, -1)), r);
lua_pop(L, 2);
}
i--;
}
return push_hypotheses(L, r);
}
static int hypotheses_is_nil(lua_State * L) {
lua_pushboolean(L, !to_hypotheses(L, 1));
return 1;
}
static int hypotheses_head(lua_State * L) {
hypotheses const & hs = to_hypotheses(L, 1);
if (!hs)
throw exception("head method expects a non-empty hypotheses list");
push_expr(L, head(hs).first);
push_boolean(L, head(hs).second);
return 2;
}
static int hypotheses_tail(lua_State * L) {
hypotheses const & hs = to_hypotheses(L, 1);
if (!hs)
throw exception("tail method expects a non-empty hypotheses list");
push_hypotheses(L, tail(hs));
return 1;
}
static int hypotheses_next(lua_State * L) {
hypotheses & hs = to_hypotheses(L, lua_upvalueindex(1));
if (hs) {
push_hypotheses(L, tail(hs));
lua_replace(L, lua_upvalueindex(1));
push_expr(L, head(hs).first);
push_boolean(L, head(hs).second);
return 2;
} else { } else {
lua_pushnil(L); return false;
return 1;
} }
} }
static int hypotheses_items(lua_State * L) {
hypotheses & hs = to_hypotheses(L, 1);
push_hypotheses(L, hs); // upvalue(1): hypotheses
lua_pushcclosure(L, &safe_function<hypotheses_next>, 1); // create closure with 1 upvalue
return 1;
}
static int hypotheses_len(lua_State * L) {
lua_pushinteger(L, length(to_hypotheses(L, 1)));
return 1;
}
static const struct luaL_Reg hypotheses_m[] = {
{"__gc", hypotheses_gc}, // never throws
{"__len", safe_function<hypotheses_len>},
{"size", safe_function<hypotheses_len>},
{"pairs", safe_function<hypotheses_items>},
{"is_nil", safe_function<hypotheses_is_nil>},
{"empty", safe_function<hypotheses_is_nil>},
{"head", safe_function<hypotheses_head>},
{"tail", safe_function<hypotheses_tail>},
{0, 0}
};
DECL_UDATA(goal) DECL_UDATA(goal)
static int mk_goal(lua_State * L) { return push_goal(L, goal(to_hypotheses(L, 1), to_expr(L, 2))); } static int mk_goal(lua_State * L) { return push_goal(L, goal(to_expr(L, 1), to_expr(L, 2))); }
static int goal_hypotheses(lua_State * L) { return push_hypotheses(L, to_goal(L, 1).get_hypotheses()); } static int goal_meta(lua_State * L) { return push_expr(L, to_goal(L, 1).get_meta()); }
static int goal_conclusion(lua_State * L) { return push_expr(L, to_goal(L, 1).get_conclusion()); } static int goal_type(lua_State * L) { return push_expr(L, to_goal(L, 1).get_type()); }
static int goal_tostring(lua_State * L) { static int goal_tostring(lua_State * L) {
std::ostringstream out; std::ostringstream out;
goal & g = to_goal(L, 1); goal & g = to_goal(L, 1);
@ -249,7 +149,11 @@ static int goal_tostring(lua_State * L) {
lua_pushstring(L, out.str().c_str()); lua_pushstring(L, out.str().c_str());
return 1; return 1;
} }
static int goal_mk_meta(lua_State * L) { return push_expr(L, to_goal(L, 1).mk_meta(to_name_ext(L, 2), to_expr(L, 3))); } static int goal_mk_meta(lua_State * L) {
int nargs = lua_gettop(L);
return push_expr(L, to_goal(L, 1).mk_meta(to_name_ext(L, 2), to_expr(L, 3), nargs == 4 ? lua_toboolean(L, 4) : true));
}
static int goal_pp(lua_State * L) { static int goal_pp(lua_State * L) {
int nargs = lua_gettop(L); int nargs = lua_gettop(L);
goal & g = to_goal(L, 1); goal & g = to_goal(L, 1);
@ -263,29 +167,28 @@ static int goal_pp(lua_State * L) {
return push_format(L, g.pp(to_environment(L, 2), to_formatter(L, 3), to_options(L, 4))); return push_format(L, g.pp(to_environment(L, 2), to_formatter(L, 3), to_options(L, 4)));
} }
} }
static int goal_validate(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate()); } static int goal_validate_locals(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate_locals()); }
static int goal_validate(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate(to_environment(L, 2))); }
static int goal_instantiate(lua_State * L) { return push_goal(L, to_goal(L, 1).instantiate_metavars(to_substitution(L, 2))); }
static int goal_abstract(lua_State * L) { return push_expr(L, to_goal(L, 1).abstract(to_expr(L, 2))); }
static int goal_name(lua_State * L) { return push_name(L, to_goal(L, 1).get_name()); }
static const struct luaL_Reg goal_m[] = { static const struct luaL_Reg goal_m[] = {
{"__gc", goal_gc}, // never throws {"__gc", goal_gc}, // never throws
{"__tostring", safe_function<goal_tostring>}, {"__tostring", safe_function<goal_tostring>},
{"hypotheses", safe_function<goal_hypotheses>}, {"abstract", safe_function<goal_abstract>},
{"hyps", safe_function<goal_hypotheses>},
{"conclusion", safe_function<goal_conclusion>},
{"mk_meta", safe_function<goal_mk_meta>}, {"mk_meta", safe_function<goal_mk_meta>},
{"pp", safe_function<goal_pp>}, {"pp", safe_function<goal_pp>},
{"validate", safe_function<goal_validate>}, {"validate", safe_function<goal_validate>},
{"validate_locals", safe_function<goal_validate_locals>},
{"instantiate", safe_function<goal_instantiate>},
{"meta", safe_function<goal_meta>},
{"type", safe_function<goal_type>},
{"name", safe_function<goal_name>},
{0, 0} {0, 0}
}; };
void open_goal(lua_State * L) { void open_goal(lua_State * L) {
luaL_newmetatable(L, hypotheses_mt);
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, hypotheses_m, 0);
SET_GLOBAL_FUN(hypotheses_pred, "is_hypotheses");
SET_GLOBAL_FUN(mk_hypotheses, "hypotheses");
luaL_newmetatable(L, goal_mt); luaL_newmetatable(L, goal_mt);
lua_pushvalue(L, -1); lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index"); lua_setfield(L, -2, "__index");

78
src/library/tactic/goal.h
View file

@ -15,49 +15,69 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
/** /**
\brief A hypothesis is a local variable + a flag indicating whether it is "contextual" or not. \brief A goal is just encoding the synthesis problem <tt>(?m l_1 .... l_n) : t</tt>
Only contextual ones are used to build the context of new metavariables. That is, we want to find a term \c ?m s.t. <tt>(?m l_1 ... l_n)</tt> has type \c t
The terms \c l_i are just local constants.
We can convert any metavariable
<tt>?m : Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
into a goal by simply creating the local constants
<tt>l_1 : A_1, ..., l_n : A_n[l_1, ..., l_{n-1}]</tt>
and then, create the goal
<tt>?m l_1 ... l_n : B[l_1, ..., l_n]</tt>
Now, suppose we find a term \c b with type <tt>B[l_1, ... l_n]</tt>, then we can simply
find \c ?m by abstracting <tt>l_1, ..., l_n</tt>
We can check whether a goal is well formed in an environment by type checking.
*/ */
typedef std::pair<expr, bool> hypothesis;
typedef list<hypothesis> hypotheses;
class goal { class goal {
hypotheses m_hypotheses; expr m_meta;
expr m_conclusion; expr m_type;
public: public:
goal() {} goal() {}
goal(hypotheses const & hs, expr const & c); goal(expr const & m, expr const & t):m_meta(m), m_type(t) {}
hypotheses const & get_hypotheses() const { return m_hypotheses; }
expr const & get_conclusion() const { return m_conclusion; } expr const & get_meta() const { return m_meta; }
expr const & get_type() const { return m_type; }
name get_name() const { return mlocal_name(get_app_fn(m_meta)); }
expr get_mvar() const { return get_app_fn(m_meta); }
/** /**
\brief Create a metavarible application <tt>(m l_1 ... l_n)</tt> with type \c type, \brief Given a term \c v with type get_type(), build a lambda abstraction
where \c l_1 ... \c l_n are the contextual hypotheses of this goal, and that is the solution for the metavariable associated with this goal.
\c m is a metavariable with name \c n.
*/ */
expr mk_meta(name const & n, expr const & type) const; expr abstract(expr const & v) const;
/** /**
brief Return true iff this is a valid goal. \brief Create a metavariable application <tt>(?m l_1 ... l_n)</tt> with the given type,
We say a goal is valid when the conclusion only contains local constants that are in hypotheses, and the locals from this goal. If <tt>only_contextual == true</tt>, then we only include
and each hypothesis only contains local constants that occur in the previous hypotheses. the local constants that are marked as contextual.
*/ */
bool validate() const; expr mk_meta(name const & m, expr const & type, bool only_contextual = true) const;
/**
brief Return true iff get_type() only contains local constants that arguments
of get_meta(), and each argument of get_meta() only contains local constants
that are previous arguments.
*/
bool validate_locals() const;
/**
\brief Return true iff \c validate_locals() return true and type of \c get_meta() in
\c env is get_type()
*/
bool validate(environment const & env) const;
/** \brief Instatiate the metavariables in this goal using the given substitution */
goal instantiate_metavars(substitution const & s) const; goal instantiate_metavars(substitution const & s) const;
format pp(environment const & env, formatter const & fmt, options const & opts) const; format pp(environment const & env, formatter const & fmt, options const & opts) const;
}; };
inline goal update(goal const & g, expr const & c) { return goal(g.get_hypotheses(), c); }
inline goal update(goal const & g, hypotheses const & hs) { return goal(hs, g.get_conclusion()); }
inline goal update(goal const & g, buffer<hypothesis> const & hs) { return goal(to_list(hs.begin(), hs.end()), g.get_conclusion()); }
inline hypotheses add_hypothesis(expr const & l, hypotheses const & hs) {
lean_assert(is_local(l));
return cons(hypothesis(l, true), hs);
}
inline hypotheses add_hypothesis(hypothesis const & h, hypotheses const & hs) {
return cons(h, hs);
}
io_state_stream const & operator<<(io_state_stream const & out, goal const & g); io_state_stream const & operator<<(io_state_stream const & out, goal const & g);
UDATA_DEFS_CORE(hypotheses)
UDATA_DEFS(goal) UDATA_DEFS(goal)
void open_goal(lua_State * L); void open_goal(lua_State * L);
} }

92
src/library/tactic/proof_builder.cpp
View file

@ -1,92 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include "util/exception.h"
#include "util/sstream.h"
#include "util/luaref.h"
#include "library/kernel_bindings.h"
#include "library/tactic/proof_builder.h"
namespace lean {
expr find(proof_map const & m, name const & n) {
expr const * r = m.find(n);
if (r)
return *r;
throw exception(sstream() << "proof for goal '" << n << "' not found");
}
proof_builder add_proofs(proof_builder const & pb, list<std::pair<name, expr>> const & prs) {
return proof_builder([=](proof_map const & m, substitution const & s) -> expr {
proof_map new_m(m);
for (auto const & np : prs) {
new_m.insert(np.first, np.second);
}
return pb(new_m, s);
});
}
proof_builder add_proof(proof_builder const & pb, name const & goal_name, expr const & pr) {
return add_proofs(pb, list<std::pair<name, expr>>(mk_pair(goal_name, pr)));
}
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_find(lua_State * L) {
return push_expr(L, find(to_proof_map(L, 1), to_name_ext(L, 2)));
}
static int proof_map_insert(lua_State * L) {
to_proof_map(L, 1).insert(to_name_ext(L, 2), to_expr(L, 3));
return 0;
}
static int proof_map_erase(lua_State * L) {
to_proof_map(L, 1).erase(to_name_ext(L, 2));
return 0;
}
static const struct luaL_Reg proof_map_m[] = {
{"__gc", proof_map_gc}, // never throws
{"find", safe_function<proof_map_find>},
{"insert", safe_function<proof_map_insert>},
{"erase", safe_function<proof_map_erase>},
{0, 0}
};
proof_builder to_proof_builder(lua_State * L, int idx) {
luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun
luaref f(L, idx);
return proof_builder([=](proof_map const & m, substitution const & s) {
lua_State * L = f.get_state();
f.push();
push_proof_map(L, m);
push_substitution(L, s);
pcall(L, 2, 1, 0);
expr r = to_expr(L, -1);
lua_pop(L, 1);
return r;
});
}
void open_proof_builder(lua_State * L) {
luaL_newmetatable(L, proof_map_mt);
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, proof_map_m, 0);
SET_GLOBAL_FUN(proof_map_pred, "is_proof_map");
SET_GLOBAL_FUN(mk_proof_map, "proof_map");
}
}

34
src/library/tactic/proof_builder.h
View file

@ -1,34 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <utility>
#include <algorithm>
#include "util/lua.h"
#include "util/name.h"
#include "util/rb_map.h"
#include "kernel/expr.h"
namespace lean {
typedef rb_map<name, expr, name_quick_cmp> proof_map;
/**
\brief Return the proof (of inhabitated type) for the goal named \c n in the \c proof_map \c m.
Throw an exception if \c m does not contain a proof for \c n.
*/
expr find(proof_map const & m, name const & n);
/**
\brief A proof builder creates an inhabitant a goal type (aka
conclusion) using the inhabitants for its subgoals.
*/
typedef std::function<expr(proof_map const &, substitution const &)> proof_builder;
proof_builder add_proofs(proof_builder const & pb, list<std::pair<name, expr>> const & prs);
proof_builder add_proof(proof_builder const & pb, name const & goal_name, expr const & pr);
/** \brief Convert a Lua function on position \c idx (on the Lua stack) into a proof_builder_fn */
proof_builder to_proof_builder(lua_State * L, int idx);
UDATA_DEFS_CORE(proof_map)
void open_proof_builder(lua_State * L);
}

130
src/library/tactic/proof_state.cpp
View file

@ -24,48 +24,32 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
static name g_proof_state_goal_names {"tactic", "goal_names"}; static name g_proof_state_goal_names {"tactic", "goal_names"};
static name g_proof_state_minimize_contextual {"tactic", "mimimize_contextual"};
RegisterBoolOption(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES, "(tactic) display goal names when pretty printing proof state"); RegisterBoolOption(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES, "(tactic) display goal names when pretty printing proof state");
RegisterBoolOption(g_proof_state_minimize_contextual, LEAN_PROOF_STATE_MINIMIZE_CONTEXTUAL,
"(tactic) only hypotheses, that are not propositions, are marked as 'contextual'");
bool get_proof_state_goal_names(options const & opts) { return opts.get_bool(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES); } bool get_proof_state_goal_names(options const & opts) { return opts.get_bool(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES); }
bool get_proof_state_minimize_contextual(options const & opts) {
return opts.get_bool(g_proof_state_minimize_contextual, LEAN_PROOF_STATE_MINIMIZE_CONTEXTUAL);
}
optional<name> get_ith_goal_name(goals const & gs, unsigned i) {
unsigned j = 1;
for (auto const & p : gs) {
if (i == j) return some(p.first);
j++;
}
return optional<name>();
}
format proof_state::pp(environment const & env, formatter const & fmt, options const & opts) const { format proof_state::pp(environment const & env, formatter const & fmt, options const & opts) const {
bool show_goal_names = get_proof_state_goal_names(opts); bool show_goal_names = get_proof_state_goal_names(opts);
unsigned indent = get_pp_indent(opts); unsigned indent = get_pp_indent(opts);
format r; format r;
bool first = true; bool first = true;
for (auto const & p : get_goals()) { for (auto const & g : get_goals()) {
if (first) first = false; else r += line(); if (first) first = false; else r += line();
if (show_goal_names) { if (show_goal_names) {
r += group(format{format(p.first), colon(), nest(indent, compose(line(), p.second.pp(env, fmt, opts)))}); r += group(format{format(g.get_name()), colon(), nest(indent, compose(line(), g.pp(env, fmt, opts)))});
} else { } else {
r += p.second.pp(env, fmt, opts); r += g.pp(env, fmt, opts);
} }
} }
if (first) r = format("no goals"); if (first) r = format("no goals");
return r; return r;
} }
goals map_goals(proof_state const & s, std::function<optional<goal>(name const & gn, goal const & g)> f) { goals map_goals(proof_state const & s, std::function<optional<goal>(goal const & g)> f) {
return map_filter(s.get_goals(), [=](std::pair<name, goal> const & in, std::pair<name, goal> & out) -> bool { return map_filter(s.get_goals(), [=](goal const & in, goal & out) -> bool {
check_interrupted(); check_interrupted();
optional<goal> new_goal = f(in.first, in.second); optional<goal> new_goal = f(in);
if (new_goal) { if (new_goal) {
out.first = in.first; out = *new_goal;
out.second = *new_goal;
return true; return true;
} else { } else {
return false; return false;
@ -73,55 +57,24 @@ goals map_goals(proof_state const & s, std::function<optional<goal>(name const &
}); });
} }
void proof_state::get_goal_names(name_set & r) const { proof_state to_proof_state(expr const & mvar, name_generator ngen) {
for (auto const & p : get_goals())
r.insert(p.first);
}
static name g_main("main");
proof_builder mk_init_proof_builder(list<expr> const & locals) {
return proof_builder([=](proof_map const & m, substitution const &) -> expr {
expr r = find(m, g_main);
for (expr const & l : locals)
r = Fun(l, r);
return r;
});
}
static proof_state to_proof_state(environment const * env, expr const & mvar, name_generator ngen) {
if (!is_metavar(mvar)) if (!is_metavar(mvar))
throw exception("invalid 'to_proof_state', argument is not a metavariable"); throw exception("invalid 'to_proof_state', argument is not a metavariable");
optional<type_checker> tc;
if (env)
tc.emplace(*env, ngen.mk_child());
expr t = mlocal_type(mvar); expr t = mlocal_type(mvar);
list<expr> init_ls; buffer<expr> ls;
hypotheses hs;
while (is_pi(t)) { while (is_pi(t)) {
expr l = mk_local(ngen.next(), binding_name(t), binding_domain(t), binding_info(t)); expr l = mk_local(ngen.next(), binding_name(t), binding_domain(t), binding_info(t));
bool c = true; ls.push_back(l);
if (tc)
c = !tc->is_prop(binding_domain(t));
hs = hypotheses(hypothesis(l, c), hs);
t = instantiate(binding_body(t), l); t = instantiate(binding_body(t), l);
init_ls = list<expr>(l, init_ls);
} }
goals gs(mk_pair(g_main, goal(hs, t))); expr meta = mk_app(mvar, ls);
return proof_state(gs, mk_init_proof_builder(init_ls), ngen, init_ls); goals gs(goal(meta, t));
return proof_state(gs, substitution(), ngen, meta);
} }
static name g_tmp_prefix = name::mk_internal_unique_name(); static name g_tmp_prefix = name::mk_internal_unique_name();
proof_state to_proof_state(expr const & mvar, name_generator const & ngen) { return to_proof_state(nullptr, mvar, ngen); } proof_state to_proof_state(expr const & mvar) {
proof_state to_proof_state(expr const & mvar) { return to_proof_state(mvar, name_generator(g_tmp_prefix)); } return to_proof_state(mvar, name_generator(g_tmp_prefix));
proof_state to_proof_state(environment const & env, expr const & mvar, name_generator const & ngen, options const & opts) {
bool min_ctx = get_proof_state_minimize_contextual(opts) && env.impredicative();
if (!min_ctx)
return to_proof_state(mvar, ngen);
else
return to_proof_state(&env, mvar, ngen);
}
proof_state to_proof_state(environment const & env, expr const & meta, options const & opts) {
return to_proof_state(env, meta, name_generator(g_tmp_prefix), opts);
} }
io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s) { io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s) {
@ -130,15 +83,6 @@ io_state_stream const & operator<<(io_state_stream const & out, proof_state cons
return out; return out;
} }
optional<expr> to_proof(proof_state const & s) {
if (s.is_final_state()) {
substitution a;
proof_map m;
return some_expr(s.get_pb()(m, a));
}
return none_expr();
}
DECL_UDATA(goals) DECL_UDATA(goals)
static int mk_goals(lua_State * L) { static int mk_goals(lua_State * L) {
@ -149,12 +93,7 @@ static int mk_goals(lua_State * L) {
i--; i--;
} }
while (i > 0) { while (i > 0) {
lua_rawgeti(L, i, 1); r = goals(to_goal(L, i), r);
lua_rawgeti(L, i, 2);
if (!(lua_isstring(L, -2) || is_name(L, -2)) || !is_goal(L, -1))
throw exception(sstream() << "arg #" << i << " must be a pair: name, goal");
r = goals(mk_pair(to_name_ext(L, -2), to_goal(L, -1)), r);
lua_pop(L, 2);
i--; i--;
} }
return push_goals(L, r); return push_goals(L, r);
@ -169,9 +108,7 @@ static int goals_head(lua_State * L) {
goals const & hs = to_goals(L, 1); goals const & hs = to_goals(L, 1);
if (!hs) if (!hs)
throw exception("head method expects a non-empty goal list"); throw exception("head method expects a non-empty goal list");
push_name(L, head(hs).first); return push_goal(L, head(hs));
push_goal(L, head(hs).second);
return 2;
} }
static int goals_tail(lua_State * L) { static int goals_tail(lua_State * L) {
@ -187,9 +124,7 @@ static int goals_next(lua_State * L) {
if (hs) { if (hs) {
push_goals(L, tail(hs)); push_goals(L, tail(hs));
lua_replace(L, lua_upvalueindex(1)); lua_replace(L, lua_upvalueindex(1));
push_name(L, head(hs).first); return push_goal(L, head(hs));
push_goal(L, head(hs).second);
return 2;
} else { } else {
lua_pushnil(L); lua_pushnil(L);
return 1; return 1;
@ -204,8 +139,7 @@ static int goals_items(lua_State * L) {
} }
static int goals_len(lua_State * L) { static int goals_len(lua_State * L) {
lua_pushinteger(L, length(to_goals(L, 1))); return push_integer(L, length(to_goals(L, 1)));
return 1;
} }
static const struct luaL_Reg goals_m[] = { static const struct luaL_Reg goals_m[] = {
@ -227,9 +161,9 @@ static int mk_proof_state(lua_State * L) {
if (nargs == 2) { if (nargs == 2) {
return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2))); return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2)));
} else if (nargs == 3) { } else if (nargs == 3) {
return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_proof_builder(L, 3))); return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_substitution(L, 3)));
} else if (nargs == 4) { } else if (nargs == 4) {
return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_proof_builder(L, 3), to_name_generator(L, 4))); return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_substitution(L, 3), to_name_generator(L, 4)));
} else { } else {
throw exception("proof_state invalid number of arguments"); throw exception("proof_state invalid number of arguments");
} }
@ -239,14 +173,8 @@ static int to_proof_state(lua_State * L) {
int nargs = lua_gettop(L); int nargs = lua_gettop(L);
if (nargs == 1) if (nargs == 1)
return push_proof_state(L, to_proof_state(to_expr(L, 1))); return push_proof_state(L, to_proof_state(to_expr(L, 1)));
else if (nargs == 2 && is_expr(L, 1))
return push_proof_state(L, to_proof_state(to_expr(L, 1), to_name_generator(L, 2)));
else if (nargs == 2)
return push_proof_state(L, to_proof_state(to_environment(L, 1), to_expr(L, 2)));
else if (nargs == 3)
return push_proof_state(L, to_proof_state(to_environment(L, 1), to_expr(L, 2), to_options(L, 3)));
else else
return push_proof_state(L, to_proof_state(to_environment(L, 1), to_expr(L, 2), to_name_generator(L, 3), to_options(L, 4))); return push_proof_state(L, to_proof_state(to_expr(L, 1), to_name_generator(L, 2)));
} }
static int proof_state_tostring(lua_State * L) { static int proof_state_tostring(lua_State * L) {
@ -261,9 +189,9 @@ static int proof_state_tostring(lua_State * L) {
} }
static int proof_state_get_goals(lua_State * L) { return push_goals(L, to_proof_state(L, 1).get_goals()); } static int proof_state_get_goals(lua_State * L) { return push_goals(L, to_proof_state(L, 1).get_goals()); }
static int proof_state_apply_proof_builder(lua_State * L) { static int proof_state_get_ngen(lua_State * L) { return push_name_generator(L, to_proof_state(L, 1).get_ngen()); }
return push_expr(L, to_proof_state(L, 1).get_pb()(to_proof_map(L, 2), to_substitution(L, 3))); static int proof_state_get_subst(lua_State * L) { return push_substitution(L, to_proof_state(L, 1).get_subst()); }
} static int proof_state_get_initial(lua_State * L) { return push_list_expr(L, to_proof_state(L, 1).get_initial()); }
static int proof_state_is_final_state(lua_State * L) { return push_boolean(L, to_proof_state(L, 1).is_final_state()); } static int proof_state_is_final_state(lua_State * L) { return push_boolean(L, to_proof_state(L, 1).is_final_state()); }
static int proof_state_pp(lua_State * L) { static int proof_state_pp(lua_State * L) {
int nargs = lua_gettop(L); int nargs = lua_gettop(L);
@ -278,17 +206,15 @@ static int proof_state_pp(lua_State * L) {
return push_format(L, s.pp(to_environment(L, 2), to_formatter(L, 3), to_options(L, 4))); return push_format(L, s.pp(to_environment(L, 2), to_formatter(L, 3), to_options(L, 4)));
} }
static int to_proof(lua_State * L) { return push_optional_expr(L, to_proof(to_proof_state(L, 1))); }
static const struct luaL_Reg proof_state_m[] = { static const struct luaL_Reg proof_state_m[] = {
{"__gc", proof_state_gc}, // never throws {"__gc", proof_state_gc}, // never throws
{"__tostring", safe_function<proof_state_tostring>}, {"__tostring", safe_function<proof_state_tostring>},
{"pp", safe_function<proof_state_pp>}, {"pp", safe_function<proof_state_pp>},
{"get_goals", safe_function<proof_state_get_goals>},
{"pb", safe_function<proof_state_apply_proof_builder>},
{"goals", safe_function<proof_state_get_goals>}, {"goals", safe_function<proof_state_get_goals>},
{"subst", safe_function<proof_state_get_subst>},
{"initial", safe_function<proof_state_get_initial>},
{"ngen", safe_function<proof_state_get_ngen>},
{"is_final_state", safe_function<proof_state_is_final_state>}, {"is_final_state", safe_function<proof_state_is_final_state>},
{"to_proof", safe_function<to_proof>},
{0, 0} {0, 0}
}; };

54
src/library/tactic/proof_state.h
View file

@ -11,37 +11,34 @@ Author: Leonardo de Moura
#include "util/optional.h" #include "util/optional.h"
#include "util/name_set.h" #include "util/name_set.h"
#include "library/tactic/goal.h" #include "library/tactic/goal.h"
#include "library/tactic/proof_builder.h"
namespace lean { namespace lean {
typedef std::pair<name, goal> named_goal; typedef list<goal> goals;
typedef list<named_goal> goals;
/** \brief Return the name of the i-th goal, return none if i == 0 or i > size(g) */
optional<name> get_ith_goal_name(goals const & gs, unsigned i);
class proof_state { class proof_state {
goals m_goals; goals m_goals;
proof_builder m_proof_builder; substitution m_subst;
name_generator m_ngen; name_generator m_ngen;
list<expr> m_init_locals; // The following term is of the form (?m l_1 ... l_n), it captures the
// metavariable this proof state is trying to synthesize, and
// the context [l_1, ..., l_n]. The context is important because it allows
// us to "reinterpret" an expression in this context.
expr m_inital;
public: public:
proof_state(goals const & gs, proof_builder const & pb, name_generator const & ngen, list<expr> const & ls = list<expr>()): proof_state(goals const & gs, substitution const & s, name_generator const & ngen, expr const & ini):
m_goals(gs), m_proof_builder(pb), m_ngen(ngen), m_init_locals(ls) {} m_goals(gs), m_subst(s), m_ngen(ngen), m_inital(ini) {}
proof_state(proof_state const & s, goals const & gs, proof_builder const & pb, name_generator const & ngen): proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen):
proof_state(gs, pb, ngen, s.m_init_locals) {} proof_state(gs, subst, ngen, s.m_inital) {}
proof_state(proof_state const & s, goals const & gs, proof_builder const & pb):proof_state(s, gs, pb, s.m_ngen) {} proof_state(proof_state const & s, goals const & gs, substitution const & subst):proof_state(s, gs, subst, s.m_ngen) {}
proof_state(proof_state const & s, goals const & gs):proof_state(s, gs, s.m_proof_builder) {} proof_state(proof_state const & s, goals const & gs):proof_state(s, gs, s.m_subst) {}
proof_state(proof_state const & s, name_generator const & ngen): proof_state(proof_state const & s, name_generator const & ngen):proof_state(s.m_goals, s.m_subst, ngen, s.m_inital) {}
proof_state(s.m_goals, s.m_proof_builder, ngen, s.m_init_locals) {}
goals const & get_goals() const { return m_goals; } goals const & get_goals() const { return m_goals; }
proof_builder const & get_pb() const { return m_proof_builder; } substitution const & get_subst() const { return m_subst; }
name_generator const & ngen() const { return m_ngen; } name_generator const & get_ngen() const { return m_ngen; }
list<expr> const & get_init_locals() const { return m_init_locals; } expr const & get_initial() const { return m_inital; }
/** \brief Return true iff this state does not have any goals left */ /** \brief Return true iff this state does not have any goals left */
bool is_final_state() const { return empty(m_goals); } bool is_final_state() const { return empty(m_goals); }
/** \brief Store in \c r the goal names */
void get_goal_names(name_set & r) const;
optional<name> get_ith_goal_name(unsigned i) const { return ::lean::get_ith_goal_name(get_goals(), i); }
format pp(environment const & env, formatter const & fmt, options const & opts) const; format pp(environment const & env, formatter const & fmt, options const & opts) const;
}; };
@ -49,19 +46,10 @@ inline optional<proof_state> some_proof_state(proof_state const & s) { return so
inline optional<proof_state> none_proof_state() { return optional<proof_state> (); } inline optional<proof_state> none_proof_state() { return optional<proof_state> (); }
/** \brief Create a proof state for a metavariable \c mvar */ /** \brief Create a proof state for a metavariable \c mvar */
proof_state to_proof_state(expr const & mvar, name_generator const & ngen); proof_state to_proof_state(expr const & mvar, name_generator ngen);
proof_state to_proof_state(expr const & mvar); proof_state to_proof_state(expr const & mvar);
/**
\brief Similar to the previous \c to_proof_state functions, but when \c opts contains tactic.minimize_context, and
Type.{0} in \c env is impredicative, then only hypothesis that are not prositions are marked as "contextual".
*/
proof_state to_proof_state(environment const & env, expr const & mvar, name_generator const & ngen, options const & opts = options());
proof_state to_proof_state(environment const & env, expr const & mvar, options const & opts = options());
/** \brief Try to extract a proof from the given proof state */ goals map_goals(proof_state const & s, std::function<optional<goal>(goal const & g)> f);
optional<expr> to_proof(proof_state const & s);
goals map_goals(proof_state const & s, std::function<optional<goal>(name const & gn, goal const & g)> f);
io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s); io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s);
UDATA_DEFS_CORE(goals) UDATA_DEFS_CORE(goals)

2
src/library/tactic/register_module.h
View file

@ -7,7 +7,6 @@ Author: Leonardo de Moura
#pragma once #pragma once
#include "util/script_state.h" #include "util/script_state.h"
#include "library/tactic/goal.h" #include "library/tactic/goal.h"
#include "library/tactic/proof_builder.h"
#include "library/tactic/proof_state.h" #include "library/tactic/proof_state.h"
#include "library/tactic/tactic.h" #include "library/tactic/tactic.h"
#include "library/tactic/apply_tactic.h" #include "library/tactic/apply_tactic.h"
@ -16,7 +15,6 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
inline void open_tactic_module(lua_State * L) { inline void open_tactic_module(lua_State * L) {
open_goal(L); open_goal(L);
open_proof_builder(L);
open_proof_state(L); open_proof_state(L);
open_tactic(L); open_tactic(L);
open_apply_tactic(L); open_apply_tactic(L);

131
src/library/tactic/tactic.cpp
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include "util/sstream.h" #include "util/sstream.h"
#include "util/interrupt.h" #include "util/interrupt.h"
#include "util/lazy_list_fn.h" #include "util/lazy_list_fn.h"
#include "util/list_fn.h"
#include "kernel/instantiate.h" #include "kernel/instantiate.h"
#include "kernel/replace_visitor.h" #include "kernel/replace_visitor.h"
#include "library/kernel_bindings.h" #include "library/kernel_bindings.h"
@ -173,105 +174,65 @@ tactic take(tactic const & t, unsigned k) {
tactic assumption_tactic() { tactic assumption_tactic() {
return tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> { return tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
list<std::pair<name, expr>> proofs; substitution subst = s.get_subst();
goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> optional<goal> { goals new_gs = map_goals(s, [&](goal const & g) -> optional<goal> {
expr const & c = g.get_conclusion(); expr const & t = g.get_type();
optional<expr> pr; optional<expr> h;
for (auto const & p : g.get_hypotheses()) { buffer<expr> locals;
check_interrupted(); get_app_args(g.get_meta(), locals);
if (mlocal_type(p.first) == c) { for (auto const & l : locals) {
pr = p.first; if (mlocal_type(l) == t) {
h = l;
break; break;
} }
} }
if (pr) { if (h) {
proofs.emplace_front(gname, *pr); subst = subst.assign(g.get_mvar(), g.abstract(*h), justification());
return optional<goal>(); return optional<goal>();
} else { } else {
return some(g); return some(g);
} }
}); });
if (empty(proofs)) return some(proof_state(s, new_gs, subst));
return none_proof_state();
return some(proof_state(s, new_gs, add_proofs(s.get_pb(), proofs)));
}); });
} }
tactic beta_tactic() { tactic beta_tactic() {
return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> { return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
bool reduced = false; bool reduced = false;
goals new_gs = map_goals(s, [&](name const &, goal const & g) -> optional<goal> { goals new_gs = map_goals(s, [&](goal const & g) -> optional<goal> {
hypotheses new_hs = map(g.get_hypotheses(), [&](hypothesis const & h) { expr new_meta = beta_reduce(g.get_meta());
expr new_h = update_mlocal(h.first, beta_reduce(mlocal_type(h.first))); expr new_type = beta_reduce(g.get_type());
if (new_h != h.first) if (new_meta != g.get_meta() || new_type != g.get_type())
reduced = true;
return hypothesis(new_h, h.second);
});
expr const & c = g.get_conclusion();
expr new_c = beta_reduce(c);
if (new_c != c)
reduced = true; reduced = true;
return some(goal(new_hs, new_c)); return some(goal(new_meta, new_type));
}); });
return reduced ? some(proof_state(s, new_gs)) : none_proof_state(); return reduced ? some(proof_state(s, new_gs)) : none_proof_state();
}); });
} }
proof_state_seq focus_core(tactic const & t, name const & gname, environment const & env, io_state const & ios, proof_state const & s) { proof_state_seq focus_core(tactic const & t, unsigned i, environment const & env, io_state const & ios, proof_state const & s) {
for (auto const & p : s.get_goals()) { goals gs = s.get_goals();
if (p.first == gname) { if (i >= length(gs))
proof_builder pb = proof_builder([=](proof_map const & m, substitution const &) -> expr { return find(m, gname); }); return proof_state_seq();
proof_state new_s(s, goals(p), pb); // new state with singleton goal goal const & g = get_ith(gs, i);
return map(t(env, ios, new_s), [=](proof_state const & s2) { proof_state new_s(s, goals(g)); // singleton goal
// we have to put back the goals that were not selected return map(t(env, ios, new_s), [=](proof_state const & s2) {
list<std::pair<name, name>> renamed_goals; // we have to put back the goals that were not selected
goals new_gs = map_append(s.get_goals(), [&](std::pair<name, goal> const & p) { buffer<goal> tmp;
if (p.first == gname) { to_buffer(gs, tmp);
name_set used_names; buffer<goal> new_gs;
s.get_goal_names(used_names); new_gs.append(i, tmp.data());
used_names.erase(gname); for (auto g : s2.get_goals())
return map(s2.get_goals(), [&](std::pair<name, goal> const & p2) -> std::pair<name, goal> { new_gs.push_back(g);
name uname = mk_unique(used_names, p2.first); new_gs.append(tmp.size()-i-1, tmp.data()+i+1);
used_names.insert(uname); return proof_state(s2, to_list(new_gs.begin(), new_gs.end()));
renamed_goals.emplace_front(p2.first, uname);
return mk_pair(uname, p2.second);
});
} else {
return goals(p);
}
});
proof_builder pb1 = s.get_pb();
proof_builder pb2 = s2.get_pb();
proof_builder new_pb = proof_builder(
[=](proof_map const & m, substitution const & a) -> expr {
proof_map m1(m); // map for pb1
proof_map m2; // map for pb2
for (auto p : renamed_goals) {
m2.insert(p.first, find(m, p.second));
m1.erase(p.first);
}
m1.insert(gname, pb2(m2, a));
return pb1(m1, a);
});
return proof_state(s2, new_gs, new_pb);
});
}
}
return proof_state_seq(); // tactic is not applicable
}
tactic focus(tactic const & t, name const & gname) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
return focus_core(t, gname, env, ios, s);
}); });
} }
tactic focus(tactic const & t, int i) { tactic focus(tactic const & t, unsigned i) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
if (optional<name> n = s.get_ith_goal_name(i)) return focus_core(t, i, env, ios, s);
return focus_core(t, *n, env, ios, s);
else
return proof_state_seq();
}); });
} }
@ -347,15 +308,15 @@ public:
}; };
optional<proof_state> unfold_tactic_core(unfold_core_fn & fn, proof_state const & s) { optional<proof_state> unfold_tactic_core(unfold_core_fn & fn, proof_state const & s) {
goals new_gs = map_goals(s, [&](name const &, goal const & g) -> optional<goal> { bool reduced = false;
hypotheses new_hs = map(g.get_hypotheses(), [&](hypothesis const & h) { goals new_gs = map_goals(s, [&](goal const & g) -> optional<goal> {
expr l = update_mlocal(h.first, fn(mlocal_type(h.first))); expr new_meta = fn(g.get_meta());
return hypothesis(l, h.second); expr new_type = fn(g.get_type());
}); if (new_meta != g.get_meta() || new_type != g.get_type())
expr new_c = fn(g.get_conclusion()); reduced = true;
return some(goal(new_hs, new_c)); return some(goal(new_meta, new_type));
}); });
if (fn.unfolded()) { if (reduced) {
return some(proof_state(s, new_gs)); return some(proof_state(s, new_gs));
} else { } else {
return none_proof_state(); return none_proof_state();
@ -455,10 +416,8 @@ static int tactic_focus(lua_State * L) {
int nargs = lua_gettop(L); int nargs = lua_gettop(L);
if (nargs == 1) if (nargs == 1)
return push_tactic(L, focus(to_tactic(L, 1))); return push_tactic(L, focus(to_tactic(L, 1)));
else if (lua_isnumber(L, 2))
return push_tactic(L, focus(to_tactic(L, 1), lua_tointeger(L, 2)));
else else
return push_tactic(L, focus(to_tactic(L, 1), to_name_ext(L, 2))); return push_tactic(L, focus(to_tactic(L, 1), lua_tointeger(L, 2)));
} }
static int mk_lua_tactic01(lua_State * L) { static int mk_lua_tactic01(lua_State * L) {
luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun

7
src/library/tactic/tactic.h
View file

@ -118,16 +118,11 @@ typedef std::function<bool(environment const & env, io_state const & ios, proof_
tactic cond(proof_state_pred p, tactic const & t1, tactic const & t2); tactic cond(proof_state_pred p, tactic const & t1, tactic const & t2);
/** \brief Syntax-sugar for cond(p, t, id_tactic()) */ /** \brief Syntax-sugar for cond(p, t, id_tactic()) */
inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_tactic()); } inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_tactic()); }
/**
\brief Return a tactic that applies \c t only to the goal named \c gname.
The tactic fails if the input state does not have a goal named \c gname.
*/
tactic focus(tactic const & t, name const & gname);
/** /**
\brief Return a tactic that applies \c t only to the i-th goal. \brief Return a tactic that applies \c t only to the i-th goal.
The tactic fails if the input state does have at least i goals. The tactic fails if the input state does have at least i goals.
*/ */
tactic focus(tactic const & t, int i); tactic focus(tactic const & t, unsigned i);
inline tactic focus(tactic const & t) { return focus(t, 1); } inline tactic focus(tactic const & t) { return focus(t, 1); }
/** \brief Return a tactic that unfolds the definition named \c n. */ /** \brief Return a tactic that unfolds the definition named \c n. */
tactic unfold_tactic(name const & n); tactic unfold_tactic(name const & n);

14
tests/lua/goal1.lua
View file

@ -3,14 +3,14 @@ local A = Local("A", Type)
env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Bool)))) env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Bool))))
local eq = Const("eq") local eq = Const("eq")
local a = Local("a", A) local a = Local("a", A)
local b = mk_local("b", "a", A) local b = Local("b", A)
local H = Local("H", eq(A, a, b)) local H = Local("H", eq(A, a, b))
local hs = hypotheses(H, a, b, A) local t = eq(A, b, a)
local g = goal(hs, eq(A, b, a)) local m = mk_metavar("m", Pi(A, a, b, H, t))(A, a, b, H)
print(g) print(m)
assert(g:validate()) print(env:type_check(m))
local g = goal(m, t)
assert(g:validate(env))
local m1 = g:mk_meta("m1", Bool) local m1 = g:mk_meta("m1", Bool)
print(tostring(m1)) print(tostring(m1))
print(env:type_check(m1)) print(env:type_check(m1))
assert(not goal(hypotheses(H, A, a, b), eq(A, b, a)):validate())

13
tests/lua/proof_state1.lua
View file

@ -7,13 +7,6 @@ local b = Local("b", A)
local H = Local("H", eq(A, a, b)) local H = Local("H", eq(A, a, b))
local m = mk_metavar("m", Pi(A, a, b, H, eq(A, a, b))) local m = mk_metavar("m", Pi(A, a, b, H, eq(A, a, b)))
print(to_proof_state(m)) print(to_proof_state(m))
local s = to_proof_state(m) local s = to_proof_state(m)
local n, g = s:goals():head() local g = s:goals():head()
local hs = g:hyps() print(g)
local h = hs:head()
local pm = proof_map()
pm:insert("main", h)
local r = s:pb(pm, substitution())
print(r)
assert(env:infer_type(r) == env:infer_type(m))