summaryrefslogtreecommitdiff
path: root/tests/coq
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v14
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v18
2 files changed, 10 insertions, 22 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 0d55b171..f1af0c21 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -55,8 +55,8 @@ Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) :=
hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize)
.
-(** [hashmap::HashMap::{0}::clear_slots] *)
-Fixpoint hash_map_clear_slots_loop_fwd_back
+(** [hashmap::HashMap::{0}::clear] *)
+Fixpoint hash_map_clear_loop_fwd_back
(T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) :
result (vec (List_t T))
:=
@@ -68,21 +68,15 @@ Fixpoint hash_map_clear_slots_loop_fwd_back
then (
i1 <- usize_add i 1%usize;
slots0 <- vec_index_mut_back (List_t T) slots i ListNil;
- hash_map_clear_slots_loop_fwd_back T n0 slots0 i1)
+ hash_map_clear_loop_fwd_back T n0 slots0 i1)
else Return slots
end
.
-(** [hashmap::HashMap::{0}::clear_slots] *)
-Definition hash_map_clear_slots_fwd_back
- (T : Type) (n : nat) (slots : vec (List_t T)) : result (vec (List_t T)) :=
- hash_map_clear_slots_loop_fwd_back T n slots (0%usize)
-.
-
(** [hashmap::HashMap::{0}::clear] *)
Definition hash_map_clear_fwd_back
(T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
- v <- hash_map_clear_slots_fwd_back T n self.(Hash_map_slots);
+ v <- hash_map_clear_loop_fwd_back T n self.(Hash_map_slots) (0%usize);
Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor)
self.(Hash_map_max_load) v)
.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 670e527a..7c86dbe1 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -58,8 +58,8 @@ Definition hashmap_hash_map_new_fwd
hashmap_hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize)
.
-(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
-Fixpoint hashmap_hash_map_clear_slots_loop_fwd_back
+(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+Fixpoint hashmap_hash_map_clear_loop_fwd_back
(T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) :
result (vec (Hashmap_list_t T))
:=
@@ -71,25 +71,19 @@ Fixpoint hashmap_hash_map_clear_slots_loop_fwd_back
then (
i1 <- usize_add i 1%usize;
slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil;
- hashmap_hash_map_clear_slots_loop_fwd_back T n0 slots0 i1)
+ hashmap_hash_map_clear_loop_fwd_back T n0 slots0 i1)
else Return slots
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
-Definition hashmap_hash_map_clear_slots_fwd_back
- (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) :
- result (vec (Hashmap_list_t T))
- :=
- hashmap_hash_map_clear_slots_loop_fwd_back T n slots (0%usize)
-.
-
(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
Definition hashmap_hash_map_clear_fwd_back
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
result (Hashmap_hash_map_t T)
:=
- v <- hashmap_hash_map_clear_slots_fwd_back T n self.(Hashmap_hash_map_slots);
+ v <-
+ hashmap_hash_map_clear_loop_fwd_back T n self.(Hashmap_hash_map_slots)
+ (0%usize);
Return (mkHashmap_hash_map_t (0%usize)
self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) v)
.