From f3e16bb43a8ff27a5184d9fa452277cc6a59410f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 19 Mar 2024 05:29:29 +0100
Subject: Regenerate the tests

---
 tests/coq/hashmap/Hashmap_Funs.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'tests/coq/hashmap')

diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 0478edbe..ab424e42 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -398,9 +398,7 @@ Definition hashMap_get_mut_in_list
   (T : Type) (n : nat) (ls : List_t T) (key : usize) :
   result (T * (T -> result (List_t T)))
   :=
-  p <- hashMap_get_mut_in_list_loop T n ls key;
-  let (t, back_'a) := p in
-  Return (t, back_'a)
+  hashMap_get_mut_in_list_loop T n ls key
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::get_mut]:
-- 
cgit v1.2.3


From 5e99d127e0a746f5779779756fccf79f15c19d10 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 20 Mar 2024 06:17:41 +0100
Subject: Regenerate the code

---
 tests/coq/hashmap/Hashmap_Funs.v | 26 ++++++++++++--------------
 1 file changed, 12 insertions(+), 14 deletions(-)

(limited to 'tests/coq/hashmap')

diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index ab424e42..d709a8d5 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -26,9 +26,9 @@ Fixpoint hashMap_allocate_slots_loop
   | S n2 =>
     if n1 s> 0%usize
     then (
-      v <- alloc_vec_Vec_push (List_t T) slots List_Nil;
+      slots1 <- alloc_vec_Vec_push (List_t T) slots List_Nil;
       n3 <- usize_sub n1 1%usize;
-      hashMap_allocate_slots_loop T n2 v n3)
+      hashMap_allocate_slots_loop T n2 slots1 n3)
     else Return slots
   end
 .
@@ -190,8 +190,8 @@ Fixpoint hashMap_move_elements_from_list_loop
   | S n1 =>
     match ls with
     | List_Cons k v tl =>
-      hm <- hashMap_insert_no_resize T n1 ntable k v;
-      hashMap_move_elements_from_list_loop T n1 hm tl
+      ntable1 <- hashMap_insert_no_resize T n1 ntable k v;
+      hashMap_move_elements_from_list_loop T n1 ntable1 tl
     | List_Nil => Return ntable
     end
   end
@@ -224,12 +224,10 @@ Fixpoint hashMap_move_elements_loop
           (core_slice_index_SliceIndexUsizeSliceTInst (List_t T)) slots i;
       let (l, index_mut_back) := p in
       let (ls, l1) := core_mem_replace (List_t T) l List_Nil in
-      hm <- hashMap_move_elements_from_list T n1 ntable ls;
+      ntable1 <- hashMap_move_elements_from_list T n1 ntable ls;
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back l1;
-      back_'a <- hashMap_move_elements_loop T n1 hm slots1 i2;
-      let (hm1, v) := back_'a in
-      Return (hm1, v))
+      hashMap_move_elements_loop T n1 ntable1 slots1 i2)
     else Return (ntable, slots)
   end
 .
@@ -241,9 +239,7 @@ Definition hashMap_move_elements
   (slots : alloc_vec_Vec (List_t T)) (i : usize) :
   result ((HashMap_t T) * (alloc_vec_Vec (List_t T)))
   :=
-  back_'a <- hashMap_move_elements_loop T n ntable slots i;
-  let (hm, v) := back_'a in
-  Return (hm, v)
+  hashMap_move_elements_loop T n ntable slots i
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::try_resize]:
@@ -284,9 +280,11 @@ Definition hashMap_insert
   (T : Type) (n : nat) (self : HashMap_t T) (key : usize) (value : T) :
   result (HashMap_t T)
   :=
-  hm <- hashMap_insert_no_resize T n self key value;
-  i <- hashMap_len T hm;
-  if i s> hm.(hashMap_max_load) then hashMap_try_resize T n hm else Return hm
+  self1 <- hashMap_insert_no_resize T n self key value;
+  i <- hashMap_len T self1;
+  if i s> self1.(hashMap_max_load)
+  then hashMap_try_resize T n self1
+  else Return self1
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
-- 
cgit v1.2.3