feat: ByteArray.hash

bollu · Dec 2, 2022 · 681bbe5 · 681bbe5
1 parent a67a508
commit 681bbe5
Show file tree

Hide file tree

Showing 5 changed files with 17 additions and 0 deletions.
diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean
@@ -67,6 +67,12 @@ def set : (a : ByteArray) → (@& Fin a.size) → UInt8 → ByteArray
 def uset : (a : ByteArray) → (i : USize) → UInt8 → i.toNat < a.size → ByteArray
   | ⟨bs⟩, i, v, h => ⟨bs.uset i v h⟩
 
+@[extern "lean_byte_array_hash"]
+protected opaque hash (a : @& ByteArray) : UInt64
+
+instance : Hashable ByteArray where
+  hash := ByteArray.hash
+
 def isEmpty (s : ByteArray) : Bool :=
   s.size == 0
 

diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
@@ -856,6 +856,7 @@ static inline uint8_t* lean_sarray_cptr(lean_object * o) { return lean_to_sarray
 LEAN_SHARED lean_obj_res lean_byte_array_mk(lean_obj_arg a);
 LEAN_SHARED lean_obj_res lean_byte_array_data(lean_obj_arg a);
 LEAN_SHARED lean_obj_res lean_copy_byte_array(lean_obj_arg a);
+LEAN_SHARED uint64_t lean_byte_array_hash(b_lean_obj_arg a);
 
 static inline lean_obj_res lean_mk_empty_byte_array(b_lean_obj_arg capacity) {
     if (!lean_is_scalar(capacity)) lean_internal_panic_out_of_memory();

diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "runtime/interrupt.h"
 #include "runtime/buffer.h"
 #include "runtime/io.h"
+#include "runtime/hash.h"
 
 #ifdef __GLIBC__
 #include <execinfo.h>
@@ -2055,6 +2056,10 @@ extern "C" LEAN_EXPORT obj_res lean_byte_array_push(obj_arg a, uint8 b) {
     return r;
 }
 
+extern "C" LEAN_EXPORT uint64_t lean_byte_array_hash(b_obj_arg a) {
+    return hash_str(lean_sarray_size(a), lean_sarray_cptr(a), 11);
+}
+
 extern "C" LEAN_EXPORT obj_res lean_copy_float_array(obj_arg a) {
     return lean_copy_sarray(a, lean_sarray_capacity(a));
 }

diff --git a/tests/lean/bytearray.lean b/tests/lean/bytearray.lean
@@ -16,5 +16,8 @@ pure ()
 
 #eval tst
 
+#eval "abcd".hash
+#eval [97, 98, 99, 100].toByteArray.hash
+
 #eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.toUInt64LE! == 0x1122334455667788
 #eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.toUInt64BE! == 0x8877665544332211
diff --git a/tests/lean/bytearray.lean.expected.out b/tests/lean/bytearray.lean.expected.out
@@ -5,5 +5,7 @@
 4
 [1, 20, 3, 4, 1, 20, 3, 4]
 [20, 3]
+11774739814239950349
+11774739814239950349
 true
 true