summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap_on_disk
diff options
context:
space:
mode:
authorSon Ho2022-12-17 12:55:40 +0100
committerSon HO2023-02-03 11:21:46 +0100
commitacdfede396a36723258e0a6d7b264cec9ca99672 (patch)
tree9ac729846efb96491bb35e03aca7d8796f50285d /tests/fstar/hashmap_on_disk
parent01a95c7da8cc0c937d94e6a9bc753d2ceb163c17 (diff)
Regenerate the files
Diffstat (limited to 'tests/fstar/hashmap_on_disk')
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst83
1 files changed, 14 insertions, 69 deletions
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index d6da4562..c4f2b039 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -25,11 +25,7 @@ let rec hashmap_hash_map_allocate_slots_fwd
| Return slots0 ->
begin match usize_sub n 1 with
| Fail e -> Fail e
- | Return i ->
- begin match hashmap_hash_map_allocate_slots_fwd t slots0 i with
- | Fail e -> Fail e
- | Return v -> Return v
- end
+ | Return i -> hashmap_hash_map_allocate_slots_fwd t slots0 i
end
end
@@ -57,10 +53,7 @@ let hashmap_hash_map_new_with_capacity_fwd
(** [hashmap_main::hashmap::HashMap::{0}::new] *)
let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
- begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 with
- | Fail e -> Fail e
- | Return hm -> Return hm
- end
+ hashmap_hash_map_new_with_capacity_fwd t 32 4 5
(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
let rec hashmap_hash_map_clear_slots_fwd_back
@@ -77,11 +70,7 @@ let rec hashmap_hash_map_clear_slots_fwd_back
| Return slots0 ->
begin match usize_add i 1 with
| Fail e -> Fail e
- | Return i1 ->
- begin match hashmap_hash_map_clear_slots_fwd_back t slots0 i1 with
- | Fail e -> Fail e
- | Return slots1 -> Return slots1
- end
+ | Return i1 -> hashmap_hash_map_clear_slots_fwd_back t slots0 i1
end
end
else Return slots
@@ -112,11 +101,7 @@ let rec hashmap_hash_map_insert_in_list_fwd
| HashmapListCons ckey cvalue ls0 ->
if ckey = key
then Return false
- else
- begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 with
- | Fail e -> Fail e
- | Return b -> Return b
- end
+ else hashmap_hash_map_insert_in_list_fwd t key value ls0
| HashmapListNil -> Return true
end
@@ -213,11 +198,7 @@ let rec hashmap_hash_map_move_elements_from_list_fwd_back
begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with
| Fail e -> Fail e
| Return ntable0 ->
- begin match
- hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl with
- | Fail e -> Fail e
- | Return ntable1 -> Return ntable1
- end
+ hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl
end
| HashmapListNil -> Return ntable
end
@@ -247,11 +228,7 @@ let rec hashmap_hash_map_move_elements_fwd_back
begin match usize_add i 1 with
| Fail e -> Fail e
| Return i1 ->
- begin match
- hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1 with
- | Fail e -> Fail e
- | Return (ntable1, slots1) -> Return (ntable1, slots1)
- end
+ hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1
end
end
end
@@ -310,11 +287,7 @@ let hashmap_hash_map_insert_fwd_back
| Fail e -> Fail e
| Return i ->
if i > self0.hashmap_hash_map_max_load
- then
- begin match hashmap_hash_map_try_resize_fwd_back t self0 with
- | Fail e -> Fail e
- | Return self1 -> Return self1
- end
+ then hashmap_hash_map_try_resize_fwd_back t self0
else Return self0
end
end
@@ -329,11 +302,7 @@ let rec hashmap_hash_map_contains_key_in_list_fwd
| HashmapListCons ckey x ls0 ->
if ckey = key
then Return true
- else
- begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 with
- | Fail e -> Fail e
- | Return b -> Return b
- end
+ else hashmap_hash_map_contains_key_in_list_fwd t key ls0
| HashmapListNil -> Return false
end
@@ -351,11 +320,7 @@ let hashmap_hash_map_contains_key_fwd
vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
with
| Fail e -> Fail e
- | Return l ->
- begin match hashmap_hash_map_contains_key_in_list_fwd t key l with
- | Fail e -> Fail e
- | Return b -> Return b
- end
+ | Return l -> hashmap_hash_map_contains_key_in_list_fwd t key l
end
end
end
@@ -369,11 +334,7 @@ let rec hashmap_hash_map_get_in_list_fwd
| HashmapListCons ckey cvalue ls0 ->
if ckey = key
then Return cvalue
- else
- begin match hashmap_hash_map_get_in_list_fwd t key ls0 with
- | Fail e -> Fail e
- | Return x -> Return x
- end
+ else hashmap_hash_map_get_in_list_fwd t key ls0
| HashmapListNil -> Fail Failure
end
@@ -391,11 +352,7 @@ let hashmap_hash_map_get_fwd
vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
with
| Fail e -> Fail e
- | Return l ->
- begin match hashmap_hash_map_get_in_list_fwd t key l with
- | Fail e -> Fail e
- | Return x -> Return x
- end
+ | Return l -> hashmap_hash_map_get_in_list_fwd t key l
end
end
end
@@ -410,11 +367,7 @@ let rec hashmap_hash_map_get_mut_in_list_fwd
| HashmapListCons ckey cvalue ls0 ->
if ckey = key
then Return cvalue
- else
- begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 with
- | Fail e -> Fail e
- | Return x -> Return x
- end
+ else hashmap_hash_map_get_mut_in_list_fwd t key ls0
| HashmapListNil -> Fail Failure
end
@@ -450,11 +403,7 @@ let hashmap_hash_map_get_mut_fwd
vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
hash_mod with
| Fail e -> Fail e
- | Return l ->
- begin match hashmap_hash_map_get_mut_in_list_fwd t key l with
- | Fail e -> Fail e
- | Return x -> Return x
- end
+ | Return l -> hashmap_hash_map_get_mut_in_list_fwd t key l
end
end
end
@@ -510,11 +459,7 @@ let rec hashmap_hash_map_remove_from_list_fwd
| HashmapListCons i cvalue tl0 -> Return (Some cvalue)
| HashmapListNil -> Fail Failure
end
- else
- begin match hashmap_hash_map_remove_from_list_fwd t key tl with
- | Fail e -> Fail e
- | Return opt -> Return opt
- end
+ else hashmap_hash_map_remove_from_list_fwd t key tl
| HashmapListNil -> Return None
end