chore(kernel): remove dummy file

src/kernel/expr.h

@@ -122,6 +122,7 @@ public:
 };
 
 typedef list_ref<expr> exprs;
+typedef pair<expr, expr> expr_pair;
 
 inline serializer & operator<<(serializer & s, expr const & e) { e.serialize(s); return s; }
 inline serializer & operator<<(serializer & s, exprs const & es) { es.serialize(s); return s; }
@@ -148,6 +149,12 @@ unsigned get_depth(expr const & e);
 unsigned get_loose_bvar_range(expr const & e);
 
 struct expr_hash { unsigned operator()(expr const & e) const { return hash(e); } };
+struct expr_pair_hash {
+    unsigned operator()(expr_pair const & p) const { return hash(hash(p.first), hash(p.second)); }
+};
+struct expr_pair_eq {
+    bool operator()(expr_pair const & p1, expr_pair const & p2) const { return p1.first == p2.first && p1.second == p2.second; }
+};
 
 // =======================================
 // Testers

src/kernel/expr_pair.h

@@ -1,21 +0,0 @@
-/*
-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 "kernel/expr.h"
-namespace lean {
-typedef pair<level, level> level_pair;
-typedef pair<expr, expr> expr_pair;
-/** \brief Functional object for hashing expression pairs. */
-struct expr_pair_hash {
-    unsigned operator()(expr_pair const & p) const { return hash(hash(p.first), hash(p.second)); }
-};
-
-/** \brief Functional object for comparing expression pairs. */
-struct expr_pair_eq {
-    bool operator()(expr_pair const & p1, expr_pair const & p2) const { return p1.first == p2.first && p1.second == p2.second; }
-};
-}

src/kernel/instantiate.cpp

@@ -16,48 +16,6 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
-class instantiate_univ_cache {
-    typedef std::tuple<constant_info, levels, expr> entry;
-    unsigned                     m_capacity;
-    std::vector<optional<entry>> m_cache;
-public:
-    instantiate_univ_cache(unsigned capacity):m_capacity(capacity) {
-        if (m_capacity == 0)
-            m_capacity++;
-    }
-
-    optional<expr> is_cached(constant_info const & d, levels const & ls) {
-        if (m_cache.empty())
-            return none_expr();
-        lean_assert(m_cache.size() == m_capacity);
-        unsigned idx = d.get_name().hash() % m_capacity;
-        if (auto it = m_cache[idx]) {
-            constant_info info_c; levels ls_c; expr r_c;
-            std::tie(info_c, ls_c, r_c) = *it;
-            if (!is_eqp(info_c, d))
-                return none_expr();
-            if (ls == ls_c)
-                return some_expr(r_c);
-            else
-                return none_expr();
-        }
-        return none_expr();
-    }
-
-    void save(constant_info const & d, levels const & ls, expr const & r) {
-        if (m_cache.empty())
-            m_cache.resize(m_capacity);
-        lean_assert(m_cache.size() == m_capacity);
-        unsigned idx = d.get_name().hash() % m_cache.size();
-        m_cache[idx] = entry(d, ls, r);
-    }
-
-    void clear() {
-        m_cache.clear();
-        lean_assert(m_cache.empty());
-    }
-};
-
 template<bool rev>
 struct instantiate_easy_fn {
     unsigned n;
@@ -178,6 +136,48 @@ expr instantiate_lparams(expr const & e, names const & lps, levels const & ls) {
         });
 }
 
+class instantiate_univ_cache {
+    typedef std::tuple<constant_info, levels, expr> entry;
+    unsigned                     m_capacity;
+    std::vector<optional<entry>> m_cache;
+public:
+    instantiate_univ_cache(unsigned capacity):m_capacity(capacity) {
+        if (m_capacity == 0)
+            m_capacity++;
+    }
+
+    optional<expr> is_cached(constant_info const & d, levels const & ls) {
+        if (m_cache.empty())
+            return none_expr();
+        lean_assert(m_cache.size() == m_capacity);
+        unsigned idx = d.get_name().hash() % m_capacity;
+        if (auto it = m_cache[idx]) {
+            constant_info info_c; levels ls_c; expr r_c;
+            std::tie(info_c, ls_c, r_c) = *it;
+            if (!is_eqp(info_c, d))
+                return none_expr();
+            if (ls == ls_c)
+                return some_expr(r_c);
+            else
+                return none_expr();
+        }
+        return none_expr();
+    }
+
+    void save(constant_info const & d, levels const & ls, expr const & r) {
+        if (m_cache.empty())
+            m_cache.resize(m_capacity);
+        lean_assert(m_cache.size() == m_capacity);
+        unsigned idx = d.get_name().hash() % m_cache.size();
+        m_cache[idx] = entry(d, ls, r);
+    }
+
+    void clear() {
+        m_cache.clear();
+        lean_assert(m_cache.empty());
+    }
+};
+
 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);
 

src/kernel/level.h

@@ -73,6 +73,7 @@ public:
 };
 
 typedef list_ref<level> levels;
+typedef pair<level, level> level_pair;
 
 bool operator==(level const & l1, level const & l2);
 inline bool operator!=(level const & l1, level const & l2) { return !operator==(l1, l2); }

src/kernel/type_checker.h

@@ -14,7 +14,6 @@ Author: Leonardo de Moura
 #include "util/name_generator.h"
 #include "kernel/environment.h"
 #include "kernel/local_ctx.h"
-#include "kernel/expr_pair.h"
 #include "kernel/expr_maps.h"
 #include "kernel/equiv_manager.h"
 #include "kernel/abstract_type_context.h"

src/library/expr_pair.h

@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #pragma once
 #include <utility>
 #include "util/hash.h"
-#include "kernel/expr_pair.h"
 #include "library/expr_lt.h"
 
 namespace lean {