From df4d60b71bcabf9897656d6d74157a4c7d8d539c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 16 May 2023 11:45:43 +0200
Subject: Make good progress on generating code for HOL4

---
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 36 ++++++++++++++--------------
 1 file changed, 18 insertions(+), 18 deletions(-)

(limited to 'tests/coq/hashmap_on_disk/HashmapMain_Funs.v')

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))
 .
-- 
cgit v1.2.3