diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index d1e1375a9c..b469a7153c 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -144,6 +144,11 @@ optional local_context::get_local_decl(expr const & e) const { return get_local_decl(mlocal_name(e)); } +expr local_context::get_local(name const & n) const { + lean_assert(get_local_decl(n)); + return get_local_decl(n)->mk_ref(); +} + void local_context::for_each(std::function const & fn) const { m_idx2local_decl.for_each([&](unsigned, local_decl const & d) { fn(d); }); } diff --git a/src/library/local_context.h b/src/library/local_context.h index 6c565b72f1..6980d1c500 100644 --- a/src/library/local_context.h +++ b/src/library/local_context.h @@ -100,6 +100,11 @@ public: optional get_last_local_decl() const; + /** Return a local_decl_ref associated with the given name. + + \pre get_local_decl(n) */ + expr get_local(name const & n) const; + bool rename_user_name(name const & from, name const & to); /** \brief Execute fn for each local declaration created after \c d. */ diff --git a/src/library/metavar_context.cpp b/src/library/metavar_context.cpp index f3d19b254b..46a5f5101f 100644 --- a/src/library/metavar_context.cpp +++ b/src/library/metavar_context.cpp @@ -60,10 +60,14 @@ optional metavar_context::get_metavar_decl(expr const & e) const { return optional(); } -optional metavar_context::get_hypothesis_of(expr const & mvar, name const & H) const { +optional metavar_context::get_local_decl(expr const & mvar, name const & n) const { auto mdecl = get_metavar_decl(mvar); if (!mdecl) return optional(); - return mdecl->get_context().get_local_decl(H); + return mdecl->get_context().get_local_decl(n); +} + +expr metavar_context::get_local(expr const & mvar, name const & n) const { + return get_local_decl(mvar, n)->mk_ref(); } void metavar_context::assign(level const & u, level const & l) { diff --git a/src/library/metavar_context.h b/src/library/metavar_context.h index 963239f044..29fd2f6ee8 100644 --- a/src/library/metavar_context.h +++ b/src/library/metavar_context.h @@ -37,7 +37,16 @@ public: optional get_metavar_decl(expr const & mvar) const; - optional get_hypothesis_of(expr const & mvar, name const & H) const; + /** \brief Return the local_decl for `n` in the local context for the metavariable `mvar` + \pre is_metavar(mvar) */ + optional get_local_decl(expr const & mvar, name const & n) const; + + /** \brief Return the local_decl_ref for `n` in the local context for the metavariable `mvar` + + \pre is_metavar(mvar) + \pre get_metavar_decl(mvar) + \pre get_metavar_decl(mvar)->get_context().get_local_decl(n) */ + expr get_local(expr const & mvar, name const & n) const; bool is_assigned(level const & l) const { lean_assert(is_metavar_decl_ref(l)); diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 2c2153c437..c296d929cb 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -259,7 +259,7 @@ struct cases_tactic_fn { subst.erase(idx_name); idx_name = new_name; } - expr H_idx = m_mctx.get_hypothesis_of(mvar, idx_name)->mk_ref(); + expr H_idx = m_mctx.get_local(mvar, idx_name); mvar = clear(m_mctx, mvar, H_idx); } hsubstitution new_subst; diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index 7e9c2b4210..f7f25c0f8a 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -133,7 +133,7 @@ list induction(environment const & env, options const & opts, transparency local_context lctx = mctx.get_metavar_decl(*mvar2)->get_context(); /* store old index name -> new index name */ for (unsigned i = 0; i < indices.size(); i++) { - base_subst.insert(mlocal_name(indices[i]), lctx.get_local_decl(indices_H[i])->mk_ref()); + base_subst.insert(mlocal_name(indices[i]), lctx.get_local(indices_H[i])); } } optional g2 = mctx.get_metavar_decl(*mvar2); @@ -142,7 +142,7 @@ list induction(environment const & env, options const & opts, transparency local_context lctx2 = g2->get_context(); indices.clear(); /* update indices buffer */ for (unsigned i = 0; i < indices_H.size() - 1; i++) - indices.push_back(lctx2.get_local_decl(indices_H[i])->mk_ref()); + indices.push_back(lctx2.get_local(indices_H[i])); level g_lvl = get_level(ctx2, g2->get_type()); local_decl H2_decl = *lctx2.get_last_local_decl(); expr H2 = H2_decl.mk_ref(); @@ -252,7 +252,7 @@ list induction(environment const & env, options const & opts, transparency /* Save name of constructor parameters that have been introduced for new goal. */ buffer params; for (name const & n : param_names) - params.push_back(aux_M_lctx.get_local_decl(n)->mk_ref()); + params.push_back(aux_M_lctx.get_local(n)); params_buffer.push_back(to_list(params)); } if (slist) { @@ -260,7 +260,7 @@ list induction(environment const & env, options const & opts, transparency hsubstitution S = base_subst; lean_assert(extra_names.size() == nextra); for (unsigned i = indices.size() + 1, j = 0; i < to_revert.size(); i++, j++) { - S.insert(mlocal_name(to_revert[i]), aux_M_lctx.get_local_decl(extra_names[j])->mk_ref()); + S.insert(mlocal_name(to_revert[i]), aux_M_lctx.get_local(extra_names[j])); } subst_buffer.push_back(S); } diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index e7cf82dc6a..1b85b2e56d 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -59,8 +59,8 @@ expr subst(environment const & env, options const & opts, transparency_mode cons metavar_decl g2 = *mctx.get_metavar_decl(*mvar2); local_context lctx = g2.get_context(); expr type = g2.get_type(); - lhs = lctx.get_local_decl(lhsH2[0])->mk_ref(); - expr H2 = lctx.get_local_decl(lhsH2[1])->mk_ref(); + lhs = lctx.get_local(lhsH2[0]); + expr H2 = lctx.get_local(lhsH2[1]); bool depH2 = depends_on(type, H2); expr new_type = instantiate(abstract_local(type, lhs), rhs); type_context ctx2 = mk_type_context_for(env, opts, mctx, g2.get_context(), m); @@ -94,7 +94,7 @@ expr subst(environment const & env, options const & opts, transparency_mode cons for (unsigned i = 0; i < to_revert.size() - 2; i++) { lean_assert(check_hypothesis_in_context(mctx, mvar, mlocal_name(to_revert[i+2]))); lean_assert(check_hypothesis_in_context(mctx, *mvar6, new_Hnames[i])); - new_subst.insert(mlocal_name(to_revert[i+2]), lctx.get_local_decl(new_Hnames[i])->mk_ref()); + new_subst.insert(mlocal_name(to_revert[i+2]), lctx.get_local(new_Hnames[i])); } new_subst.insert(mlocal_name(init_lhs), apply(rhs, new_subst)); *subst = new_subst; @@ -108,7 +108,7 @@ vm_obj tactic_subst_core(name const & n, bool symm, tactic_state const & s) { try { metavar_context mctx = s.mctx(); expr mvar = head(s.goals()); - expr H = mctx.get_hypothesis_of(mvar, n)->mk_ref(); + expr H = mctx.get_local(mvar, n); expr new_mvar = subst(s.env(), s.get_options(), transparency_mode::Semireducible, mctx, mvar, H, symm, nullptr); return mk_tactic_success(set_mctx_goals(s, mctx, cons(new_mvar, tail(s.goals())))); } catch (exception & ex) {