From a7b37d0e09b869fb0fbac2d9cbd6534a45bb9676 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Jan 2016 14:06:47 -0800
Subject: [PATCH] perf(library/type_context): cache type class resolution
 failures too

---
 src/library/type_context.cpp | 40 +++++++++++++++++-------------------
 src/library/type_context.h   | 29 +++++++++++++-------------
 2 files changed, 33 insertions(+), 36 deletions(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 8605a65da..f4e4a9583 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -1694,32 +1694,21 @@ void type_context::init_search(expr const & type) {
     m_ci_choices_ini_sz = m_ci_choices.size();
 }
 
-optional<expr> type_context::check_ci_cache(expr const & type) const {
-    if (m_ci_multiple_instances) {
+void type_context::cache_ci_result(expr const & type, optional<expr> const & inst) {
+    if (!m_ci_multiple_instances) {
         // We do not cache results when multiple instances have to be generated.
-        return none_expr();
+        m_ci_cache.insert(mk_pair(type, inst));
     }
-    auto it = m_ci_cache.find(type);
-    if (it != m_ci_cache.end())
-        return some_expr(it->second);
-    else
-        return none_expr();
-}
-
-void type_context::cache_ci_result(expr const & type, expr const & inst) {
-    if (m_ci_multiple_instances) {
-        // We do not cache results when multiple instances have to be generated.
-        return;
-    }
-    m_ci_cache.insert(mk_pair(type, inst));
 }
 
 optional<expr> type_context::ensure_no_meta(optional<expr> r) {
     while (true) {
-        if (!r)
+        if (!r) {
+            cache_ci_result(mlocal_type(m_ci_main_mvar), r);
             return none_expr();
+        }
         if (!has_expr_metavar_relaxed(*r)) {
-            cache_ci_result(mlocal_type(m_ci_main_mvar), *r);
+            cache_ci_result(mlocal_type(m_ci_main_mvar), r);
             return r;
         }
         r = next_solution();
@@ -1727,9 +1716,18 @@ optional<expr> type_context::ensure_no_meta(optional<expr> r) {
 }
 
 optional<expr> type_context::mk_class_instance_core(expr const & type) {
-    if (auto r = check_ci_cache(type)) {
-        lean_trace("class_instances", tout() << "cached instance for " << type << "\n" << *r << "\n";);
-        return r;
+    if (!m_ci_multiple_instances) {
+        /* We do not cache results when multiple instances have to be generated. */
+        auto it = m_ci_cache.find(type);
+        if (it != m_ci_cache.end()) {
+            /* instance/failure is already cached */
+            lean_trace("class_instances",
+                       if (it->second)
+                           tout() << "cached instance for " << type << "\n" << *(it->second) << "\n";
+                       else
+                           tout() << "cached failure for " << type << "\n";);
+            return it->second;
+        }
     }
     init_search(type);
     auto r = search();
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 23726e584..570a1d174 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -269,24 +269,24 @@ class type_context {
         void commit() { m_keep = true; }
     };
 
-    pos_info_provider const *     m_pip;
-    std::vector<pair<name, expr>> m_ci_local_instances;
-    expr_struct_map<expr>         m_ci_cache;
-    bool                          m_ci_multiple_instances;
-    expr                          m_ci_main_mvar;
-    ci_state                      m_ci_state;    // active state
-    std::vector<ci_choice>        m_ci_choices;
-    unsigned                      m_ci_choices_ini_sz;
-    bool                          m_ci_displayed_trace_header;
-    optional<pos_info>            m_ci_pos;
+    pos_info_provider const *       m_pip;
+    std::vector<pair<name, expr>>   m_ci_local_instances;
+    expr_struct_map<optional<expr>> m_ci_cache;
+    bool                            m_ci_multiple_instances;
+    expr                            m_ci_main_mvar;
+    ci_state                        m_ci_state;    // active state
+    std::vector<ci_choice>          m_ci_choices;
+    unsigned                        m_ci_choices_ini_sz;
+    bool                            m_ci_displayed_trace_header;
+    optional<pos_info>              m_ci_pos;
 
     /* subsingleton instance cache, we also cache failures */
     expr_struct_map<optional<expr>> m_ss_cache;
 
     // configuration options
-    unsigned                      m_ci_max_depth;
-    bool                          m_ci_trans_instances;
-    bool                          m_ci_trace_instances;
+    unsigned                        m_ci_max_depth;
+    bool                            m_ci_trans_instances;
+    bool                            m_ci_trace_instances;
 
     optional<name> constant_is_class(expr const & e);
     optional<name> is_full_class(expr type);
@@ -320,8 +320,7 @@ class type_context {
     optional<expr> mk_nested_instance(expr const & type);
     bool mk_nested_instance(expr const & m, expr const & m_type);
     optional<expr> mk_class_instance_core(expr const & type);
-    optional<expr> check_ci_cache(expr const & type) const;
-    void cache_ci_result(expr const & type, expr const & inst);
+    void cache_ci_result(expr const & type, optional<expr> const & inst);
     type_context(environment const & env, options const & o, tmp_local_generator * gen,
                  bool gen_owner, bool multiple_instances);
 public: