max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library): encapsulate tactic's Lean implementation better

Browse source
This commit is contained in:
Sebastian Ullrich 2018-03-01 14:10:43 +01:00
parent 39270fd46f
commit e1fc2bdbea
7 changed files with 55 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/dsimplify.cpp
View file

@ -390,7 +390,7 @@ class tactic_dsimplify_fn : public dsimplify_core_fn {
m_s = *new_s;
m_ctx.set_mctx(m_s.mctx());
m_defeq_canonizer.set_state(m_s.dcs());
vm_obj p = cfield(r, 0);
vm_obj p = tactic::get_result_value(r);
m_a = cfield(p, 0);
vm_obj p1 = cfield(p, 1);
expr new_e = to_expr(cfield(p1, 0));

2
src/library/tactic/simplify.cpp
View file

@ -1140,7 +1140,7 @@ class vm_simplify_fn : public simplify_ext_core_fn {
m_s = *new_s;
m_ctx.set_mctx(m_s.mctx());
m_defeq_canonizer.set_state(m_s.dcs());
vm_obj t = cfield(r, 0);
vm_obj t = tactic::get_result_value(r);
/* t : A × expr × option expr × bool */
m_a = cfield(t, 0);
vm_obj t1 = cfield(t, 1);

12
src/library/tactic/smt/congruence_tactics.cpp
View file

@ -186,21 +186,21 @@ vm_obj cc_state_internalize(vm_obj const & ccs, vm_obj const & e, vm_obj const &
vm_obj cc_state_is_eqv(vm_obj const & ccs, vm_obj const & e1, vm_obj const & e2, vm_obj const & _s) {
cc_state_proc({
bool r = cc.is_eqv(to_expr(e1), to_expr(e2));
return tactic::mk_success(mk_vm_bool(r), s);
return tactic::mk_result(mk_vm_bool(r), s);
});
}
vm_obj cc_state_is_not_eqv(vm_obj const & ccs, vm_obj const & e1, vm_obj const & e2, vm_obj const & _s) {
cc_state_proc({
bool r = cc.is_not_eqv(to_expr(e1), to_expr(e2));
return tactic::mk_success(mk_vm_bool(r), s);
return tactic::mk_result(mk_vm_bool(r), s);
});
}
vm_obj cc_state_eqv_proof(vm_obj const & ccs, vm_obj const & e1, vm_obj const & e2, vm_obj const & _s) {
cc_state_proc({
if (optional<expr> r = cc.get_proof(to_expr(e1), to_expr(e2))) {
return tactic::mk_success(to_obj(*r), s);
return tactic::mk_result(to_obj(*r), s);
} else {
return tactic::mk_exception("cc_state.eqv_proof failed to build proof", s);
}
@ -210,7 +210,7 @@ vm_obj cc_state_eqv_proof(vm_obj const & ccs, vm_obj const & e1, vm_obj const &
vm_obj cc_state_proof_for(vm_obj const & ccs, vm_obj const & e, vm_obj const & _s) {
cc_state_proc({
if (optional<expr> r = cc.get_eq_proof(to_expr(e), mk_true())) {
return tactic::mk_success(to_obj(mk_of_eq_true(cc.ctx(), *r)), s);
return tactic::mk_result(to_obj(mk_of_eq_true(cc.ctx(), *r)), s);
} else {
return tactic::mk_exception("cc_state.get_proof_for failed to build proof", s);
}
@ -220,7 +220,7 @@ vm_obj cc_state_proof_for(vm_obj const & ccs, vm_obj const & e, vm_obj const & _
vm_obj cc_state_refutation_for(vm_obj const & ccs, vm_obj const & e, vm_obj const & _s) {
cc_state_proc({
if (optional<expr> r = cc.get_eq_proof(to_expr(e), mk_false())) {
return tactic::mk_success(to_obj(mk_not_of_eq_false(cc.ctx(), *r)), s);
return tactic::mk_result(to_obj(mk_not_of_eq_false(cc.ctx(), *r)), s);
} else {
return tactic::mk_exception("cc_state.get_refutation_for failed to build proof", s);
}
@ -230,7 +230,7 @@ vm_obj cc_state_refutation_for(vm_obj const & ccs, vm_obj const & e, vm_obj cons
vm_obj cc_state_proof_for_false(vm_obj const & ccs, vm_obj const & _s) {
cc_state_proc({
if (auto pr = cc.get_inconsistency_proof()) {
return tactic::mk_success(to_obj(*pr), s);
return tactic::mk_result(to_obj(*pr), s);
} else {
return tactic::mk_exception("cc_state.false_proof failed, state is not inconsistent", s);
}

24
src/library/tactic/smt/smt_state.cpp
View file

@ -141,12 +141,8 @@ vm_obj to_obj(smt_goal const & s) {
return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_smt_goal))) vm_smt_goal(s));
}
vm_obj tactic_result_to_smt_tactic_result(vm_obj const & r, vm_obj const & ss) {
return tactic::mk_result(mk_vm_pair(tactic::get_result_value(r), ss), tactic::get_result_state(r));
}
vm_obj mk_smt_tactic_success(vm_obj const & a, vm_obj const & ss, vm_obj const & ts) {
return mk_vm_constructor(0, mk_vm_pair(a, ss), ts);
return tactic::mk_result(mk_vm_pair(a, ss), ts);
}
vm_obj mk_smt_tactic_success(vm_obj const & ss, vm_obj const & ts) {
@ -157,6 +153,10 @@ vm_obj mk_smt_tactic_success(vm_obj const & ss, tactic_state const & ts) {
return mk_smt_tactic_success(ss, to_obj(ts));
}
vm_obj tactic_success_to_smt_tactic_success(vm_obj const & r, vm_obj const & ss) {
return mk_smt_tactic_success(tactic::get_result_value(r), ss, tactic::get_result_state(r));
}
/* Remove auxiliary definitions introduced by the equation compiler.
Reason: ematching will close the goal by instantiating them.
Then later, the equation compiler will fail to eliminate this application
@ -518,7 +518,7 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s
}
if (is_nil(ss)) {
/* There is no SMT state associated with any goal. */
return tactic_result_to_smt_tactic_result(r1, ss);
return tactic_success_to_smt_tactic_success(r1, ss);
}
/* We only handle the common cases:
1) goals is of the form (a_1, a_2, ..., a_m)
@ -538,17 +538,17 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s
vm_obj new_ts = tactic::get_result_state(r1);
if (is_eqp(tactic::to_state(ts), tactic::to_state(new_ts))) {
/* The tactic_state was not modified */
return tactic_result_to_smt_tactic_result(r1, ss);
return tactic_success_to_smt_tactic_success(r1, ss);
}
list<expr> goals = tactic::to_state(ts).goals();
list<expr> new_goals = tactic::to_state(new_ts).goals();
if (goals == new_goals) {
/* Set of goals did not change. */
return tactic_result_to_smt_tactic_result(r1, ss);
return tactic_success_to_smt_tactic_success(r1, ss);
}
if (!new_goals) {
/* There are no new goals */
return tactic_result_to_smt_tactic_result(r1, mk_vm_nil());
return tactic_success_to_smt_tactic_success(r1, mk_vm_nil());
}
if (!goals) {
return tactic::mk_exception("failed to lift tactic to smt_tactic, there were no goals to be solved", tactic::to_state(ts));
@ -557,12 +557,12 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s
/* Main goal was solved */
/* remove one SMT goal */
vm_obj new_ss = tail(ss);
return tactic_result_to_smt_tactic_result(r1, new_ss);
return tactic_success_to_smt_tactic_success(r1, new_ss);
}
metavar_context const & mctx = tactic::to_state(new_ts).mctx();
if (tail(new_goals) == tail(goals) && same_hyps(mctx, head(new_goals), head(goals))) {
/* The set of hypotheses in the main goal did not change */
return tactic_result_to_smt_tactic_result(r1, ss);
return tactic_success_to_smt_tactic_success(r1, ss);
}
vm_obj new_ss = ss;
while (true) {
@ -571,7 +571,7 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s
tactic::to_state(ts));
}
if (tail(new_goals) == tail(goals)) {
return tactic_result_to_smt_tactic_result(r1, new_ss);
return tactic_success_to_smt_tactic_success(r1, new_ss);
}
/* copy smt state */
new_ss = mk_vm_cons(head(new_ss), new_ss);

7
src/library/tactic/user_attribute.cpp
View file

@ -283,7 +283,7 @@ vm_obj user_attribute_get_cache_core(vm_obj const &, vm_obj const &, vm_obj cons
result = invoke(cache_handler, to_obj(to_list(instances)), to_obj(s0));
was_updated = get_vm_state().env_was_updated();
}
if (tactic::is_success(result)) {
if (tactic::is_result_success(result)) {
if (!was_updated) {
user_attr_cache::entry entry;
entry.m_env = env;
@ -291,15 +291,14 @@ vm_obj user_attribute_get_cache_core(vm_obj const &, vm_obj const &, vm_obj cons
entry.m_dep_fingerprints = map2<unsigned>(deps, [&](name const & n) {
return get_attribute(env, n).get_fingerprint(env);
});
entry.m_val = cfield(result, 0);
entry.m_val = tactic::get_result_value(result);
cache.m_cache.erase(attr.get_name());
cache.m_cache.insert(mk_pair(attr.get_name(), entry));
return tactic::mk_success(entry.m_val, s);
} else {
lean_trace("user_attributes_cache", tout() << "did not cache result for [" << attr.get_name() << "] "
"because VM environment has been updated with temporary declarations\n";);
vm_obj r = cfield(result, 0);
return tactic::mk_success(r, s);
return tactic::mk_success(tactic::get_result_value(result), s);
}
} else {
return result;

3
src/library/vm/interaction_state.h
View file

@ -39,6 +39,9 @@ struct interaction_monad {
static bool is_silent_exception(vm_obj const & ex);
static vm_obj mk_result(vm_obj const & a, vm_obj const & s);
static bool is_result_exception(vm_obj const & r);
static vm_obj get_exception_message(vm_obj const & r);
static vm_obj get_exception_pos(vm_obj const & r);
static vm_obj get_exception_state(vm_obj const & r);
static bool is_result_success(vm_obj const & r);
static vm_obj get_result_value(vm_obj const & r);
static vm_obj get_result_state(vm_obj const & r);

39
src/library/vm/interaction_state_imp.h
View file

@ -26,6 +26,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
#include "library/vm/vm_expr.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_pos_info.h"
#include "library/compiler/vm_compiler.h"
namespace lean {
@ -89,6 +90,24 @@ bool interaction_monad<State>::is_result_exception(vm_obj const & r) {
return is_constructor(r) && cidx(r) == 1;
}
template<typename State>
vm_obj interaction_monad<State>::get_exception_message(vm_obj const & r) {
lean_assert(is_result_exception(r));
return cfield(r, 0);
}
template<typename State>
vm_obj interaction_monad<State>::get_exception_pos(vm_obj const & r) {
lean_assert(is_result_exception(r));
return cfield(r, 1);
}
template<typename State>
vm_obj interaction_monad<State>::get_exception_state(vm_obj const & r) {
lean_assert(is_result_exception(r));
return cfield(r, 2);
}
template<typename State>
bool interaction_monad<State>::is_result_success(vm_obj const & r) {
return is_constructor(r) && cidx(r) == 0;
@ -113,7 +132,7 @@ vm_obj interaction_monad<State>::mk_success(vm_obj const & a, State const & s) {
template<typename State>
vm_obj interaction_monad<State>::mk_success(State const & s) {
return mk_success(mk_vm_unit(), s);
return mk_result(mk_vm_unit(), s);
}
template<typename State>
@ -133,8 +152,8 @@ vm_obj interaction_monad<State>::mk_exception(vm_obj const & fn, vm_obj const &
template<typename State>
vm_obj interaction_monad<State>::update_exception_state(vm_obj const & ex, State const & s) {
lean_assert(!is_success(ex));
return mk_vm_constructor(1, cfield(ex, 0), cfield(ex, 1), to_obj(s));
lean_assert(is_result_exception(ex));
return mk_exception(get_exception_message(ex), get_exception_pos(ex), s);
}
template<typename State>
@ -186,20 +205,20 @@ void interaction_monad<State>::report_exception(vm_state & S, vm_obj const & r)
template<typename State>
auto interaction_monad<State>::is_success(vm_obj const & r) -> optional<State> {
if (is_result_success(r))
return some(to_state(cfield(r, 1)));
return some(to_state(get_result_state(r)));
return {};
}
template<typename State>
auto interaction_monad<State>::is_exception(vm_state & S, vm_obj const & ex) -> optional<exception_info> {
if (is_result_exception(ex) && !is_none(cfield(ex, 0))) {
vm_obj fmt = S.invoke(get_some_value(cfield(ex, 0)), mk_vm_unit());
if (is_result_exception(ex) && !is_none(get_exception_message(ex))) {
vm_obj fmt = S.invoke(get_some_value(get_exception_message(ex)), mk_vm_unit());
optional<pos_info> p;
if (!is_none(cfield(ex, 1))) {
auto vm_p = get_some_value(cfield(ex, 1));
p = some(mk_pair(to_unsigned(cfield(vm_p, 0)), to_unsigned(cfield(vm_p, 1))));
if (!is_none(get_exception_pos(ex))) {
auto vm_p = get_some_value(get_exception_pos(ex));
p = some(to_pos_info(vm_p));
}
return optional<exception_info>(to_format(fmt), p, to_state(cfield(ex, 2)));
return optional<exception_info>(to_format(fmt), p, to_state(get_exception_state(ex)));
} else {
return {};
}