diff --git a/src/library/tactic/boolean.cpp b/src/library/tactic/boolean.cpp index 2645a6c5d6..b3a764645d 100644 --- a/src/library/tactic/boolean.cpp +++ b/src/library/tactic/boolean.cpp @@ -52,8 +52,8 @@ tactic conj_tactic(bool all) { } } if (found) { - proof_builder p = s.get_proof_builder(); - proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr { + proof_builder pr_builder = s.get_proof_builder(); + proof_builder new_pr_builder = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { proof_map new_m(m); for (auto nc : proof_info) { 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, 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()); - return some_proof_state(s, new_goals, new_p); + return some_proof_state(s, new_goals, new_pr_builder); } else { return none_proof_state(); } @@ -90,8 +90,8 @@ tactic imp_tactic(name const & H_name, bool all) { } }); if (found) { - proof_builder p = s.get_proof_builder(); - proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr { + proof_builder pr_builder = s.get_proof_builder(); + proof_builder new_pr_builder = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { proof_map new_m(m); for (auto const & info : proof_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 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 { return none_proof_state(); } @@ -144,8 +144,8 @@ tactic conj_hyp_tactic(bool all) { } }); if (found) { - proof_builder p = s.get_proof_builder(); - proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr { + proof_builder pr_builder = s.get_proof_builder(); + proof_builder new_pr_builder = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { proof_map new_m(m); for (auto const & info : proof_info) { name const & goal_name = info.first; @@ -163,9 +163,9 @@ tactic conj_hyp_tactic(bool all) { } 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 { return none_proof_state(); } diff --git a/src/library/tactic/proof_builder.h b/src/library/tactic/proof_builder.h index 0f49592fd1..3c0f3744c4 100644 --- a/src/library/tactic/proof_builder.h +++ b/src/library/tactic/proof_builder.h @@ -16,17 +16,36 @@ Author: Leonardo de Moura namespace lean { typedef splay_map 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); +/** + \brief Base class for functors that build a proof for the main goal based on + the proofs of the subgoals. +*/ class proof_builder_cell { void dealloc() { delete this; } MK_LEAN_RC(); public: proof_builder_cell():m_rc(0) {} 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 +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 { protected: 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 && 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); } -}; - -template -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); } + expr operator()(proof_map const & p, assignment const & a) const { return m_ptr->operator()(p, a); } }; template proof_builder mk_proof_builder(F && f) { - return proof_builder(new simple_proof_builder(std::forward(f))); + return proof_builder(new proof_builder_tpl(std::forward(f))); } } diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 1d861c21b7..cabb6230c8 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -24,16 +24,16 @@ format proof_state::pp(formatter const & fmt, options const & opts) const { static name g_main("main"); proof_state to_proof_state(environment const & env, context const & ctx, expr const & t) { - auto gfn = to_goal(env, ctx, t); - goal g = gfn.first; - goal_proof_fn fn = gfn.second; - proof_builder p = mk_proof_builder( - [=](proof_map const & m, environment const &, assignment const &) -> expr { + auto gfn = to_goal(env, ctx, t); + goal g = gfn.first; + goal_proof_fn fn = gfn.second; + proof_builder pr_builder = mk_proof_builder( + [=](proof_map const & m, assignment const &) -> expr { expr p = find(m, g_main); if (!p) throw exception(sstream() << "failed to find proof for '" << g_main << "' goal"); 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); } } diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 75ad791865..fbe3a73ce4 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -29,7 +29,7 @@ expr tactic::solve(environment const & env, io_state const & io, proof_state con proof_state final = p->first; assignment a(final.get_menv()); 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) { @@ -113,15 +113,15 @@ tactic assumption_tactic() { return g; } }); - proof_builder p = s.get_proof_builder(); - proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr { + proof_builder pr_builder = s.get_proof_builder(); + proof_builder new_pr_builder = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { proof_map new_m(m); for (auto const & np : proofs) { 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); }); }