feat(library): add cache_helper

src/library/app_builder.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/trace.h"
 #include "library/match.h"
 #include "library/constants.h"
+#include "library/cache_helper.h"
 #include "library/app_builder.h"
 #include "library/tmp_type_context.h"
 #include "library/relation_manager.h"
@@ -120,24 +121,13 @@ public:
     environment const & env() const { return m_env; }
 };
 
-struct app_builder_cache_helper {
-    typedef std::unique_ptr<app_builder_cache> cache_ptr;
-    cache_ptr m_cache_ptr[4];
-
-    void ensure_compatible(type_context const & ctx) {
-        unsigned midx = ctx.mode_idx();
-        if (!m_cache_ptr[midx] || !is_eqp(ctx.env(), m_cache_ptr[midx]->env())) {
-            m_cache_ptr[midx].reset(new app_builder_cache(ctx.env()));
-        }
-    }
-};
+typedef cache_compatibility_helper<app_builder_cache> app_builder_cache_helper;
 
 MK_THREAD_LOCAL_GET_DEF(app_builder_cache_helper, get_abch);
 
 /** Return an app_builder_cache for the transparency_mode in ctx, and compatible with the environment. */
 app_builder_cache & get_app_builder_cache_for(type_context const & ctx) {
-    get_abch().ensure_compatible(ctx);
-    return *get_abch().m_cache_ptr[ctx.mode_idx()].get();
+    return get_abch().get_cache_for(ctx);
 }
 
 /** \brief Helper for creating simple applications where some arguments are inferred using

src/library/cache_helper.h

@@ -0,0 +1,34 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <memory>
+#include "library/type_context.h"
+
+namespace lean {
+/** \brief Helper class for making sure we have a cache that is compatible
+    with a given environment and transparency mode. */
+template<typename Cache>
+class cache_compatibility_helper {
+    std::unique_ptr<Cache> m_cache_ptr[4];
+public:
+    Cache & get_cache_for(environment const & env, transparency_mode m) {
+        unsigned midx = static_cast<unsigned>(m);
+        if (!m_cache_ptr[midx] || !is_eqp(env, m_cache_ptr[midx]->env())) {
+            m_cache_ptr[midx].reset(new Cache(env));
+        }
+        return *m_cache_ptr[midx].get();
+    }
+
+    Cache & get_cache_for(type_context const & ctx) {
+        return get_cache_for(ctx.env(), ctx.mode());
+    }
+
+    void clear() {
+        for (unsigned i = 0; i < 4; i++) m_cache_ptr[i].reset();
+    }
+};
+}

src/library/fun_info.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/trace.h"
 #include "library/expr_unsigned_map.h"
 #include "library/fun_info.h"
+#include "library/cache_helper.h"
 
 namespace lean {
 static name * g_fun_info = nullptr;
@@ -41,28 +42,19 @@ struct fun_info_cache {
     narg_cache   m_cache_get_spec;
     prefix_cache m_cache_prefix;
     fun_info_cache(environment const & env):m_env(env) {}
+    environment const & env() const { return m_env; }
 };
 
-struct fun_info_cache_helper {
-    typedef std::unique_ptr<fun_info_cache> cache_ptr;
-    cache_ptr m_cache_ptr;
-
-    void ensure_compatible(environment const & env) {
-        if (!m_cache_ptr || !is_eqp(env, m_cache_ptr->m_env)) {
-            m_cache_ptr.reset(new fun_info_cache(env));
-        }
-    }
-};
+typedef cache_compatibility_helper<fun_info_cache> fun_info_cache_helper;
 
 MK_THREAD_LOCAL_GET_DEF(fun_info_cache_helper, get_fich);
 
-fun_info_cache & get_fun_info_cache_for(environment const & env) {
-    get_fich().ensure_compatible(env);
-    return *get_fich().m_cache_ptr.get();
+fun_info_cache & get_fun_info_cache_for(type_context const & ctx) {
+    return get_fich().get_cache_for(ctx);
 }
 
 void clear_fun_info_cache() {
-    get_fich().m_cache_ptr.reset();
+    get_fich().clear();
 }
 
 static list<unsigned> collect_deps(expr const & type, buffer<expr> const & locals) {
@@ -118,7 +110,7 @@ static list<unsigned> get_core(type_context & ctx,
 }
 
 fun_info get_fun_info(type_context & ctx, expr const & e) {
-    fun_info_cache & cache = get_fun_info_cache_for(ctx.env());
+    fun_info_cache & cache = get_fun_info_cache_for(ctx);
     auto it = cache.m_cache_get.find(e);
     if (it != cache.m_cache_get.end())
         return it->second;
@@ -130,7 +122,7 @@ fun_info get_fun_info(type_context & ctx, expr const & e) {
 }
 
 fun_info get_fun_info(type_context & ctx, expr const & e, unsigned nargs) {
-    fun_info_cache & cache = get_fun_info_cache_for(ctx.env());
+    fun_info_cache & cache = get_fun_info_cache_for(ctx);
     expr_unsigned key(e, nargs);
     auto it = cache.m_cache_get_nargs.find(key);
     if (it != cache.m_cache_get_nargs.end())
@@ -230,7 +222,7 @@ unsigned get_specialization_prefix_size(type_context & ctx, expr const & fn, uns
 
       This procecure returns the size of group a)
     */
-    fun_info_cache & cache = get_fun_info_cache_for(ctx.env());
+    fun_info_cache & cache = get_fun_info_cache_for(ctx);
     expr_unsigned key(fn, nargs);
     auto it = cache.m_cache_prefix.find(key);
     if (it != cache.m_cache_prefix.end())
@@ -263,7 +255,7 @@ fun_info get_specialized_fun_info(type_context & ctx, expr const & a) {
     expr g = a;
     for (unsigned i = 0; i < num_rest_args; i++)
         g = app_fn(g);
-    fun_info_cache & cache = get_fun_info_cache_for(ctx.env());
+    fun_info_cache & cache = get_fun_info_cache_for(ctx);
     expr_unsigned key(g, num_rest_args);
     auto it = cache.m_cache_get_spec.find(key);
     if (it != cache.m_cache_get_spec.end()) {