feat(library/definition_cache): store the hashcode of direct dependencies

Actually we store the has code of their types.

src/frontends/lean/parser.cpp

@@ -120,12 +120,12 @@ parser::~parser() {
 void parser::cache_definition(name const & n, expr const & pre_type, expr const & pre_value,
                               level_param_names const & ls, expr const & type, expr const & value) {
     if (m_cache)
-        m_cache->add(n, pre_type, pre_value, ls, type, value);
+        m_cache->add(m_env, n, pre_type, pre_value, ls, type, value);
 }
 
 optional<std::tuple<level_param_names, expr, expr>> parser::find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value) {
     if (m_cache)
-        return m_cache->find(n, pre_type, pre_value);
+        return m_cache->find(m_env, n, pre_type, pre_value);
     else
         return optional<std::tuple<level_param_names, expr, expr>>();
 }

src/library/definition_cache.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/interrupt.h"
+#include "kernel/for_each_fn.h"
 #include "library/placeholder.h"
 #include "library/kernel_serializer.h"
 #include "library/definition_cache.h"
@@ -118,6 +119,12 @@ public:
     bool operator()(expr const & a, expr const & b) { return compare(a, b); }
 };
 
+definition_cache::entry::entry(expr const & pre_t, expr const & pre_v,
+                               level_param_names const & ps, expr const & t, expr const & v,
+                               dependencies const & deps):
+    m_pre_type(pre_t), m_pre_value(pre_v), m_params(ps),
+    m_type(t), m_value(v), m_dependencies(deps) {}
+
 definition_cache::definition_cache() {}
 
 void definition_cache::load(std::istream & in) {
@@ -130,19 +137,46 @@ void definition_cache::load(std::istream & in) {
         level_param_names ls;
         expr pre_type, pre_value, type, value;
         d >> n >> pre_type >> pre_value >> ls >> type >> value;
-        add_core(n, pre_type, pre_value, ls, type, value);
+        dependencies deps;
+        unsigned num;
+        d >> num;
+        for (unsigned i = 0; i < num; i++) {
+            name n; unsigned h;
+            d >> n >> h;
+            deps.insert(n, h);
         }
+        add_core(n, pre_type, pre_value, ls, type, value, deps);
+    }
+}
+
+void definition_cache::collect_dependencies(environment const & env, expr const & e, dependencies & deps) {
+    for_each(e, [&](expr const & e, unsigned) {
+            if (!is_constant(e))
+                return true;
+            name const & n = const_name(e);
+            if (deps.contains(n))
+                return true;
+            auto d = env.find(n);
+            if (!d)
+                return true;
+            deps.insert(n, hash_bi(d->get_type()));
+            return true;
+        });
 }
 
 void definition_cache::add_core(name const & n, expr const & pre_type, expr const & pre_value,
-                                 level_param_names const & ls, expr const & type, expr const & value) {
+                                level_param_names const & ls, expr const & type, expr const & value,
-    m_definitions.insert(n, entry(pre_type, pre_value, ls, type, value));
+                                dependencies const & deps) {
+    m_definitions.insert(n, entry(pre_type, pre_value, ls, type, value, deps));
 }
 
-void definition_cache::add(name const & n, expr const & pre_type, expr const & pre_value,
+void definition_cache::add(environment const & env, name const & n, expr const & pre_type, expr const & pre_value,
                            level_param_names const & ls, expr const & type, expr const & value) {
+    dependencies deps;
+    collect_dependencies(env, type, deps);
+    collect_dependencies(env, value, deps);
     lock_guard<mutex> lc(m_mutex);
-    add_core(n, pre_type, pre_value, ls, type, value);
+    add_core(n, pre_type, pre_value, ls, type, value, deps);
 }
 
 void definition_cache::erase(name const & n) {
@@ -155,32 +189,55 @@ void definition_cache::clear() {
     m_definitions.clear();
 }
 
-optional<std::tuple<level_param_names, expr, expr>> definition_cache::find(name const & n, expr const & pre_type, expr const & pre_value) {
+/** \brief Return true iff the type of all declarations in deps still have the same hashcode
-    entry const * it;
+    stored in deps. */
+bool definition_cache::check_dependencies(environment const & env, dependencies const & deps) {
+    bool ok = true;
+    deps.for_each([&](name const & n, unsigned h) {
+            if (ok) {
+                if (auto d = env.find(n)) {
+                    if (h != hash_bi(d->get_type()))
+                        ok = false;
+                } else {
+                    ok = false;
+                }
+            }
+        });
+    return ok;
+}
+
+optional<std::tuple<level_param_names, expr, expr>>
+definition_cache::find(environment const & env, name const & n, expr const & pre_type, expr const & pre_value) {
+    entry e;
     {
         lock_guard<mutex> lc(m_mutex);
-        it = m_definitions.find(n);
+        if (auto it = m_definitions.find(n)) {
-    }
+            e = *it;
-    if (it) {
+        } else {
-        level_param_names ls;
-        expr c_pre_type, c_pre_value, type, value;
-        std::tie(c_pre_type, c_pre_value, ls, type, value) = *it;
-        if (expr_eq_modulo_placeholders_fn()(c_pre_type, pre_type) &&
-            expr_eq_modulo_placeholders_fn()(c_pre_value, pre_value))
-            return some(std::make_tuple(ls, type, value));
-    }
             return optional<std::tuple<level_param_names, expr, expr>>();
         }
+    }
+    level_param_names ls;
+    if (expr_eq_modulo_placeholders_fn()(e.m_pre_type, pre_type) &&
+        expr_eq_modulo_placeholders_fn()(e.m_pre_value, pre_value) &&
+        check_dependencies(env, e.m_dependencies)) {
+        return some(std::make_tuple(e.m_params, e.m_type, e.m_value));
+    } else {
+        return optional<std::tuple<level_param_names, expr, expr>>();
+    }
+}
 
 void definition_cache::save(std::ostream & out) {
     lock_guard<mutex> lc(m_mutex);
     serializer s(out);
     s << m_definitions.size();
     m_definitions.for_each([&](name const & n, entry const & e) {
-            level_param_names ls;
+            s << n << e.m_pre_type << e.m_pre_value << e.m_params
-            expr c_pre_type, c_pre_value, type, value;
+              << e.m_type << e.m_value;
-            std::tie(c_pre_type, c_pre_value, ls, type, value) = e;
+            s << static_cast<unsigned>(e.m_dependencies.size());
-            s << n << c_pre_type << c_pre_value << ls << type << value;
+            e.m_dependencies.for_each([&](name const & n, unsigned h) {
+                    s << n << h;
+                });
         });
 }
 }

src/library/definition_cache.h

@@ -15,21 +15,37 @@ namespace lean {
     after elaboration.
 */
 class definition_cache {
-    typedef std::tuple<expr, expr, level_param_names, expr, expr> entry;
+    typedef name_map<unsigned> dependencies; // store the hash code for the type of used constants
+    struct entry {
+        expr              m_pre_type;
+        expr              m_pre_value;
+        level_param_names m_params;
+        expr              m_type;
+        expr              m_value;
+        dependencies      m_dependencies;
+        entry() {}
+        entry(expr const & pre_t, expr const & pre_v, level_param_names const & ps, expr const & t, expr const & v,
+              dependencies const & deps);
+        entry(expr const & pre_t, expr const & pre_v, level_param_names const & ps, expr const & t, expr const & v);
+    };
     mutex           m_mutex;
     name_map<entry> m_definitions;
+    void collect_dependencies(environment const & env, expr const & e, dependencies & deps);
+    bool check_dependencies(environment const & env, dependencies const & deps);
     void add_core(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls,
-                  expr const & type, expr const & value);
+                  expr const & type, expr const & value, dependencies const & deps);
 public:
     definition_cache();
     /** \brief Add the cache entry (n, pre_type, pre_value) -> (ls, type, value) */
-    void add(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value);
+    void add(environment const & env, name const & n, expr const & pre_type, expr const & pre_value,
+             level_param_names const & ls, expr const & type, expr const & value);
     /** \brief Return (if available) elaborated (level_names, type, value) for (n, pre_type, pre_value).
         The pre_type and pre_value are compared modulo placeholders names if the cached values.
         In principle, we could have compared only the name and pre_type, but we only want to use cached values if the
         user intent (captured by pre_value) did not change.
     */
-    optional<std::tuple<level_param_names, expr, expr>> find(name const & n, expr const & pre_type, expr const & pre_value);
+    optional<std::tuple<level_param_names, expr, expr>>
+    find(environment const & env, name const & n, expr const & pre_type, expr const & pre_value);
     /** \brief Store the cache content into the given stream */
     void save(std::ostream & out);
     /** \brief Load the cache content from the given stream */