summaryrefslogtreecommitdiff
path: root/tests/coq/hashmap
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v37
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v36
2 files changed, 36 insertions, 37 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 1245c654..6bc82677 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -49,7 +49,7 @@ Definition hash_map_new_with_capacity_fwd
i0 <- usize_div i max_load_divisor;
Return
{|
- Hash_map_num_entries := (0%usize);
+ Hash_map_num_entries := 0%usize;
Hash_map_max_load_factor := (max_load_dividend, max_load_divisor);
Hash_map_max_load := i0;
Hash_map_slots := slots
@@ -58,7 +58,7 @@ Definition hash_map_new_with_capacity_fwd
(** [hashmap::HashMap::{0}::new] *)
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)
+ hash_map_new_with_capacity_fwd T n 32%usize 4%usize 5%usize
.
(** [hashmap::HashMap::{0}::clear] *)
@@ -82,10 +82,10 @@ Fixpoint hash_map_clear_loop_fwd_back
(** [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_loop_fwd_back T n self.(Hash_map_slots) (0%usize);
+ v <- hash_map_clear_loop_fwd_back T n self.(Hash_map_slots) 0%usize;
Return
{|
- Hash_map_num_entries := (0%usize);
+ Hash_map_num_entries := 0%usize;
Hash_map_max_load_factor := self.(Hash_map_max_load_factor);
Hash_map_max_load := self.(Hash_map_max_load);
Hash_map_slots := v
@@ -186,7 +186,7 @@ Definition hash_map_insert_no_resize_fwd_back
.
(** [core::num::u32::{9}::MAX] *)
-Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
+Definition core_num_u32_max_body : result u32 := Return 4294967295%u32.
Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
(** [hashmap::HashMap::{0}::move_elements_from_list] *)
@@ -259,8 +259,7 @@ Definition hash_map_try_resize_fwd_back
i2 <- usize_mul capacity 2%usize;
ntable <- hash_map_new_with_capacity_fwd T n i2 i i0;
p <-
- hash_map_move_elements_fwd_back T n ntable self.(Hash_map_slots)
- (0%usize);
+ hash_map_move_elements_fwd_back T n ntable self.(Hash_map_slots) 0%usize;
let (ntable0, _) := p in
Return
{|
@@ -546,36 +545,36 @@ Definition hash_map_remove_back
(** [hashmap::test1] *)
Definition test1_fwd (n : nat) : result unit :=
hm <- hash_map_new_fwd u64 n;
- hm0 <- hash_map_insert_fwd_back u64 n hm (0%usize) (42%u64);
- hm1 <- hash_map_insert_fwd_back u64 n hm0 (128%usize) (18%u64);
- hm2 <- hash_map_insert_fwd_back u64 n hm1 (1024%usize) (138%u64);
- hm3 <- hash_map_insert_fwd_back u64 n hm2 (1056%usize) (256%u64);
- i <- hash_map_get_fwd u64 n hm3 (128%usize);
+ hm0 <- hash_map_insert_fwd_back u64 n hm 0%usize 42%u64;
+ hm1 <- hash_map_insert_fwd_back u64 n hm0 128%usize 18%u64;
+ hm2 <- hash_map_insert_fwd_back u64 n hm1 1024%usize 138%u64;
+ hm3 <- hash_map_insert_fwd_back u64 n hm2 1056%usize 256%u64;
+ i <- hash_map_get_fwd u64 n hm3 128%usize;
if negb (i s= 18%u64)
then Fail_ Failure
else (
- hm4 <- hash_map_get_mut_back u64 n hm3 (1024%usize) (56%u64);
- i0 <- hash_map_get_fwd u64 n hm4 (1024%usize);
+ hm4 <- hash_map_get_mut_back u64 n hm3 1024%usize 56%u64;
+ i0 <- hash_map_get_fwd u64 n hm4 1024%usize;
if negb (i0 s= 56%u64)
then Fail_ Failure
else (
- x <- hash_map_remove_fwd u64 n hm4 (1024%usize);
+ x <- hash_map_remove_fwd u64 n hm4 1024%usize;
match x with
| None => Fail_ Failure
| Some x0 =>
if negb (x0 s= 56%u64)
then Fail_ Failure
else (
- hm5 <- hash_map_remove_back u64 n hm4 (1024%usize);
- i1 <- hash_map_get_fwd u64 n hm5 (0%usize);
+ hm5 <- hash_map_remove_back u64 n hm4 1024%usize;
+ i1 <- hash_map_get_fwd u64 n hm5 0%usize;
if negb (i1 s= 42%u64)
then Fail_ Failure
else (
- i2 <- hash_map_get_fwd u64 n hm5 (128%usize);
+ i2 <- hash_map_get_fwd u64 n hm5 128%usize;
if negb (i2 s= 18%u64)
then Fail_ Failure
else (
- i3 <- hash_map_get_fwd u64 n hm5 (1056%usize);
+ i3 <- hash_map_get_fwd u64 n hm5 1056%usize;
if negb (i3 s= 256%u64) then Fail_ Failure else Return tt)))
end))
.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 804f466a..2d1bcda6 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -51,7 +51,7 @@ Definition hashmap_hash_map_new_with_capacity_fwd
i0 <- usize_div i max_load_divisor;
Return
{|
- Hashmap_hash_map_num_entries := (0%usize);
+ Hashmap_hash_map_num_entries := 0%usize;
Hashmap_hash_map_max_load_factor := (max_load_dividend, max_load_divisor);
Hashmap_hash_map_max_load := i0;
Hashmap_hash_map_slots := slots
@@ -61,7 +61,7 @@ Definition hashmap_hash_map_new_with_capacity_fwd
(** [hashmap_main::hashmap::HashMap::{0}::new] *)
Definition hashmap_hash_map_new_fwd
(T : Type) (n : nat) : result (Hashmap_hash_map_t T) :=
- hashmap_hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize)
+ hashmap_hash_map_new_with_capacity_fwd T n 32%usize 4%usize 5%usize
.
(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
@@ -89,10 +89,10 @@ Definition hashmap_hash_map_clear_fwd_back
:=
v <-
hashmap_hash_map_clear_loop_fwd_back T n self.(Hashmap_hash_map_slots)
- (0%usize);
+ 0%usize;
Return
{|
- Hashmap_hash_map_num_entries := (0%usize);
+ Hashmap_hash_map_num_entries := 0%usize;
Hashmap_hash_map_max_load_factor :=
self.(Hashmap_hash_map_max_load_factor);
Hashmap_hash_map_max_load := self.(Hashmap_hash_map_max_load);
@@ -204,7 +204,7 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back
.
(** [core::num::u32::{9}::MAX] *)
-Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
+Definition core_num_u32_max_body : result u32 := Return 4294967295%u32.
Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
@@ -283,7 +283,7 @@ Definition hashmap_hash_map_try_resize_fwd_back
ntable <- hashmap_hash_map_new_with_capacity_fwd T n i2 i i0;
p <-
hashmap_hash_map_move_elements_fwd_back T n ntable
- self.(Hashmap_hash_map_slots) (0%usize);
+ self.(Hashmap_hash_map_slots) 0%usize;
let (ntable0, _) := p in
Return
{|
@@ -602,36 +602,36 @@ Definition hashmap_hash_map_remove_back
(** [hashmap_main::hashmap::test1] *)
Definition hashmap_test1_fwd (n : nat) : result unit :=
hm <- hashmap_hash_map_new_fwd u64 n;
- hm0 <- hashmap_hash_map_insert_fwd_back u64 n hm (0%usize) (42%u64);
- hm1 <- hashmap_hash_map_insert_fwd_back u64 n hm0 (128%usize) (18%u64);
- hm2 <- hashmap_hash_map_insert_fwd_back u64 n hm1 (1024%usize) (138%u64);
- hm3 <- hashmap_hash_map_insert_fwd_back u64 n hm2 (1056%usize) (256%u64);
- i <- hashmap_hash_map_get_fwd u64 n hm3 (128%usize);
+ hm0 <- hashmap_hash_map_insert_fwd_back u64 n hm 0%usize 42%u64;
+ hm1 <- hashmap_hash_map_insert_fwd_back u64 n hm0 128%usize 18%u64;
+ hm2 <- hashmap_hash_map_insert_fwd_back u64 n hm1 1024%usize 138%u64;
+ hm3 <- hashmap_hash_map_insert_fwd_back u64 n hm2 1056%usize 256%u64;
+ i <- hashmap_hash_map_get_fwd u64 n hm3 128%usize;
if negb (i s= 18%u64)
then Fail_ Failure
else (
- hm4 <- hashmap_hash_map_get_mut_back u64 n hm3 (1024%usize) (56%u64);
- i0 <- hashmap_hash_map_get_fwd u64 n hm4 (1024%usize);
+ hm4 <- hashmap_hash_map_get_mut_back u64 n hm3 1024%usize 56%u64;
+ i0 <- hashmap_hash_map_get_fwd u64 n hm4 1024%usize;
if negb (i0 s= 56%u64)
then Fail_ Failure
else (
- x <- hashmap_hash_map_remove_fwd u64 n hm4 (1024%usize);
+ x <- hashmap_hash_map_remove_fwd u64 n hm4 1024%usize;
match x with
| None => Fail_ Failure
| Some x0 =>
if negb (x0 s= 56%u64)
then Fail_ Failure
else (
- hm5 <- hashmap_hash_map_remove_back u64 n hm4 (1024%usize);
- i1 <- hashmap_hash_map_get_fwd u64 n hm5 (0%usize);
+ hm5 <- hashmap_hash_map_remove_back u64 n hm4 1024%usize;
+ i1 <- hashmap_hash_map_get_fwd u64 n hm5 0%usize;
if negb (i1 s= 42%u64)
then Fail_ Failure
else (
- i2 <- hashmap_hash_map_get_fwd u64 n hm5 (128%usize);
+ i2 <- hashmap_hash_map_get_fwd u64 n hm5 128%usize;
if negb (i2 s= 18%u64)
then Fail_ Failure
else (
- i3 <- hashmap_hash_map_get_fwd u64 n hm5 (1056%usize);
+ i3 <- hashmap_hash_map_get_fwd u64 n hm5 1056%usize;
if negb (i3 s= 256%u64) then Fail_ Failure else Return tt)))
end))
.
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 14:56:48 +0000