diff options
| author | Son Ho | 2022-02-13 22:30:07 +0100 |
|---|---|---|
| committer | Son Ho | 2022-02-13 22:30:07 +0100 |
| commit | fab63abb07bcd1f1c28c5be386549185b4139003 (patch) | |
| tree | 14611f8303c789c8181384e69eeba2f1bfa94c39 | |
| parent | 1b95a1c00ab5f3d628275687cbf5f08517bce401 (diff) | |
Make progress on map_s
| -rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index b8788c8c..099fd2c6 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -464,6 +464,7 @@ let slots_t_al_v (#t : Type0) (slots : slots_t t) : assoc_list t = /// lemmas shown to the user. type hash_map_s t = list (slot_s t) +// TODO: why not always have the condition on the length? // 'nes': "non-empty slots" type hash_map_s_nes (t : Type0) : Type0 = hm:hash_map_s t{is_pos_usize (length hm)} @@ -616,6 +617,7 @@ type map_s (t : Type0) = { max_load_divis : usize; } +(* val to_v (#t : Type0) (hm : hash_map_t t) : map_s t let to_v #t hm = let slots = hash_map_t_v hm in @@ -629,6 +631,10 @@ let to_v #t hm = val len_s (#t : Type0) (m : map_s t) : nat let len_s #t m = hash_map_s_len m.slots +val find_s (#t : Type0) (m : map_s t) (k : key) : option t +let find_s #t m k = hash_map_s_find m.slots k +*) + let map_s_max_load (#t : Type0) (m : map_s t{m.max_load_divis > 0}) : nat = let capacity = length m.slots in let dividend = m.max_load_divid in |