summaryrefslogtreecommitdiff
path: root/tests/coq
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq')
-rw-r--r--tests/coq/arrays/Arrays.v10
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v140
-rw-r--r--tests/coq/demo/Demo.v2
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v26
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v28
-rw-r--r--tests/coq/misc/External_Funs.v6
-rw-r--r--tests/coq/misc/Loops.v22
-rw-r--r--tests/coq/misc/NoNestedBorrows.v9
-rw-r--r--tests/coq/misc/Paper.v2
9 files changed, 119 insertions, 126 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 580e72f0..049d63cb 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -36,19 +36,19 @@ Definition array_to_mut_slice_
(** [arrays::array_len]:
Source: 'src/arrays.rs', lines 25:0-25:40 *)
Definition array_len (T : Type) (s : array T 32%usize) : result usize :=
- s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i
+ s1 <- array_to_slice T 32%usize s; Return (slice_len T s1)
.
(** [arrays::shared_array_len]:
Source: 'src/arrays.rs', lines 29:0-29:48 *)
Definition shared_array_len (T : Type) (s : array T 32%usize) : result usize :=
- s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i
+ s1 <- array_to_slice T 32%usize s; Return (slice_len T s1)
.
(** [arrays::shared_slice_len]:
Source: 'src/arrays.rs', lines 33:0-33:44 *)
Definition shared_slice_len (T : Type) (s : slice T) : result usize :=
- let i := slice_len T s in Return i
+ Return (slice_len T s)
.
(** [arrays::index_array_shared]:
@@ -326,8 +326,8 @@ Definition update_mut_slice (x : slice u32) : result (slice u32) :=
Definition update_all : result unit :=
_ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
_ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
- a <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
- p <- array_to_slice_mut u32 2%usize a;
+ x <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
+ p <- array_to_slice_mut u32 2%usize x;
let (s, to_slice_mut_back) := p in
s1 <- update_mut_slice s;
_ <- to_slice_mut_back s1;
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index a0338557..c2cca26d 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -201,9 +201,9 @@ Definition betree_Leaf_split
p1 <- betree_List_hd (u64 * u64) content1;
let (pivot, _) := p1 in
p2 <- betree_NodeIdCounter_fresh_id node_id_cnt;
- let (id0, nic) := p2 in
- p3 <- betree_NodeIdCounter_fresh_id nic;
- let (id1, nic1) := p3 in
+ let (id0, node_id_cnt1) := p2 in
+ p3 <- betree_NodeIdCounter_fresh_id node_id_cnt1;
+ let (id1, node_id_cnt2) := p3 in
p4 <- betree_store_leaf_node id0 content0 st;
let (st1, _) := p4 in
p5 <- betree_store_leaf_node id1 content1 st1;
@@ -218,7 +218,8 @@ Definition betree_Leaf_split
betree_Leaf_id := id1;
betree_Leaf_size := params.(betree_Params_split_size)
|} in
- Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2, nic1))
+ Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2,
+ node_id_cnt2))
.
(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
@@ -286,22 +287,22 @@ Fixpoint betree_Node_apply_upserts
if b
then (
p <- betree_List_pop_front (u64 * betree_Message_t) msgs;
- let (msg, l) := p in
+ let (msg, msgs1) := p in
let (_, m) := msg in
match m with
| Betree_Message_Insert _ => Fail_ Failure
| Betree_Message_Delete => Fail_ Failure
| Betree_Message_Upsert s =>
v <- betree_upsert_update prev s;
- betree_Node_apply_upserts n1 l (Some v) key st
+ betree_Node_apply_upserts n1 msgs1 (Some v) key st
end)
else (
p <- core_option_Option_unwrap u64 prev st;
let (st1, v) := p in
- l <-
+ msgs1 <-
betree_List_push_front (u64 * betree_Message_t) msgs (key,
Betree_Message_Insert v);
- Return (st1, (v, l)))
+ Return (st1, (v, msgs1)))
end
.
@@ -351,9 +352,9 @@ with betree_Node_lookup
then (
p3 <- betree_Internal_lookup_in_children n1 node key st1;
let (st2, p4) := p3 in
- let (o, i) := p4 in
+ let (o, node1) := p4 in
_ <- lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l);
- Return (st2, (o, Betree_Node_Internal i)))
+ Return (st2, (o, Betree_Node_Internal node1)))
else
match msg with
| Betree_Message_Insert v =>
@@ -369,23 +370,24 @@ with betree_Node_lookup
| Betree_Message_Upsert ufs =>
p3 <- betree_Internal_lookup_in_children n1 node key st1;
let (st2, p4) := p3 in
- let (v, i) := p4 in
+ let (v, node1) := p4 in
p5 <-
betree_Node_apply_upserts n1 (Betree_List_Cons (k,
Betree_Message_Upsert ufs) l) v key st2;
let (st3, p6) := p5 in
- let (v1, l1) := p6 in
- msgs1 <- lookup_first_message_for_key_back l1;
- p7 <- betree_store_internal_node i.(betree_Internal_id) msgs1 st3;
+ let (v1, pending1) := p6 in
+ msgs1 <- lookup_first_message_for_key_back pending1;
+ p7 <-
+ betree_store_internal_node node1.(betree_Internal_id) msgs1 st3;
let (st4, _) := p7 in
- Return (st4, (Some v1, Betree_Node_Internal i))
+ Return (st4, (Some v1, Betree_Node_Internal node1))
end
| Betree_List_Nil =>
p2 <- betree_Internal_lookup_in_children n1 node key st1;
let (st2, p3) := p2 in
- let (o, i) := p3 in
+ let (o, node1) := p3 in
_ <- lookup_first_message_for_key_back Betree_List_Nil;
- Return (st2, (o, Betree_Node_Internal i))
+ Return (st2, (o, Betree_Node_Internal node1))
end
| Betree_Node_Leaf node =>
p <- betree_load_leaf_node node.(betree_Leaf_id) st;
@@ -413,8 +415,8 @@ Fixpoint betree_Node_filter_messages_for_key
p1 <-
betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k,
m) l);
- let (_, l1) := p1 in
- betree_Node_filter_messages_for_key n1 key l1)
+ let (_, msgs1) := p1 in
+ betree_Node_filter_messages_for_key n1 key msgs1)
else Return (Betree_List_Cons (k, m) l)
| Betree_List_Nil => Return Betree_List_Nil
end
@@ -463,17 +465,17 @@ Definition betree_Node_apply_to_internal
then
match new_msg with
| Betree_Message_Insert i =>
- l <- betree_Node_filter_messages_for_key n key msgs1;
- l1 <-
- betree_List_push_front (u64 * betree_Message_t) l (key,
+ msgs2 <- betree_Node_filter_messages_for_key n key msgs1;
+ msgs3 <-
+ betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
Betree_Message_Insert i);
- lookup_first_message_for_key_back l1
+ lookup_first_message_for_key_back msgs3
| Betree_Message_Delete =>
- l <- betree_Node_filter_messages_for_key n key msgs1;
- l1 <-
- betree_List_push_front (u64 * betree_Message_t) l (key,
+ msgs2 <- betree_Node_filter_messages_for_key n key msgs1;
+ msgs3 <-
+ betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
Betree_Message_Delete);
- lookup_first_message_for_key_back l1
+ lookup_first_message_for_key_back msgs3
| Betree_Message_Upsert s =>
p1 <- betree_List_hd (u64 * betree_Message_t) msgs1;
let (_, m) := p1 in
@@ -481,32 +483,33 @@ Definition betree_Node_apply_to_internal
| Betree_Message_Insert prev =>
v <- betree_upsert_update (Some prev) s;
p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1;
- let (_, l) := p2 in
- l1 <-
- betree_List_push_front (u64 * betree_Message_t) l (key,
+ let (_, msgs2) := p2 in
+ msgs3 <-
+ betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
Betree_Message_Insert v);
- lookup_first_message_for_key_back l1
+ lookup_first_message_for_key_back msgs3
| Betree_Message_Delete =>
p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1;
- let (_, l) := p2 in
+ let (_, msgs2) := p2 in
v <- betree_upsert_update None s;
- l1 <-
- betree_List_push_front (u64 * betree_Message_t) l (key,
+ msgs3 <-
+ betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
Betree_Message_Insert v);
- lookup_first_message_for_key_back l1
+ lookup_first_message_for_key_back msgs3
| Betree_Message_Upsert _ =>
p2 <- betree_Node_lookup_first_message_after_key n key msgs1;
let (msgs2, lookup_first_message_after_key_back) := p2 in
- l <-
+ msgs3 <-
betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
Betree_Message_Upsert s);
- msgs3 <- lookup_first_message_after_key_back l;
- lookup_first_message_for_key_back msgs3
+ msgs4 <- lookup_first_message_after_key_back msgs3;
+ lookup_first_message_for_key_back msgs4
end
end
else (
- l <- betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg);
- lookup_first_message_for_key_back l)
+ msgs2 <-
+ betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg);
+ lookup_first_message_for_key_back msgs2)
.
(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
@@ -522,8 +525,8 @@ Fixpoint betree_Node_apply_messages_to_internal
match new_msgs with
| Betree_List_Cons new_msg new_msgs_tl =>
let (i, m) := new_msg in
- l <- betree_Node_apply_to_internal n1 msgs i m;
- betree_Node_apply_messages_to_internal n1 l new_msgs_tl
+ msgs1 <- betree_Node_apply_to_internal n1 msgs i m;
+ betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl
| Betree_List_Nil => Return msgs
end
end
@@ -570,28 +573,28 @@ Definition betree_Node_apply_to_leaf
if b
then (
p1 <- betree_List_pop_front (u64 * u64) bindings1;
- let (hd, l) := p1 in
+ let (hd, bindings2) := p1 in
match new_msg with
| Betree_Message_Insert v =>
- l1 <- betree_List_push_front (u64 * u64) l (key, v);
- lookup_mut_in_bindings_back l1
- | Betree_Message_Delete => lookup_mut_in_bindings_back l
+ bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v);
+ lookup_mut_in_bindings_back bindings3
+ | Betree_Message_Delete => lookup_mut_in_bindings_back bindings2
| Betree_Message_Upsert s =>
let (_, i) := hd in
v <- betree_upsert_update (Some i) s;
- l1 <- betree_List_push_front (u64 * u64) l (key, v);
- lookup_mut_in_bindings_back l1
+ bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v);
+ lookup_mut_in_bindings_back bindings3
end)
else
match new_msg with
| Betree_Message_Insert v =>
- l <- betree_List_push_front (u64 * u64) bindings1 (key, v);
- lookup_mut_in_bindings_back l
+ bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v);
+ lookup_mut_in_bindings_back bindings2
| Betree_Message_Delete => lookup_mut_in_bindings_back bindings1
| Betree_Message_Upsert s =>
v <- betree_upsert_update None s;
- l <- betree_List_push_front (u64 * u64) bindings1 (key, v);
- lookup_mut_in_bindings_back l
+ bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v);
+ lookup_mut_in_bindings_back bindings2
end
.
@@ -608,8 +611,8 @@ Fixpoint betree_Node_apply_messages_to_leaf
match new_msgs with
| Betree_List_Cons new_msg new_msgs_tl =>
let (i, m) := new_msg in
- l <- betree_Node_apply_to_leaf n1 bindings i m;
- betree_Node_apply_messages_to_leaf n1 l new_msgs_tl
+ bindings1 <- betree_Node_apply_to_leaf n1 bindings i m;
+ betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl
| Betree_List_Nil => Return bindings
end
end
@@ -680,38 +683,39 @@ with betree_Node_apply_messages
| Betree_Node_Internal node =>
p <- betree_load_internal_node node.(betree_Internal_id) st;
let (st1, content) := p in
- l <- betree_Node_apply_messages_to_internal n1 content msgs;
- num_msgs <- betree_List_len (u64 * betree_Message_t) n1 l;
+ content1 <- betree_Node_apply_messages_to_internal n1 content msgs;
+ num_msgs <- betree_List_len (u64 * betree_Message_t) n1 content1;
if num_msgs s>= params.(betree_Params_min_flush_size)
then (
- p1 <- betree_Internal_flush n1 node params node_id_cnt l st1;
+ p1 <- betree_Internal_flush n1 node params node_id_cnt content1 st1;
let (st2, p2) := p1 in
- let (content1, p3) := p2 in
+ let (content2, p3) := p2 in
let (node1, node_id_cnt1) := p3 in
p4 <-
- betree_store_internal_node node1.(betree_Internal_id) content1 st2;
+ betree_store_internal_node node1.(betree_Internal_id) content2 st2;
let (st3, _) := p4 in
Return (st3, (Betree_Node_Internal node1, node_id_cnt1)))
else (
- p1 <- betree_store_internal_node node.(betree_Internal_id) l st1;
+ p1 <-
+ betree_store_internal_node node.(betree_Internal_id) content1 st1;
let (st2, _) := p1 in
Return (st2, (Betree_Node_Internal node, node_id_cnt)))
| Betree_Node_Leaf node =>
p <- betree_load_leaf_node node.(betree_Leaf_id) st;
let (st1, content) := p in
- l <- betree_Node_apply_messages_to_leaf n1 content msgs;
- len <- betree_List_len (u64 * u64) n1 l;
+ content1 <- betree_Node_apply_messages_to_leaf n1 content msgs;
+ len <- betree_List_len (u64 * u64) n1 content1;
i <- u64_mul 2%u64 params.(betree_Params_split_size);
if len s>= i
then (
- p1 <- betree_Leaf_split n1 node l params node_id_cnt st1;
+ p1 <- betree_Leaf_split n1 node content1 params node_id_cnt st1;
let (st2, p2) := p1 in
- let (new_node, nic) := p2 in
+ let (new_node, node_id_cnt1) := p2 in
p3 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st2;
let (st3, _) := p3 in
- Return (st3, (Betree_Node_Internal new_node, nic)))
+ Return (st3, (Betree_Node_Internal new_node, node_id_cnt1)))
else (
- p1 <- betree_store_leaf_node node.(betree_Leaf_id) l st1;
+ p1 <- betree_store_leaf_node node.(betree_Leaf_id) content1 st1;
let (st2, _) := p1 in
Return (st2, (Betree_Node_Leaf
{| betree_Leaf_id := node.(betree_Leaf_id); betree_Leaf_size := len
@@ -744,7 +748,7 @@ Definition betree_BeTree_new
:=
node_id_cnt <- betree_NodeIdCounter_new;
p <- betree_NodeIdCounter_fresh_id node_id_cnt;
- let (id, nic) := p in
+ let (id, node_id_cnt1) := p in
p1 <- betree_store_leaf_node id Betree_List_Nil st;
let (st1, _) := p1 in
Return (st1,
@@ -754,7 +758,7 @@ Definition betree_BeTree_new
betree_Params_min_flush_size := min_flush_size;
betree_Params_split_size := split_size
|};
- betree_BeTree_node_id_cnt := nic;
+ betree_BeTree_node_id_cnt := node_id_cnt1;
betree_BeTree_root :=
(Betree_Node_Leaf
{| betree_Leaf_id := id; betree_Leaf_size := 0%u64 |})
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 2fccf6c0..d5a6e535 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -37,7 +37,7 @@ Definition incr (x : u32) : result u32 :=
(** [demo::use_incr]:
Source: 'src/demo.rs', lines 25:0-25:17 *)
Definition use_incr : result unit :=
- i <- incr 0%u32; i1 <- incr i; _ <- incr i1; Return tt
+ x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Return tt
.
(** [demo::CList]
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:
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index aff4995f..9fb3c482 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -29,9 +29,9 @@ Fixpoint hashmap_HashMap_allocate_slots_loop
| S n2 =>
if n1 s> 0%usize
then (
- v <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil;
+ slots1 <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil;
n3 <- usize_sub n1 1%usize;
- hashmap_HashMap_allocate_slots_loop T n2 v n3)
+ hashmap_HashMap_allocate_slots_loop T n2 slots1 n3)
else Return slots
end
.
@@ -204,8 +204,8 @@ Fixpoint hashmap_HashMap_move_elements_from_list_loop
| S n1 =>
match ls with
| Hashmap_List_Cons k v tl =>
- hm <- hashmap_HashMap_insert_no_resize T n1 ntable k v;
- hashmap_HashMap_move_elements_from_list_loop T n1 hm tl
+ ntable1 <- hashmap_HashMap_insert_no_resize T n1 ntable k v;
+ hashmap_HashMap_move_elements_from_list_loop T n1 ntable1 tl
| Hashmap_List_Nil => Return ntable
end
end
@@ -239,12 +239,10 @@ Fixpoint hashmap_HashMap_move_elements_loop
i;
let (l, index_mut_back) := p in
let (ls, l1) := core_mem_replace (hashmap_List_t T) l Hashmap_List_Nil in
- hm <- hashmap_HashMap_move_elements_from_list T n1 ntable ls;
+ ntable1 <- hashmap_HashMap_move_elements_from_list T n1 ntable ls;
i2 <- usize_add i 1%usize;
slots1 <- index_mut_back l1;
- back_'a <- hashmap_HashMap_move_elements_loop T n1 hm slots1 i2;
- let (hm1, v) := back_'a in
- Return (hm1, v))
+ hashmap_HashMap_move_elements_loop T n1 ntable1 slots1 i2)
else Return (ntable, slots)
end
.
@@ -256,9 +254,7 @@ Definition 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)))
:=
- back_'a <- hashmap_HashMap_move_elements_loop T n ntable slots i;
- let (hm, v) := back_'a in
- Return (hm, v)
+ hashmap_HashMap_move_elements_loop T n ntable slots i
.
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]:
@@ -304,11 +300,11 @@ Definition hashmap_HashMap_insert
(T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) (value : T) :
result (hashmap_HashMap_t T)
:=
- hm <- hashmap_HashMap_insert_no_resize T n self key value;
- i <- hashmap_HashMap_len T hm;
- if i s> hm.(hashmap_HashMap_max_load)
- then hashmap_HashMap_try_resize T n hm
- else Return hm
+ self1 <- hashmap_HashMap_insert_no_resize T n self key value;
+ i <- hashmap_HashMap_len T self1;
+ if i s> self1.(hashmap_HashMap_max_load)
+ then hashmap_HashMap_try_resize T n self1
+ else Return self1
.
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 91ea88c9..faf91fef 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -45,9 +45,9 @@ Definition custom_swap
:=
p <- core_mem_swap T x y st;
let (st1, p1) := p in
- let (t, t1) := p1 in
- let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, t1)) in
- Return (st1, (t, back_'a))
+ let (x1, y1) := p1 in
+ let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
+ Return (st1, (x1, back_'a))
.
(** [external::test_custom_swap]:
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 85b54510..7c83a014 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -29,16 +29,16 @@ Definition sum (n : nat) (max : u32) : result u32 :=
(** [loops::sum_with_mut_borrows]: loop 0:
Source: 'src/loops.rs', lines 19:0-31:1 *)
Fixpoint sum_with_mut_borrows_loop
- (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
+ (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
match n with
| O => Fail_ OutOfFuel
| S n1 =>
- if mi s< max
+ if i s< max
then (
- ms1 <- u32_add ms mi;
- mi1 <- u32_add mi 1%u32;
- sum_with_mut_borrows_loop n1 max mi1 ms1)
- else u32_mul ms 2%u32
+ ms <- u32_add s i;
+ mi <- u32_add i 1%u32;
+ sum_with_mut_borrows_loop n1 max mi ms)
+ else u32_mul s 2%u32
end
.
@@ -245,10 +245,10 @@ Definition get_elem_mut
p <-
alloc_vec_Vec_index_mut (List_t usize) usize
(core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
- let (l, index_mut_back) := p in
- p1 <- get_elem_mut_loop n x l;
+ let (ls, index_mut_back) := p in
+ p1 <- get_elem_mut_loop n x ls;
let (i, back) := p1 in
- let back1 := fun (ret : usize) => l1 <- back ret; index_mut_back l1 in
+ let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in
Return (i, back1)
.
@@ -273,10 +273,10 @@ Definition get_elem_shared
(n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
result usize
:=
- l <-
+ ls <-
alloc_vec_Vec_index (List_t usize) usize
(core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
- get_elem_shared_loop n x l
+ get_elem_shared_loop n x ls
.
(** [loops::id_mut]:
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 73c4ee58..76dc4cf6 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -475,9 +475,7 @@ Definition id_mut_pair1
(T1 T2 : Type) (x : T1) (y : T2) :
result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
:=
- let back_'a := fun (ret : (T1 * T2)) => let (t, t1) := ret in Return (t, t1)
- in
- Return ((x, y), back_'a)
+ Return ((x, y), Return)
.
(** [no_nested_borrows::id_mut_pair2]:
@@ -486,10 +484,7 @@ Definition id_mut_pair2
(T1 T2 : Type) (p : (T1 * T2)) :
result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
:=
- let (t, t1) := p in
- let back_'a :=
- fun (ret : (T1 * T2)) => let (t2, t3) := ret in Return (t2, t3) in
- Return ((t, t1), back_'a)
+ let (t, t1) := p in Return ((t, t1), Return)
.
(** [no_nested_borrows::id_mut_pair3]:
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 769cf34c..ad77fa2a 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -16,7 +16,7 @@ Definition ref_incr (x : i32) : result i32 :=
(** [paper::test_incr]:
Source: 'src/paper.rs', lines 8:0-8:18 *)
Definition test_incr : result unit :=
- i <- ref_incr 0%i32; if negb (i s= 1%i32) then Fail_ Failure else Return tt
+ x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt
.
(** Unit test for [paper::test_incr] *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-22 00:18:08 +0000