diff --git a/src/library/blast/assumption.cpp b/src/library/blast/assumption.cpp index 1169d51b3..e19ae45c5 100644 --- a/src/library/blast/assumption.cpp +++ b/src/library/blast/assumption.cpp @@ -19,7 +19,7 @@ optional assumption_action() { if (!hidx) return none_expr(); // TODO(Leo): cleanup - hypothesis const * h = s.get(*hidx); + hypothesis const * h = s.get_hypothesis_decl(*hidx); if (h->get_value()) { return some_expr(*h->get_value()); } else { diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 6d187264b..fd67453d0 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -173,7 +173,7 @@ 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(e); + hypothesis const * h = s.get_hypothesis_decl(e); lean_assert(h); return h->get_type(); } else { @@ -500,7 +500,7 @@ class blastenv { virtual expr visit_local(expr const & e) { // TODO(Leo): cleanup 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()) { return visit(*r); } @@ -786,7 +786,7 @@ public: virtual expr infer_local(expr const & e) const { state const & s = curr_state(); if (is_href(e)) { - hypothesis const * h = s.get(e); + hypothesis const * h = s.get_hypothesis_decl(e); lean_assert(h); return h->get_type(); } else { diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index fd770b2e4..ec4626a09 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -120,7 +120,7 @@ goal state::to_goal() const { get_sorted_hypotheses(hidxs); buffer hyps; for (unsigned hidx : hidxs) { - hypothesis const * h = get(hidx); + hypothesis const * h = get_hypothesis_decl(hidx); lean_assert(h); // 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()); @@ -360,8 +360,8 @@ 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(hidx1); - hypothesis const * h2 = m_state.get(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); @@ -397,7 +397,7 @@ 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(hidx_provider); + 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; @@ -512,7 +512,7 @@ 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(e); + hypothesis const * h = m_state.get_hypothesis_decl(e); if (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; expr const & h = hrefs[i]; lean_assert(is_href(h)); - hypothesis const * hdecl = get(h); + hypothesis const * hdecl = get_hypothesis_decl(h); lean_assert(hdecl); expr t = abstract_locals(hdecl->get_type(), i, hrefs); if (is_lambda) diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 2a4021abe..3a6f18314 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -143,7 +143,6 @@ public: state(); bool is_uref_assigned(level const & l) const { - lean_assert(is_uref(l)); return m_uassignment.contains(uref_index(l)); } @@ -162,11 +161,12 @@ public: level instantiate_urefs(level const & l); /** \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_set const & ctx, expr const & 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); /** \brief Make sure the metavariable declaration context of mref1 is a @@ -208,15 +208,13 @@ public: \c hidx_provider. */ 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(expr const & h) const { - lean_assert(is_href(h)); - return get(href_index(h)); - } + hypothesis const * get_hypothesis_decl(unsigned hidx) const { return m_context.find(hidx); } + hypothesis const * get_hypothesis_decl(expr const & h) const { return get_hypothesis_decl(href_index(h)); } + void for_each_hypothesis(std::function const & fn) const { m_context.for_each(fn); } optional find_active_hypothesis(std::function const & fn) const { // NOLINT return m_active.find_if([&](unsigned hidx) { - return fn(hidx, *get(hidx)); + return fn(hidx, *get_hypothesis_decl(hidx)); }); }