refactor: move lean_name_eq to runtime, add lean_name_hash in C

src/Lean/Data/Name.lean

@@ -12,8 +12,8 @@ namespace Lean
 instance : Coe String Name := ⟨Name.mkSimple⟩
 
 namespace Name
-
-@[export lean_name_hash] def hashEx : Name → UInt64 :=
+-- Remark: we export the `Name.hash` to make sure it matches the hash implemented in C++
+@[export lean_name_hash_exported] def hashEx : Name → UInt64 :=
   Name.hash
 
 def getPrefix : Name → Name

src/include/lean/lean.h

@@ -1686,6 +1686,21 @@ lean_obj_res lean_st_ref_swap(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
 /* pointer address unsafe primitive  */
 static inline size_t lean_ptr_addr(b_lean_obj_arg a) { return (size_t)a; }
 
+/* Name primitives */
+uint8_t lean_name_eq(b_lean_obj_arg n1, b_lean_obj_arg n2);
+
+static inline uint64_t lean_name_hash_ptr(b_lean_obj_arg n) {
+    assert(!lean_is_scalar(n));
+    return lean_ctor_get_uint64(n, sizeof(lean_object*)*2);
+}
+
+static inline uint64_t lean_name_hash(b_lean_obj_arg n) {
+    if (lean_is_scalar(n))
+        return 1723;
+    else
+        return lean_name_hash_ptr(n);
+}
+
 #ifdef __cplusplus
 }
 #endif

src/runtime/object.cpp

@@ -2076,6 +2076,39 @@ extern "C" object * lean_array_push(obj_arg a, obj_arg v) {
     return r;
 }
 
+// =======================================
+// Name primitives
+
+extern "C" uint8 lean_name_eq(b_lean_obj_arg n1, b_lean_obj_arg n2) {
+    if (n1 == n2)
+        return true;
+    if (lean_is_scalar(n1) != lean_is_scalar(n2) || lean_name_hash_ptr(n1) != lean_name_hash_ptr(n2))
+        return false;
+    while (true) {
+        lean_assert(!lean_is_scalar(n1));
+        lean_assert(!lean_is_scalar(n2));
+        lean_assert(n1 && n2);
+        lean_assert(lean_name_hash_ptr(n1) == lean_name_hash_ptr(n2));
+        if (lean_ptr_tag(n1) != lean_ptr_tag(n2))
+            return false;
+        if (lean_ptr_tag(n1) == 1) {
+            if (!lean_string_eq(lean_ctor_get(n1, 1), lean_ctor_get(n2, 1)))
+                return false;
+        } else {
+            if (!lean_nat_eq(lean_ctor_get(n1, 1), lean_ctor_get(n1, 1)))
+                return false;
+        }
+        n1 = lean_ctor_get(n1, 0);
+        n2 = lean_ctor_get(n2, 0);
+        if (n1 == n2)
+            return true;
+        if (lean_is_scalar(n1) != lean_is_scalar(n2))
+            return false;
+        if (lean_name_hash_ptr(n1) != lean_name_hash_ptr(n2))
+            return false;
+    }
+}
+
 // =======================================
 // Runtime info
 

src/util/name.cpp

@@ -27,39 +27,6 @@ static inline obj_res name_mk_string_of_cstr(obj_arg p, char const * s) {
     return lean_name_mk_string(p, mk_string(s));
 }
 
-extern "C" uint64_t lean_name_hash(obj_arg n);
-uint64_t name::hash(b_obj_arg n) { inc(n); return lean_name_hash(n); }
-
-bool name::eq_core(b_obj_arg n1, b_obj_arg n2) {
-    while (true) {
-        lean_assert(!is_scalar(n1));
-        lean_assert(!is_scalar(n2));
-        lean_assert(n1 && n2);
-        lean_assert(name::hash(n1) == name::hash(n2));
-        if (cnstr_tag(n1) != cnstr_tag(n2))
-            return false;
-        if (cnstr_tag(n1) == static_cast<unsigned>(name_kind::STRING)) {
-            if (!string_eq(cnstr_get(n1, 1), cnstr_get(n2, 1)))
-                return false;
-        } else {
-            if (!nat_eq(cnstr_get(n1, 1), cnstr_get(n1, 1)))
-                return false;
-        }
-        n1 = cnstr_get(n1, 0);
-        n2 = cnstr_get(n2, 0);
-        if (n1 == n2)
-            return true;
-        if (is_scalar(n1) != is_scalar(n2))
-            return false;
-        if (name::hash(n1) != name::hash(n2))
-            return false;
-    }
-}
-
-extern "C" uint8 lean_name_eq(b_obj_arg a1, b_obj_arg a2) {
-    return name::eq(a1, a2);
-}
-
 constexpr char const * anonymous_str = "[anonymous]";
 
 bool is_greek_unicode(unsigned u) { return 0x391 <= u && u <= 0x3DD; }

src/util/name.h

@@ -40,19 +40,15 @@ inline bool is_id_rest(char const * begin, char const * end) {
                       reinterpret_cast<unsigned char const *>(end));
 }
 
+extern "C" uint64_t lean_name_hash_exported(b_lean_obj_arg n);
+
+
 enum class name_kind { ANONYMOUS, STRING, NUMERAL };
 /** \brief Hierarchical names. */
 class name : public object_ref {
 public:
     /* Low level primitives */
-    static bool eq_core(b_obj_arg n1, b_obj_arg n2);
-    static bool eq(b_obj_arg n1, b_obj_arg n2) {
-        if (n1 == n2)
-            return true;
-        if (is_scalar(n1) != is_scalar(n2) || name::hash(n1) != name::hash(n2))
-            return false;
-        return eq_core(n1, n2);
-    }
+    static bool eq(b_obj_arg n1, b_obj_arg n2) { return lean_name_eq(n1, n2); }
     static name_kind kind(object * o) { return static_cast<name_kind>(obj_tag(o)); }
     static bool is_anonymous(object * o) { return is_scalar(o); }
     static object * get_prefix(object * o) { return cnstr_get(o, 0); }
@@ -98,7 +94,10 @@ public:
     static name mk_internal_unique_name();
     name & operator=(name const & other) { object_ref::operator=(other); return *this; }
     name & operator=(name && other) { object_ref::operator=(other); return *this; }
-    static uint64_t hash(b_obj_arg n);
+    static uint64_t hash(b_obj_arg n) {
+       lean_assert(lean_name_hash(n) == lean_name_hash_exported(n));
+       return lean_name_hash(n);
+    }
     uint64_t hash() const { return hash(raw()); }
     /** \brief Return true iff \c n1 is a prefix of \c n2. */
     friend bool is_prefix_of(name const & n1, name const & n2);