From 471bbd4040429019b958c109847bf2e02b34a25c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Oct 2013 11:02:19 -0700
Subject: [PATCH] refactor(kernel/metavar): combine several splay_trees (at
 metavar_env) into a single one

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/metavar.cpp | 43 +++++++++++++++++++++---------------------
 src/kernel/metavar.h   | 14 ++++++++------
 2 files changed, 30 insertions(+), 27 deletions(-)

diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index ed4aa90f0..4ff96a25e 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -88,9 +88,7 @@ static name g_unique_name = name::mk_internal_unique_name();
 void swap(metavar_env & a, metavar_env & b) {
     swap(a.m_name_generator,         b.m_name_generator);
     swap(a.m_substitution,           b.m_substitution);
-    swap(a.m_metavar_types,          b.m_metavar_types);
-    swap(a.m_metavar_contexts,       b.m_metavar_contexts);
-    swap(a.m_metavar_justifications, b.m_metavar_justifications);
+    swap(a.m_metavar_data,           b.m_metavar_data);
     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();
     name m = m_name_generator.next();
     expr r = ::lean::mk_metavar(m);
-    if (ctx)
-        m_metavar_contexts.insert(m, ctx);
-    if (type)
-        m_metavar_types.insert(m, type);
+    m_metavar_data.insert(m, data(type, ctx));
     return r;
 }
 
@@ -129,8 +124,9 @@ context metavar_env::get_context(expr 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);
-    return it ? *it : context();
+    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
+    lean_assert(it);
+    return it->m_context;
 }
 
 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) {
-    auto it = const_cast<metavar_env*>(this)->m_metavar_types.splay_find(m);
-    if (it) {
-        return *it;
+    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
+    lean_assert(it);
+    if (it->m_type) {
+        return it->m_type;
     } else {
         expr t = mk_metavar(get_context(m));
-        const_cast<metavar_env*>(this)->m_metavar_types.insert(m, t);
+        it->m_type = t;
         return t;
     }
 }
 
 bool metavar_env::has_type(name const & m) const {
-    auto it = const_cast<metavar_env*>(this)->m_metavar_types.splay_find(m);
-    return it;
+    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
+    lean_assert(it);
+    return it->m_type;
 }
 
 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));
 }
 
-
 justification metavar_env::get_justification(expr const & m) const {
     lean_assert(is_metavar(m));
     return get_justification(metavar_name(m));
 }
 
 justification metavar_env::get_justification(name const & m) const {
-    auto it = const_cast<metavar_env*>(this)->m_metavar_justifications.splay_find(m);
-    return it ? *it : justification();
+    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
+    lean_assert(it);
+    return it->m_justification;
 }
 
 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));
     inc_timestamp();
     m_substitution.assign(m, t);
-    if (j)
-        m_metavar_justifications.insert(m, j);
+    if (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) {
@@ -206,7 +207,7 @@ struct found_unassigned{};
 name metavar_env::find_unassigned_metavar() const {
     name r;
     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)) {
                     r = m;
                     throw found_unassigned();
diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
index 6ec65ab8b..671ddf938 100644
--- a/src/kernel/metavar.h
+++ b/src/kernel/metavar.h
@@ -99,15 +99,17 @@ void swap(substitution & s1, substitution & s2);
    4- Collecting constraints
 */
 class metavar_env {
-    typedef splay_map<name, expr, name_quick_cmp>          name2expr;
-    typedef splay_map<name, context, name_quick_cmp>       name2context;
-    typedef splay_map<name, justification, name_quick_cmp> name2justification;
+    struct data {
+        expr          m_type;          // type of the metavariable
+        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;
     substitution       m_substitution;
-    name2expr          m_metavar_types;
-    name2context       m_metavar_contexts;
-    name2justification m_metavar_justifications;
+    name2data          m_metavar_data;
     unsigned           m_timestamp;
 
     void inc_timestamp();