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/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 6 ++----
1 file changed, 2 insertions(+), 4 deletions(-)
(limited to 'tests/fstar/hashmap_on_disk')
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index b16dcada..9b5baaeb 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -324,8 +324,7 @@ let hashmap_HashMap_get_mut_in_list
(t : Type0) (ls : hashmap_List_t t) (key : usize) :
result (t & (t -> result (hashmap_List_t t)))
=
- let* (x, back_'a) = hashmap_HashMap_get_mut_in_list_loop t ls key in
- Return (x, back_'a)
+ hashmap_HashMap_get_mut_in_list_loop t ls key
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
Source: 'src/hashmap.rs', lines 257:4-257:67 *)
@@ -446,8 +445,7 @@ let insert_on_disk
(key : usize) (value : u64) (st : state) : result (state & unit) =
let* (st1, hm) = hashmap_utils_deserialize st in
let* hm1 = hashmap_HashMap_insert u64 hm key value in
- let* (st2, _) = hashmap_utils_serialize hm1 st1 in
- Return (st2, ())
+ hashmap_utils_serialize hm1 st1
(** [hashmap_main::main]:
Source: 'src/hashmap_main.rs', lines 16:0-16:13 *)
--
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/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 27 ++++++++++++------------
1 file changed, 13 insertions(+), 14 deletions(-)
(limited to 'tests/fstar/hashmap_on_disk')
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 9b5baaeb..97f4151f 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -22,9 +22,10 @@ let rec hashmap_HashMap_allocate_slots_loop
=
if n > 0
then
- let* v = alloc_vec_Vec_push (hashmap_List_t t) slots Hashmap_List_Nil in
+ let* slots1 = alloc_vec_Vec_push (hashmap_List_t t) slots Hashmap_List_Nil
+ in
let* n1 = usize_sub n 1 in
- hashmap_HashMap_allocate_slots_loop t v n1
+ hashmap_HashMap_allocate_slots_loop t slots1 n1
else Return slots
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]:
@@ -149,8 +150,8 @@ let rec hashmap_HashMap_move_elements_from_list_loop
=
begin match ls with
| Hashmap_List_Cons k v tl ->
- let* hm = hashmap_HashMap_insert_no_resize t ntable k v in
- hashmap_HashMap_move_elements_from_list_loop t hm tl
+ let* ntable1 = hashmap_HashMap_insert_no_resize t ntable k v in
+ hashmap_HashMap_move_elements_from_list_loop t ntable1 tl
| Hashmap_List_Nil -> Return ntable
end
@@ -178,12 +179,10 @@ let rec hashmap_HashMap_move_elements_loop
(core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) slots i
in
let (ls, l1) = core_mem_replace (hashmap_List_t t) l Hashmap_List_Nil in
- let* hm = hashmap_HashMap_move_elements_from_list t ntable ls in
+ let* ntable1 = hashmap_HashMap_move_elements_from_list t ntable ls in
let* i2 = usize_add i 1 in
let* slots1 = index_mut_back l1 in
- let* back_'a = hashmap_HashMap_move_elements_loop t hm slots1 i2 in
- let (hm1, v) = back_'a in
- Return (hm1, v)
+ hashmap_HashMap_move_elements_loop t ntable1 slots1 i2
else Return (ntable, slots)
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]:
@@ -193,9 +192,7 @@ let hashmap_HashMap_move_elements
(slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) :
result ((hashmap_HashMap_t t) & (alloc_vec_Vec (hashmap_List_t t)))
=
- let* back_'a = hashmap_HashMap_move_elements_loop t ntable slots i in
- let (hm, v) = back_'a in
- Return (hm, v)
+ hashmap_HashMap_move_elements_loop t ntable slots i
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]:
Source: 'src/hashmap.rs', lines 140:4-140:28 *)
@@ -223,9 +220,11 @@ let hashmap_HashMap_insert
(t : Type0) (self : hashmap_HashMap_t t) (key : usize) (value : t) :
result (hashmap_HashMap_t t)
=
- let* hm = hashmap_HashMap_insert_no_resize t self key value in
- let* i = hashmap_HashMap_len t hm in
- if i > hm.max_load then hashmap_HashMap_try_resize t hm else Return hm
+ let* self1 = hashmap_HashMap_insert_no_resize t self key value in
+ let* i = hashmap_HashMap_len t self1 in
+ if i > self1.max_load
+ then hashmap_HashMap_try_resize t self1
+ else Return self1
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
Source: 'src/hashmap.rs', lines 206:4-219:5 *)
--
cgit v1.2.3