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

refactor(library/tactic): simplify proof_builder API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-25 10:50:33 -08:00
parent 500ed7a05b
commit ccaa272f9a
4 changed files with 45 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/library/tactic/boolean.cpp
View file

@ -52,8 +52,8 @@ tactic conj_tactic(bool all) {
} }
} }
if (found) { if (found) {
proof_builder p = s.get_proof_builder(); proof_builder pr_builder = s.get_proof_builder();
proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr { proof_builder new_pr_builder = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
proof_map new_m(m); proof_map new_m(m);
for (auto nc : proof_info) { for (auto nc : proof_info) {
name const & n = nc.first; name const & n = nc.first;
@ -62,10 +62,10 @@ tactic conj_tactic(bool all) {
new_m.erase(name(n, 1)); new_m.erase(name(n, 1));
new_m.erase(name(n, 2)); new_m.erase(name(n, 2));
} }
return p(new_m, env, a); return pr_builder(new_m, a);
}); });
goals new_goals = to_list(new_goals_buf.begin(), new_goals_buf.end()); goals new_goals = to_list(new_goals_buf.begin(), new_goals_buf.end());
return some_proof_state(s, new_goals, new_p); return some_proof_state(s, new_goals, new_pr_builder);
} else { } else {
return none_proof_state(); return none_proof_state();
} }
@ -90,8 +90,8 @@ tactic imp_tactic(name const & H_name, bool all) {
} }
}); });
if (found) { if (found) {
proof_builder p = s.get_proof_builder(); proof_builder pr_builder = s.get_proof_builder();
proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr { proof_builder new_pr_builder = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
proof_map new_m(m); proof_map new_m(m);
for (auto const & info : proof_info) { for (auto const & info : proof_info) {
name const & goal_name = std::get<0>(info); name const & goal_name = std::get<0>(info);
@ -102,9 +102,9 @@ tactic imp_tactic(name const & H_name, bool all) {
expr const & c_pr = find(m, goal_name); // proof for the new conclusion expr const & c_pr = find(m, goal_name); // proof for the new conclusion
new_m.insert(goal_name, Discharge(h, c, Fun(hyp_name, h, c_pr))); new_m.insert(goal_name, Discharge(h, c, Fun(hyp_name, h, c_pr)));
} }
return p(new_m, env, a); return pr_builder(new_m, a);
}); });
return some_proof_state(s, new_goals, new_p); return some_proof_state(s, new_goals, new_pr_builder);
} else { } else {
return none_proof_state(); return none_proof_state();
} }
@ -144,8 +144,8 @@ tactic conj_hyp_tactic(bool all) {
} }
}); });
if (found) { if (found) {
proof_builder p = s.get_proof_builder(); proof_builder pr_builder = s.get_proof_builder();
proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr { proof_builder new_pr_builder = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
proof_map new_m(m); proof_map new_m(m);
for (auto const & info : proof_info) { for (auto const & info : proof_info) {
name const & goal_name = info.first; name const & goal_name = info.first;
@ -163,9 +163,9 @@ tactic conj_hyp_tactic(bool all) {
} }
new_m.insert(goal_name, pr); new_m.insert(goal_name, pr);
} }
return p(new_m, env, a); return pr_builder(new_m, a);
}); });
return some_proof_state(s, new_goals, new_p); return some_proof_state(s, new_goals, new_pr_builder);
} else { } else {
return none_proof_state(); return none_proof_state();
} }

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

@ -16,17 +16,36 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
typedef splay_map<name, expr, name_quick_cmp> proof_map; typedef splay_map<name, expr, name_quick_cmp> proof_map;
/**
\brief Return the proof 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); expr find(proof_map const & m, name const & n);
/**
\brief Base class for functors that build a proof for the main goal based on
the proofs of the subgoals.
*/
class proof_builder_cell { class proof_builder_cell {
void dealloc() { delete this; } void dealloc() { delete this; }
MK_LEAN_RC(); MK_LEAN_RC();
public: public:
proof_builder_cell():m_rc(0) {} proof_builder_cell():m_rc(0) {}
virtual ~proof_builder_cell() {} virtual ~proof_builder_cell() {}
virtual expr operator()(proof_map const & p, environment const & env, assignment const & a) const = 0; virtual expr operator()(proof_map const & p, assignment const & a) const = 0;
}; };
template<typename F>
class proof_builder_tpl : public proof_builder_cell {
F m_f;
public:
proof_builder_tpl(F && f):m_f(f) {}
virtual expr operator()(proof_map const & p, assignment const & a) const { return m_f(p, a); }
};
/**
\brief Smart pointer for a proof builder functor.
*/
class proof_builder { class proof_builder {
protected: protected:
proof_builder_cell * m_ptr; proof_builder_cell * m_ptr;
@ -40,19 +59,11 @@ public:
proof_builder & operator=(proof_builder const & s) { LEAN_COPY_REF(proof_builder, s); } proof_builder & operator=(proof_builder const & s) { LEAN_COPY_REF(proof_builder, s); }
proof_builder & operator=(proof_builder && s) { LEAN_MOVE_REF(proof_builder, s); } proof_builder & operator=(proof_builder && s) { LEAN_MOVE_REF(proof_builder, s); }
expr operator()(proof_map const & p, environment const & env, assignment const & a) const { return m_ptr->operator()(p, env, a); } expr operator()(proof_map const & p, assignment const & a) const { return m_ptr->operator()(p, a); }
};
template<typename F>
class simple_proof_builder : public proof_builder_cell {
F m_f;
public:
simple_proof_builder(F && f):m_f(f) {}
virtual expr operator()(proof_map const & p, environment const & env, assignment const & a) const { return m_f(p, env, a); }
}; };
template<typename F> template<typename F>
proof_builder mk_proof_builder(F && f) { proof_builder mk_proof_builder(F && f) {
return proof_builder(new simple_proof_builder<F>(std::forward<F>(f))); return proof_builder(new proof_builder_tpl<F>(std::forward<F>(f)));
} }
} }

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

@ -24,16 +24,16 @@ format proof_state::pp(formatter const & fmt, options const & opts) const {
static name g_main("main"); static name g_main("main");
proof_state to_proof_state(environment const & env, context const & ctx, expr const & t) { proof_state to_proof_state(environment const & env, context const & ctx, expr const & t) {
auto gfn = to_goal(env, ctx, t); auto gfn = to_goal(env, ctx, t);
goal g = gfn.first; goal g = gfn.first;
goal_proof_fn fn = gfn.second; goal_proof_fn fn = gfn.second;
proof_builder p = mk_proof_builder( proof_builder pr_builder = mk_proof_builder(
[=](proof_map const & m, environment const &, assignment const &) -> expr { [=](proof_map const & m, assignment const &) -> expr {
expr p = find(m, g_main); expr p = find(m, g_main);
if (!p) if (!p)
throw exception(sstream() << "failed to find proof for '" << g_main << "' goal"); throw exception(sstream() << "failed to find proof for '" << g_main << "' goal");
return fn(p); return fn(p);
}); });
return proof_state(goals(mk_pair(g_main, g)), metavar_env(), p); return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder);
} }
} }

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

@ -29,7 +29,7 @@ expr tactic::solve(environment const & env, io_state const & io, proof_state con
proof_state final = p->first; proof_state final = p->first;
assignment a(final.get_menv()); assignment a(final.get_menv());
proof_map m; proof_map m;
return final.get_proof_builder()(m, env, a); return final.get_proof_builder()(m, a);
} }
expr tactic::solve(environment const & env, io_state const & io, context const & ctx, expr const & t) { expr tactic::solve(environment const & env, io_state const & io, context const & ctx, expr const & t) {
@ -113,15 +113,15 @@ tactic assumption_tactic() {
return g; return g;
} }
}); });
proof_builder p = s.get_proof_builder(); proof_builder pr_builder = s.get_proof_builder();
proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr { proof_builder new_pr_builder = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
proof_map new_m(m); proof_map new_m(m);
for (auto const & np : proofs) { for (auto const & np : proofs) {
new_m.insert(np.first, np.second); new_m.insert(np.first, np.second);
} }
return p(new_m, env, a); return pr_builder(new_m, a);
}); });
return proof_state(s, new_goals, new_p); return proof_state(s, new_goals, new_pr_builder);
}); });
} }