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

feat(library/tactic): refine repeat and repeat_at_most tacticals

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-24 11:18:32 -08:00
parent 8e87ef5da8
commit 22c49146ae
1 changed files with 8 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -159,39 +159,19 @@ tactic par(tactic t1, tactic t2, unsigned check_ms) {
tactic repeat(tactic t) {
return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq {
tactic t1(t);
proof_state_seq r = t1(env, io, s1);
// TODO(Leo): pull should be executed lazily
auto p = r.pull();
if (!p) {
return to_proof_state_seq(s1);
} else {
return map_append(to_proof_state_seq(p), [=](proof_state const & s2) {
check_interrupted();
tactic t2 = repeat(t1);
return t2(env, io, s2);
});
}
return repeat(s1, [=](proof_state const & s2) {
tactic _t1(t);
return _t1(env, io, s2);
});
});
}
tactic repeat_at_most(tactic t, unsigned k) {
return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq {
if (k == 0)
return to_proof_state_seq(s1);
tactic t1(t);
proof_state_seq r = t1(env, io, s1);
// TODO(Leo): pull should be executed lazily
auto p = r.pull();
if (!p) {
return to_proof_state_seq(s1);
} else {
return map_append(to_proof_state_seq(p), [=](proof_state const & s2) {
check_interrupted();
tactic t2 = repeat_at_most(t1, k - 1);
return t2(env, io, s2);
});
}
return repeat_at_most(s1, [=](proof_state const & s2) {
tactic _t1(t);
return _t1(env, io, s2);
}, k);
});
}