From 4cfebe7f1c38de0ddc27520eaa74eef0e2f67f67 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 21 Sep 2015 16:08:34 -0700
Subject: [PATCH] refactor(kernel): move instantiate_univ_cache to separate .h
 file

---
 src/kernel/instantiate.cpp          | 33 +++--------------------
 src/kernel/instantiate_univ_cache.h | 42 +++++++++++++++++++++++++++++
 2 files changed, 45 insertions(+), 30 deletions(-)
 create mode 100644 src/kernel/instantiate_univ_cache.h

diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp
index a51cbcba7..58ddfd931 100644
--- a/src/kernel/instantiate.cpp
+++ b/src/kernel/instantiate.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 #include "kernel/declaration.h"
 #include "kernel/instantiate.h"
+#include "kernel/instantiate_univ_cache.h"
 
 #ifndef LEAN_INST_UNIV_CACHE_SIZE
 #define LEAN_INST_UNIV_CACHE_SIZE 1023
@@ -139,36 +140,8 @@ expr instantiate_univ_params(expr const & e, level_param_names const & ps, level
         });
 }
 
-class instantiate_univ_cache {
-    typedef std::tuple<declaration, levels, expr> entry;
-    std::vector<optional<entry>> m_cache;
-public:
-    instantiate_univ_cache() {
-        m_cache.resize(LEAN_INST_UNIV_CACHE_SIZE);
-    }
-
-    optional<expr> is_cached(declaration const & d, levels const & ls) {
-        unsigned idx = d.get_name().hash() % LEAN_INST_UNIV_CACHE_SIZE;
-        if (auto it = m_cache[idx]) {
-            declaration d_c; levels ls_c; expr r_c;
-            std::tie(d_c, ls_c, r_c) = *it;
-            if (!is_eqp(d_c, d))
-                return none_expr();
-            if (ls == ls_c)
-                return some_expr(r_c);
-            else
-                return none_expr();
-        }
-        return none_expr();
-    }
-    void save(declaration const & d, levels const & ls, expr const & r) {
-        unsigned idx = d.get_name().hash() % LEAN_INST_UNIV_CACHE_SIZE;
-        m_cache[idx] = entry(d, ls, r);
-    }
-};
-
-MK_THREAD_LOCAL_GET_DEF(instantiate_univ_cache, get_type_univ_cache);
-MK_THREAD_LOCAL_GET_DEF(instantiate_univ_cache, get_value_univ_cache);
+MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_type_univ_cache, LEAN_INST_UNIV_CACHE_SIZE);
+MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_value_univ_cache, LEAN_INST_UNIV_CACHE_SIZE);
 
 expr instantiate_type_univ_params(declaration const & d, levels const & ls) {
     lean_assert(d.get_num_univ_params() == length(ls));
diff --git a/src/kernel/instantiate_univ_cache.h b/src/kernel/instantiate_univ_cache.h
new file mode 100644
index 000000000..8ba58fe1c
--- /dev/null
+++ b/src/kernel/instantiate_univ_cache.h
@@ -0,0 +1,42 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <algorithm>
+#include <limits>
+#include <vector>
+#include "kernel/declaration.h"
+
+namespace lean {
+class instantiate_univ_cache {
+    typedef std::tuple<declaration, levels, expr> entry;
+    std::vector<optional<entry>> m_cache;
+public:
+    instantiate_univ_cache(unsigned capacity) {
+        m_cache.resize(capacity);
+    }
+
+    optional<expr> is_cached(declaration const & d, levels const & ls) {
+        unsigned idx = d.get_name().hash() % m_cache.size();
+        if (auto it = m_cache[idx]) {
+            declaration d_c; levels ls_c; expr r_c;
+            std::tie(d_c, ls_c, r_c) = *it;
+            if (!is_eqp(d_c, d))
+                return none_expr();
+            if (ls == ls_c)
+                return some_expr(r_c);
+            else
+                return none_expr();
+        }
+        return none_expr();
+    }
+
+    void save(declaration const & d, levels const & ls, expr const & r) {
+        unsigned idx = d.get_name().hash() % m_cache.size();
+        m_cache[idx] = entry(d, ls, r);
+    }
+};
+}