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

perf(library/unifier): delay the instantiation of metavariables occurring in the types of local constants

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-23 14:21:47 -07:00
parent 69d9c8b95d
commit 13fe28dd1c
6 changed files with 46 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/elaborator.cpp
View file

@ -539,8 +539,8 @@ public:
static expr instantiate_meta(expr const & meta, substitution & subst) {
buffer<expr> locals;
expr mvar = get_app_args(meta, locals);
mvar = update_mlocal(mvar, subst.instantiate(mlocal_type(mvar)));
for (auto & local : locals) local = subst.instantiate(local);
mvar = update_mlocal(mvar, subst.instantiate_all(mlocal_type(mvar)));
for (auto & local : locals) local = subst.instantiate_all(local);
return ::lean::mk_app(mvar, locals);
}

20
src/kernel/metavar.cpp
View file

@ -95,6 +95,7 @@ protected:
substitution & m_subst;
justification m_jst;
bool m_use_jst;
bool m_inst_local_types;
void save_jst(justification const & j) { m_jst = mk_composite1(m_jst, j); }
@ -117,6 +118,13 @@ protected:
return update_constant(c, visit_levels(const_levels(c)));
}
virtual expr visit_local(expr const & l) {
if (m_inst_local_types)
return replace_visitor::visit_local(l);
else
return l;
}
virtual expr visit_meta(expr const & m) {
name const & m_name = mlocal_name(m);
auto p1 = m_subst.get_expr_assignment(m_name);
@ -167,23 +175,23 @@ protected:
}
public:
instantiate_metavars_fn(substitution & s, bool use_jst):
m_subst(s), m_use_jst(use_jst) {}
instantiate_metavars_fn(substitution & s, bool use_jst, bool inst_local_types):
m_subst(s), m_use_jst(use_jst), m_inst_local_types(inst_local_types) {}
justification const & get_justification() const { return m_jst; }
};
std::pair<expr, justification> substitution::instantiate_metavars(expr const & e) {
std::pair<expr, justification> substitution::instantiate_metavars_core(expr const & e, bool inst_local_types) {
if (!has_metavar(e)) {
return mk_pair(e, justification());
} else {
instantiate_metavars_fn fn(*this, true);
instantiate_metavars_fn fn(*this, true, inst_local_types);
expr r = fn(e);
return mk_pair(r, fn.get_justification());
}
}
expr substitution::instantiate_metavars_wo_jst(expr const & e) {
return instantiate_metavars_fn(*this, false)(e);
expr substitution::instantiate_metavars_wo_jst(expr const & e, bool inst_local_types) {
return instantiate_metavars_fn(*this, false, inst_local_types)(e);
}

17
src/kernel/metavar.h
View file

@ -25,7 +25,8 @@ class substitution {
friend class instantiate_metavars_fn;
std::pair<level, justification> instantiate_metavars(level const & l, bool use_jst);
expr instantiate_metavars_wo_jst(expr const & e);
expr instantiate_metavars_wo_jst(expr const & e, bool inst_local_types);
std::pair<expr, justification> instantiate_metavars_core(expr const & e, bool inst_local_types);
bool occurs_expr_core(name const & m, expr const & e, name_set & visited) const;
public:
@ -53,9 +54,19 @@ public:
void assign(level const & m, level const & t, justification const & j) { assign(meta_id(m), t, j); }
void assign(level const & m, level const & t) { assign(m, t, justification ()); }
std::pair<expr, justification> instantiate_metavars(expr const & e);
std::pair<level, justification> instantiate_metavars(level const & l) { return instantiate_metavars(l, true); }
/** \brief Instantiate metavariables occurring in \c e, by default this method does not visit the types of local constants.
For substituting the metavariables occurring in local constants, use instantiate_metavars_all.
*/
std::pair<expr, justification> instantiate_metavars(expr const & e) { return instantiate_metavars_core(e, false); }
/** \brief \c see instantiate_metavars */
std::pair<expr, justification> instantiate_metavars_all(expr const & e) { return instantiate_metavars_core(e, true); }
/** \brief Similar to \c instantiate_metavars, but does not compute a justification for the substitutions. */
expr instantiate(expr const & e) { return instantiate_metavars_wo_jst(e, false); }
/** \brief Similar to instantiate, but also substitute metavariables occurring in the types of local constansts */
expr instantiate_all(expr const & e) { return instantiate_metavars_wo_jst(e, true); }
void forget_justifications() { m_expr_jsts = jst_map(); m_level_jsts = jst_map(); }
template<typename F>
@ -76,8 +87,6 @@ public:
opt_level_jst get_assignment(level const & m) const { lean_assert(is_meta(m)); return get_level_assignment(meta_id(m)); }
optional<level> get_level(level const & m) const { lean_assert(is_meta(m)); return get_level(meta_id(m)); }
expr instantiate(expr const & e) { return instantiate_metavars_wo_jst(e); }
/** \brief Return true iff the metavariable \c m occurrs (directly or indirectly) in \c e. */
bool occurs_expr(name const & m, expr const & e) const;
bool occurs(expr const & m, expr const & e) const { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); }

7
src/library/kernel_bindings.cpp
View file

@ -1690,6 +1690,12 @@ static int subst_instantiate(lua_State * L) {
return 2;
}
static int subst_instantiate_all(lua_State * L) {
auto r = to_substitution(L, 1).instantiate_metavars_all(to_expr(L, 2));
push_expr(L, r.first); push_justification(L, r.second);
return 2;
}
static int subst_for_each_expr(lua_State * L) {
substitution const & s = to_substitution(L, 1);
luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
@ -1731,6 +1737,7 @@ static const struct luaL_Reg substitution_m[] = {
{"get_level_assignment", safe_function<subst_get_level_assignment>},
{"get_assignment", safe_function<subst_get_assignment>},
{"instantiate", safe_function<subst_instantiate>},
{"instantiate_all", safe_function<subst_instantiate_all>},
{"for_each_expr", safe_function<subst_for_each_expr>},
{"for_each_level", safe_function<subst_for_each_level>},
{0, 0}

6
src/library/tactic/apply_tactic.cpp
View file

@ -124,7 +124,7 @@ proof_state_seq apply_tactic_core(environment const & env, io_state const & ios,
name_generator new_ngen(ngen);
type_checker tc(env, new_ngen.mk_child());
substitution new_subst = subst;
expr new_e = new_subst.instantiate(e);
expr new_e = new_subst.instantiate_all(e);
expr new_p = g.abstract(new_e);
check_has_no_local(new_p, _e, "apply");
new_subst.assign(g.get_name(), new_p);
@ -139,7 +139,7 @@ proof_state_seq apply_tactic_core(environment const & env, io_state const & ios,
unsigned i = metas.size();
while (i > 0) {
--i;
new_gs = cons(goal(metas[i], new_subst.instantiate(tc.infer(metas[i]))), new_gs);
new_gs = cons(goal(metas[i], new_subst.instantiate_all(tc.infer(metas[i]))), new_gs);
}
}
return proof_state(new_gs, new_subst, new_ngen);
@ -187,7 +187,7 @@ tactic apply_tactic(expr const & e, bool refresh_univ_mvars) {
if (refresh_univ_mvars) {
name_generator ngen = s.get_ngen();
substitution new_subst = s.get_subst();
expr new_e = refresh_univ_metavars(new_subst.instantiate(e), ngen);
expr new_e = refresh_univ_metavars(new_subst.instantiate_all(e), ngen);
proof_state new_s(s.get_goals(), new_subst, ngen);
return apply_tactic_core(env, ios, new_s, new_e, true, true);
} else {

9
src/library/unifier.cpp
View file

@ -48,13 +48,18 @@ bool is_simple_meta(expr const & e) {
return (bool)is_simple_meta(e, args); // NOLINT
}
/** \brief Return true iff \c locals contains \c local */
bool contains_local(expr const & local, buffer<expr> const & locals) {
return std::any_of(locals.begin(), locals.end(), [&](expr const & l) { return mlocal_name(local) == mlocal_name(l); });
}
// Return true if all local constants in \c e are in locals
bool context_check(expr const & e, buffer<expr> const & locals) {
bool failed = false;
for_each(e, [&](expr const & e, unsigned) {
if (failed)
return false;
if (is_local(e) && std::find(locals.begin(), locals.end(), e) == locals.end()) {
if (is_local(e) && !contains_local(e, locals)) {
failed = true;
return false;
}
@ -77,7 +82,7 @@ lbool occurs_context_check(substitution & s, expr const & e, expr const & m, buf
if (r == l_false) {
return false;
} else if (is_local(e)) {
if (std::find(locals.begin(), locals.end(), e) == locals.end()) {
if (!contains_local(e, locals)) {
// right-hand-side contains variable that is not in the scope
// of metavariable.
r = l_false;