feat(library): add environment fingerprint

src/library/CMakeLists.txt

@@ -9,6 +9,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   explicit.cpp num.cpp string.cpp head_map.cpp match.cpp
   definition_cache.cpp declaration_index.cpp
   print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp
-  protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp)
+  protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp
+  fingerprint.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/fingerprint.cpp

@@ -0,0 +1,47 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/hash.h"
+#include "util/int64.h"
+#include "kernel/environment.h"
+
+namespace lean {
+struct fingerprint_ext : public environment_extension {
+    uint64 m_fingerprint;
+    fingerprint_ext():m_fingerprint(0) {}
+};
+
+struct fingerprint_ext_reg {
+    unsigned m_ext_id;
+    fingerprint_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<fingerprint_ext>()); }
+};
+
+static fingerprint_ext_reg * g_ext = nullptr;
+static fingerprint_ext const & get_extension(environment const & env) {
+    return static_cast<fingerprint_ext const &>(env.get_extension(g_ext->m_ext_id));
+}
+static environment update(environment const & env, fingerprint_ext const & ext) {
+    return env.update(g_ext->m_ext_id, std::make_shared<fingerprint_ext>(ext));
+}
+
+environment update_fingerprint(environment const & env, unsigned h) {
+    fingerprint_ext ext = get_extension(env);
+    ext.m_fingerprint = hash(ext.m_fingerprint, static_cast<uint64>(h));
+    return update(env, ext);
+}
+
+uint64 get_fingerprint(environment const & env) {
+    return get_extension(env).m_fingerprint;
+}
+
+void initialize_fingerprint() {
+    g_ext     = new fingerprint_ext_reg();
+}
+
+void finalize_fingerprint() {
+    delete g_ext;
+}
+}

src/library/fingerprint.h

@@ -0,0 +1,16 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/int64.h"
+#include "kernel/environment.h"
+
+namespace lean {
+environment update_fingerprint(environment const & env, unsigned h);
+uint64 get_fingerprint(environment const & env);
+void initialize_fingerprint();
+void finalize_fingerprint();
+}

src/library/init_module.cpp

@@ -28,9 +28,11 @@ Author: Leonardo de Moura
 #include "library/sorry.h"
 #include "library/placeholder.h"
 #include "library/print.h"
+#include "library/fingerprint.h"
 
 namespace lean {
 void initialize_library_module() {
+    initialize_fingerprint();
     initialize_print();
     initialize_placeholder();
     initialize_match();
@@ -82,5 +84,6 @@ void finalize_library_module() {
     finalize_match();
     finalize_placeholder();
     finalize_print();
+    finalize_fingerprint();
 }
 }

src/util/hash.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "util/debug.h"
+#include "util/int64.h"
 
 namespace lean {
 
@@ -20,6 +21,13 @@ inline unsigned hash(unsigned h1, unsigned h2) {
     return h2;
 }
 
+inline uint64 hash(uint64 h1, uint64 h2) {
+    h2 -= h1; h2 ^= (h1 << 16);
+    h1 -= h2; h2 ^= (h1 << 32);
+    h2 -= h1; h2 ^= (h1 << 20);
+    return h2;
+}
+
 template<typename H>
 unsigned hash(unsigned n, H h, unsigned init_value = 31) {
     unsigned a, b, c;
@@ -69,6 +77,4 @@ unsigned hash(unsigned n, H h, unsigned init_value = 31) {
         return c;
     }
 }
-
-
 }