max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library): add helper methods

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-29 08:31:33 -07:00
parent b317d4bc58
commit 78f81034c6
7 changed files with 35 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/local_context.cpp
View file

@ -144,6 +144,11 @@ optional<local_decl> 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<void(local_decl const &)> const & fn) const {
m_idx2local_decl.for_each([&](unsigned, local_decl const & d) { fn(d); });
}

5
src/library/local_context.h
View file

@ -100,6 +100,11 @@ public:
optional<local_decl> 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. */

8
src/library/metavar_context.cpp
View file

@ -60,10 +60,14 @@ optional<metavar_decl> metavar_context::get_metavar_decl(expr const & e) const {
return optional<metavar_decl>();
}
optional<local_decl> metavar_context::get_hypothesis_of(expr const & mvar, name const & H) const {
optional<local_decl> metavar_context::get_local_decl(expr const & mvar, name const & n) const {
auto mdecl = get_metavar_decl(mvar);
if (!mdecl) return optional<local_decl>();
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) {

11
src/library/metavar_context.h
View file

@ -37,7 +37,16 @@ public:
optional<metavar_decl> get_metavar_decl(expr const & mvar) const;
optional<local_decl> 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<local_decl> 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));

2
src/library/tactic/cases_tactic.cpp
View file

@ -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;

8
src/library/tactic/induction_tactic.cpp
View file

@ -133,7 +133,7 @@ list<expr> 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<metavar_decl> g2 = mctx.get_metavar_decl(*mvar2);
@ -142,7 +142,7 @@ list<expr> 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<expr> induction(environment const & env, options const & opts, transparency
/* Save name of constructor parameters that have been introduced for new goal. */
buffer<expr> 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<expr> 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);
}

8
src/library/tactic/subst_tactic.cpp
View file

@ -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) {