diff --git a/library/init/data/hashable.lean b/library/init/data/hashable.lean index 79a97ba7b6..fbc5d661be 100644 --- a/library/init/data/hashable.lean +++ b/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) diff --git a/library/init/data/uint.lean b/library/init/data/uint.lean index 7f8e770903..f8f4075acc 100644 --- a/library/init/data/uint.lean +++ b/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 diff --git a/library/init/data/usize.lean b/library/init/data/usize.lean index a40fe3b9ac..a9cfed5f96 100644 --- a/library/init/data/usize.lean +++ b/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⟩ diff --git a/src/library/vm/vm_string.cpp b/src/library/vm/vm_string.cpp index 5441dc737f..c766c58c28 100644 --- a/src/library/vm/vm_string.cpp +++ b/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);