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

refactor(library/blast): rename state::get ==> state::get_hypothesis_decl

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-09 14:52:21 -08:00
parent fb7a47cf2b
commit b59dd2305c
4 changed files with 17 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/assumption.cpp
View file

@ -19,7 +19,7 @@ optional<expr> assumption_action() {
if (!hidx) if (!hidx)
return none_expr(); return none_expr();
// TODO(Leo): cleanup // TODO(Leo): cleanup
hypothesis const * h = s.get(*hidx); hypothesis const * h = s.get_hypothesis_decl(*hidx);
if (h->get_value()) { if (h->get_value()) {
return some_expr(*h->get_value()); return some_expr(*h->get_value());
} else { } else {

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

@ -173,7 +173,7 @@ class blastenv {
virtual expr infer_local(expr const & e) const { virtual expr infer_local(expr const & e) const {
if (is_href(e)) { if (is_href(e)) {
state const & s = m_benv.m_curr_state; state const & s = m_benv.m_curr_state;
hypothesis const * h = s.get(e); hypothesis const * h = s.get_hypothesis_decl(e);
lean_assert(h); lean_assert(h);
return h->get_type(); return h->get_type();
} else { } else {
@ -500,7 +500,7 @@ class blastenv {
virtual expr visit_local(expr const & e) { virtual expr visit_local(expr const & e) {
// TODO(Leo): cleanup // TODO(Leo): cleanup
if (is_href(e)) { if (is_href(e)) {
hypothesis const * h = m_state.get(e); hypothesis const * h = m_state.get_hypothesis_decl(e);
if (auto r = h->get_value()) { if (auto r = h->get_value()) {
return visit(*r); return visit(*r);
} }
@ -786,7 +786,7 @@ public:
virtual expr infer_local(expr const & e) const { virtual expr infer_local(expr const & e) const {
state const & s = curr_state(); state const & s = curr_state();
if (is_href(e)) { if (is_href(e)) {
hypothesis const * h = s.get(e); hypothesis const * h = s.get_hypothesis_decl(e);
lean_assert(h); lean_assert(h);
return h->get_type(); return h->get_type();
} else { } else {

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

@ -120,7 +120,7 @@ goal state::to_goal() const {
get_sorted_hypotheses(hidxs); get_sorted_hypotheses(hidxs);
buffer<expr> hyps; buffer<expr> hyps;
for (unsigned hidx : hidxs) { for (unsigned hidx : hidxs) {
hypothesis const * h = get(hidx); hypothesis const * h = get_hypothesis_decl(hidx);
lean_assert(h); lean_assert(h);
// after we add support for let-decls in goals, we must convert back h->get_value() if it is available // 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());
@ -360,8 +360,8 @@ struct hypothesis_dep_depth_lt {
hypothesis_dep_depth_lt(state const & s): m_state(s) {} hypothesis_dep_depth_lt(state const & s): m_state(s) {}
bool operator()(unsigned hidx1, unsigned hidx2) const { bool operator()(unsigned hidx1, unsigned hidx2) const {
hypothesis const * h1 = m_state.get(hidx1); hypothesis const * h1 = m_state.get_hypothesis_decl(hidx1);
hypothesis const * h2 = m_state.get(hidx2); hypothesis const * h2 = m_state.get_hypothesis_decl(hidx2);
return return
h1 && h2 && h1->get_dep_depth() < h2->get_dep_depth() && 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() && hidx1 < hidx2);
@ -397,7 +397,7 @@ void state::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) {
return false; return false;
} else if (is_href(l)) { } else if (is_href(l)) {
unsigned hidx_provider = href_index(l); unsigned hidx_provider = href_index(l);
hypothesis const * h_provider = get(hidx_provider); hypothesis const * h_provider = get_hypothesis_decl(hidx_provider);
lean_assert(h_provider); lean_assert(h_provider);
if (h_user.m_dep_depth <= h_provider->m_dep_depth) if (h_user.m_dep_depth <= h_provider->m_dep_depth)
h_user.m_dep_depth = h_provider->m_dep_depth + 1; h_user.m_dep_depth = h_provider->m_dep_depth + 1;
@ -512,7 +512,7 @@ struct expand_hrefs_fn : public replace_visitor {
virtual expr visit_local(expr const & e) { virtual expr visit_local(expr const & e) {
if (is_href(e) && std::find(m_hrefs.begin(), m_hrefs.end(), e) != m_hrefs.end()) { if (is_href(e) && std::find(m_hrefs.begin(), m_hrefs.end(), e) != m_hrefs.end()) {
hypothesis const * h = m_state.get(e); hypothesis const * h = m_state.get_hypothesis_decl(e);
if (h->get_value()) { if (h->get_value()) {
return visit(*h->get_value()); return visit(*h->get_value());
} }
@ -542,7 +542,7 @@ expr state::mk_binding(bool is_lambda, unsigned num, expr const * hrefs, expr co
--i; --i;
expr const & h = hrefs[i]; expr const & h = hrefs[i];
lean_assert(is_href(h)); lean_assert(is_href(h));
hypothesis const * hdecl = get(h); hypothesis const * hdecl = get_hypothesis_decl(h);
lean_assert(hdecl); lean_assert(hdecl);
expr t = abstract_locals(hdecl->get_type(), i, hrefs); expr t = abstract_locals(hdecl->get_type(), i, hrefs);
if (is_lambda) if (is_lambda)

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

@ -143,7 +143,6 @@ public:
state(); state();
bool is_uref_assigned(level const & l) const { bool is_uref_assigned(level const & l) const {
lean_assert(is_uref(l));
return m_uassignment.contains(uref_index(l)); return m_uassignment.contains(uref_index(l));
} }
@ -162,11 +161,12 @@ public:
level instantiate_urefs(level const & l); level instantiate_urefs(level const & l);
/** \brief Create a new metavariable using the given type and context. /** \brief Create a new metavariable using the given type and context.
\pre ctx must be a subset of the hypotheses in the main branch. */ \pre ctx must be a subset of the hypotheses in the current branch. */
expr mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type); expr mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type);
expr mk_metavar(hypothesis_idx_set const & ctx, expr const & type); expr mk_metavar(hypothesis_idx_set const & ctx, expr const & type);
/** \brief Create a new metavariable using the given type. /** \brief Create a new metavariable using the given type.
The context of this metavariable will be all assumption hypotheses occurring in the main branch. */ The context of this metavariable will be all assumption hypotheses occurring
in the current branch. */
expr mk_metavar(expr const & type); expr mk_metavar(expr const & type);
/** \brief Make sure the metavariable declaration context of mref1 is a /** \brief Make sure the metavariable declaration context of mref1 is a
@ -208,15 +208,13 @@ public:
\c hidx_provider. */ \c hidx_provider. */
bool hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const; bool hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const;
hypothesis const * get(unsigned hidx) const { return m_context.find(hidx); } hypothesis const * get_hypothesis_decl(unsigned hidx) const { return m_context.find(hidx); }
hypothesis const * get(expr const & h) const { hypothesis const * get_hypothesis_decl(expr const & h) const { return get_hypothesis_decl(href_index(h)); }
lean_assert(is_href(h));
return get(href_index(h));
}
void for_each_hypothesis(std::function<void(unsigned, hypothesis const &)> const & fn) const { m_context.for_each(fn); } void for_each_hypothesis(std::function<void(unsigned, hypothesis const &)> const & fn) const { m_context.for_each(fn); }
optional<unsigned> find_active_hypothesis(std::function<bool(unsigned, hypothesis const &)> const & fn) const { // NOLINT optional<unsigned> find_active_hypothesis(std::function<bool(unsigned, hypothesis const &)> const & fn) const { // NOLINT
return m_active.find_if([&](unsigned hidx) { return m_active.find_if([&](unsigned hidx) {
return fn(hidx, *get(hidx)); return fn(hidx, *get_hypothesis_decl(hidx));
}); });
} }