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

refactor(kernel/metavar): combine several splay_trees (at metavar_env) into a single one

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-25 11:02:19 -07:00
parent 5e34f410b3
commit 471bbd4040
2 changed files with 30 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/kernel/metavar.cpp
View file

@ -88,9 +88,7 @@ static name g_unique_name = name::mk_internal_unique_name();
void swap(metavar_env & a, metavar_env & b) { void swap(metavar_env & a, metavar_env & b) {
swap(a.m_name_generator, b.m_name_generator); swap(a.m_name_generator, b.m_name_generator);
swap(a.m_substitution, b.m_substitution); swap(a.m_substitution, b.m_substitution);
swap(a.m_metavar_types, b.m_metavar_types); swap(a.m_metavar_data, b.m_metavar_data);
swap(a.m_metavar_contexts, b.m_metavar_contexts);
swap(a.m_metavar_justifications, b.m_metavar_justifications);
std::swap(a.m_timestamp, b.m_timestamp); std::swap(a.m_timestamp, b.m_timestamp);
} }
@ -115,10 +113,7 @@ expr metavar_env::mk_metavar(context const & ctx, expr const & type) {
inc_timestamp(); inc_timestamp();
name m = m_name_generator.next(); name m = m_name_generator.next();
expr r = ::lean::mk_metavar(m); expr r = ::lean::mk_metavar(m);
if (ctx) m_metavar_data.insert(m, data(type, ctx));
m_metavar_contexts.insert(m, ctx);
if (type)
m_metavar_types.insert(m, type);
return r; return r;
} }
@ -129,8 +124,9 @@ context metavar_env::get_context(expr const & m) const {
} }
context metavar_env::get_context(name const & m) const { context metavar_env::get_context(name const & m) const {
auto it = const_cast<metavar_env*>(this)->m_metavar_contexts.splay_find(m); auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
return it ? *it : context(); lean_assert(it);
return it->m_context;
} }
expr metavar_env::get_type(expr const & m) { expr metavar_env::get_type(expr const & m) {
@ -148,19 +144,21 @@ expr metavar_env::get_type(expr const & m) {
} }
expr metavar_env::get_type(name const & m) { expr metavar_env::get_type(name const & m) {
auto it = const_cast<metavar_env*>(this)->m_metavar_types.splay_find(m); auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
if (it) { lean_assert(it);
return *it; if (it->m_type) {
return it->m_type;
} else { } else {
expr t = mk_metavar(get_context(m)); expr t = mk_metavar(get_context(m));
const_cast<metavar_env*>(this)->m_metavar_types.insert(m, t); it->m_type = t;
return t; return t;
} }
} }
bool metavar_env::has_type(name const & m) const { bool metavar_env::has_type(name const & m) const {
auto it = const_cast<metavar_env*>(this)->m_metavar_types.splay_find(m); auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
return it; lean_assert(it);
return it->m_type;
} }
bool metavar_env::has_type(expr const & m) const { bool metavar_env::has_type(expr const & m) const {
@ -168,15 +166,15 @@ bool metavar_env::has_type(expr const & m) const {
return has_type(metavar_name(m)); return has_type(metavar_name(m));
} }
justification metavar_env::get_justification(expr const & m) const { justification metavar_env::get_justification(expr const & m) const {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
return get_justification(metavar_name(m)); return get_justification(metavar_name(m));
} }
justification metavar_env::get_justification(name const & m) const { justification metavar_env::get_justification(name const & m) const {
auto it = const_cast<metavar_env*>(this)->m_metavar_justifications.splay_find(m); auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
return it ? *it : justification(); lean_assert(it);
return it->m_justification;
} }
bool metavar_env::is_assigned(name const & m) const { bool metavar_env::is_assigned(name const & m) const {
@ -192,8 +190,11 @@ void metavar_env::assign(name const & m, expr const & t, justification const & j
lean_assert(!is_assigned(m)); lean_assert(!is_assigned(m));
inc_timestamp(); inc_timestamp();
m_substitution.assign(m, t); m_substitution.assign(m, t);
if (j) if (j) {
m_metavar_justifications.insert(m, j); auto it = m_metavar_data.splay_find(m);
lean_assert(it);
it->m_justification = j;
}
} }
void metavar_env::assign(expr const & m, expr const & t, justification const & j) { void metavar_env::assign(expr const & m, expr const & t, justification const & j) {
@ -206,7 +207,7 @@ struct found_unassigned{};
name metavar_env::find_unassigned_metavar() const { name metavar_env::find_unassigned_metavar() const {
name r; name r;
try { try {
m_metavar_types.for_each([&](name const & m, expr const &) { m_metavar_data.for_each([&](name const & m, data const &) {
if (!m_substitution.is_assigned(m)) { if (!m_substitution.is_assigned(m)) {
r = m; r = m;
throw found_unassigned(); throw found_unassigned();

14
src/kernel/metavar.h
View file

@ -99,15 +99,17 @@ void swap(substitution & s1, substitution & s2);
4- Collecting constraints 4- Collecting constraints
*/ */
class metavar_env { class metavar_env {
typedef splay_map<name, expr, name_quick_cmp> name2expr; struct data {
typedef splay_map<name, context, name_quick_cmp> name2context; expr m_type; // type of the metavariable
typedef splay_map<name, justification, name_quick_cmp> name2justification; context m_context; // context where the metavariable was defined
justification m_justification; // justification for assigned metavariables.
data(expr const & t = expr(), context const & ctx = context()):m_type(t), m_context(ctx) {}
};
typedef splay_map<name, data, name_quick_cmp> name2data;
name_generator m_name_generator; name_generator m_name_generator;
substitution m_substitution; substitution m_substitution;
name2expr m_metavar_types; name2data m_metavar_data;
name2context m_metavar_contexts;
name2justification m_metavar_justifications;
unsigned m_timestamp; unsigned m_timestamp;
void inc_timestamp(); void inc_timestamp();