summaryrefslogtreecommitdiff
path: root/tests/hashmap
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/hashmap/Hashmap.Funs.fst56
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Funs.fst89
2 files changed, 78 insertions, 67 deletions
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index 80783781..f75a0c01 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -21,13 +21,13 @@ let rec hash_map_allocate_slots_fwd
| _ ->
begin match vec_push_back (list_t t) slots ListNil with
| Fail -> Fail
- | Return v ->
+ | Return slots0 ->
begin match usize_sub n 1 with
| Fail -> Fail
| Return i ->
- begin match hash_map_allocate_slots_fwd t v i with
+ begin match hash_map_allocate_slots_fwd t slots0 i with
| Fail -> Fail
- | Return v0 -> Return v0
+ | Return v -> Return v
end
end
end
@@ -72,13 +72,13 @@ let rec hash_map_clear_slots_fwd_back
then
begin match vec_index_mut_back (list_t t) slots i ListNil with
| Fail -> Fail
- | Return v ->
+ | Return slots0 ->
begin match usize_add i 1 with
| Fail -> Fail
| Return i1 ->
- begin match hash_map_clear_slots_fwd_back t v i1 with
+ begin match hash_map_clear_slots_fwd_back t slots0 i1 with
| Fail -> Fail
- | Return v0 -> Return v0
+ | Return slots1 -> Return slots1
end
end
end
@@ -129,7 +129,7 @@ let rec hash_map_insert_in_list_back
else
begin match hash_map_insert_in_list_back t key value ls0 with
| Fail -> Fail
- | Return l -> Return (ListCons ckey cvalue l)
+ | Return ls1 -> Return (ListCons ckey cvalue ls1)
end
| ListNil -> let l = ListNil in Return (ListCons key value l)
end
@@ -200,10 +200,10 @@ let rec hash_map_move_elements_from_list_fwd_back
| ListCons k v tl ->
begin match hash_map_insert_no_resize_fwd_back t ntable k v with
| Fail -> Fail
- | Return hm ->
- begin match hash_map_move_elements_from_list_fwd_back t hm tl with
+ | Return ntable0 ->
+ begin match hash_map_move_elements_from_list_fwd_back t ntable0 tl with
| Fail -> Fail
- | Return hm0 -> Return hm0
+ | Return ntable1 -> Return ntable1
end
end
| ListNil -> Return ntable
@@ -224,17 +224,18 @@ let rec hash_map_move_elements_fwd_back
let ls = mem_replace_fwd (list_t t) l ListNil in
begin match hash_map_move_elements_from_list_fwd_back t ntable ls with
| Fail -> Fail
- | Return hm ->
+ | Return ntable0 ->
let l0 = mem_replace_back (list_t t) l ListNil in
begin match vec_index_mut_back (list_t t) slots i l0 with
| Fail -> Fail
- | Return v ->
+ | Return slots0 ->
begin match usize_add i 1 with
| Fail -> Fail
| Return i1 ->
- begin match hash_map_move_elements_fwd_back t hm v i1 with
+ begin match hash_map_move_elements_fwd_back t ntable0 slots0 i1
+ with
| Fail -> Fail
- | Return (hm0, v0) -> Return (hm0, v0)
+ | Return (ntable1, slots1) -> Return (ntable1, slots1)
end
end
end
@@ -265,9 +266,9 @@ let hash_map_try_resize_fwd_back
hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0
with
| Fail -> Fail
- | Return (hm, _) ->
+ | Return (ntable0, _) ->
Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
- hm.hash_map_max_load hm.hash_map_slots)
+ ntable0.hash_map_max_load ntable0.hash_map_slots)
end
end
end
@@ -284,22 +285,23 @@ let hash_map_insert_fwd_back
=
begin match hash_map_insert_no_resize_fwd_back t self key value with
| Fail -> Fail
- | Return hm ->
- begin match hash_map_len_fwd t hm with
+ | Return self0 ->
+ begin match hash_map_len_fwd t self0 with
| Fail -> Fail
| Return i ->
- if i > hm.hash_map_max_load
+ if i > self0.hash_map_max_load
then
begin match
- hash_map_try_resize_fwd_back t (Mkhash_map_t hm.hash_map_num_entries
- hm.hash_map_max_load_factor hm.hash_map_max_load hm.hash_map_slots)
- with
+ hash_map_try_resize_fwd_back t (Mkhash_map_t
+ self0.hash_map_num_entries self0.hash_map_max_load_factor
+ self0.hash_map_max_load self0.hash_map_slots) with
| Fail -> Fail
- | Return hm0 -> Return hm0
+ | Return self1 -> Return self1
end
else
- Return (Mkhash_map_t hm.hash_map_num_entries
- hm.hash_map_max_load_factor hm.hash_map_max_load hm.hash_map_slots)
+ Return (Mkhash_map_t self0.hash_map_num_entries
+ self0.hash_map_max_load_factor self0.hash_map_max_load
+ self0.hash_map_slots)
end
end
@@ -410,7 +412,7 @@ let rec hash_map_get_mut_in_list_back
else
begin match hash_map_get_mut_in_list_back t key ls0 ret with
| Fail -> Fail
- | Return l -> Return (ListCons ckey cvalue l)
+ | Return ls1 -> Return (ListCons ckey cvalue ls1)
end
| ListNil -> Fail
end
@@ -509,7 +511,7 @@ let rec hash_map_remove_from_list_back
else
begin match hash_map_remove_from_list_back t key tl with
| Fail -> Fail
- | Return l -> Return (ListCons ckey x l)
+ | Return tl0 -> Return (ListCons ckey x tl0)
end
| ListNil -> Return ListNil
end
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index cf0df7a7..a4167186 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -23,13 +23,13 @@ let rec hashmap_hash_map_allocate_slots_fwd
| _ ->
begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
| Fail -> Fail
- | Return v ->
+ | Return slots0 ->
begin match usize_sub n 1 with
| Fail -> Fail
| Return i ->
- begin match hashmap_hash_map_allocate_slots_fwd t v i st with
+ begin match hashmap_hash_map_allocate_slots_fwd t slots0 i st with
| Fail -> Fail
- | Return (st0, v0) -> Return (st0, v0)
+ | Return (st0, v) -> Return (st0, v)
end
end
end
@@ -77,11 +77,11 @@ let rec hashmap_hash_map_clear_slots_fwd
begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
with
| Fail -> Fail
- | Return v ->
+ | Return slots0 ->
begin match usize_add i 1 with
| Fail -> Fail
| Return i1 ->
- begin match hashmap_hash_map_clear_slots_fwd t v i1 st with
+ begin match hashmap_hash_map_clear_slots_fwd t slots0 i1 st with
| Fail -> Fail
| Return (st0, _) -> Return (st0, ())
end
@@ -101,13 +101,13 @@ let rec hashmap_hash_map_clear_slots_back
begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
with
| Fail -> Fail
- | Return v ->
+ | Return slots0 ->
begin match usize_add i 1 with
| Fail -> Fail
| Return i1 ->
- begin match hashmap_hash_map_clear_slots_back t v i1 st with
+ begin match hashmap_hash_map_clear_slots_back t slots0 i1 st with
| Fail -> Fail
- | Return (st0, v0) -> Return (st0, v0)
+ | Return (st0, slots1) -> Return (st0, slots1)
end
end
end
@@ -175,7 +175,7 @@ let rec hashmap_hash_map_insert_in_list_back
else
begin match hashmap_hash_map_insert_in_list_back t key value ls0 st with
| Fail -> Fail
- | Return (st0, l) -> Return (st0, HashmapListCons ckey cvalue l)
+ | Return (st0, ls1) -> Return (st0, HashmapListCons ckey cvalue ls1)
end
| HashmapListNil ->
let l = HashmapListNil in Return (st, HashmapListCons key value l)
@@ -288,8 +288,9 @@ let rec hashmap_hash_map_move_elements_from_list_fwd
| HashmapListCons k v tl ->
begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
| Fail -> Fail
- | Return (st0, hm) ->
- begin match hashmap_hash_map_move_elements_from_list_fwd t hm tl st0 with
+ | Return (st0, ntable0) ->
+ begin match hashmap_hash_map_move_elements_from_list_fwd t ntable0 tl st0
+ with
| Fail -> Fail
| Return (st1, _) -> Return (st1, ())
end
@@ -309,11 +310,11 @@ let rec hashmap_hash_map_move_elements_from_list_back
| HashmapListCons k v tl ->
begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
| Fail -> Fail
- | Return (st0, hm) ->
- begin match hashmap_hash_map_move_elements_from_list_back t hm tl st0
- with
+ | Return (st0, ntable0) ->
+ begin match
+ hashmap_hash_map_move_elements_from_list_back t ntable0 tl st0 with
| Fail -> Fail
- | Return (st1, hm0) -> Return (st1, hm0)
+ | Return (st1, ntable1) -> Return (st1, ntable1)
end
end
| HashmapListNil -> Return (st, ntable)
@@ -336,15 +337,16 @@ let rec hashmap_hash_map_move_elements_fwd
begin match hashmap_hash_map_move_elements_from_list_back t ntable ls st
with
| Fail -> Fail
- | Return (st0, hm) ->
+ | Return (st0, ntable0) ->
let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
| Fail -> Fail
- | Return v ->
+ | Return slots0 ->
begin match usize_add i 1 with
| Fail -> Fail
| Return i1 ->
- begin match hashmap_hash_map_move_elements_fwd t hm v i1 st0 with
+ begin match
+ hashmap_hash_map_move_elements_fwd t ntable0 slots0 i1 st0 with
| Fail -> Fail
| Return (st1, _) -> Return (st1, ())
end
@@ -371,17 +373,19 @@ let rec hashmap_hash_map_move_elements_back
begin match hashmap_hash_map_move_elements_from_list_back t ntable ls st
with
| Fail -> Fail
- | Return (st0, hm) ->
+ | Return (st0, ntable0) ->
let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
| Fail -> Fail
- | Return v ->
+ | Return slots0 ->
begin match usize_add i 1 with
| Fail -> Fail
| Return i1 ->
- begin match hashmap_hash_map_move_elements_back t hm v i1 st0 with
+ begin match
+ hashmap_hash_map_move_elements_back t ntable0 slots0 i1 st0 with
| Fail -> Fail
- | Return (st1, (hm0, v0)) -> Return (st1, (hm0, v0))
+ | Return (st1, (ntable1, slots1)) ->
+ Return (st1, (ntable1, slots1))
end
end
end
@@ -447,10 +451,11 @@ let hashmap_hash_map_try_resize_back
hashmap_hash_map_move_elements_back t ntable
self.hashmap_hash_map_slots 0 st0 with
| Fail -> Fail
- | Return (st1, (hm, _)) ->
+ | Return (st1, (ntable0, _)) ->
Return (st1, Mkhashmap_hash_map_t
self.hashmap_hash_map_num_entries (i, i0)
- hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots)
+ ntable0.hashmap_hash_map_max_load
+ ntable0.hashmap_hash_map_slots)
end
end
end
@@ -468,16 +473,18 @@ let hashmap_hash_map_insert_fwd
=
begin match hashmap_hash_map_insert_no_resize_back t self key value st with
| Fail -> Fail
- | Return (st0, hm) ->
- begin match hashmap_hash_map_len_fwd t hm st0 with
+ | Return (st0, self0) ->
+ begin match hashmap_hash_map_len_fwd t self0 st0 with
| Fail -> Fail
| Return (st1, i) ->
- if i > hm.hashmap_hash_map_max_load
+ if i > self0.hashmap_hash_map_max_load
then
begin match
hashmap_hash_map_try_resize_fwd t (Mkhashmap_hash_map_t
- hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor
- hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1 with
+ self0.hashmap_hash_map_num_entries
+ self0.hashmap_hash_map_max_load_factor
+ self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots)
+ st1 with
| Fail -> Fail
| Return (st2, _) -> Return (st2, ())
end
@@ -493,23 +500,25 @@ let hashmap_hash_map_insert_back
=
begin match hashmap_hash_map_insert_no_resize_back t self key value st with
| Fail -> Fail
- | Return (st0, hm) ->
- begin match hashmap_hash_map_len_fwd t hm st0 with
+ | Return (st0, self0) ->
+ begin match hashmap_hash_map_len_fwd t self0 st0 with
| Fail -> Fail
| Return (st1, i) ->
- if i > hm.hashmap_hash_map_max_load
+ if i > self0.hashmap_hash_map_max_load
then
begin match
hashmap_hash_map_try_resize_back t (Mkhashmap_hash_map_t
- hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor
- hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1 with
+ self0.hashmap_hash_map_num_entries
+ self0.hashmap_hash_map_max_load_factor
+ self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots)
+ st1 with
| Fail -> Fail
- | Return (st2, hm0) -> Return (st2, hm0)
+ | Return (st2, self1) -> Return (st2, self1)
end
else
- Return (st1, Mkhashmap_hash_map_t hm.hashmap_hash_map_num_entries
- hm.hashmap_hash_map_max_load_factor hm.hashmap_hash_map_max_load
- hm.hashmap_hash_map_slots)
+ Return (st1, Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries
+ self0.hashmap_hash_map_max_load_factor
+ self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots)
end
end
@@ -630,7 +639,7 @@ let rec hashmap_hash_map_get_mut_in_list_back
else
begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret st with
| Fail -> Fail
- | Return (st0, l) -> Return (st0, HashmapListCons ckey cvalue l)
+ | Return (st0, ls1) -> Return (st0, HashmapListCons ckey cvalue ls1)
end
| HashmapListNil -> Fail
end
@@ -740,7 +749,7 @@ let rec hashmap_hash_map_remove_from_list_back
else
begin match hashmap_hash_map_remove_from_list_back t key tl st with
| Fail -> Fail
- | Return (st0, l) -> Return (st0, HashmapListCons ckey x l)
+ | Return (st0, tl0) -> Return (st0, HashmapListCons ckey x tl0)
end
| HashmapListNil -> Return (st, HashmapListNil)
end
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-02 10:27:03 +0000