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

refactor(library/tactic): modify par and try_for tactics

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-23 17:03:59 -08:00
parent 924187b055
commit 16cf60a04b
2 changed files with 9 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -132,35 +132,7 @@ tactic try_for(tactic t, unsigned ms, unsigned check_ms) {
check_ms = 1;
return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
tactic _t(t);
proof_state_seq r;
std::atomic<bool> done(false);
interruptible_thread th([&]() {
try {
r = _t(env, io, s);
} catch (...) {
r = proof_state_seq();
}
done = true;
});
try {
auto start = std::chrono::steady_clock::now();
std::chrono::milliseconds d(ms);
std::chrono::milliseconds small(check_ms);
while (!done) {
auto curr = std::chrono::steady_clock::now();
if (std::chrono::duration_cast<std::chrono::milliseconds>(curr - start) > d)
break;
check_interrupted();
std::this_thread::sleep_for(small);
}
th.request_interrupt();
th.join();
return r;
} catch (...) {
th.request_interrupt();
th.join();
throw;
}
return timeout(_t(env, io, s), ms, check_ms);
});
}
@ -184,44 +156,7 @@ tactic par(tactic t1, tactic t2, unsigned check_ms) {
return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
tactic _t1(t1);
tactic _t2(t2);
proof_state_seq r1;
proof_state_seq r2;
std::atomic<bool> done1(false);
std::atomic<bool> done2(false);
interruptible_thread th1([&]() {
try {
r1 = _t1(env, io, s);
} catch (...) {
r1 = proof_state_seq();
}
done1 = true;
});
interruptible_thread th2([&]() {
try {
r2 = _t2(env, io, s);
} catch (...) {
r2 = proof_state_seq();
}
done2 = true;
});
try {
std::chrono::milliseconds small(check_ms);
while (!done1 && !done2) {
check_interrupted();
std::this_thread::sleep_for(small);
}
th1.request_interrupt();
th2.request_interrupt();
th1.join();
th2.join();
return orelse(r1, r2);
} catch (...) {
th1.request_interrupt();
th2.request_interrupt();
th1.join();
th2.join();
throw;
}
return par(_t1(env, io, s), _t2(env, io, s), check_ms);
});
}

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

@ -17,18 +17,18 @@ Author: Leonardo de Moura
using namespace lean;
tactic loop_tactic() {
return mk_tactic([=](environment const &, io_state const &, proof_state const &) -> proof_state_seq {
return mk_simple_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state {
while (true) {
check_interrupted();
}
return proof_state_seq();
return s;
});
}
tactic set_tactic(std::atomic<bool> * flag) {
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 {
*flag = true;
return to_proof_state_seq(s);
return s;
});
}
@ -73,13 +73,15 @@ static void tst1() {
100),
env, io, ctx, q);
lean_assert(!flag1);
std::cout << "Before nested try_for...\n";
check_failure(orelse(try_for(try_for(loop_tactic(), 10000), 100),
set_tactic(&flag1)),
env, io, ctx, q);
lean_assert(flag1);
std::cout << "Before parallel 3 parallel tactics...\n";
std::cout << "proof 2: " << par(loop_tactic(), par(loop_tactic(), t)).solve(env, io, ctx, q) << "\n";
#endif
std::cout << "Before hello1 and 2...\n";
std::cout << "proof 2: " << orelse(then(repeat_at_most(append(trace_tactic("hello1"), trace_tactic("hello2")), 5), fail_tactic()),
t).solve(env, io, ctx, q) << "\n";
std::cout << "------------------\n";