feat(library/init/data/hashable): add builtin string hash

library/init/data/hashable.lean

@@ -4,10 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.usize
+import init.data.usize init.data.string
 universes u
 
 class hashable (α : Type u) :=
 (hash : α → usize)
 
+-- TODO: mark as builtin
+def string.hash (s : string) : usize :=
+default usize
+
+instance : hashable string :=
+⟨string.hash⟩
+
 export hashable (hash)

library/init/data/uint.lean

@@ -16,47 +16,45 @@ def uint32 := fin uint32_sz
 def uint64_sz : nat := 18446744073709551616
 def uint64 := fin uint64_sz
 
-instance : decidable_eq uint16 :=
-infer_instance_as (decidable_eq (fin uint16_sz))
+instance : decidable_eq uint16 := infer_instance_as (decidable_eq (fin uint16_sz))
+instance : decidable_eq uint32 := infer_instance_as (decidable_eq (fin uint32_sz))
+instance : decidable_eq uint64 := infer_instance_as (decidable_eq (fin uint64_sz))
 
-instance : decidable_eq uint32 :=
-infer_instance_as (decidable_eq (fin uint32_sz))
+instance : has_zero uint16  := ⟨fin.of_nat 0⟩
+instance : has_one uint16   := ⟨fin.of_nat 1⟩
+instance : has_add uint16   := ⟨fin.add⟩
+instance : has_sub uint16   := ⟨fin.sub⟩
+instance : has_mul uint16   := ⟨fin.mul⟩
+instance : has_mod uint16   := ⟨fin.mod⟩
+instance : has_modn uint16  := ⟨fin.modn⟩
+instance : has_div uint16   := ⟨fin.div⟩
+instance : has_lt uint16    := ⟨fin.lt⟩
+instance : has_le uint16    := ⟨fin.le⟩
+instance : inhabited uint16 := ⟨0⟩
 
-instance : decidable_eq uint64 :=
-infer_instance_as (decidable_eq (fin uint64_sz))
+instance : has_zero uint32  := ⟨fin.of_nat 0⟩
+instance : has_one uint32   := ⟨fin.of_nat 1⟩
+instance : has_add uint32   := ⟨fin.add⟩
+instance : has_sub uint32   := ⟨fin.sub⟩
+instance : has_mul uint32   := ⟨fin.mul⟩
+instance : has_mod uint32   := ⟨fin.mod⟩
+instance : has_modn uint32  := ⟨fin.modn⟩
+instance : has_div uint32   := ⟨fin.div⟩
+instance : has_lt uint32    := ⟨fin.lt⟩
+instance : has_le uint32    := ⟨fin.le⟩
+instance : inhabited uint32 := ⟨0⟩
 
-instance : has_zero uint16 := ⟨fin.of_nat 0⟩
-instance : has_one uint16  := ⟨fin.of_nat 1⟩
-instance : has_add uint16  := ⟨fin.add⟩
-instance : has_sub uint16  := ⟨fin.sub⟩
-instance : has_mul uint16  := ⟨fin.mul⟩
-instance : has_mod uint16  := ⟨fin.mod⟩
-instance : has_modn uint16 := ⟨fin.modn⟩
-instance : has_div uint16  := ⟨fin.div⟩
-instance : has_lt uint16   := ⟨fin.lt⟩
-instance : has_le uint16   := ⟨fin.le⟩
-
-instance : has_zero uint32 := ⟨fin.of_nat 0⟩
-instance : has_one uint32  := ⟨fin.of_nat 1⟩
-instance : has_add uint32  := ⟨fin.add⟩
-instance : has_sub uint32  := ⟨fin.sub⟩
-instance : has_mul uint32  := ⟨fin.mul⟩
-instance : has_mod uint32  := ⟨fin.mod⟩
-instance : has_modn uint32 := ⟨fin.modn⟩
-instance : has_div uint32  := ⟨fin.div⟩
-instance : has_lt uint32   := ⟨fin.lt⟩
-instance : has_le uint32   := ⟨fin.le⟩
-
-instance : has_zero uint64 := ⟨fin.of_nat 0⟩
-instance : has_one uint64  := ⟨fin.of_nat 1⟩
-instance : has_add uint64  := ⟨fin.add⟩
-instance : has_sub uint64  := ⟨fin.sub⟩
-instance : has_mul uint64  := ⟨fin.mul⟩
-instance : has_mod uint64  := ⟨fin.mod⟩
-instance : has_modn uint64 := ⟨fin.modn⟩
-instance : has_div uint64  := ⟨fin.div⟩
-instance : has_lt uint64   := ⟨fin.lt⟩
-instance : has_le uint64   := ⟨fin.le⟩
+instance : has_zero uint64  := ⟨fin.of_nat 0⟩
+instance : has_one uint64   := ⟨fin.of_nat 1⟩
+instance : has_add uint64   := ⟨fin.add⟩
+instance : has_sub uint64   := ⟨fin.sub⟩
+instance : has_mul uint64   := ⟨fin.mul⟩
+instance : has_mod uint64   := ⟨fin.mod⟩
+instance : has_modn uint64  := ⟨fin.modn⟩
+instance : has_div uint64   := ⟨fin.div⟩
+instance : has_lt uint64    := ⟨fin.lt⟩
+instance : has_le uint64    := ⟨fin.le⟩
+instance : inhabited uint64 := ⟨0⟩
 
 def uint16.of_nat (n : nat) : uint16 := fin.of_nat n
 def uint16.to_nat (u : uint16) : nat := fin.val u

library/init/data/usize.lean

@@ -19,13 +19,14 @@ nat.pos_pow_of_pos _ (nat.zero_lt_bit0 nat.one_ne_zero)
 def usize.of_nat (a : nat) : usize :=
 ⟨a % usize_sz, nat.mod_lt _ usize_sz_pos⟩
 
-instance : has_zero usize := ⟨usize.of_nat 0⟩
-instance : has_one usize  := ⟨usize.of_nat 1⟩
-instance : has_add usize  := ⟨fin.add⟩
-instance : has_sub usize  := ⟨fin.sub⟩
-instance : has_mul usize  := ⟨fin.mul⟩
-instance : has_mod usize  := ⟨fin.mod⟩
-instance : has_modn usize := ⟨fin.modn⟩
-instance : has_div usize  := ⟨fin.div⟩
-instance : has_lt usize   := ⟨fin.lt⟩
-instance : has_le usize   := ⟨fin.le⟩
+instance : has_zero usize  := ⟨usize.of_nat 0⟩
+instance : has_one usize   := ⟨usize.of_nat 1⟩
+instance : has_add usize   := ⟨fin.add⟩
+instance : has_sub usize   := ⟨fin.sub⟩
+instance : has_mul usize   := ⟨fin.mul⟩
+instance : has_mod usize   := ⟨fin.mod⟩
+instance : has_modn usize  := ⟨fin.modn⟩
+instance : has_div usize   := ⟨fin.div⟩
+instance : has_lt usize    := ⟨fin.lt⟩
+instance : has_le usize    := ⟨fin.le⟩
+instance : inhabited usize := ⟨0⟩

src/library/vm/vm_string.cpp

@@ -491,6 +491,11 @@ vm_obj string_iterator_extract(vm_obj const & it1, vm_obj const & it2) {
     return mk_vm_some(to_obj(s1.m_value.substr(pos1, pos2 - pos1), pos2 - pos1));
 }
 
+vm_obj string_hash(vm_obj const & s) {
+    std::string const & _s = to_string(s);
+    return mk_vm_nat(hash_str(_s.size(), _s.data(), 13));
+}
+
 void initialize_vm_string() {
     DECLARE_VM_BUILTIN(name({"string_imp", "mk"}),             string_imp_mk);
     DECLARE_VM_BUILTIN(name({"string_imp", "data"}),           string_imp_data);
@@ -506,6 +511,7 @@ void initialize_vm_string() {
     DECLARE_VM_BUILTIN(name({"string", "has_decidable_eq"}),  string_has_decidable_eq);
     // DECLARE_VM_BUILTIN(name({"string", "cmp"}),               string_cmp);
     DECLARE_VM_BUILTIN(name({"string", "has_decidable_lt"}),  string_has_decidable_lt);
+    DECLARE_VM_BUILTIN(name({"string", "hash"}),              string_hash);
 
     DECLARE_VM_BUILTIN(name({"string", "iterator", "curr"}),           string_iterator_curr);
     DECLARE_VM_BUILTIN(name({"string", "iterator", "set_curr"}),       string_iterator_set_curr);