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

feat(library/tactic): add cond and when tacticals.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-24 12:04:32 -08:00
parent 40d612eca0
commit 1c607f3350
2 changed files with 31 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -207,4 +207,25 @@ inline tactic determ(tactic const & t) { return take(t, 1); }
may be infinite or too big.
*/
tactic force(tactic const & t);
/**
\brief Return a tactic that applies the predicate \c p to the input state.
If \c p returns true, then applies \c t1. Otherwise, applies \c t2.
*/
template<typename P>
tactic cond(P && p, tactic const & t1, tactic const & t2) {
return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
return mk_proof_state_seq([=]() {
if (p(env, io, s)) {
return t1(env, io, s).pull();
} else {
return t2(env, io, s).pull();
}
});
});
}
/**
\brief Syntax-sugar for cond(p, t, id_tactic())
*/
template<typename P>
tactic when(P && p, tactic const & t) { return cond(std::forward<P>(p), t, id_tactic()); }
}

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

@ -92,6 +92,16 @@ static void tst1() {
std::cout << "------------------\n";
std::cout << "proof 2: " << force(take(repeat_at_most(interleave(id_tactic(), id_tactic()), 100) << trace_tactic("foo") << t,
5)).solve(env, io, ctx, q) << "\n";
std::cout << "proof 2: " << then(cond([](environment const &, io_state const &, proof_state const &) { return true; },
trace_tactic("then branch.1") + trace_tactic("then branch.2"),
trace_tactic("else branch")),
t).solve(env, io, ctx, q) << "\n";
std::cout << "proof 2: " << then(when([](environment const &, io_state const &, proof_state const &) { return true; },
trace_tactic("when branch.1") + trace_tactic("when branch.2")),
t).solve(env, io, ctx, q) << "\n";
std::cout << "done\n";
}