feat(kernel/level,library/blast/expr): add universe level hash consing support in the kernel, simplify blast/expr even more

src/kernel/expr.cpp

@@ -307,10 +307,12 @@ expr_macro::~expr_macro() {
 LEAN_THREAD_VALUE(bool, g_expr_cache_enabled, true);
 MK_THREAD_LOCAL_GET_DEF(expr_struct_set, get_expr_cache);
 bool enable_expr_caching(bool f) {
-    bool r = g_expr_cache_enabled;
+    bool r1 = enable_level_caching(f);
+    bool r2 = g_expr_cache_enabled;
+    lean_verify(r1 == r2);
     g_expr_cache_enabled = f;
     get_expr_cache().clear();
-    return r;
+    return r2;
 }
 inline expr cache(expr const & e) {
     if (g_expr_cache_enabled) {

src/kernel/expr.h

@@ -477,6 +477,7 @@ inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const
 /** \brief Return application (...((f x_{n-1}) x_{n-2}) ... x_0) */
 expr mk_app_vars(expr const & f, unsigned n, tag g = nulltag);
 
+/** \brief Enable hash-consing (caching) for expressions (and universe levels) */
 bool enable_expr_caching(bool f);
 /** \brief Helper class for temporarily enabling/disabling expression caching */
 struct scoped_expr_caching {

src/kernel/level.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include <algorithm>
 #include <vector>
+#include <unordered_set>
 #include "util/safe_arith.h"
 #include "util/buffer.h"
 #include "util/rc.h"
@@ -18,6 +19,8 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 
 namespace lean {
+level cache(level const & e);
+
 level_cell const & to_cell(level const & l) {
     return *l.m_ptr;
 }
@@ -192,7 +195,7 @@ bool is_explicit(level const & l) {
 }
 
 level mk_succ(level const & l) {
-    return level(new level_succ(l));
+    return cache(level(new level_succ(l)));
 }
 
 /** \brief Convert (succ^k l) into (l, k). If l is not a succ, then return (l, 0) */
@@ -230,7 +233,7 @@ level mk_max(level const & l1, level const & l2)  {
             lean_assert(p1.second != p2.second);
             return p1.second > p2.second ? l1 : l2;
         } else {
-            return level(new level_max_core(false, l1, l2));
+            return cache(level(new level_max_core(false, l1, l2)));
         }
     }
 }
@@ -245,12 +248,12 @@ level mk_imax(level const & l1, level const & l2) {
     else if (l1 == l2)
         return l1;  // imax u u = u
     else
-        return level(new level_max_core(true,  l1, l2));
+        return cache(level(new level_max_core(true,  l1, l2)));
 }
 
-level mk_param_univ(name const & n) { return level(new level_param_core(level_kind::Param, n)); }
-level mk_global_univ(name const & n) { return level(new level_param_core(level_kind::Global, n)); }
-level mk_meta_univ(name const & n) { return level(new level_param_core(level_kind::Meta, n)); }
+level mk_param_univ(name const & n)  { return cache(level(new level_param_core(level_kind::Param, n))); }
+level mk_global_univ(name const & n) { return cache(level(new level_param_core(level_kind::Global, n))); }
+level mk_meta_univ(name const & n)   { return cache(level(new level_param_core(level_kind::Meta, n))); }
 
 static level * g_level_zero = nullptr;
 static level * g_level_one  = nullptr;
@@ -258,6 +261,33 @@ level const & mk_level_zero() { return *g_level_zero; }
 level const & mk_level_one() { return *g_level_one; }
 bool is_one(level const & l) { return l == mk_level_one(); }
 
+typedef typename std::unordered_set<level, level_hash> level_table;
+LEAN_THREAD_VALUE(bool, g_level_cache_enabled, true);
+MK_THREAD_LOCAL_GET_DEF(level_table, get_level_cache);
+bool enable_level_caching(bool f) {
+    bool r = g_level_cache_enabled;
+    g_level_cache_enabled = f;
+    get_level_cache().clear();
+    get_level_cache().insert(mk_level_zero());
+    get_level_cache().insert(mk_level_one());
+    return r;
+}
+level cache(level const & e) {
+    if (g_level_cache_enabled) {
+        level_table & cache = get_level_cache();
+        auto it = cache.find(e);
+        if (it != cache.end()) {
+            return *it;
+        } else {
+            cache.insert(e);
+        }
+    }
+    return e;
+}
+bool is_cached(level const & e) {
+    return get_level_cache().find(e) != get_level_cache().end();
+}
+
 level::level():level(mk_level_zero()) {}
 level::level(level_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
 level::level(level const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }

src/kernel/level.h

@@ -79,6 +79,10 @@ inline optional<level> none_level() { return optional<level>(); }
 inline optional<level> some_level(level const & e) { return optional<level>(e); }
 inline optional<level> some_level(level && e) { return optional<level>(std::forward<level>(e)); }
 
+bool enable_level_caching(bool f);
+level cache(level const & l);
+bool is_cached(level const & l);
+
 level const & mk_level_zero();
 level const & mk_level_one();
 level mk_max(level const & l1, level const & l2);

src/library/blast/expr.cpp

@@ -19,54 +19,30 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace blast {
-typedef typename std::unordered_set<level, level_hash>                 level_table;
 typedef typename std::vector<expr> expr_array;
-
-LEAN_THREAD_PTR(level_table, g_level_table);
 LEAN_THREAD_PTR(expr_array,  g_var_array);
 LEAN_THREAD_PTR(expr_array,  g_mref_array);
 LEAN_THREAD_PTR(expr_array,  g_href_array);
 
-scope_hash_consing::scope_hash_consing() {
-    lean_assert(g_level_table == nullptr);
+scope_hash_consing::scope_hash_consing():
+    scoped_expr_caching(true) {
     lean_assert(g_var_array   == nullptr);
     lean_assert(g_mref_array  == nullptr);
     lean_assert(g_href_array  == nullptr);
-    g_level_table = new level_table();
     g_var_array   = new expr_array();
     g_mref_array  = new expr_array();
     g_href_array  = new expr_array();
-    g_level_table->insert(lean::mk_level_zero());
-    g_level_table->insert(lean::mk_level_one());
 }
 
 scope_hash_consing::~scope_hash_consing() {
-    delete g_level_table;
     delete g_var_array;
     delete g_mref_array;
     delete g_href_array;
-    g_level_table = nullptr;
     g_var_array   = nullptr;
     g_mref_array  = nullptr;
     g_href_array  = nullptr;
 }
 
-#ifdef LEAN_DEBUG
-static bool is_cached(level const & l) {
-    lean_assert(g_level_table);
-    return g_level_table->find(l) != g_level_table->end();
-}
-#endif
-
-static level cache(level const & l) {
-    lean_assert(g_level_table);
-    auto r = g_level_table->find(l);
-    if (r != g_level_table->end())
-        return *r;
-    g_level_table->insert(l);
-    return l;
-}
-
 level mk_level_zero() {
     return lean::mk_level_zero();
 }
@@ -78,30 +54,30 @@ level mk_level_one() {
 level mk_max(level const & l1, level const & l2) {
     lean_assert(is_cached(l1));
     lean_assert(is_cached(l2));
-    return cache(lean::mk_max(l1, l2));
+    return lean::mk_max(l1, l2);
 }
 
 level mk_imax(level const & l1, level const & l2) {
     lean_assert(is_cached(l1));
     lean_assert(is_cached(l2));
-    return cache(lean::mk_max(l1, l2));
+    return lean::mk_max(l1, l2);
 }
 
 level mk_succ(level const & l) {
     lean_assert(is_cached(l));
-    return cache(lean::mk_succ(l));
+    return lean::mk_succ(l);
 }
 
 level mk_param_univ(name const & n) {
-    return cache(lean::mk_param_univ(n));
+    return lean::mk_param_univ(n);
 }
 
 level mk_global_univ(name const & n) {
-    return cache(lean::mk_global_univ(n));
+    return lean::mk_global_univ(n);
 }
 
 level mk_meta_univ(name const & n) {
-    return cache(lean::mk_meta_univ(n));
+    return lean::mk_meta_univ(n);
 }
 
 level update_succ(level const & l, level const & new_arg) {

src/library/blast/expr.h

@@ -20,7 +20,7 @@ namespace blast {
 
 // Auxiliary object for resetting the the thread local hash-consing tables.
 // It also uses an assertion to make sure it is not being used in a recursion.
-class scope_hash_consing {
+class scope_hash_consing : public scoped_expr_caching {
 public:
     scope_hash_consing();
     ~scope_hash_consing();
@@ -81,8 +81,6 @@ bool has_local(expr const & e);
 level update_succ(level const & l, level const & new_arg);
 level update_max(level const & l, level const & new_lhs, level const & new_rhs);
 
-level replace(level const & l, std::function<optional<level>(level const & l)> const & f);
-
 expr update_app(expr const & e, expr const & new_fn, expr const & new_arg);
 expr update_metavar(expr const & e, expr const & new_type);
 expr update_binding(expr const & e, expr const & new_domain, expr const & new_body);
@@ -90,25 +88,6 @@ expr update_sort(expr const & e, level const & new_level);
 expr update_constant(expr const & e, levels const & new_levels);
 expr update_macro(expr const & e, unsigned num, expr const * args);
 
-expr replace(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f);
-inline expr replace(expr const & e, std::function<optional<expr>(expr const &)> const & f) {
-    return blast::replace(e, [&](expr const & e, unsigned) { return f(e); });
-}
-
-expr lift_free_vars(expr const & e, unsigned s, unsigned d);
-expr lift_free_vars(expr const & e, unsigned d);
-
-expr instantiate(expr const & e, unsigned n, expr const * s);
-expr instantiate_rev(expr const & e, unsigned n, expr const * s);
-
-level instantiate(level const & l, level_param_names const & ps, levels const & ls);
-expr  instantiate_univ_params(expr const & e, level_param_names const & ps, levels const & ls);
-expr  instantiate_type_univ_params(declaration const & d, levels const & ls);
-expr  instantiate_value_univ_params(declaration const & d, levels const & ls);
-
-expr abstract_hrefs(expr const & e, unsigned n, expr const * s);
-expr abstract_locals(expr const & e, unsigned n, expr const * s);
-
 void initialize_expr();
 void finalize_expr();
 }