diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 36 |
1 files changed, 18 insertions, 18 deletions
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)) . |