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

feat(library/tactic): add mk_simple_tactic template

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-23 15:53:45 -08:00
parent f19944cf09
commit d1adfd52e6
2 changed files with 19 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -77,7 +77,7 @@ tactic trace_tactic(char const * msg) {
}
tactic assumption_tactic() {
return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state_seq {
return mk_simple_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state {
list<std::pair<name, expr>> proofs;
goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
expr const & c = g.get_conclusion();
@ -104,7 +104,7 @@ tactic assumption_tactic() {
}
return p(new_m, env, a);
});
return to_proof_state_seq(proof_state(s, new_goals, new_p));
return proof_state(s, new_goals, new_p);
});
}

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

@ -65,6 +65,23 @@ public:
template<typename F>
tactic mk_tactic(F && f) { return tactic(new simple_tactic_cell<F>(std::forward<F>(f))); }
/**
\brief Create a tactic using the given functor.
<code>
proof_state operator()(environment const & env, io_state const & io, proof_state const & s)
</code>
\remark The functor is invoked on demand.
*/
template<typename F>
tactic mk_simple_tactic(F && f) {
return
mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) {
return proof_state_seq([=]() { return some(mk_pair(f(env, io, s), proof_state_seq())); });
});
}
inline proof_state_seq to_proof_state_seq(proof_state const & s) {
return proof_state_seq([=]() { return some(mk_pair(s, proof_state_seq())); });
}