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

refactor(library/blast): get_hypothesis_decl return a reference

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-18 18:20:02 -08:00
parent b61eb3ea0c
commit f8a20341cb
9 changed files with 85 additions and 104 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/blast/blast.cpp
View file

@ -150,9 +150,8 @@ class blastenv {
virtual expr infer_local(expr const & e) const {
if (is_href(e)) {
state const & s = m_benv.m_curr_state;
hypothesis const * h = s.get_hypothesis_decl(e);
lean_assert(h);
return h->get_type();
hypothesis const & h = s.get_hypothesis_decl(e);
return h.get_type();
} else {
return mlocal_type(e);
}
@ -789,9 +788,8 @@ public:
virtual expr infer_local(expr const & e) const {
state const & s = curr_state();
if (is_href(e)) {
hypothesis const * h = s.get_hypothesis_decl(e);
lean_assert(h);
return h->get_type();
hypothesis const & h = s.get_hypothesis_decl(e);
return h.get_type();
} else {
return mlocal_type(e);
}

13
src/library/blast/congruence_closure.cpp
View file

@ -238,10 +238,9 @@ void congruence_closure::add(hypothesis_idx hidx) {
clear_todo();
state & s = curr_state();
app_builder & b = get_app_builder();
hypothesis const * h = s.get_hypothesis_decl(hidx);
lean_assert(h);
hypothesis const & h = s.get_hypothesis_decl(hidx);
try {
expr const & type = h->get_type();
expr const & type = h.get_type();
expr p;
bool is_neg = is_not(type, p);
if (is_neg && !is_standard(env()))
@ -250,18 +249,18 @@ void congruence_closure::add(hypothesis_idx hidx) {
if (is_relation_app(p, R, lhs, rhs)) {
if (is_neg) {
internalize(get_iff_name(), p);
add_eqv(get_iff_name(), p, mk_false(), b.mk_iff_false_intro(h->get_self()));
add_eqv(get_iff_name(), p, mk_false(), b.mk_iff_false_intro(h.get_self()));
} else {
internalize(R, lhs);
internalize(R, rhs);
add_eqv(R, lhs, rhs, h->get_self());
add_eqv(R, lhs, rhs, h.get_self());
}
} else if (is_prop(p)) {
internalize(get_iff_name(), p);
if (is_neg) {
add_eqv(get_iff_name(), p, mk_false(), b.mk_iff_false_intro(h->get_self()));
add_eqv(get_iff_name(), p, mk_false(), b.mk_iff_false_intro(h.get_self()));
} else {
add_eqv(get_iff_name(), p, mk_true(), b.mk_iff_true_intro(h->get_self()));
add_eqv(get_iff_name(), p, mk_true(), b.mk_iff_true_intro(h.get_self()));
}
}
} catch (app_builder_exception &) {}

14
src/library/blast/no_confusion_action.cpp
View file

@ -36,9 +36,8 @@ struct no_confusion_proof_step_cell : public proof_step_cell {
}
state & s = curr_state();
app_builder & b = get_app_builder();
hypothesis const * h = s.get_hypothesis_decl(href_index(m_eq_href));
lean_assert(h);
expr type = h->get_type();
hypothesis const & h = s.get_hypothesis_decl(href_index(m_eq_href));
expr type = h.get_type();
expr lhs, rhs;
lean_verify(is_eq(type, lhs, rhs));
name nc_name(m_I_name, "no_confusion");
@ -54,9 +53,8 @@ action_result no_confusion_action(hypothesis_idx hidx) {
try {
state & s = curr_state();
app_builder & b = get_app_builder();
hypothesis const * h = s.get_hypothesis_decl(hidx);
lean_assert(h);
expr type = h->get_type();
hypothesis const & h = s.get_hypothesis_decl(hidx);
expr type = h.get_type();
expr lhs, rhs;
if (!is_eq(type, lhs, rhs))
return action_result::failed();
@ -90,14 +88,14 @@ action_result no_confusion_action(hypothesis_idx hidx) {
unsigned cnstr_arity = get_arity(env().get(*c1).get_type());
lean_assert(cnstr_arity >= num_params);
unsigned num_new_eqs = cnstr_arity - num_params;
s.push_proof_step(new no_confusion_proof_step_cell(const_name(I), target, h->get_self(), num_new_eqs));
s.push_proof_step(new no_confusion_proof_step_cell(const_name(I), target, h.get_self(), num_new_eqs));
s.set_target(binding_domain(nct));
s.del_hypothesis(hidx);
trace_action("no_confusion");
return action_result::new_branch();
} else {
name nc_name(const_name(I), "no_confusion");
expr pr = b.mk_app(nc_name, {target, lhs, rhs, h->get_self()});
expr pr = b.mk_app(nc_name, {target, lhs, rhs, h.get_self()});
trace_action("no_confusion");
return action_result::solved(pr);
}

6
src/library/blast/proof_expr.cpp
View file

@ -23,9 +23,9 @@ struct unfold_hypotheses_ge_fn : public replace_visitor {
virtual expr visit_local(expr const & e) {
if (is_href(e)) {
hypothesis const * h = m_state.get_hypothesis_decl(e);
if (h->get_proof_depth() >= m_depth && h->get_value()) {
return visit(*h->get_value());
hypothesis const & h = m_state.get_hypothesis_decl(e);
if (h.get_proof_depth() >= m_depth && h.get_value()) {
return visit(*h.get_value());
}
}
return replace_visitor::visit_local(e);

27
src/library/blast/recursor_action.cpp
View file

@ -35,14 +35,13 @@ static recursor_branch_extension & get_extension() {
optional<name> is_recursor_action_target(hypothesis_idx hidx) {
state & s = curr_state();
hypothesis const * h = s.get_hypothesis_decl(hidx);
lean_assert(h);
expr const & type = h->get_type();
hypothesis const & h = s.get_hypothesis_decl(hidx);
expr const & type = h.get_type();
if (!is_app(type) && !is_constant(type))
return optional<name>();
if (is_relation_app(type))
return optional<name>(); // we don't apply recursors to equivalence relations: =, ~, <->, etc.
if (!h->is_assumption())
if (!h.is_assumption())
return optional<name>(); // we only consider assumptions
if (get_type_context().is_class(type)) {
// we don't eliminate type classes instances
@ -139,9 +138,8 @@ struct recursor_proof_step_cell : public proof_step_cell {
action_result recursor_action(hypothesis_idx hidx, name const & R) {
state & s = curr_state();
hypothesis const * h = s.get_hypothesis_decl(hidx);
lean_assert(h);
expr const & type = h->get_type();
hypothesis const & h = s.get_hypothesis_decl(hidx);
expr const & type = h.get_type();
lean_assert(is_constant(get_app_fn(type)));
recursor_info rec_info = get_recursor_info(env(), R);
@ -242,7 +240,7 @@ action_result recursor_action(hypothesis_idx hidx, name const & R) {
expr motive = target;
if (rec_info.has_dep_elim())
motive = s.mk_lambda(h->get_self(), motive);
motive = s.mk_lambda(h.get_self(), motive);
motive = s.mk_lambda(indices, motive);
rec = mk_app(rec, motive);
@ -261,8 +259,8 @@ action_result recursor_action(hypothesis_idx hidx, name const & R) {
return action_result::failed(); // ill-formed type
curr_pos++;
}
rec = mk_app(rec, h->get_self());
rec_type = relaxed_whnf(instantiate(binding_body(rec_type), h->get_self()));
rec = mk_app(rec, h.get_self());
rec_type = relaxed_whnf(instantiate(binding_body(rec_type), h.get_self()));
consumed_major = true;
curr_pos++;
} else {
@ -298,9 +296,8 @@ action_result recursor_action(hypothesis_idx hidx, name const & R) {
action_result recursor_action(hypothesis_idx hidx) {
state & s = curr_state();
hypothesis const * h = s.get_hypothesis_decl(hidx);
lean_assert(h);
expr const & type = h->get_type();
hypothesis const & h = s.get_hypothesis_decl(hidx);
expr const & type = h.get_type();
expr const & I = get_app_fn(type);
if (!is_constant(I))
return action_result::failed();
@ -347,8 +344,8 @@ action_result recursor_action() {
if (ext.m_rec_queue.empty())
return action_result::failed();
unsigned hidx = ext.m_rec_queue.erase_min();
hypothesis const * h_decl = curr_state().get_hypothesis_decl(hidx);
if (h_decl->is_dead())
hypothesis const & h_decl = curr_state().get_hypothesis_decl(hidx);
if (h_decl.is_dead())
continue;
if (optional<name> R = is_recursor_action_target(hidx)) {
Try(recursor_action(hidx, *R));

35
src/library/blast/simple_actions.cpp
View file

@ -16,11 +16,10 @@ action_result assumption_action() {
state const & s = curr_state();
expr const & target = s.get_target();
for (hypothesis_idx hidx : s.get_head_related()) {
hypothesis const * h = s.get_hypothesis_decl(hidx);
lean_assert(h);
if (is_def_eq(h->get_type(), target)) {
hypothesis const & h = s.get_hypothesis_decl(hidx);
if (is_def_eq(h.get_type(), target)) {
trace_action("assumption");
return action_result(h->get_self());
return action_result(h.get_self());
}
}
return action_result::failed();
@ -45,18 +44,17 @@ static optional<expr> try_not_refl_relation(hypothesis const & h) {
action_result assumption_contradiction_actions(hypothesis_idx hidx) {
state const & s = curr_state();
app_builder & b = get_app_builder();
hypothesis const * h = s.get_hypothesis_decl(hidx);
lean_assert(h);
expr const & type = h->get_type();
hypothesis const & h = s.get_hypothesis_decl(hidx);
expr const & type = h.get_type();
if (blast::is_false(type)) {
trace_action("contradiction");
return action_result(b.mk_false_rec(s.get_target(), h->get_self()));
return action_result(b.mk_false_rec(s.get_target(), h.get_self()));
}
if (is_def_eq(type, s.get_target())) {
trace_action("assumption");
return action_result(h->get_self());
return action_result(h.get_self());
}
if (auto pr = try_not_refl_relation(*h)) {
if (auto pr = try_not_refl_relation(h)) {
trace_action("contradiction");
return action_result(*pr);
}
@ -64,18 +62,18 @@ action_result assumption_contradiction_actions(hypothesis_idx hidx) {
bool is_neg1 = is_not(type, p1);
/* try to find complement */
for (hypothesis_idx hidx2 : s.get_head_related(hidx)) {
hypothesis const * h2 = s.get_hypothesis_decl(hidx2);
expr type2 = h2->get_type();
hypothesis const & h2 = s.get_hypothesis_decl(hidx2);
expr type2 = h2.get_type();
expr p2 = type2;
bool is_neg2 = is_not(type2, p2);
if (is_neg1 != is_neg2) {
if (is_def_eq(p1, p2)) {
trace_action("contradiction");
if (is_neg1) {
return action_result(b.mk_app(get_absurd_name(), {s.get_target(), h2->get_self(), h->get_self()}));
return action_result(b.mk_app(get_absurd_name(), {s.get_target(), h2.get_self(), h.get_self()}));
} else {
lean_assert(is_neg2);
return action_result(b.mk_app(get_absurd_name(), {s.get_target(), h->get_self(), h2->get_self()}));
return action_result(b.mk_app(get_absurd_name(), {s.get_target(), h.get_self(), h2.get_self()}));
}
}
}
@ -112,9 +110,8 @@ action_result trivial_action() {
bool discard(hypothesis_idx hidx) {
state s = curr_state();
hypothesis const * h = s.get_hypothesis_decl(hidx);
lean_assert(h);
expr type = h->get_type();
hypothesis const & h = s.get_hypothesis_decl(hidx);
expr type = h.get_type();
// We only discard a hypothesis if it doesn't have dependencies.
if (s.has_target_forward_deps(hidx))
return false;
@ -132,8 +129,8 @@ bool discard(hypothesis_idx hidx) {
for (hypothesis_idx hidx2 : s.get_head_related(hidx)) {
if (hidx == hidx2)
continue;
hypothesis const * h2 = s.get_hypothesis_decl(hidx2);
expr type2 = h2->get_type();
hypothesis const & h2 = s.get_hypothesis_decl(hidx2);
expr type2 = h2.get_type();
if (is_def_eq(type, type2))
return true;
}

62
src/library/blast/state.cpp
View file

@ -208,10 +208,9 @@ goal state::to_goal() const {
get_sorted_hypotheses(hidxs);
buffer<expr> hyps;
for (unsigned hidx : hidxs) {
hypothesis const * h = get_hypothesis_decl(hidx);
lean_assert(h);
hypothesis const & h = get_hypothesis_decl(hidx);
// after we add support for let-decls in goals, we must convert back h->get_value() if it is available
expr new_h = lean::mk_local(name(H, hidx), h->get_name(), convert(h->get_type()), binder_info());
expr new_h = lean::mk_local(name(H, hidx), h.get_name(), convert(h.get_type()), binder_info());
hidx2local.insert(hidx, new_h);
hyps.push_back(new_h);
}
@ -227,7 +226,7 @@ void state::display_active(output_channel & out) const {
bool first = true;
m_branch.m_active.for_each([&](hypothesis_idx hidx) {
if (first) first = false; else out << ", ";
out << get_hypothesis_decl(hidx)->get_name();
out << get_hypothesis_decl(hidx).get_name();
});
out << "}\n";
}
@ -455,11 +454,11 @@ struct hypothesis_dep_depth_lt {
hypothesis_dep_depth_lt(state const & s): m_state(s) {}
bool operator()(unsigned hidx1, unsigned hidx2) const {
hypothesis const * h1 = m_state.get_hypothesis_decl(hidx1);
hypothesis const * h2 = m_state.get_hypothesis_decl(hidx2);
hypothesis const & h1 = m_state.get_hypothesis_decl(hidx1);
hypothesis const & h2 = m_state.get_hypothesis_decl(hidx2);
return
h1 && h2 && h1->get_dep_depth() < h2->get_dep_depth() &&
(h1->get_dep_depth() == h2->get_dep_depth() && hidx1 < hidx2);
h1.get_dep_depth() < h2.get_dep_depth() &&
(h1.get_dep_depth() == h2.get_dep_depth() && hidx1 < hidx2);
}
};
@ -481,7 +480,7 @@ void state::sort_hypotheses(hypothesis_idx_buffer_set & r) const {
void state::to_hrefs(hypothesis_idx_buffer const & hidxs, buffer<expr> & r) const {
for (hypothesis_idx hidx : hidxs)
r.push_back(get_hypothesis_decl(hidx)->get_self());
r.push_back(get_hypothesis_decl(hidx).get_self());
}
void state::add_forward_dep(unsigned hidx_user, unsigned hidx_provider) {
@ -516,10 +515,9 @@ void state::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) {
return false;
} else if (is_href(l)) {
unsigned hidx_provider = href_index(l);
hypothesis const * h_provider = get_hypothesis_decl(hidx_provider);
lean_assert(h_provider);
if (h_user.m_dep_depth <= h_provider->m_dep_depth)
h_user.m_dep_depth = h_provider->m_dep_depth + 1;
hypothesis const & h_provider = get_hypothesis_decl(hidx_provider);
if (h_user.m_dep_depth <= h_provider.m_dep_depth)
h_user.m_dep_depth = h_provider.m_dep_depth + 1;
if (!h_user.m_deps.contains(hidx_provider)) {
h_user.m_deps.insert(hidx_provider);
add_forward_dep(hidx_user, hidx_provider);
@ -578,7 +576,7 @@ expr state::mk_hypothesis(expr const & type) {
void state::del_hypotheses(buffer<hypothesis_idx> const & to_delete, hypothesis_idx_set const & to_delete_set) {
for (hypothesis_idx h : to_delete) {
hypothesis h_decl = *get_hypothesis_decl(h);
hypothesis h_decl = get_hypothesis_decl(h);
if (m_branch.m_active.contains(h)) {
m_branch.m_active.erase(h);
remove_from_indices(h_decl, h);
@ -677,10 +675,9 @@ list<hypothesis_idx> state::get_occurrences_of(head_index const & h) const {
}
list<hypothesis_idx> state::get_head_related(hypothesis_idx hidx) const {
hypothesis const * h = get_hypothesis_decl(hidx);
lean_assert(h);
hypothesis const & h = get_hypothesis_decl(hidx);
/* update m_head_to_hyps */
if (auto i = to_head_index(*h))
if (auto i = to_head_index(h))
return get_occurrences_of(*i);
else
return list<hypothesis_idx>();
@ -715,9 +712,8 @@ branch_extension & state::get_extension(unsigned extid) {
lean_assert(ext->get_rc() == 1);
ext->initialized();
m_branch.m_active.for_each([&](hypothesis_idx hidx) {
hypothesis const * h = get_hypothesis_decl(hidx);
lean_assert(h);
ext->hypothesis_activated(*h, hidx);
hypothesis const & h = get_hypothesis_decl(hidx);
ext->hypothesis_activated(h, hidx);
});
return *ext;
} else {
@ -728,15 +724,14 @@ branch_extension & state::get_extension(unsigned extid) {
}
void state::update_indices(hypothesis_idx hidx) {
hypothesis const * h = get_hypothesis_decl(hidx);
lean_assert(h);
hypothesis const & h = get_hypothesis_decl(hidx);
/* update m_head_to_hyps */
if (auto i = to_head_index(*h))
if (auto i = to_head_index(h))
m_branch.m_head_to_hyps.insert(*i, hidx);
unsigned n = get_extension_manager().get_num_extensions();
for (unsigned i = 0; i < n; i++) {
branch_extension * ext = get_extension_core(i);
if (ext) ext->hypothesis_activated(*h, hidx);
if (ext) ext->hypothesis_activated(h, hidx);
}
/* TODO(Leo): update congruence closure indices */
}
@ -756,8 +751,8 @@ optional<unsigned> state::activate_hypothesis() {
if (m_branch.m_todo_queue.empty())
return optional<unsigned>();
unsigned hidx = m_branch.m_todo_queue.erase_min();
hypothesis const * h_decl = get_hypothesis_decl(hidx);
if (!h_decl->is_dead()) {
hypothesis const & h_decl = get_hypothesis_decl(hidx);
if (!h_decl.is_dead()) {
m_branch.m_active.insert(hidx);
update_indices(hidx);
return optional<unsigned>(hidx);
@ -799,9 +794,9 @@ struct expand_hrefs_fn : public replace_visitor {
virtual expr visit_local(expr const & e) {
if (is_href(e) && std::find(m_hrefs.begin(), m_hrefs.end(), e) != m_hrefs.end()) {
hypothesis const * h = m_state.get_hypothesis_decl(e);
if (h->get_value()) {
return visit(*h->get_value());
hypothesis const & h = m_state.get_hypothesis_decl(e);
if (h.get_value()) {
return visit(*h.get_value());
}
}
return replace_visitor::visit_local(e);
@ -827,13 +822,12 @@ expr state::mk_binding(bool is_lambda, unsigned num, expr const * hrefs, expr co
--i;
expr const & h = hrefs[i];
lean_assert(is_href(h));
hypothesis const * hdecl = get_hypothesis_decl(h);
lean_assert(hdecl);
expr t = abstract_locals(hdecl->get_type(), i, hrefs);
hypothesis const & hdecl = get_hypothesis_decl(h);
expr t = abstract_locals(hdecl.get_type(), i, hrefs);
if (is_lambda)
r = ::lean::mk_lambda(hdecl->get_name(), t, r);
r = ::lean::mk_lambda(hdecl.get_name(), t, r);
else
r = ::lean::mk_pi(hdecl->get_name(), t, r);
r = ::lean::mk_pi(hdecl.get_name(), t, r);
}
return r;
}

6
src/library/blast/state.h
View file

@ -280,13 +280,13 @@ public:
\c hidx_provider. */
bool hidx_depends_on(hypothesis_idx hidx_user, hypothesis_idx hidx_provider) const;
hypothesis const * get_hypothesis_decl(hypothesis_idx hidx) const { return m_branch.m_hyp_decls.find(hidx); }
hypothesis const * get_hypothesis_decl(expr const & h) const { return get_hypothesis_decl(href_index(h)); }
hypothesis const & get_hypothesis_decl(hypothesis_idx hidx) const { auto h = m_branch.m_hyp_decls.find(hidx); lean_assert(h); return *h; }
hypothesis const & get_hypothesis_decl(expr const & h) const { return get_hypothesis_decl(href_index(h)); }
void for_each_hypothesis(std::function<void(hypothesis_idx, hypothesis const &)> const & fn) const { m_branch.m_hyp_decls.for_each(fn); }
optional<hypothesis_idx> find_active_hypothesis(std::function<bool(hypothesis_idx, hypothesis const &)> const & fn) const { // NOLINT
return m_branch.m_active.find_if([&](hypothesis_idx hidx) {
return fn(hidx, *get_hypothesis_decl(hidx));
return fn(hidx, get_hypothesis_decl(hidx));
});
}

16
src/library/blast/subst_action.cpp
View file

@ -46,9 +46,8 @@ bool subst_core(hypothesis_idx hidx) {
state & s = curr_state();
state saved = s;
app_builder & b = get_app_builder();
hypothesis const * h = s.get_hypothesis_decl(hidx);
lean_assert(h);
expr type = h->get_type();
hypothesis const & h = s.get_hypothesis_decl(hidx);
expr type = h.get_type();
expr lhs, rhs;
lean_verify(is_eq(type, lhs, rhs));
lean_assert(is_href(rhs));
@ -60,7 +59,7 @@ bool subst_core(hypothesis_idx hidx) {
s.collect_direct_forward_deps(hidx, to_revert);
unsigned num = revert(to_revert);
expr target = s.get_target();
expr new_target = abstract(target, h->get_self());
expr new_target = abstract(target, h.get_self());
bool dep = !closed(new_target);
bool skip = to_revert.empty();
if (dep) {
@ -72,7 +71,7 @@ bool subst_core(hypothesis_idx hidx) {
skip = false;
if (!skip) {
new_target = instantiate(new_target, lhs);
s.push_proof_step(new subst_proof_step_cell(target, h->get_self(), rhs, dep));
s.push_proof_step(new subst_proof_step_cell(target, h.get_self(), rhs, dep));
s.set_target(new_target);
intros_action(num);
}
@ -89,9 +88,8 @@ bool subst_core(hypothesis_idx hidx) {
action_result subst_action(hypothesis_idx hidx) {
state & s = curr_state();
app_builder & b = get_app_builder();
hypothesis const * h = s.get_hypothesis_decl(hidx);
lean_assert(h);
expr type = h->get_type();
hypothesis const & h = s.get_hypothesis_decl(hidx);
expr type = h.get_type();
expr lhs, rhs;
if (!is_eq(type, lhs, rhs))
return action_result::failed();
@ -106,7 +104,7 @@ action_result subst_action(hypothesis_idx hidx) {
state saved = s;
try {
expr new_eq = b.mk_eq(rhs, lhs);
expr new_pr = b.mk_eq_symm(h->get_self());
expr new_pr = b.mk_eq_symm(h.get_self());
expr new_href = s.mk_hypothesis(new_eq, new_pr);
if (subst_core(href_index(new_href))) {
return action_result::new_branch();