diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index a2cbc9441e8..8146a169d08 100644 --- 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 index 8972b1b44e7..86fec99ab65 100644 --- 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 index 8d863be68c6..14a88f3fe4a 100644 --- 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 @@ -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 index 4baad04f203..d7a697357d3 100644 --- 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 index 2776ec93a51..0f2c5e4ccb8 100644 --- 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