diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index b25079536..f06dd2f3e 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -51,7 +51,7 @@ class context { state & m_state; // We map each metavariable to a metavariable application and the mref associated with it. name_map> & m_mvar2meta_mref; - name_map & m_local2lref; + name_map & m_local2href; expr visit_sort(expr const & e) { return blast::mk_sort(to_blast_level(sort_level(e))); @@ -129,12 +129,12 @@ class context { // Local has already been processed continue; } - auto lref = m_local2lref.find(mlocal_name(l)); - if (!lref) { - // One of the arguments is a local constant that is not in m_local2lref + auto href = m_local2href.find(mlocal_name(l)); + if (!href) { + // One of the arguments is a local constant that is not in m_local2href throw_unsupported_metavar_occ(e); } - ctx.push_back(lref_index(*lref)); + ctx.push_back(href_index(*href)); } unsigned prefix_sz = i; expr aux = e; @@ -152,7 +152,7 @@ class context { } virtual expr visit_local(expr const & e) { - if (auto r = m_local2lref.find(mlocal_name(e))) + if (auto r = m_local2href.find(mlocal_name(e))) return * r; else throw blast_exception("blast tactic failed, ill-formed input goal", e); @@ -179,8 +179,8 @@ class context { public: to_blast_expr_fn(environment const & env, state & s, - name_map> & mvar2meta_mref, name_map & local2lref): - m_tc(env), m_state(s), m_mvar2meta_mref(mvar2meta_mref), m_local2lref(local2lref) {} + name_map> & mvar2meta_mref, name_map & local2href): + m_tc(env), m_state(s), m_mvar2meta_mref(mvar2meta_mref), m_local2href(local2href) {} }; void init_mvar2mref(name_map> & m) { @@ -193,16 +193,16 @@ class context { state s; type_checker_ptr norm_tc = mk_type_checker(m_env, name_generator(*g_prefix), UnfoldReducible); name_map> mvar2meta_mref; - name_map local2lref; - to_blast_expr_fn to_blast_expr(m_env, s, mvar2meta_mref, local2lref); + name_map local2href; + to_blast_expr_fn to_blast_expr(m_env, s, mvar2meta_mref, local2href); buffer hs; g.get_hyps(hs); for (expr const & h : hs) { lean_assert(is_local(h)); expr type = normalize(*norm_tc, mlocal_type(h)); expr new_type = to_blast_expr(type); - expr lref = s.add_hypothesis(local_pp_name(h), new_type, none_expr(), some_expr(h)); - local2lref.insert(mlocal_name(h), lref); + expr href = s.add_hypothesis(local_pp_name(h), new_type, none_expr(), some_expr(h)); + local2href.insert(mlocal_name(h), href); } expr target = normalize(*norm_tc, g.get_type()); expr new_target = to_blast_expr(target); diff --git a/src/library/blast/branch.cpp b/src/library/blast/branch.cpp index c0e912964..df6f3c717 100644 --- a/src/library/blast/branch.cpp +++ b/src/library/blast/branch.cpp @@ -50,13 +50,13 @@ void branch::add_forward_dep(unsigned hidx_user, unsigned hidx_provider) { } void branch::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) { - if (!has_lref(e) && !has_mref(e)) + if (!has_href(e) && !has_mref(e)) return; // nothing to be done for_each(e, [&](expr const & l, unsigned) { - if (!has_lref(l) && !has_mref(l)) { + if (!has_href(l) && !has_mref(l)) { return false; - } else if (is_lref(l)) { - unsigned hidx_provider = lref_index(l); + } else if (is_href(l)) { + unsigned hidx_provider = href_index(l); hypothesis const * h_provider = get(hidx_provider); lean_assert(h_provider); if (h_user.m_depth <= h_provider->m_depth) @@ -91,7 +91,7 @@ expr branch::add_hypothesis(name const & n, expr const & type, optional co m_next++; add_deps(new_h, new_hidx); m_context.insert(new_hidx, new_h); - return blast::mk_lref(new_hidx); + return blast::mk_href(new_hidx); } static name * g_prefix = nullptr; @@ -111,12 +111,12 @@ bool branch::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const { void branch::set_target(expr const & t) { m_target = t; m_target_deps.clear(); - if (has_lref(t) || has_mref(t)) { + if (has_href(t) || has_mref(t)) { for_each(t, [&](expr const & e, unsigned) { - if (!has_lref(e) && !has_mref(e)) { + if (!has_href(e) && !has_mref(e)) { return false; - } else if (is_lref(e)) { - m_target_deps.insert(lref_index(e)); + } else if (is_href(e)) { + m_target_deps.insert(href_index(e)); return false; } else if (is_mref(e)) { m_mvar_idxs.insert(mref_index(e)); diff --git a/src/library/blast/branch.h b/src/library/blast/branch.h index 6160e2d04..1b70a014d 100644 --- a/src/library/blast/branch.h +++ b/src/library/blast/branch.h @@ -30,8 +30,8 @@ class branch { modified. A hypothesis is fixed when it occurs in the type of some metavariable. */ void fix_hypothesis(unsigned idx); void fix_hypothesis(expr const & e) { - lean_assert(is_lref(e)); - fix_hypothesis(lref_index(e)); + lean_assert(is_href(e)); + fix_hypothesis(href_index(e)); } void add_forward_dep(unsigned hidx_user, unsigned hidx_provider); @@ -50,8 +50,8 @@ public: hypothesis const * get(unsigned hidx) const { return m_context.find(hidx); } hypothesis const * get(expr const & h) const { - lean_assert(is_lref(h)); - return get(lref_index(h)); + lean_assert(is_href(h)); + return get(href_index(h)); } void for_each_hypothesis(std::function const & fn) const { m_context.for_each(fn); } /** \brief Store in \c r the hypotheses in this branch sorted by depth */ @@ -60,7 +60,7 @@ public: void set_target(expr const & t); expr const & get_target() const { return m_target; } /** \brief Return true iff the target depends on the given hypothesis */ - bool target_depends_on(expr const & h) const { return m_target_deps.contains(lref_index(h)); } + bool target_depends_on(expr const & h) const { return m_target_deps.contains(href_index(h)); } bool has_mvar(expr const & e) const { return m_mvar_idxs.contains(mref_index(e)); } }; diff --git a/src/library/blast/expr.cpp b/src/library/blast/expr.cpp index de66ecf3e..881af06ca 100644 --- a/src/library/blast/expr.cpp +++ b/src/library/blast/expr.cpp @@ -31,19 +31,19 @@ LEAN_THREAD_PTR(level_table, g_level_table); LEAN_THREAD_PTR(expr_table, g_expr_table); LEAN_THREAD_PTR(expr_array, g_var_array); LEAN_THREAD_PTR(expr_array, g_mref_array); -LEAN_THREAD_PTR(expr_array, g_lref_array); +LEAN_THREAD_PTR(expr_array, g_href_array); scope_hash_consing::scope_hash_consing() { m_level_table = g_level_table; m_expr_table = g_expr_table; m_var_array = g_var_array; m_mref_array = g_mref_array; - m_lref_array = g_lref_array; + m_href_array = g_href_array; g_level_table = new level_table(); g_expr_table = new expr_table(); g_var_array = new expr_array(); g_mref_array = new expr_array(); - g_lref_array = new expr_array(); + g_href_array = new expr_array(); g_level_table->insert(lean::mk_level_zero()); g_level_table->insert(lean::mk_level_one()); } @@ -53,12 +53,12 @@ scope_hash_consing::~scope_hash_consing() { delete g_expr_table; delete g_var_array; delete g_mref_array; - delete g_lref_array; + delete g_href_array; g_level_table = reinterpret_cast(m_level_table); g_expr_table = reinterpret_cast(m_expr_table); g_var_array = reinterpret_cast(m_var_array); g_mref_array = reinterpret_cast(m_mref_array); - g_lref_array = reinterpret_cast(m_lref_array); + g_href_array = reinterpret_cast(m_href_array); } #ifdef LEAN_DEBUG @@ -150,26 +150,26 @@ level update_max(level const & l, level const & new_lhs, level const & new_rhs) } static name * g_prefix = nullptr; -static expr * g_dummy_type = nullptr; // dummy type for lref/mref +static expr * g_dummy_type = nullptr; // dummy type for href/mref -static expr mk_lref_core(unsigned idx) { +static expr mk_href_core(unsigned idx) { return mk_local(name(*g_prefix, idx), *g_dummy_type); } -expr mk_lref(unsigned idx) { - lean_assert(g_lref_array); +expr mk_href(unsigned idx) { + lean_assert(g_href_array); lean_assert(g_expr_table); - while (g_lref_array->size() <= idx) { - unsigned j = g_lref_array->size(); - expr new_ref = mk_lref_core(j); - g_lref_array->push_back(new_ref); + while (g_href_array->size() <= idx) { + unsigned j = g_href_array->size(); + expr new_ref = mk_href_core(j); + g_href_array->push_back(new_ref); g_expr_table->insert(new_ref); } - lean_assert(idx < g_lref_array->size()); - return (*g_lref_array)[idx]; + lean_assert(idx < g_href_array->size()); + return (*g_href_array)[idx]; } -bool is_lref(expr const & e) { +bool is_href(expr const & e) { return is_local(e) && mlocal_type(e) == *g_dummy_type; } @@ -199,12 +199,12 @@ unsigned mref_index(expr const & e) { return mlocal_name(e).get_numeral(); } -unsigned lref_index(expr const & e) { - lean_assert(is_lref(e)); +unsigned href_index(expr const & e) { + lean_assert(is_href(e)); return mlocal_name(e).get_numeral(); } -bool has_lref(expr const & e) { +bool has_href(expr const & e) { return has_local(e); } @@ -332,7 +332,7 @@ class replace_rec_fn { lean_assert(is_mref(e)); return save_result(e, offset, e); case expr_kind::Local: - lean_assert(is_lref(e)); + lean_assert(is_href(e)); return save_result(e, offset, e); case expr_kind::App: { expr new_f = apply(app_fn(e), offset); @@ -558,18 +558,18 @@ expr instantiate_value_univ_params(declaration const & d, levels const & ls) { return r; } -expr abstract_lrefs(expr const & e, unsigned n, expr const * subst) { - if (!has_lref(e)) +expr abstract_hrefs(expr const & e, unsigned n, expr const * subst) { + if (!has_href(e)) return e; - lean_assert(std::all_of(subst, subst+n, [](expr const & e) { return closed(e) && is_lref(e); })); + lean_assert(std::all_of(subst, subst+n, [](expr const & e) { return closed(e) && is_href(e); })); return blast::replace(e, [=](expr const & m, unsigned offset) -> optional { - if (!has_lref(m)) - return some_expr(m); // skip: m does not contain lref's - if (is_lref(m)) { + if (!has_href(m)) + return some_expr(m); // skip: m does not contain href's + if (is_href(m)) { unsigned i = n; while (i > 0) { --i; - if (lref_index(subst[i]) == lref_index(m)) + if (href_index(subst[i]) == href_index(m)) return some_expr(blast::mk_var(offset + n - i - 1)); } return none_expr(); diff --git a/src/library/blast/expr.h b/src/library/blast/expr.h index 08f50bfdf..fa8340928 100644 --- a/src/library/blast/expr.h +++ b/src/library/blast/expr.h @@ -24,7 +24,7 @@ class scope_hash_consing { void * m_expr_table; void * m_var_array; void * m_mref_array; - void * m_lref_array; + void * m_href_array; public: scope_hash_consing(); ~scope_hash_consing(); @@ -40,9 +40,9 @@ level mk_global_univ(name const & n); level mk_meta_univ(name const & n); expr mk_var(unsigned idx); -// mk_lref and mk_mref are helper functions for creating local constants and meta-variables used in the blast tactic. +// mk_href and mk_mref are helper functions for creating hypotheses and meta-variables used in the blast tactic. // Remark: the local constants and metavariables manipulated by the blast tactic do **not** store their types. -expr mk_lref(unsigned idx); +expr mk_href(unsigned idx); expr mk_mref(unsigned idx); expr mk_sort(level const & l); expr mk_constant(name const & n, levels const & ls); @@ -67,12 +67,12 @@ inline expr mk_lambda(name const & n, expr const & t, expr const & e) { } expr mk_macro(macro_definition const & m, unsigned num, expr const * args); -bool is_lref(expr const & e); -unsigned lref_index(expr const & e); +bool is_href(expr const & e); +unsigned href_index(expr const & e); bool is_mref(expr const & e); unsigned mref_index(expr const & e); -/** \brief Return true iff \c e contain lref's */ -bool has_lref(expr const & e); +/** \brief Return true iff \c e contain href's */ +bool has_href(expr const & e); /** \brief Return true iff \c e contain mref's */ bool has_mref(expr const & e); @@ -104,7 +104,7 @@ expr instantiate_univ_params(expr const & e, level_param_names const & ps, leve expr instantiate_type_univ_params(declaration const & d, levels const & ls); expr instantiate_value_univ_params(declaration const & d, levels const & ls); -expr abstract_lrefs(expr const & e, unsigned n, expr const * s); +expr abstract_hrefs(expr const & e, unsigned n, expr const * s); void initialize_expr(); void finalize_expr(); diff --git a/src/library/blast/hypothesis.h b/src/library/blast/hypothesis.h index 28d339c5b..9a87d44ac 100644 --- a/src/library/blast/hypothesis.h +++ b/src/library/blast/hypothesis.h @@ -42,6 +42,6 @@ public: optional const & get_justification() const { return m_justification; } void mark_fixed() { m_fixed = true; } /** \brief Return true iff this hypothesis depends on \c h. */ - bool depends_on(expr const & h) const { return m_deps.contains(lref_index(h)); } + bool depends_on(expr const & h) const { return m_deps.contains(href_index(h)); } }; }} diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 6be392bae..146104866 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -18,10 +18,10 @@ expr state::mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type) { for (unsigned const & hidx : ctx) ctx_as_set.insert(hidx); for_each(type, [&](expr const & e, unsigned) { - if (!has_lref(e)) + if (!has_href(e)) return false; - if (is_lref(e)) { - lean_assert(ctx_as_set.contains(lref_index(e))); + if (is_href(e)) { + lean_assert(ctx_as_set.contains(href_index(e))); m_main.fix_hypothesis(e); return false; } @@ -45,8 +45,8 @@ goal state::to_goal(branch const & b) const { name M("M"); std::function convert = [&](expr const & e) { return lean::replace(e, [&](expr const & e) { - if (is_lref(e)) { - auto r = hidx2local.find(lref_index(e)); + if (is_href(e)) { + auto r = hidx2local.find(href_index(e)); lean_assert(r); return some_expr(*r); } else if (is_mref(e)) { @@ -103,9 +103,9 @@ void state::display(environment const & env, io_state const & ios) const { #ifdef LEAN_DEBUG bool state::check_deps(expr const & e, branch const & b, unsigned hidx, hypothesis const & h) const { for_each(e, [&](expr const & n, unsigned) { - if (is_lref(n)) { + if (is_href(n)) { lean_assert(h.depends_on(n)); - lean_assert(b.hidx_depends_on(hidx, lref_index(n))); + lean_assert(b.hidx_depends_on(hidx, href_index(n))); } else if (is_mref(n)) { // metavariable is in the set of used metavariables lean_assert(b.has_mvar(n)); @@ -126,7 +126,7 @@ bool state::check_invariant(branch const & b) const { lean_assert(check_deps(b, hidx, h)); }); for_each(b.get_target(), [&](expr const & n, unsigned) { - if (is_lref(n)) { + if (is_href(n)) { lean_assert(b.target_depends_on(n)); } else if (is_mref(n)) { // metavariable is in the set of used metavariables