From 5572d7f3ec166330ccd04e1bfc914dbd35e55885 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 Dec 2016 18:33:46 -0800
Subject: [PATCH] perf(kernel,library/module): enable expr caching when
 deserializing .olean files

---
 src/kernel/expr.cpp    | 14 +++++++++-----
 src/kernel/expr.h      |  1 +
 src/kernel/level.cpp   |  6 ++++--
 src/kernel/level.h     |  1 +
 src/library/module.cpp |  1 +
 5 files changed, 16 insertions(+), 7 deletions(-)

diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 00de8157c5..fad672f26d 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -348,13 +348,11 @@ bool enable_expr_caching(bool f) {
     DEBUG_CODE(bool r1 =) enable_level_caching(f);
     bool r2 = g_expr_cache_enabled;
     lean_assert(r1 == r2);
-    expr_cache new_cache;
-    get_expr_cache().swap(new_cache);
+    cache(mk_Prop());
+    cache(mk_Type());
     if (f) {
         clear_abstract_cache();
         clear_instantiate_cache();
-        cache(mk_Prop());
-        cache(mk_Type());
     }
     g_expr_cache_enabled = f;
     return r2;
@@ -362,7 +360,13 @@ bool enable_expr_caching(bool f) {
 bool is_cached(expr const & e) {
     return get_expr_cache().find(e) != get_expr_cache().end();
 }
-
+void flush_expr_cache() {
+    flush_level_cache();
+    expr_cache new_cache;
+    get_expr_cache().swap(new_cache);
+    clear_abstract_cache();
+    clear_instantiate_cache();
+}
 expr mk_var(unsigned idx, tag g) {
     return cache(expr(new (get_var_allocator().allocate()) expr_var(idx, g)));
 }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index c4aed15618..dc3f65b994 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -503,6 +503,7 @@ struct scoped_expr_caching {
 };
 /** \brief Return true iff \c e is in the cache */
 bool is_cached(expr const & e);
+void flush_expr_cache();
 // =======================================
 
 // =======================================
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 88cb411a7a..5431bd834b 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -267,12 +267,14 @@ MK_THREAD_LOCAL_GET_DEF(level_cache, get_level_cache);
 bool enable_level_caching(bool f) {
     bool r = g_level_cache_enabled;
     g_level_cache_enabled = f;
-    level_cache new_cache;
-    get_level_cache().swap(new_cache);
     get_level_cache().insert(mk_level_zero());
     get_level_cache().insert(mk_level_one());
     return r;
 }
+void flush_level_cache() {
+    level_cache new_cache;
+    get_level_cache().swap(new_cache);
+}
 level cache(level const & e) {
     if (g_level_cache_enabled) {
         level_cache & cache = get_level_cache();
diff --git a/src/kernel/level.h b/src/kernel/level.h
index 0a6e64c6cf..c6dd70fcae 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -82,6 +82,7 @@ inline optional<level> some_level(level && e) { return optional<level>(std::forw
 bool enable_level_caching(bool f);
 level cache(level const & l);
 bool is_cached(level const & l);
+void flush_level_cache();
 
 level const & mk_level_zero();
 level const & mk_level_one();
diff --git a/src/library/module.cpp b/src/library/module.cpp
index d44da3a66a..a6e371ac53 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -439,6 +439,7 @@ void import_module(std::vector<char> const & olean_code, std::string const & fil
     // TODO(gabriel): update extension
     std::string s(olean_code.data(), olean_code.size());
     std::istringstream in(s, std::ios_base::binary);
+    scoped_expr_caching enable_caching(true);
     deserializer d(in, optional<std::string>(file_name));
     unsigned obj_counter = 0;
     while (true) {