2013-11-21 18:44:53 +00:00
|
|
|
/*
|
|
|
|
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
|
|
|
|
Author: Leonardo de Moura
|
|
|
|
*/
|
2013-11-21 23:31:55 +00:00
|
|
|
#include <utility>
|
2013-11-22 02:39:33 +00:00
|
|
|
#include <chrono>
|
2013-11-24 01:06:00 +00:00
|
|
|
#include <string>
|
2013-11-28 01:47:29 +00:00
|
|
|
#include "util/luaref.h"
|
|
|
|
#include "util/script_state.h"
|
2013-11-23 23:33:25 +00:00
|
|
|
#include "util/sstream.h"
|
2013-11-21 23:31:55 +00:00
|
|
|
#include "util/interrupt.h"
|
2013-11-22 02:39:33 +00:00
|
|
|
#include "util/lazy_list_fn.h"
|
2013-12-01 16:51:56 +00:00
|
|
|
#include "kernel/replace_visitor.h"
|
|
|
|
#include "kernel/instantiate.h"
|
2013-12-18 00:35:39 +00:00
|
|
|
#include "kernel/update_expr.h"
|
2013-12-22 22:10:42 +00:00
|
|
|
#include "kernel/builtin.h"
|
2013-11-28 01:47:29 +00:00
|
|
|
#include "library/kernel_bindings.h"
|
2013-12-22 22:10:42 +00:00
|
|
|
#include "library/basic_thms.h"
|
2013-11-21 18:44:53 +00:00
|
|
|
#include "library/tactic/tactic.h"
|
|
|
|
|
|
|
|
namespace lean {
|
2013-11-25 21:04:09 +00:00
|
|
|
solve_result::solve_result(expr const & pr):m_kind(solve_result_kind::Proof) { new (&m_proof) expr(pr); }
|
|
|
|
solve_result::solve_result(counterexample const & cex):m_kind(solve_result_kind::Counterexample) { new (&m_cex) counterexample(cex); }
|
|
|
|
solve_result::solve_result(list<proof_state> const & fs):m_kind(solve_result_kind::Failure) { new (&m_failures) list<proof_state>(fs); }
|
2013-11-28 01:47:29 +00:00
|
|
|
void solve_result::init(solve_result const & r) {
|
|
|
|
m_kind = r.m_kind;
|
2013-11-25 21:04:09 +00:00
|
|
|
switch (m_kind) {
|
2013-11-28 01:47:29 +00:00
|
|
|
case solve_result_kind::None: break;
|
2013-11-25 21:04:09 +00:00
|
|
|
case solve_result_kind::Proof: new (&m_proof) expr(r.m_proof); break;
|
|
|
|
case solve_result_kind::Counterexample: new (&m_cex) counterexample(r.m_cex); break;
|
|
|
|
case solve_result_kind::Failure: new (&m_failures) list<proof_state>(r.m_failures); break;
|
|
|
|
}
|
|
|
|
}
|
2013-11-28 01:47:29 +00:00
|
|
|
void solve_result::destroy() {
|
2013-11-25 21:04:09 +00:00
|
|
|
switch (m_kind) {
|
2013-11-28 01:47:29 +00:00
|
|
|
case solve_result_kind::None: break;
|
2013-11-25 21:04:09 +00:00
|
|
|
case solve_result_kind::Proof: m_proof.~expr(); break;
|
|
|
|
case solve_result_kind::Counterexample: m_cex.~counterexample(); break;
|
|
|
|
case solve_result_kind::Failure: m_failures.~list<proof_state>(); break;
|
|
|
|
}
|
|
|
|
}
|
2013-11-28 01:47:29 +00:00
|
|
|
solve_result::solve_result(solve_result const & r) {
|
|
|
|
init(r);
|
|
|
|
}
|
|
|
|
solve_result::~solve_result() {
|
|
|
|
destroy();
|
|
|
|
}
|
|
|
|
solve_result & solve_result::operator=(solve_result & other) {
|
|
|
|
if (this == &other)
|
|
|
|
return *this;
|
|
|
|
destroy();
|
|
|
|
init(other);
|
|
|
|
return *this;
|
|
|
|
}
|
|
|
|
solve_result & solve_result::operator=(solve_result && other) {
|
|
|
|
lean_assert(this != &other);
|
|
|
|
destroy();
|
|
|
|
init(other);
|
|
|
|
return *this;
|
|
|
|
}
|
2013-11-25 21:04:09 +00:00
|
|
|
|
2013-11-21 18:44:53 +00:00
|
|
|
tactic & tactic::operator=(tactic const & s) {
|
2013-12-13 23:00:30 +00:00
|
|
|
LEAN_COPY_REF(s);
|
2013-11-21 18:44:53 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
tactic & tactic::operator=(tactic && s) {
|
2013-12-13 23:00:30 +00:00
|
|
|
LEAN_MOVE_REF(s);
|
2013-11-21 18:44:53 +00:00
|
|
|
}
|
2013-11-21 20:34:37 +00:00
|
|
|
|
2013-11-30 19:28:10 +00:00
|
|
|
/**
|
|
|
|
\brief Try to extract a proof from the given proof state
|
|
|
|
*/
|
|
|
|
optional<expr> to_proof(proof_state const & s) {
|
|
|
|
if (s.is_proof_final_state()) {
|
|
|
|
try {
|
2013-12-13 01:47:11 +00:00
|
|
|
assignment a(s.get_menv().copy());
|
2013-11-30 19:28:10 +00:00
|
|
|
proof_map m;
|
2013-12-08 18:34:38 +00:00
|
|
|
return some_expr(s.get_proof_builder()(m, a));
|
2013-11-30 19:28:10 +00:00
|
|
|
} catch (...) {
|
|
|
|
}
|
|
|
|
}
|
2013-12-08 18:34:38 +00:00
|
|
|
return none_expr();
|
2013-11-30 19:28:10 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
/**
|
|
|
|
\brief Try to extract a counterexample from the given proof state.
|
|
|
|
*/
|
|
|
|
optional<counterexample> to_counterexample(proof_state const & s) {
|
|
|
|
if (s.is_cex_final_state()) {
|
2013-12-13 01:47:11 +00:00
|
|
|
assignment a(s.get_menv().copy());
|
2013-11-30 19:28:10 +00:00
|
|
|
name goal_name(head(s.get_goals()).first);
|
|
|
|
try {
|
|
|
|
return some(s.get_cex_builder()(goal_name, optional<counterexample>(), a));
|
|
|
|
} catch (...) {
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return optional<counterexample>();
|
|
|
|
}
|
|
|
|
|
2013-12-13 00:33:31 +00:00
|
|
|
solve_result tactic::solve(ro_environment const & env, io_state const & io, proof_state const & s1) {
|
2013-11-25 21:04:09 +00:00
|
|
|
proof_state_seq r = operator()(env, io, s1);
|
|
|
|
list<proof_state> failures;
|
|
|
|
while (true) {
|
|
|
|
check_interrupted();
|
|
|
|
auto p = r.pull();
|
|
|
|
if (!p) {
|
|
|
|
return solve_result(failures);
|
|
|
|
} else {
|
|
|
|
proof_state s2 = p->first;
|
|
|
|
r = p->second;
|
2013-11-30 19:28:10 +00:00
|
|
|
optional<expr> pr = to_proof(s2);
|
|
|
|
if (pr)
|
|
|
|
return solve_result(*pr);
|
|
|
|
optional<counterexample> cex = to_counterexample(s2);
|
|
|
|
if (cex)
|
|
|
|
return solve_result(*cex);
|
2013-11-25 21:04:09 +00:00
|
|
|
failures = cons(s2, failures);
|
|
|
|
}
|
|
|
|
}
|
2013-11-22 00:44:31 +00:00
|
|
|
}
|
|
|
|
|
2013-12-13 00:33:31 +00:00
|
|
|
solve_result tactic::solve(ro_environment const & env, io_state const & io, context const & ctx, expr const & t) {
|
2013-11-22 01:25:19 +00:00
|
|
|
proof_state s = to_proof_state(env, ctx, t);
|
|
|
|
return solve(env, io, s);
|
|
|
|
}
|
|
|
|
|
2013-11-22 02:39:33 +00:00
|
|
|
tactic id_tactic() {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic1([](ro_environment const &, io_state const &, proof_state const & s) -> proof_state {
|
2013-11-24 08:38:52 +00:00
|
|
|
return s;
|
2013-11-22 02:39:33 +00:00
|
|
|
});
|
|
|
|
}
|
2013-11-22 01:25:19 +00:00
|
|
|
|
2013-11-22 02:39:33 +00:00
|
|
|
tactic fail_tactic() {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([](ro_environment const &, io_state const &, proof_state const &) -> proof_state_seq {
|
2013-11-22 02:39:33 +00:00
|
|
|
return proof_state_seq();
|
|
|
|
});
|
|
|
|
}
|
2013-11-22 01:25:19 +00:00
|
|
|
|
|
|
|
tactic now_tactic() {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic01([](ro_environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
|
2013-11-22 01:25:19 +00:00
|
|
|
if (!empty(s.get_goals()))
|
2013-11-25 18:39:40 +00:00
|
|
|
return none_proof_state();
|
2013-11-22 02:39:33 +00:00
|
|
|
else
|
2013-11-25 18:39:40 +00:00
|
|
|
return some(s);
|
2013-11-22 01:25:19 +00:00
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2013-11-23 23:33:25 +00:00
|
|
|
tactic trace_tactic(std::string const & msg) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic1([=](ro_environment const &, io_state const & io, proof_state const & s) -> proof_state {
|
2013-11-24 08:38:52 +00:00
|
|
|
io.get_diagnostic_channel() << msg << "\n";
|
|
|
|
io.get_diagnostic_channel().get_stream().flush();
|
|
|
|
return s;
|
2013-11-23 23:33:25 +00:00
|
|
|
});
|
|
|
|
}
|
|
|
|
|
|
|
|
tactic trace_tactic(sstream const & msg) {
|
|
|
|
return trace_tactic(msg.str());
|
|
|
|
}
|
|
|
|
|
|
|
|
tactic trace_tactic(char const * msg) {
|
|
|
|
return trace_tactic(std::string(msg));
|
|
|
|
}
|
|
|
|
|
2013-11-25 00:44:02 +00:00
|
|
|
tactic trace_state_tactic() {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic1([=](ro_environment const &, io_state const & io, proof_state const & s) -> proof_state {
|
2013-11-25 00:44:02 +00:00
|
|
|
options opts = io.get_options();
|
|
|
|
format fmt = s.pp(io.get_formatter(), opts);
|
2013-11-30 19:28:10 +00:00
|
|
|
io.get_diagnostic_channel() << "Proof state:\n" << mk_pair(fmt, opts) << "\n";
|
2013-11-25 00:44:02 +00:00
|
|
|
io.get_diagnostic_channel().get_stream().flush();
|
|
|
|
return s;
|
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2013-11-25 00:29:04 +00:00
|
|
|
tactic suppress_trace(tactic const & t) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
|
2013-11-25 00:29:04 +00:00
|
|
|
io_state new_io(io);
|
|
|
|
std::shared_ptr<output_channel> out(new string_output_channel());
|
|
|
|
new_io.set_diagnostic_channel(out);
|
|
|
|
return t(env, new_io, s);
|
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2013-11-22 01:25:19 +00:00
|
|
|
tactic assumption_tactic() {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic01([](ro_environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
|
2013-11-22 01:25:19 +00:00
|
|
|
list<std::pair<name, expr>> proofs;
|
2013-12-08 07:21:07 +00:00
|
|
|
goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> optional<goal> {
|
2013-11-22 01:25:19 +00:00
|
|
|
expr const & c = g.get_conclusion();
|
2013-12-08 07:21:07 +00:00
|
|
|
optional<expr> pr;
|
2013-11-22 01:25:19 +00:00
|
|
|
for (auto const & p : g.get_hypotheses()) {
|
|
|
|
check_interrupted();
|
|
|
|
if (p.second == c) {
|
2013-11-25 00:29:04 +00:00
|
|
|
pr = mk_constant(p.first, p.second);
|
2013-11-22 01:25:19 +00:00
|
|
|
break;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if (pr) {
|
2013-12-08 07:21:07 +00:00
|
|
|
proofs.emplace_front(gname, *pr);
|
|
|
|
return optional<goal>();
|
2013-11-22 01:25:19 +00:00
|
|
|
} else {
|
2013-12-08 07:21:07 +00:00
|
|
|
return some(g);
|
2013-11-22 01:25:19 +00:00
|
|
|
}
|
|
|
|
});
|
2013-12-01 15:53:46 +00:00
|
|
|
if (empty(proofs))
|
2013-11-29 02:23:38 +00:00
|
|
|
return none_proof_state();
|
2013-12-01 15:53:46 +00:00
|
|
|
proof_builder new_pb = add_proofs(s.get_proof_builder(), proofs);
|
2013-12-01 16:51:56 +00:00
|
|
|
return some(proof_state(s, new_gs, new_pb));
|
2013-11-22 01:25:19 +00:00
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2013-12-22 22:10:42 +00:00
|
|
|
tactic trivial_tactic() {
|
|
|
|
return mk_tactic01([](ro_environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
|
|
|
|
list<std::pair<name, expr>> proofs;
|
|
|
|
goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> optional<goal> {
|
|
|
|
expr const & c = env->normalize(g.get_conclusion(), context(), true);
|
|
|
|
if (c == True) {
|
|
|
|
proofs.emplace_front(gname, Trivial);
|
|
|
|
return optional<goal>();
|
|
|
|
} else {
|
|
|
|
return some(g);
|
|
|
|
}
|
|
|
|
});
|
|
|
|
if (empty(proofs))
|
|
|
|
return none_proof_state();
|
|
|
|
proof_builder new_pb = add_proofs(s.get_proof_builder(), proofs);
|
|
|
|
return some(proof_state(s, new_gs, new_pb));
|
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2013-11-24 19:22:40 +00:00
|
|
|
tactic then(tactic const & t1, tactic const & t2) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq {
|
2013-11-24 19:22:40 +00:00
|
|
|
return map_append(t1(env, io, s1), [=](proof_state const & s2) {
|
2013-11-22 02:39:33 +00:00
|
|
|
check_interrupted();
|
2013-11-24 19:22:40 +00:00
|
|
|
return t2(env, io, s2);
|
2013-12-07 22:59:21 +00:00
|
|
|
}, "THEN tactical");
|
2013-11-22 02:39:33 +00:00
|
|
|
});
|
|
|
|
}
|
2013-11-21 20:34:37 +00:00
|
|
|
|
2013-11-24 19:22:40 +00:00
|
|
|
tactic orelse(tactic const & t1, tactic const & t2) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
|
2013-12-07 22:59:21 +00:00
|
|
|
return orelse(t1(env, io, s), t2(env, io, s), "ORELSE tactical");
|
2013-11-22 02:39:33 +00:00
|
|
|
});
|
|
|
|
}
|
2013-11-21 20:34:37 +00:00
|
|
|
|
2013-11-25 00:29:04 +00:00
|
|
|
tactic using_params(tactic const & t, options const & opts) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
|
2013-11-25 00:29:04 +00:00
|
|
|
io_state new_io(io);
|
|
|
|
new_io.set_options(join(opts, io.get_options()));
|
|
|
|
return t(env, new_io, s);
|
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2013-11-24 19:22:40 +00:00
|
|
|
tactic try_for(tactic const & t, unsigned ms, unsigned check_ms) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
|
2013-11-24 19:22:40 +00:00
|
|
|
return timeout(t(env, io, s), ms, check_ms);
|
2013-11-22 02:39:33 +00:00
|
|
|
});
|
|
|
|
}
|
2013-11-23 00:15:03 +00:00
|
|
|
|
2013-11-24 19:22:40 +00:00
|
|
|
tactic append(tactic const & t1, tactic const & t2) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
|
2013-12-07 22:59:21 +00:00
|
|
|
return append(t1(env, io, s), t2(env, io, s), "APPEND tactical");
|
2013-11-23 00:15:03 +00:00
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2013-11-24 19:22:40 +00:00
|
|
|
tactic interleave(tactic const & t1, tactic const & t2) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
|
2013-12-07 22:59:21 +00:00
|
|
|
return interleave(t1(env, io, s), t2(env, io, s), "INTERLEAVE tactical");
|
2013-11-23 00:15:03 +00:00
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2013-11-24 19:22:40 +00:00
|
|
|
tactic par(tactic const & t1, tactic const & t2, unsigned check_ms) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
|
2013-11-24 19:22:40 +00:00
|
|
|
return par(t1(env, io, s), t2(env, io, s), check_ms);
|
2013-11-23 00:15:03 +00:00
|
|
|
});
|
|
|
|
}
|
2013-11-23 00:39:25 +00:00
|
|
|
|
2013-11-24 19:22:40 +00:00
|
|
|
tactic repeat(tactic const & t) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq {
|
2013-11-24 19:18:32 +00:00
|
|
|
return repeat(s1, [=](proof_state const & s2) {
|
2013-11-24 19:22:40 +00:00
|
|
|
return t(env, io, s2);
|
2013-12-07 22:59:21 +00:00
|
|
|
}, "REPEAT tactical");
|
2013-11-23 00:39:25 +00:00
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2013-11-24 19:22:40 +00:00
|
|
|
tactic repeat_at_most(tactic const & t, unsigned k) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq {
|
2013-11-24 19:18:32 +00:00
|
|
|
return repeat_at_most(s1, [=](proof_state const & s2) {
|
2013-11-24 19:22:40 +00:00
|
|
|
return t(env, io, s2);
|
2013-12-07 22:59:21 +00:00
|
|
|
}, k, "REPEAT_AT_MOST tactical");
|
2013-11-23 00:39:25 +00:00
|
|
|
});
|
|
|
|
}
|
2013-11-23 01:05:18 +00:00
|
|
|
|
2013-11-24 19:22:40 +00:00
|
|
|
tactic take(tactic const & t, unsigned k) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
|
2013-11-24 19:22:40 +00:00
|
|
|
return take(k, t(env, io, s));
|
2013-11-23 01:05:18 +00:00
|
|
|
});
|
|
|
|
}
|
2013-11-28 01:47:29 +00:00
|
|
|
|
2013-12-13 00:33:31 +00:00
|
|
|
proof_state_seq focus_core(tactic const & t, name const & gname, ro_environment const & env, io_state const & io, proof_state const & s) {
|
2013-11-30 19:28:10 +00:00
|
|
|
for (auto const & p : s.get_goals()) {
|
|
|
|
if (p.first == gname) {
|
|
|
|
proof_builder pb = mk_proof_builder(
|
|
|
|
[=](proof_map const & m, assignment const &) -> expr {
|
|
|
|
return find(m, gname);
|
|
|
|
});
|
|
|
|
cex_builder cb = mk_cex_builder_for(gname);
|
|
|
|
proof_state new_s(s, goals(p), pb, cb); // new state with singleton goal
|
|
|
|
return map(t(env, io, new_s), [=](proof_state const & s2) {
|
|
|
|
// we have to put back the goals that were not selected
|
|
|
|
list<std::pair<name, name>> renamed_goals;
|
|
|
|
goals new_gs = map_append(s.get_goals(), [&](std::pair<name, goal> const & p) {
|
|
|
|
if (p.first == gname) {
|
|
|
|
name_set used_names;
|
|
|
|
s.get_goal_names(used_names);
|
|
|
|
used_names.erase(gname);
|
|
|
|
return map(s2.get_goals(), [&](std::pair<name, goal> const & p2) -> std::pair<name, goal> {
|
|
|
|
name uname = mk_unique(used_names, p2.first);
|
|
|
|
used_names.insert(uname);
|
|
|
|
renamed_goals.emplace_front(p2.first, uname);
|
|
|
|
return mk_pair(uname, p2.second);
|
|
|
|
});
|
|
|
|
} else {
|
|
|
|
return goals(p);
|
|
|
|
}
|
|
|
|
});
|
|
|
|
proof_builder pb1 = s.get_proof_builder();
|
|
|
|
proof_builder pb2 = s2.get_proof_builder();
|
|
|
|
proof_builder new_pb = mk_proof_builder(
|
|
|
|
[=](proof_map const & m, assignment const & a) -> expr {
|
|
|
|
proof_map m1(m); // map for pb1
|
|
|
|
proof_map m2; // map for pb2
|
|
|
|
for (auto p : renamed_goals) {
|
|
|
|
m2.insert(p.first, find(m, p.second));
|
|
|
|
m1.erase(p.first);
|
|
|
|
}
|
|
|
|
m1.insert(gname, pb2(m2, a));
|
|
|
|
return pb1(m1, a);
|
|
|
|
});
|
|
|
|
cex_builder cb1 = s.get_cex_builder();
|
|
|
|
cex_builder cb2 = s2.get_cex_builder();
|
|
|
|
cex_builder new_cb = mk_cex_builder(
|
|
|
|
[=](name const & n, optional<counterexample> const & cex, assignment const & a) -> counterexample {
|
|
|
|
for (auto p : renamed_goals) {
|
|
|
|
if (p.second == n)
|
|
|
|
return cb2(p.first, cex, a);
|
|
|
|
}
|
|
|
|
return cb1(n, cex, a);
|
|
|
|
});
|
|
|
|
return proof_state(s2, new_gs, new_pb, new_cb);
|
|
|
|
});
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return proof_state_seq(); // tactic is not applicable
|
|
|
|
}
|
|
|
|
|
|
|
|
tactic focus(tactic const & t, name const & gname) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
|
2013-11-30 19:28:10 +00:00
|
|
|
return focus_core(t, gname, env, io, s);
|
|
|
|
});
|
|
|
|
}
|
|
|
|
|
|
|
|
tactic focus(tactic const & t, int i) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
|
2013-12-05 12:41:08 +00:00
|
|
|
if (optional<name> n = s.get_ith_goal_name(i))
|
|
|
|
return focus_core(t, *n, env, io, s);
|
|
|
|
else
|
|
|
|
return proof_state_seq();
|
2013-11-30 19:28:10 +00:00
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2013-12-01 18:41:05 +00:00
|
|
|
class unfold_core_fn : public replace_visitor {
|
|
|
|
protected:
|
|
|
|
bool m_unfolded;
|
|
|
|
|
|
|
|
virtual expr visit_app(expr const & e, context const & ctx) {
|
|
|
|
expr const & f = arg(e, 0);
|
|
|
|
if (is_constant(f)) {
|
|
|
|
buffer<expr> new_args;
|
|
|
|
for (unsigned i = 0; i < num_args(e); i++)
|
|
|
|
new_args.push_back(visit(arg(e, i), ctx));
|
|
|
|
if (is_lambda(new_args[0]))
|
|
|
|
return apply_beta(new_args[0], new_args.size() - 1, new_args.data() + 1);
|
|
|
|
else
|
|
|
|
return update_app(e, new_args);
|
|
|
|
} else {
|
|
|
|
return replace_visitor::visit_app(e, ctx);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
public:
|
|
|
|
unfold_core_fn():m_unfolded(false) {}
|
|
|
|
bool unfolded() const { return m_unfolded; }
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
|
|
class unfold_fn : public unfold_core_fn {
|
2013-12-01 16:51:56 +00:00
|
|
|
protected:
|
|
|
|
name const & m_name;
|
|
|
|
expr const & m_def;
|
|
|
|
|
|
|
|
virtual expr visit_constant(expr const & c, context const &) {
|
|
|
|
if (const_name(c) == m_name) {
|
|
|
|
m_unfolded = true;
|
|
|
|
return m_def;
|
|
|
|
} else {
|
|
|
|
return c;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2013-12-01 18:41:05 +00:00
|
|
|
public:
|
|
|
|
unfold_fn(name const & n, expr const & d):m_name(n), m_def(d) {}
|
|
|
|
};
|
|
|
|
|
|
|
|
class unfold_all_fn : public unfold_core_fn {
|
|
|
|
protected:
|
2013-12-13 00:33:31 +00:00
|
|
|
ro_environment m_env;
|
2013-12-01 18:41:05 +00:00
|
|
|
|
|
|
|
virtual expr visit_constant(expr const & c, context const &) {
|
2013-12-13 00:33:31 +00:00
|
|
|
optional<object> obj = m_env->find_object(const_name(c));
|
refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking a valid term.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 20:47:36 +00:00
|
|
|
if (should_unfold(obj)) {
|
2013-12-01 18:41:05 +00:00
|
|
|
m_unfolded = true;
|
2013-12-08 22:37:38 +00:00
|
|
|
return obj->get_value();
|
2013-12-01 16:51:56 +00:00
|
|
|
} else {
|
2013-12-01 18:41:05 +00:00
|
|
|
return c;
|
2013-12-01 16:51:56 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
public:
|
2013-12-13 00:33:31 +00:00
|
|
|
unfold_all_fn(ro_environment const & env):m_env(env) {}
|
2013-12-01 16:51:56 +00:00
|
|
|
};
|
|
|
|
|
2013-12-01 18:41:05 +00:00
|
|
|
optional<proof_state> unfold_tactic_core(unfold_core_fn & fn, proof_state const & s) {
|
2013-12-08 07:21:07 +00:00
|
|
|
goals new_gs = map_goals(s, [&](name const &, goal const & g) -> optional<goal> {
|
2013-12-01 18:41:05 +00:00
|
|
|
hypotheses new_hs = map(g.get_hypotheses(), [&](hypothesis const & h) { return hypothesis(h.first, fn(h.second)); });
|
|
|
|
expr new_c = fn(g.get_conclusion());
|
2013-12-08 07:21:07 +00:00
|
|
|
return some(goal(new_hs, new_c));
|
2013-12-01 18:41:05 +00:00
|
|
|
});
|
|
|
|
if (fn.unfolded()) {
|
2013-12-08 07:21:07 +00:00
|
|
|
return some(proof_state(s, new_gs));
|
2013-12-01 18:41:05 +00:00
|
|
|
} else {
|
|
|
|
return none_proof_state();
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2013-12-01 16:51:56 +00:00
|
|
|
tactic unfold_tactic(name const & n) {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
|
|
|
|
optional<object> obj = env->find_object(n);
|
2013-12-08 22:37:38 +00:00
|
|
|
if (!obj || !obj->is_definition())
|
2013-12-01 16:51:56 +00:00
|
|
|
return none_proof_state(); // tactic failed
|
2013-12-08 22:37:38 +00:00
|
|
|
unfold_fn fn(n, obj->get_value());
|
2013-12-01 18:41:05 +00:00
|
|
|
return unfold_tactic_core(fn, s);
|
|
|
|
});
|
|
|
|
}
|
|
|
|
|
|
|
|
tactic unfold_tactic() {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
|
2013-12-01 18:41:05 +00:00
|
|
|
unfold_all_fn fn(env);
|
|
|
|
return unfold_tactic_core(fn, s);
|
2013-12-01 16:51:56 +00:00
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2013-12-02 16:10:51 +00:00
|
|
|
class beta_fn : public replace_visitor {
|
|
|
|
protected:
|
|
|
|
bool m_reduced;
|
|
|
|
|
|
|
|
virtual expr visit_app(expr const & e, context const & ctx) {
|
|
|
|
expr const & f = arg(e, 0);
|
|
|
|
if (is_lambda(f)) {
|
|
|
|
m_reduced = true;
|
|
|
|
buffer<expr> new_args;
|
|
|
|
for (unsigned i = 0; i < num_args(e); i++)
|
|
|
|
new_args.push_back(visit(arg(e, i), ctx));
|
|
|
|
lean_assert(is_lambda(new_args[0]));
|
|
|
|
return apply_beta(new_args[0], new_args.size() - 1, new_args.data() + 1);
|
|
|
|
} else {
|
|
|
|
return replace_visitor::visit_app(e, ctx);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
public:
|
|
|
|
beta_fn():m_reduced(false) {}
|
|
|
|
bool reduced() const { return m_reduced; }
|
|
|
|
};
|
|
|
|
|
|
|
|
tactic beta_tactic() {
|
2013-12-13 00:33:31 +00:00
|
|
|
return mk_tactic01([=](ro_environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
|
2013-12-02 16:10:51 +00:00
|
|
|
beta_fn fn;
|
2013-12-08 07:21:07 +00:00
|
|
|
goals new_gs = map_goals(s, [&](name const &, goal const & g) -> optional<goal> {
|
2013-12-02 16:10:51 +00:00
|
|
|
hypotheses new_hs = map(g.get_hypotheses(), [&](hypothesis const & h) { return hypothesis(h.first, fn(h.second)); });
|
|
|
|
expr new_c = fn(g.get_conclusion());
|
2013-12-08 07:21:07 +00:00
|
|
|
return some(goal(new_hs, new_c));
|
2013-12-02 16:10:51 +00:00
|
|
|
});
|
2013-12-22 22:10:42 +00:00
|
|
|
return fn.reduced() ? some(proof_state(s, new_gs)) : none_proof_state();
|
|
|
|
});
|
|
|
|
}
|
|
|
|
|
|
|
|
tactic normalize_tactic(bool unfold_opaque, bool all) {
|
|
|
|
return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
|
|
|
|
bool applied = false;
|
|
|
|
goals new_gs = map_goals(s, [&](name const &, goal const & g) -> optional<goal> {
|
|
|
|
if (!applied || all) {
|
|
|
|
applied = true;
|
|
|
|
expr new_c = env->normalize(g.get_conclusion(), context(), unfold_opaque);
|
|
|
|
return some(goal(g.get_hypotheses(), new_c));
|
|
|
|
} else {
|
|
|
|
return some(g);
|
|
|
|
}
|
|
|
|
});
|
|
|
|
return applied ? some(proof_state(s, new_gs)) : none_proof_state();
|
2013-12-02 16:10:51 +00:00
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2013-11-28 01:47:29 +00:00
|
|
|
DECL_UDATA(proof_state_seq)
|
|
|
|
|
|
|
|
static const struct luaL_Reg proof_state_seq_m[] = {
|
|
|
|
{"__gc", proof_state_seq_gc}, // never throws
|
|
|
|
{0, 0}
|
|
|
|
};
|
|
|
|
|
|
|
|
static int proof_state_seq_next(lua_State * L) {
|
|
|
|
proof_state_seq seq = to_proof_state_seq(L, lua_upvalueindex(1));
|
|
|
|
script_state S = to_script_state(L);
|
|
|
|
proof_state_seq::maybe_pair p;
|
|
|
|
S.exec_unprotected([&]() {
|
|
|
|
p = seq.pull();
|
|
|
|
});
|
|
|
|
if (p) {
|
|
|
|
push_proof_state_seq(L, p->second);
|
|
|
|
lua_replace(L, lua_upvalueindex(1));
|
|
|
|
push_proof_state(L, p->first);
|
|
|
|
} else {
|
|
|
|
lua_pushnil(L);
|
|
|
|
}
|
|
|
|
return 1;
|
|
|
|
}
|
|
|
|
|
|
|
|
static int push_proof_state_seq_it(lua_State * L, proof_state_seq const & seq) {
|
|
|
|
push_proof_state_seq(L, seq);
|
|
|
|
lua_pushcclosure(L, &safe_function<proof_state_seq_next>, 1); // create closure with 1 upvalue
|
|
|
|
return 1;
|
|
|
|
}
|
|
|
|
|
|
|
|
DECL_UDATA(tactic)
|
|
|
|
|
2013-11-29 17:39:31 +00:00
|
|
|
[[ noreturn ]] void throw_tactic_expected(int i) {
|
|
|
|
throw exception(sstream() << "arg #" << i << " must be a tactic or a function that returns a tactic");
|
|
|
|
}
|
|
|
|
|
|
|
|
/**
|
|
|
|
\brief We allow functions (that return tactics) to be used where a tactic
|
|
|
|
is expected. The idea is to be able to write
|
|
|
|
ORELSE(assumption_tactic, conj_tactic)
|
|
|
|
instead of
|
|
|
|
ORELSE(assumption_tactic(), conj_tactic())
|
|
|
|
*/
|
|
|
|
tactic to_tactic_ext(lua_State * L, int i) {
|
|
|
|
if (is_tactic(L, i)) {
|
2013-12-08 23:00:16 +00:00
|
|
|
return to_tactic(L, i);
|
2013-11-29 17:39:31 +00:00
|
|
|
} else if (lua_isfunction(L, i)) {
|
|
|
|
try {
|
|
|
|
lua_pushvalue(L, i);
|
|
|
|
pcall(L, 0, 1, 0);
|
|
|
|
} catch (...) {
|
|
|
|
throw_tactic_expected(i);
|
|
|
|
}
|
|
|
|
if (is_tactic(L, -1)) {
|
2013-12-08 23:00:16 +00:00
|
|
|
tactic t = to_tactic(L, -1);
|
2013-11-29 17:39:31 +00:00
|
|
|
lua_pop(L, 1);
|
2013-12-08 23:00:16 +00:00
|
|
|
return t;
|
2013-11-29 17:39:31 +00:00
|
|
|
} else {
|
|
|
|
throw_tactic_expected(i);
|
|
|
|
}
|
|
|
|
} else {
|
|
|
|
throw_tactic_expected(i);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2013-11-28 01:47:29 +00:00
|
|
|
static void check_ios(io_state * ios) {
|
|
|
|
if (!ios)
|
|
|
|
throw exception("failed to invoke tactic, io_state is not available");
|
|
|
|
}
|
|
|
|
|
2013-12-13 00:33:31 +00:00
|
|
|
static int tactic_call_core(lua_State * L, tactic t, ro_environment env, io_state ios, proof_state s) {
|
2013-11-28 01:47:29 +00:00
|
|
|
script_state S = to_script_state(L);
|
|
|
|
proof_state_seq seq;
|
|
|
|
S.exec_unprotected([&]() {
|
|
|
|
seq = t(env, ios, s);
|
|
|
|
});
|
|
|
|
return push_proof_state_seq_it(L, seq);
|
|
|
|
}
|
|
|
|
|
|
|
|
static int tactic_call(lua_State * L) {
|
|
|
|
int nargs = lua_gettop(L);
|
2013-11-29 17:39:31 +00:00
|
|
|
tactic t = to_tactic_ext(L, 1);
|
2013-12-12 19:19:09 +00:00
|
|
|
ro_shared_environment env(L, 2);
|
2013-11-28 01:47:29 +00:00
|
|
|
if (nargs == 3) {
|
|
|
|
io_state * ios = get_io_state(L);
|
|
|
|
check_ios(ios);
|
|
|
|
return tactic_call_core(L, t, env, *ios, to_proof_state(L, 3));
|
|
|
|
} else {
|
|
|
|
return tactic_call_core(L, t, env, to_io_state(L, 3), to_proof_state(L, 4));
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2013-11-29 06:11:07 +00:00
|
|
|
typedef tactic (*binary_tactic_fn)(tactic const &, tactic const &);
|
|
|
|
|
|
|
|
template<binary_tactic_fn F>
|
|
|
|
static int nary_tactic(lua_State * L) {
|
|
|
|
int nargs = lua_gettop(L);
|
|
|
|
if (nargs < 2)
|
|
|
|
throw exception("tactical expects at least two arguments");
|
2013-11-29 17:39:31 +00:00
|
|
|
tactic r = F(to_tactic_ext(L, 1), to_tactic_ext(L, 2));
|
2013-11-29 06:11:07 +00:00
|
|
|
for (int i = 3; i <= nargs; i++)
|
2013-11-29 17:39:31 +00:00
|
|
|
r = F(r, to_tactic_ext(L, i));
|
2013-11-29 06:11:07 +00:00
|
|
|
return push_tactic(L, r);
|
|
|
|
}
|
|
|
|
|
2013-11-29 17:39:31 +00:00
|
|
|
static int tactic_then(lua_State * L) { return push_tactic(L, then(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
|
|
|
|
static int tactic_orelse(lua_State * L) { return push_tactic(L, orelse(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
|
|
|
|
static int tactic_append(lua_State * L) { return push_tactic(L, append(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
|
|
|
|
static int tactic_interleave(lua_State * L) { return push_tactic(L, interleave(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
|
|
|
|
static int tactic_par(lua_State * L) { return push_tactic(L, par(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
|
2013-11-29 06:11:07 +00:00
|
|
|
|
2013-11-29 17:39:31 +00:00
|
|
|
static int tactic_repeat(lua_State * L) { return push_tactic(L, repeat(to_tactic_ext(L, 1))); }
|
|
|
|
static int tactic_repeat1(lua_State * L) { return push_tactic(L, repeat1(to_tactic_ext(L, 1))); }
|
|
|
|
static int tactic_repeat_at_most(lua_State * L) { return push_tactic(L, repeat_at_most(to_tactic_ext(L, 1), luaL_checkinteger(L, 2))); }
|
|
|
|
static int tactic_take(lua_State * L) { return push_tactic(L, take(to_tactic_ext(L, 1), luaL_checkinteger(L, 2))); }
|
|
|
|
static int tactic_determ(lua_State * L) { return push_tactic(L, determ(to_tactic_ext(L, 1))); }
|
|
|
|
static int tactic_suppress_trace(lua_State * L) { return push_tactic(L, suppress_trace(to_tactic_ext(L, 1))); }
|
|
|
|
static int tactic_try_for(lua_State * L) { return push_tactic(L, try_for(to_tactic_ext(L, 1), luaL_checkinteger(L, 2))); }
|
|
|
|
static int tactic_using_params(lua_State * L) { return push_tactic(L, using_params(to_tactic_ext(L, 1), to_options(L, 2))); }
|
|
|
|
static int tactic_try(lua_State * L) { return push_tactic(L, orelse(to_tactic_ext(L, 1), id_tactic())); }
|
2013-11-28 01:47:29 +00:00
|
|
|
|
2013-11-30 19:28:10 +00:00
|
|
|
static int tactic_focus(lua_State * L) {
|
|
|
|
int nargs = lua_gettop(L);
|
|
|
|
if (nargs == 1)
|
|
|
|
return push_tactic(L, focus(to_tactic_ext(L, 1)));
|
|
|
|
else if (lua_isnumber(L, 2))
|
|
|
|
return push_tactic(L, focus(to_tactic_ext(L, 1), lua_tointeger(L, 2)));
|
|
|
|
else
|
|
|
|
return push_tactic(L, focus(to_tactic_ext(L, 1), to_name_ext(L, 2)));
|
|
|
|
}
|
|
|
|
|
2013-11-28 01:47:29 +00:00
|
|
|
static int push_solve_result(lua_State * L, solve_result const & r) {
|
|
|
|
switch (r.kind()) {
|
|
|
|
case solve_result_kind::None: lua_pushnil(L); break;
|
|
|
|
case solve_result_kind::Proof: push_expr(L, r.get_proof()); break;
|
|
|
|
case solve_result_kind::Counterexample: push_environment(L, r.get_cex()); break;
|
|
|
|
case solve_result_kind::Failure:
|
|
|
|
lua_newtable(L);
|
|
|
|
int i = 1;
|
|
|
|
for (auto s : r.get_failures()) {
|
|
|
|
push_proof_state(L, s);
|
|
|
|
lua_rawseti(L, -2, i);
|
|
|
|
i++;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return 1;
|
|
|
|
}
|
|
|
|
|
2013-12-13 00:33:31 +00:00
|
|
|
static int tactic_solve_core(lua_State * L, tactic t, ro_environment env, io_state ios, proof_state s) {
|
2013-11-28 01:47:29 +00:00
|
|
|
script_state S = to_script_state(L);
|
|
|
|
solve_result result;
|
|
|
|
S.exec_unprotected([&]() {
|
|
|
|
result = t.solve(env, ios, s);;
|
|
|
|
});
|
|
|
|
return push_solve_result(L, result);
|
|
|
|
}
|
|
|
|
|
2013-12-13 00:33:31 +00:00
|
|
|
static int tactic_solve_core(lua_State * L, tactic t, ro_environment env, io_state ios, context ctx, expr e) {
|
2013-11-28 01:47:29 +00:00
|
|
|
script_state S = to_script_state(L);
|
|
|
|
solve_result result;
|
|
|
|
S.exec_unprotected([&]() {
|
|
|
|
result = t.solve(env, ios, ctx, e);
|
|
|
|
});
|
|
|
|
return push_solve_result(L, result);
|
|
|
|
}
|
|
|
|
|
|
|
|
static int tactic_solve(lua_State * L) {
|
|
|
|
int nargs = lua_gettop(L);
|
2013-11-29 17:39:31 +00:00
|
|
|
tactic t = to_tactic_ext(L, 1);
|
2013-12-12 19:19:09 +00:00
|
|
|
ro_shared_environment env(L, 2);
|
2013-11-28 01:47:29 +00:00
|
|
|
if (nargs == 3) {
|
|
|
|
io_state * ios = get_io_state(L);
|
|
|
|
check_ios(ios);
|
|
|
|
return tactic_solve_core(L, t, env, *ios, to_proof_state(L, 3));
|
|
|
|
} else if (nargs == 4) {
|
|
|
|
if (is_io_state(L, 3)) {
|
|
|
|
return tactic_solve_core(L, t, env, to_io_state(L, 3), to_proof_state(L, 4));
|
|
|
|
} else {
|
|
|
|
io_state * ios = get_io_state(L);
|
|
|
|
check_ios(ios);
|
2013-12-08 07:21:07 +00:00
|
|
|
return tactic_solve_core(L, t, env, *ios, to_context(L, 3), to_expr(L, 4));
|
2013-11-28 01:47:29 +00:00
|
|
|
}
|
|
|
|
} else {
|
2013-12-08 07:21:07 +00:00
|
|
|
return tactic_solve_core(L, t, env, to_io_state(L, 3), to_context(L, 4), to_expr(L, 5));
|
2013-11-28 01:47:29 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
static int mk_lua_tactic01(lua_State * L) {
|
|
|
|
luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun
|
2013-11-30 08:44:31 +00:00
|
|
|
script_state::weak_ref S = to_script_state(L).to_weak_ref();
|
2013-11-28 01:47:29 +00:00
|
|
|
luaref ref(L, 1);
|
|
|
|
return push_tactic(L,
|
2013-12-13 00:33:31 +00:00
|
|
|
mk_tactic01([=](ro_environment const & env, io_state const & ios, proof_state const & s) -> optional<proof_state> {
|
2013-11-28 21:49:18 +00:00
|
|
|
script_state S_copy(S);
|
2013-11-28 21:09:30 +00:00
|
|
|
optional<proof_state> r;
|
|
|
|
luaref coref; // Remark: we have to release the reference in a protected block.
|
|
|
|
try {
|
|
|
|
bool done = false;
|
|
|
|
lua_State * co;
|
2013-11-28 21:49:18 +00:00
|
|
|
S_copy.exec_protected([&]() {
|
2013-11-28 21:09:30 +00:00
|
|
|
co = lua_newthread(L); // create a coroutine for executing user-fun
|
|
|
|
coref = luaref(L, -1); // make sure co-routine in not deleted
|
|
|
|
lua_pop(L, 1);
|
|
|
|
ref.push(); // push user-fun on the stack
|
|
|
|
push_environment(L, env); // push args...
|
|
|
|
push_io_state(L, ios);
|
|
|
|
push_proof_state(L, s);
|
|
|
|
lua_xmove(L, co, 4); // move function and arguments to co
|
|
|
|
done = resume(co, 3);
|
|
|
|
});
|
|
|
|
while (!done) {
|
|
|
|
check_interrupted();
|
2013-12-09 22:56:48 +00:00
|
|
|
this_thread::yield(); // give another thread a chance to execute
|
2013-11-28 21:49:18 +00:00
|
|
|
S_copy.exec_protected([&]() {
|
2013-11-28 21:09:30 +00:00
|
|
|
done = resume(co, 0);
|
|
|
|
});
|
|
|
|
}
|
2013-11-28 21:49:18 +00:00
|
|
|
S_copy.exec_protected([&]() {
|
2013-11-28 21:09:30 +00:00
|
|
|
if (is_proof_state(co, -1)) {
|
|
|
|
r = to_proof_state(co, -1);
|
|
|
|
}
|
|
|
|
coref.release();
|
|
|
|
});
|
|
|
|
return r;
|
|
|
|
} catch (...) {
|
2013-11-28 21:49:18 +00:00
|
|
|
S_copy.exec_protected([&]() { coref.release(); });
|
2013-11-28 21:09:30 +00:00
|
|
|
throw;
|
|
|
|
}
|
2013-11-28 01:47:29 +00:00
|
|
|
}));
|
|
|
|
}
|
|
|
|
|
2013-11-29 01:57:24 +00:00
|
|
|
static int mk_lua_cond_tactic(lua_State * L, tactic t1, tactic t2) {
|
|
|
|
luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun
|
2013-11-30 08:44:31 +00:00
|
|
|
script_state::weak_ref S = to_script_state(L).to_weak_ref();
|
2013-11-29 01:57:24 +00:00
|
|
|
luaref ref(L, 1);
|
|
|
|
return push_tactic(L,
|
2013-12-13 00:33:31 +00:00
|
|
|
mk_tactic([=](ro_environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
|
2013-11-29 01:57:24 +00:00
|
|
|
return mk_proof_state_seq([=]() {
|
|
|
|
script_state S_copy(S);
|
|
|
|
bool cond = false;
|
|
|
|
S_copy.exec_protected([&]() {
|
|
|
|
ref.push(); // push user-fun on the stack
|
|
|
|
push_environment(L, env); // push args...
|
|
|
|
push_io_state(L, ios);
|
|
|
|
push_proof_state(L, s);
|
|
|
|
pcall(L, 3, 1, 0);
|
|
|
|
cond = lua_toboolean(L, -1);
|
|
|
|
});
|
|
|
|
if (cond) {
|
|
|
|
return t1(env, ios, s).pull();
|
|
|
|
} else {
|
|
|
|
return t2(env, ios, s).pull();
|
|
|
|
}
|
|
|
|
});
|
|
|
|
}));
|
|
|
|
}
|
|
|
|
|
|
|
|
static int mk_lua_cond_tactic(lua_State * L) {
|
2013-11-29 17:39:31 +00:00
|
|
|
return mk_lua_cond_tactic(L, to_tactic_ext(L, 2), to_tactic_ext(L, 3));
|
2013-11-29 01:57:24 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
static int mk_lua_when_tactic(lua_State * L) {
|
2013-11-29 17:39:31 +00:00
|
|
|
return mk_lua_cond_tactic(L, to_tactic_ext(L, 2), id_tactic());
|
2013-11-29 01:57:24 +00:00
|
|
|
}
|
|
|
|
|
2013-11-29 09:33:26 +00:00
|
|
|
static int mk_id_tactic(lua_State * L) { return push_tactic(L, id_tactic()); }
|
|
|
|
static int mk_now_tactic(lua_State * L) { return push_tactic(L, now_tactic()); }
|
|
|
|
static int mk_fail_tactic(lua_State * L) { return push_tactic(L, fail_tactic()); }
|
|
|
|
static int mk_trace_tactic(lua_State * L) { return push_tactic(L, trace_tactic(luaL_checkstring(L, 1))); }
|
|
|
|
static int mk_assumption_tactic(lua_State * L) { return push_tactic(L, assumption_tactic()); }
|
2013-12-22 22:10:42 +00:00
|
|
|
static int mk_trivial_tactic(lua_State * L) { return push_tactic(L, trivial_tactic()); }
|
2013-11-29 09:33:26 +00:00
|
|
|
static int mk_trace_state_tactic(lua_State * L) { return push_tactic(L, trace_state_tactic()); }
|
2013-12-01 18:41:05 +00:00
|
|
|
static int mk_unfold_tactic(lua_State * L) {
|
|
|
|
int nargs = lua_gettop(L);
|
|
|
|
if (nargs == 0)
|
|
|
|
return push_tactic(L, unfold_tactic());
|
|
|
|
else
|
|
|
|
return push_tactic(L, unfold_tactic(to_name_ext(L, 1)));
|
|
|
|
}
|
2013-12-02 16:10:51 +00:00
|
|
|
static int mk_beta_tactic(lua_State * L) { return push_tactic(L, beta_tactic()); }
|
2013-12-22 22:10:42 +00:00
|
|
|
static int mk_normalize_tactic(lua_State * L) {
|
|
|
|
int nargs = lua_gettop(L);
|
|
|
|
return push_tactic(L, normalize_tactic(nargs == 0 ? false : lua_toboolean(L, 1),
|
|
|
|
nargs <= 1 ? true : lua_toboolean(L, 2)));
|
|
|
|
}
|
|
|
|
static int mk_eval_tactic(lua_State * L) {
|
|
|
|
int nargs = lua_gettop(L);
|
|
|
|
return push_tactic(L, normalize_tactic(true, nargs == 0 ? true : lua_toboolean(L, 1)));
|
|
|
|
}
|
2013-11-28 01:47:29 +00:00
|
|
|
|
|
|
|
static const struct luaL_Reg tactic_m[] = {
|
|
|
|
{"__gc", tactic_gc}, // never throws
|
|
|
|
{"__call", safe_function<tactic_call>},
|
|
|
|
{"__concat", safe_function<tactic_then>},
|
|
|
|
{"__pow", safe_function<tactic_orelse>},
|
|
|
|
{"__add", safe_function<tactic_append>},
|
|
|
|
{"then", safe_function<tactic_then>},
|
|
|
|
{"orelse", safe_function<tactic_orelse>},
|
|
|
|
{"append", safe_function<tactic_append>},
|
2013-11-29 01:57:24 +00:00
|
|
|
{"interleave", safe_function<tactic_interleave>},
|
2013-11-28 01:47:29 +00:00
|
|
|
{"solve", safe_function<tactic_solve>},
|
|
|
|
{"par", safe_function<tactic_par>},
|
|
|
|
{"determ", safe_function<tactic_determ>},
|
|
|
|
{"repeat", safe_function<tactic_repeat>},
|
|
|
|
{"repeat1", safe_function<tactic_repeat1>},
|
|
|
|
{"repeat_at_most", safe_function<tactic_repeat_at_most>},
|
|
|
|
{"take", safe_function<tactic_take>},
|
|
|
|
{"suppress_trace", safe_function<tactic_suppress_trace>},
|
|
|
|
{"try_for", safe_function<tactic_try_for>},
|
2013-11-29 01:57:24 +00:00
|
|
|
{"using_params", safe_function<tactic_using_params>},
|
|
|
|
{"using", safe_function<tactic_using_params>},
|
2013-11-30 19:28:10 +00:00
|
|
|
{"focus", safe_function<tactic_focus>},
|
2013-11-28 01:47:29 +00:00
|
|
|
{0, 0}
|
|
|
|
};
|
|
|
|
|
2013-11-28 16:03:05 +00:00
|
|
|
static void tactic_migrate(lua_State * src, int i, lua_State * tgt) {
|
|
|
|
push_tactic(tgt, to_tactic(src, i));
|
|
|
|
}
|
|
|
|
|
2013-11-28 01:47:29 +00:00
|
|
|
void open_tactic(lua_State * L) {
|
|
|
|
luaL_newmetatable(L, proof_state_seq_mt);
|
|
|
|
lua_pushvalue(L, -1);
|
|
|
|
lua_setfield(L, -2, "__index");
|
|
|
|
setfuncs(L, proof_state_seq_m, 0);
|
|
|
|
SET_GLOBAL_FUN(proof_state_seq_pred, "is_proof_state_seq");
|
|
|
|
|
|
|
|
luaL_newmetatable(L, tactic_mt);
|
2013-11-28 16:03:05 +00:00
|
|
|
set_migrate_fn_field(L, -1, tactic_migrate);
|
2013-11-28 01:47:29 +00:00
|
|
|
lua_pushvalue(L, -1);
|
|
|
|
lua_setfield(L, -2, "__index");
|
|
|
|
setfuncs(L, tactic_m, 0);
|
|
|
|
|
2013-11-29 09:33:26 +00:00
|
|
|
SET_GLOBAL_FUN(tactic_pred, "is_tactic");
|
2013-12-06 04:00:20 +00:00
|
|
|
SET_GLOBAL_FUN(mk_trace_tactic, "trace_tac");
|
|
|
|
SET_GLOBAL_FUN(mk_id_tactic, "id_tac");
|
|
|
|
SET_GLOBAL_FUN(mk_now_tactic, "now_tac");
|
|
|
|
SET_GLOBAL_FUN(mk_fail_tactic, "fail_tac");
|
|
|
|
SET_GLOBAL_FUN(mk_trace_state_tactic, "show_tac");
|
|
|
|
SET_GLOBAL_FUN(mk_assumption_tactic, "assumption_tac");
|
2013-12-22 22:10:42 +00:00
|
|
|
SET_GLOBAL_FUN(mk_trivial_tactic, "trivial_tac");
|
2013-12-06 04:00:20 +00:00
|
|
|
SET_GLOBAL_FUN(mk_unfold_tactic, "unfold_tac");
|
|
|
|
SET_GLOBAL_FUN(mk_beta_tactic, "beta_tac");
|
2013-12-22 22:10:42 +00:00
|
|
|
SET_GLOBAL_FUN(mk_normalize_tactic, "normalize_tac");
|
|
|
|
SET_GLOBAL_FUN(mk_eval_tactic, "eval_tac");
|
2013-11-29 09:33:26 +00:00
|
|
|
SET_GLOBAL_FUN(mk_lua_tactic01, "tactic");
|
|
|
|
|
2013-11-29 01:57:24 +00:00
|
|
|
// HOL-like tactic names
|
2013-11-29 06:11:07 +00:00
|
|
|
SET_GLOBAL_FUN(nary_tactic<then>, "THEN");
|
|
|
|
SET_GLOBAL_FUN(nary_tactic<orelse>, "ORELSE");
|
|
|
|
SET_GLOBAL_FUN(nary_tactic<interleave>, "INTERLEAVE");
|
|
|
|
SET_GLOBAL_FUN(nary_tactic<append>, "APPEND");
|
|
|
|
SET_GLOBAL_FUN(nary_tactic<par>, "PAR");
|
|
|
|
SET_GLOBAL_FUN(tactic_repeat, "REPEAT");
|
|
|
|
SET_GLOBAL_FUN(tactic_repeat_at_most, "REPEAT_AT_MOST");
|
|
|
|
SET_GLOBAL_FUN(tactic_repeat1, "REPEAT1");
|
|
|
|
SET_GLOBAL_FUN(mk_lua_cond_tactic, "COND");
|
|
|
|
SET_GLOBAL_FUN(mk_lua_when_tactic, "WHEN");
|
|
|
|
SET_GLOBAL_FUN(tactic_try, "TRY");
|
|
|
|
SET_GLOBAL_FUN(tactic_try_for, "TRY_FOR");
|
|
|
|
SET_GLOBAL_FUN(tactic_take, "TAKE");
|
|
|
|
SET_GLOBAL_FUN(tactic_using_params, "USING");
|
|
|
|
SET_GLOBAL_FUN(tactic_using_params, "USING_PARAMS");
|
|
|
|
SET_GLOBAL_FUN(tactic_determ, "DETERM");
|
2013-11-30 19:28:10 +00:00
|
|
|
SET_GLOBAL_FUN(tactic_focus, "FOCUS");
|
2013-11-28 01:47:29 +00:00
|
|
|
}
|
2013-11-21 18:44:53 +00:00
|
|
|
}
|