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

perf(kernel/metavar): improve occurs_expr and occurs performance

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-17 12:55:45 -07:00
parent 50e4c6f252
commit 10b880ce3b
4 changed files with 97 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

77
src/kernel/metavar.cpp
View file

@ -54,6 +54,7 @@ optional<level> substitution::get_level(name const & m) const {
void substitution::assign(name const & m, expr const & t, justification const & j) {
lean_assert(closed(t));
m_expr_subst.insert(m, t);
m_occs_map.erase(m);
if (!j.is_none())
m_expr_jsts.insert(m, j);
}
@ -241,21 +242,74 @@ expr substitution::instantiate_metavars_wo_jst(expr const & e, bool inst_local_t
return instantiate_metavars_fn(*this, false, inst_local_types)(e);
}
static name_set merge(name_set s1, name_set const & s2) {
s2.for_each([&](name const & n) { s1.insert(n); });
return s1;
}
bool substitution::occurs_expr_core(name const & m, expr const & e, name_set & visited) const {
static bool all_unassigned(substitution const & subst, name_set const & s) {
return !s.find_if([&](name const & m) { return subst.is_expr_assigned(m); });
}
name_set substitution::get_occs(name const & m, name_set & fresh) {
lean_assert(is_expr_assigned(m));
if (fresh.contains(m)) {
return *m_occs_map.find(m);
} else if (name_set const * it = m_occs_map.find(m)) {
name_set curr_occs = *it;
if (all_unassigned(*this, curr_occs)) {
return curr_occs;
}
name_set new_occs;
curr_occs.for_each([&](name const & n) {
if (is_expr_assigned(n)) {
new_occs = merge(new_occs, get_occs(n, fresh));
} else {
// we need to update
new_occs.insert(n);
}
});
m_occs_map.insert(m, new_occs);
fresh.insert(m);
return new_occs;
} else {
expr e = *get_expr(m);
name_set occs;
::lean::for_each(e, [&](expr const & e, unsigned) {
if (!has_expr_metavar(e)) return false;
if (is_local(e)) return false; // do not process type
if (is_metavar(e)) {
name const & n = mlocal_name(e);
if (is_expr_assigned(n)) {
occs = merge(occs, get_occs(n, fresh));
} else {
occs.insert(n);
}
return false;
}
return true;
});
m_occs_map.insert(m, occs);
fresh.insert(m);
return occs;
}
}
bool substitution::occurs_expr(name const & m, expr const & e) const {
if (!has_expr_metavar(e))
return false;
name_set fresh;
bool found = false;
for_each(e, [&](expr const & e, unsigned) {
if (found || !has_expr_metavar(e)) return false;
if (is_metavar(e)) {
name const & n = mlocal_name(e);
if (n == m)
found = true;
auto s = get_expr(e);
if (!s || visited.contains(n))
return false; // do not visit type
visited.insert(n);
if (s && occurs_expr_core(m, *s, visited))
if (is_expr_assigned(n)) {
if (get_occs(n, fresh).contains(m))
found = true;
} else if (n == m) {
found = true;
}
return false; // do not visit type
}
if (is_local(e)) return false; // do not visit type
@ -263,11 +317,4 @@ bool substitution::occurs_expr_core(name const & m, expr const & e, name_set & v
});
return found;
}
bool substitution::occurs_expr(name const & m, expr const & e) const {
if (!has_expr_metavar(e))
return false;
name_set visited;
return occurs_expr_core(m, e, visited);
}
}

31
src/kernel/metavar.h
View file

@ -15,21 +15,28 @@ Author: Leonardo de Moura
namespace lean {
class substitution {
typedef name_map<expr> expr_map;
typedef name_map<level> level_map;
typedef name_map<justification> jst_map;
typedef name_map<expr> expr_map;
typedef name_map<level> level_map;
typedef name_map<justification> jst_map;
typedef name_map<name_set> occs_map;
expr_map m_expr_subst;
level_map m_level_subst;
jst_map m_expr_jsts;
jst_map m_level_jsts;
/** \brief m_occs_map is mapping that contains entries ?m -> {?m_1, ..., ?m_k}
where ?m is an assigned metavariable in m_expr_subst, and ?m_i's are unassigned
metavariables occurring directly/indirectly in the term assigned to ?m.
This mapping is built (and updated) on demand, and is used to improve the performance of #occurs_expr.
*/
occs_map m_occs_map;
friend class instantiate_metavars_fn;
pair<level, justification> instantiate_metavars(level const & l, bool use_jst);
expr instantiate_metavars_wo_jst(expr const & e, bool inst_local_types);
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;
name_set get_occs(name const & m, name_set & fresh);
public:
substitution();
typedef optional<pair<expr, justification>> opt_expr_jst;
@ -43,8 +50,12 @@ public:
optional<expr> get_expr(name const & m) const;
optional<level> get_level(name const & m) const;
justification get_expr_jst(name const & m) const { if (auto it = m_expr_jsts.find(m)) return *it; else return justification(); }
justification get_level_jst(name const & m) const { if (auto it = m_level_jsts.find(m)) return *it; else return justification(); }
justification get_expr_jst(name const & m) const {
if (auto it = m_expr_jsts.find(m)) return *it; else return justification();
}
justification get_level_jst(name const & m) const {
if (auto it = m_level_jsts.find(m)) return *it; else return justification();
}
void assign(name const & m, expr const & t, justification const & j);
void assign(name const & m, expr const & t) { assign(m, t, justification()); }
@ -58,7 +69,8 @@ public:
pair<level, justification> instantiate_metavars(level const & l) { return instantiate_metavars(l, true); }
level instantiate(level const & l) { return instantiate_metavars(l, false).first; }
/** \brief Instantiate metavariables occurring in \c e, by default this method does not visit the types of local constants.
/** \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.
*/
pair<expr, justification> instantiate_metavars(expr const & e) { return instantiate_metavars_core(e, false); }
@ -82,7 +94,10 @@ public:
}
bool is_assigned(expr const & m) const { lean_assert(is_metavar(m)); return is_expr_assigned(mlocal_name(m)); }
opt_expr_jst get_assignment(expr const & m) const { lean_assert(is_metavar(m)); return get_expr_assignment(mlocal_name(m)); }
opt_expr_jst get_assignment(expr const & m) const {
lean_assert(is_metavar(m));
return get_expr_assignment(mlocal_name(m));
}
optional<expr> get_expr(expr const & m) const { lean_assert(is_metavar(m)); return get_expr(mlocal_name(m)); }
bool is_assigned(level const & m) const { lean_assert(is_meta(m)); return is_level_assigned(meta_id(m)); }

5
src/tests/kernel/metavar.cpp
View file

@ -99,10 +99,11 @@ static void tst2() {
expr g = Const("g");
expr a = Const("a");
s.assign(m1, mk_app(f, m2), mk_assumption_justification(1));
s.assign(m2, mk_app(g, a), mk_assumption_justification(2));
lean_assert(check_assumptions(s.get_assignment(m1)->second, {1}));
lean_assert(s.occurs(m1, mk_app(f, m1)));
lean_assert(!s.occurs(m1, mk_app(f, m1)));
lean_assert(s.occurs(m2, mk_app(f, m1)));
s.assign(m2, mk_app(g, a), mk_assumption_justification(2));
lean_assert(!s.occurs(m2, mk_app(f, m1)));
lean_assert(!s.occurs(m1, mk_app(f, m2)));
lean_assert(!s.occurs(m1, mk_app(f, a)));
lean_assert(!s.occurs(m3, mk_app(f, m1)));

11
tests/lua/subst1.lua
View file

@ -24,8 +24,9 @@ assert(s:get_expr("m") == a)
local m2 = mk_metavar("m2", Prop)
s:assign(m2, f(m))
print(s:get_expr("m2"))
assert(s:occurs(m, f(m2)))
assert(s:occurs_expr("m", f(m2)))
assert(s:is_expr_assigned("m"))
-- m is assigned, so it is does not occur in f(m2)
-- assert(s:occurs_expr("m", f(m2)))
print(s:get_level("u"))
print(s:instantiate(mk_sort(u)))
assert(s:instantiate(mk_sort(u)) == mk_sort(l))
@ -33,3 +34,9 @@ assert(s:get_assignment(m) == a)
assert(s:get_assignment(u) == l)
assert(s:get_expr_assignment("m") == a)
assert(s:get_level_assignment("u") == l)
local s = substitution()
local m2 = mk_metavar("m2", Prop)
s:assign(m2, f(m))
assert(not s:is_expr_assigned("m"))
assert(s:occurs_expr("m", f(m2)))