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/arrays/Arrays.v | 10 +- tests/coq/betree/BetreeMain_Funs.v | 140 ++++++++++---------- tests/coq/demo/Demo.v | 2 +- tests/coq/hashmap/Hashmap_Funs.v | 26 ++-- tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 28 ++-- tests/coq/misc/External_Funs.v | 6 +- tests/coq/misc/Loops.v | 22 ++-- tests/coq/misc/NoNestedBorrows.v | 9 +- tests/coq/misc/Paper.v | 2 +- tests/fstar/arrays/Arrays.Funs.fst | 10 +- tests/fstar/betree/BetreeMain.Funs.fst | 141 +++++++++++---------- .../fstar/betree_back_stateful/BetreeMain.Funs.fst | 141 +++++++++++---------- tests/fstar/demo/Demo.fst | 2 +- tests/fstar/hashmap/Hashmap.Funs.fst | 24 ++-- tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 27 ++-- tests/fstar/misc/External.Funs.fst | 4 +- tests/fstar/misc/Loops.Clauses.Template.fst | 3 +- tests/fstar/misc/Loops.Funs.fst | 24 ++-- tests/fstar/misc/NoNestedBorrows.fst | 7 +- tests/fstar/misc/Paper.fst | 2 +- tests/lean/Arrays.lean | 13 +- tests/lean/BetreeMain/Funs.lean | 136 ++++++++++---------- tests/lean/Demo/Demo.lean | 6 +- tests/lean/External/Funs.lean | 6 +- tests/lean/Hashmap/Funs.lean | 29 ++--- tests/lean/HashmapMain/Funs.lean | 29 ++--- tests/lean/Loops.lean | 24 ++-- tests/lean/NoNestedBorrows.lean | 8 +- tests/lean/Paper.lean | 4 +- 29 files changed, 431 insertions(+), 454 deletions(-) (limited to 'tests') 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}::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}::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}::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}::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] *) diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst index 15c82e93..731c7290 100644 --- a/tests/fstar/arrays/Arrays.Funs.fst +++ b/tests/fstar/arrays/Arrays.Funs.fst @@ -28,17 +28,17 @@ let array_to_mut_slice_ (** [arrays::array_len]: Source: 'src/arrays.rs', lines 25:0-25:40 *) let array_len (t : Type0) (s : array t 32) : result usize = - let* s1 = array_to_slice t 32 s in let i = slice_len t s1 in Return i + let* s1 = array_to_slice t 32 s in Return (slice_len t s1) (** [arrays::shared_array_len]: Source: 'src/arrays.rs', lines 29:0-29:48 *) let shared_array_len (t : Type0) (s : array t 32) : result usize = - let* s1 = array_to_slice t 32 s in let i = slice_len t s1 in Return i + let* s1 = array_to_slice t 32 s in Return (slice_len t s1) (** [arrays::shared_slice_len]: Source: 'src/arrays.rs', lines 33:0-33:44 *) let shared_slice_len (t : Type0) (s : slice t) : result usize = - let i = slice_len t s in Return i + Return (slice_len t s) (** [arrays::index_array_shared]: Source: 'src/arrays.rs', lines 37:0-37:57 *) @@ -268,8 +268,8 @@ let update_mut_slice (x : slice u32) : result (slice u32) = let update_all : result unit = let* _ = update_array (mk_array u32 2 [ 0; 0 ]) in let* _ = update_array (mk_array u32 2 [ 0; 0 ]) in - let* a = update_array_mut_borrow (mk_array u32 2 [ 0; 0 ]) in - let* (s, to_slice_mut_back) = array_to_slice_mut u32 2 a in + let* x = update_array_mut_borrow (mk_array u32 2 [ 0; 0 ]) in + let* (s, to_slice_mut_back) = array_to_slice_mut u32 2 x in let* s1 = update_mut_slice s in let* _ = to_slice_mut_back s1 in Return () diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index 74044961..2469f98c 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -170,13 +170,14 @@ let betree_Leaf_split let (content0, content1) = p in let* p1 = betree_List_hd (u64 & u64) content1 in let (pivot, _) = p1 in - let* (id0, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in - let* (id1, nic1) = betree_NodeIdCounter_fresh_id nic in + let* (id0, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in + let* (id1, node_id_cnt2) = betree_NodeIdCounter_fresh_id node_id_cnt1 in let* (st1, _) = betree_store_leaf_node id0 content0 st in let* (st2, _) = betree_store_leaf_node id1 content1 st1 in let n = Betree_Node_Leaf { id = id0; size = params.split_size } in let n1 = Betree_Node_Leaf { id = id1; size = params.split_size } in - Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, nic1)) + Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, + node_id_cnt2)) (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 789:4-792:34 *) @@ -229,21 +230,21 @@ let rec betree_Node_apply_upserts let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in if b then - let* (msg, l) = betree_List_pop_front (u64 & betree_Message_t) msgs in + let* (msg, msgs1) = betree_List_pop_front (u64 & betree_Message_t) msgs in let (_, m) = msg in begin match m with | Betree_Message_Insert _ -> Fail Failure | Betree_Message_Delete -> Fail Failure | Betree_Message_Upsert s -> let* v = betree_upsert_update prev s in - betree_Node_apply_upserts l (Some v) key st + betree_Node_apply_upserts msgs1 (Some v) key st end else let* (st1, v) = core_option_Option_unwrap u64 prev st in - let* l = + let* msgs1 = betree_List_push_front (u64 & betree_Message_t) msgs (key, Betree_Message_Insert v) in - Return (st1, (v, l)) + Return (st1, (v, msgs1)) (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 *) @@ -277,10 +278,11 @@ and betree_Node_lookup let (k, msg) = p in if k <> key then - let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in + let* (st2, (o, node1)) = + betree_Internal_lookup_in_children node key st1 in let* _ = lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l) in - Return (st2, (o, Betree_Node_Internal i)) + Return (st2, (o, Betree_Node_Internal node1)) else begin match msg with | Betree_Message_Insert v -> @@ -294,19 +296,20 @@ and betree_Node_lookup Betree_Message_Delete) l) in Return (st1, (None, Betree_Node_Internal node)) | Betree_Message_Upsert ufs -> - let* (st2, (v, i)) = betree_Internal_lookup_in_children node key st1 - in - let* (st3, (v1, l1)) = + let* (st2, (v, node1)) = + betree_Internal_lookup_in_children node key st1 in + let* (st3, (v1, pending1)) = betree_Node_apply_upserts (Betree_List_Cons (k, Betree_Message_Upsert ufs) l) v key st2 in - let* msgs1 = lookup_first_message_for_key_back l1 in - let* (st4, _) = betree_store_internal_node i.id msgs1 st3 in - Return (st4, (Some v1, Betree_Node_Internal i)) + let* msgs1 = lookup_first_message_for_key_back pending1 in + let* (st4, _) = betree_store_internal_node node1.id msgs1 st3 in + Return (st4, (Some v1, Betree_Node_Internal node1)) end | Betree_List_Nil -> - let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in + let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1 + in let* _ = lookup_first_message_for_key_back Betree_List_Nil in - Return (st2, (o, Betree_Node_Internal i)) + Return (st2, (o, Betree_Node_Internal node1)) end | Betree_Node_Leaf node -> let* (st1, bindings) = betree_load_leaf_node node.id st in @@ -326,10 +329,10 @@ let rec betree_Node_filter_messages_for_key let (k, m) = p in if k = key then - let* (_, l1) = + let* (_, msgs1) = betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m) l) in - betree_Node_filter_messages_for_key key l1 + betree_Node_filter_messages_for_key key msgs1 else Return (Betree_List_Cons (k, m) l) | Betree_List_Nil -> Return Betree_List_Nil end @@ -372,49 +375,51 @@ let betree_Node_apply_to_internal then begin match new_msg with | Betree_Message_Insert i -> - let* l = betree_Node_filter_messages_for_key key msgs1 in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Insert i) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Delete -> - let* l = betree_Node_filter_messages_for_key key msgs1 in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Delete) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Upsert s -> let* p = betree_List_hd (u64 & betree_Message_t) msgs1 in let (_, m) = p in begin match m with | Betree_Message_Insert prev -> let* v = betree_upsert_update (Some prev) s in - let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 + in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Insert v) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Delete -> - let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in + let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 + in let* v = betree_upsert_update None s in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Insert v) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Upsert _ -> let* (msgs2, lookup_first_message_after_key_back) = betree_Node_lookup_first_message_after_key key msgs1 in - let* l = + let* msgs3 = betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Upsert s) in - let* msgs3 = lookup_first_message_after_key_back l in - lookup_first_message_for_key_back msgs3 + let* msgs4 = lookup_first_message_after_key_back msgs3 in + lookup_first_message_for_key_back msgs4 end end else - let* l = + let* msgs2 = betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in - lookup_first_message_for_key_back l + lookup_first_message_for_key_back msgs2 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 *) @@ -427,8 +432,8 @@ let rec betree_Node_apply_messages_to_internal begin match new_msgs with | Betree_List_Cons new_msg new_msgs_tl -> let (i, m) = new_msg in - let* l = betree_Node_apply_to_internal msgs i m in - betree_Node_apply_messages_to_internal l new_msgs_tl + let* msgs1 = betree_Node_apply_to_internal msgs i m in + betree_Node_apply_messages_to_internal msgs1 new_msgs_tl | Betree_List_Nil -> Return msgs end @@ -468,28 +473,28 @@ let betree_Node_apply_to_leaf let* b = betree_ListPairU64T_head_has_key u64 bindings1 key in if b then - let* (hd, l) = betree_List_pop_front (u64 & u64) bindings1 in + let* (hd, bindings2) = betree_List_pop_front (u64 & u64) bindings1 in begin match new_msg with | Betree_Message_Insert v -> - let* l1 = betree_List_push_front (u64 & u64) l (key, v) in - lookup_mut_in_bindings_back l1 - | Betree_Message_Delete -> lookup_mut_in_bindings_back l + let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in + lookup_mut_in_bindings_back bindings3 + | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings2 | Betree_Message_Upsert s -> let (_, i) = hd in let* v = betree_upsert_update (Some i) s in - let* l1 = betree_List_push_front (u64 & u64) l (key, v) in - lookup_mut_in_bindings_back l1 + let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in + lookup_mut_in_bindings_back bindings3 end else begin match new_msg with | Betree_Message_Insert v -> - let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in - lookup_mut_in_bindings_back l + let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in + lookup_mut_in_bindings_back bindings2 | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings1 | Betree_Message_Upsert s -> let* v = betree_upsert_update None s in - let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in - lookup_mut_in_bindings_back l + let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in + lookup_mut_in_bindings_back bindings2 end (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: @@ -503,8 +508,8 @@ let rec betree_Node_apply_messages_to_leaf begin match new_msgs with | Betree_List_Cons new_msg new_msgs_tl -> let (i, m) = new_msg in - let* l = betree_Node_apply_to_leaf bindings i m in - betree_Node_apply_messages_to_leaf l new_msgs_tl + let* bindings1 = betree_Node_apply_to_leaf bindings i m in + betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl | Betree_List_Nil -> Return bindings end @@ -558,31 +563,31 @@ and betree_Node_apply_messages begin match self with | Betree_Node_Internal node -> let* (st1, content) = betree_load_internal_node node.id st in - let* l = betree_Node_apply_messages_to_internal content msgs in - let* num_msgs = betree_List_len (u64 & betree_Message_t) l in + let* content1 = betree_Node_apply_messages_to_internal content msgs in + let* num_msgs = betree_List_len (u64 & betree_Message_t) content1 in if num_msgs >= params.min_flush_size then - let* (st2, (content1, p)) = - betree_Internal_flush node params node_id_cnt l st1 in + let* (st2, (content2, p)) = + betree_Internal_flush node params node_id_cnt content1 st1 in let (node1, node_id_cnt1) = p in - let* (st3, _) = betree_store_internal_node node1.id content1 st2 in + let* (st3, _) = betree_store_internal_node node1.id content2 st2 in Return (st3, (Betree_Node_Internal node1, node_id_cnt1)) else - let* (st2, _) = betree_store_internal_node node.id l st1 in + let* (st2, _) = betree_store_internal_node node.id content1 st1 in Return (st2, (Betree_Node_Internal node, node_id_cnt)) | Betree_Node_Leaf node -> let* (st1, content) = betree_load_leaf_node node.id st in - let* l = betree_Node_apply_messages_to_leaf content msgs in - let* len = betree_List_len (u64 & u64) l in + let* content1 = betree_Node_apply_messages_to_leaf content msgs in + let* len = betree_List_len (u64 & u64) content1 in let* i = u64_mul 2 params.split_size in if len >= i then - let* (st2, (new_node, nic)) = - betree_Leaf_split node l params node_id_cnt st1 in + let* (st2, (new_node, node_id_cnt1)) = + betree_Leaf_split node content1 params node_id_cnt st1 in let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil st2 in - Return (st3, (Betree_Node_Internal new_node, nic)) + Return (st3, (Betree_Node_Internal new_node, node_id_cnt1)) else - let* (st2, _) = betree_store_leaf_node node.id l st1 in + let* (st2, _) = betree_store_leaf_node node.id content1 st1 in Return (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt)) end @@ -607,12 +612,12 @@ let betree_BeTree_new result (state & betree_BeTree_t) = let* node_id_cnt = betree_NodeIdCounter_new in - let* (id, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in + let* (id, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in let* (st1, _) = betree_store_leaf_node id Betree_List_Nil st in Return (st1, { params = { min_flush_size = min_flush_size; split_size = split_size }; - node_id_cnt = nic; + node_id_cnt = node_id_cnt1; root = (Betree_Node_Leaf { id = id; size = 0 }) }) diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 74044961..2469f98c 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -170,13 +170,14 @@ let betree_Leaf_split let (content0, content1) = p in let* p1 = betree_List_hd (u64 & u64) content1 in let (pivot, _) = p1 in - let* (id0, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in - let* (id1, nic1) = betree_NodeIdCounter_fresh_id nic in + let* (id0, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in + let* (id1, node_id_cnt2) = betree_NodeIdCounter_fresh_id node_id_cnt1 in let* (st1, _) = betree_store_leaf_node id0 content0 st in let* (st2, _) = betree_store_leaf_node id1 content1 st1 in let n = Betree_Node_Leaf { id = id0; size = params.split_size } in let n1 = Betree_Node_Leaf { id = id1; size = params.split_size } in - Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, nic1)) + Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, + node_id_cnt2)) (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 789:4-792:34 *) @@ -229,21 +230,21 @@ let rec betree_Node_apply_upserts let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in if b then - let* (msg, l) = betree_List_pop_front (u64 & betree_Message_t) msgs in + let* (msg, msgs1) = betree_List_pop_front (u64 & betree_Message_t) msgs in let (_, m) = msg in begin match m with | Betree_Message_Insert _ -> Fail Failure | Betree_Message_Delete -> Fail Failure | Betree_Message_Upsert s -> let* v = betree_upsert_update prev s in - betree_Node_apply_upserts l (Some v) key st + betree_Node_apply_upserts msgs1 (Some v) key st end else let* (st1, v) = core_option_Option_unwrap u64 prev st in - let* l = + let* msgs1 = betree_List_push_front (u64 & betree_Message_t) msgs (key, Betree_Message_Insert v) in - Return (st1, (v, l)) + Return (st1, (v, msgs1)) (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 *) @@ -277,10 +278,11 @@ and betree_Node_lookup let (k, msg) = p in if k <> key then - let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in + let* (st2, (o, node1)) = + betree_Internal_lookup_in_children node key st1 in let* _ = lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l) in - Return (st2, (o, Betree_Node_Internal i)) + Return (st2, (o, Betree_Node_Internal node1)) else begin match msg with | Betree_Message_Insert v -> @@ -294,19 +296,20 @@ and betree_Node_lookup Betree_Message_Delete) l) in Return (st1, (None, Betree_Node_Internal node)) | Betree_Message_Upsert ufs -> - let* (st2, (v, i)) = betree_Internal_lookup_in_children node key st1 - in - let* (st3, (v1, l1)) = + let* (st2, (v, node1)) = + betree_Internal_lookup_in_children node key st1 in + let* (st3, (v1, pending1)) = betree_Node_apply_upserts (Betree_List_Cons (k, Betree_Message_Upsert ufs) l) v key st2 in - let* msgs1 = lookup_first_message_for_key_back l1 in - let* (st4, _) = betree_store_internal_node i.id msgs1 st3 in - Return (st4, (Some v1, Betree_Node_Internal i)) + let* msgs1 = lookup_first_message_for_key_back pending1 in + let* (st4, _) = betree_store_internal_node node1.id msgs1 st3 in + Return (st4, (Some v1, Betree_Node_Internal node1)) end | Betree_List_Nil -> - let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in + let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1 + in let* _ = lookup_first_message_for_key_back Betree_List_Nil in - Return (st2, (o, Betree_Node_Internal i)) + Return (st2, (o, Betree_Node_Internal node1)) end | Betree_Node_Leaf node -> let* (st1, bindings) = betree_load_leaf_node node.id st in @@ -326,10 +329,10 @@ let rec betree_Node_filter_messages_for_key let (k, m) = p in if k = key then - let* (_, l1) = + let* (_, msgs1) = betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m) l) in - betree_Node_filter_messages_for_key key l1 + betree_Node_filter_messages_for_key key msgs1 else Return (Betree_List_Cons (k, m) l) | Betree_List_Nil -> Return Betree_List_Nil end @@ -372,49 +375,51 @@ let betree_Node_apply_to_internal then begin match new_msg with | Betree_Message_Insert i -> - let* l = betree_Node_filter_messages_for_key key msgs1 in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Insert i) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Delete -> - let* l = betree_Node_filter_messages_for_key key msgs1 in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Delete) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Upsert s -> let* p = betree_List_hd (u64 & betree_Message_t) msgs1 in let (_, m) = p in begin match m with | Betree_Message_Insert prev -> let* v = betree_upsert_update (Some prev) s in - let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 + in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Insert v) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Delete -> - let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in + let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 + in let* v = betree_upsert_update None s in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Insert v) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Upsert _ -> let* (msgs2, lookup_first_message_after_key_back) = betree_Node_lookup_first_message_after_key key msgs1 in - let* l = + let* msgs3 = betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Upsert s) in - let* msgs3 = lookup_first_message_after_key_back l in - lookup_first_message_for_key_back msgs3 + let* msgs4 = lookup_first_message_after_key_back msgs3 in + lookup_first_message_for_key_back msgs4 end end else - let* l = + let* msgs2 = betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in - lookup_first_message_for_key_back l + lookup_first_message_for_key_back msgs2 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 *) @@ -427,8 +432,8 @@ let rec betree_Node_apply_messages_to_internal begin match new_msgs with | Betree_List_Cons new_msg new_msgs_tl -> let (i, m) = new_msg in - let* l = betree_Node_apply_to_internal msgs i m in - betree_Node_apply_messages_to_internal l new_msgs_tl + let* msgs1 = betree_Node_apply_to_internal msgs i m in + betree_Node_apply_messages_to_internal msgs1 new_msgs_tl | Betree_List_Nil -> Return msgs end @@ -468,28 +473,28 @@ let betree_Node_apply_to_leaf let* b = betree_ListPairU64T_head_has_key u64 bindings1 key in if b then - let* (hd, l) = betree_List_pop_front (u64 & u64) bindings1 in + let* (hd, bindings2) = betree_List_pop_front (u64 & u64) bindings1 in begin match new_msg with | Betree_Message_Insert v -> - let* l1 = betree_List_push_front (u64 & u64) l (key, v) in - lookup_mut_in_bindings_back l1 - | Betree_Message_Delete -> lookup_mut_in_bindings_back l + let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in + lookup_mut_in_bindings_back bindings3 + | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings2 | Betree_Message_Upsert s -> let (_, i) = hd in let* v = betree_upsert_update (Some i) s in - let* l1 = betree_List_push_front (u64 & u64) l (key, v) in - lookup_mut_in_bindings_back l1 + let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in + lookup_mut_in_bindings_back bindings3 end else begin match new_msg with | Betree_Message_Insert v -> - let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in - lookup_mut_in_bindings_back l + let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in + lookup_mut_in_bindings_back bindings2 | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings1 | Betree_Message_Upsert s -> let* v = betree_upsert_update None s in - let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in - lookup_mut_in_bindings_back l + let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in + lookup_mut_in_bindings_back bindings2 end (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: @@ -503,8 +508,8 @@ let rec betree_Node_apply_messages_to_leaf begin match new_msgs with | Betree_List_Cons new_msg new_msgs_tl -> let (i, m) = new_msg in - let* l = betree_Node_apply_to_leaf bindings i m in - betree_Node_apply_messages_to_leaf l new_msgs_tl + let* bindings1 = betree_Node_apply_to_leaf bindings i m in + betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl | Betree_List_Nil -> Return bindings end @@ -558,31 +563,31 @@ and betree_Node_apply_messages begin match self with | Betree_Node_Internal node -> let* (st1, content) = betree_load_internal_node node.id st in - let* l = betree_Node_apply_messages_to_internal content msgs in - let* num_msgs = betree_List_len (u64 & betree_Message_t) l in + let* content1 = betree_Node_apply_messages_to_internal content msgs in + let* num_msgs = betree_List_len (u64 & betree_Message_t) content1 in if num_msgs >= params.min_flush_size then - let* (st2, (content1, p)) = - betree_Internal_flush node params node_id_cnt l st1 in + let* (st2, (content2, p)) = + betree_Internal_flush node params node_id_cnt content1 st1 in let (node1, node_id_cnt1) = p in - let* (st3, _) = betree_store_internal_node node1.id content1 st2 in + let* (st3, _) = betree_store_internal_node node1.id content2 st2 in Return (st3, (Betree_Node_Internal node1, node_id_cnt1)) else - let* (st2, _) = betree_store_internal_node node.id l st1 in + let* (st2, _) = betree_store_internal_node node.id content1 st1 in Return (st2, (Betree_Node_Internal node, node_id_cnt)) | Betree_Node_Leaf node -> let* (st1, content) = betree_load_leaf_node node.id st in - let* l = betree_Node_apply_messages_to_leaf content msgs in - let* len = betree_List_len (u64 & u64) l in + let* content1 = betree_Node_apply_messages_to_leaf content msgs in + let* len = betree_List_len (u64 & u64) content1 in let* i = u64_mul 2 params.split_size in if len >= i then - let* (st2, (new_node, nic)) = - betree_Leaf_split node l params node_id_cnt st1 in + let* (st2, (new_node, node_id_cnt1)) = + betree_Leaf_split node content1 params node_id_cnt st1 in let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil st2 in - Return (st3, (Betree_Node_Internal new_node, nic)) + Return (st3, (Betree_Node_Internal new_node, node_id_cnt1)) else - let* (st2, _) = betree_store_leaf_node node.id l st1 in + let* (st2, _) = betree_store_leaf_node node.id content1 st1 in Return (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt)) end @@ -607,12 +612,12 @@ let betree_BeTree_new result (state & betree_BeTree_t) = let* node_id_cnt = betree_NodeIdCounter_new in - let* (id, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in + let* (id, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in let* (st1, _) = betree_store_leaf_node id Betree_List_Nil st in Return (st1, { params = { min_flush_size = min_flush_size; split_size = split_size }; - node_id_cnt = nic; + node_id_cnt = node_id_cnt1; root = (Betree_Node_Leaf { id = id; size = 0 }) }) diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst index 4ad7cb65..d93bc847 100644 --- a/tests/fstar/demo/Demo.fst +++ b/tests/fstar/demo/Demo.fst @@ -31,7 +31,7 @@ let incr (x : u32) : result u32 = (** [demo::use_incr]: Source: 'src/demo.rs', lines 25:0-25:17 *) let use_incr : result unit = - let* i = incr 0 in let* i1 = incr i in let* _ = incr i1 in Return () + let* x = incr 0 in let* x1 = incr x in let* _ = incr x1 in Return () (** [demo::CList] Source: 'src/demo.rs', lines 34:0-34:17 *) diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 7ca8b9c1..fba711f1 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -21,9 +21,9 @@ let rec hashMap_allocate_slots_loop = if n > 0 then - let* v = alloc_vec_Vec_push (list_t t) slots List_Nil in + let* slots1 = alloc_vec_Vec_push (list_t t) slots List_Nil in let* n1 = usize_sub n 1 in - hashMap_allocate_slots_loop t v n1 + hashMap_allocate_slots_loop t slots1 n1 else Return slots (** [hashmap::{hashmap::HashMap}::allocate_slots]: @@ -142,8 +142,8 @@ let rec hashMap_move_elements_from_list_loop = begin match ls with | List_Cons k v tl -> - let* hm = hashMap_insert_no_resize t ntable k v in - hashMap_move_elements_from_list_loop t hm tl + let* ntable1 = hashMap_insert_no_resize t ntable k v in + hashMap_move_elements_from_list_loop t ntable1 tl | List_Nil -> Return ntable end @@ -168,12 +168,10 @@ let rec hashMap_move_elements_loop alloc_vec_Vec_index_mut (list_t t) usize (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) slots i in let (ls, l1) = core_mem_replace (list_t t) l List_Nil in - let* hm = hashMap_move_elements_from_list t ntable ls in + let* ntable1 = 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_move_elements_loop t hm slots1 i2 in - let (hm1, v) = back_'a in - Return (hm1, v) + hashMap_move_elements_loop t ntable1 slots1 i2 else Return (ntable, slots) (** [hashmap::{hashmap::HashMap}::move_elements]: @@ -183,9 +181,7 @@ let hashMap_move_elements (i : usize) : result ((hashMap_t t) & (alloc_vec_Vec (list_t t))) = - let* back_'a = hashMap_move_elements_loop t ntable slots i in - let (hm, v) = back_'a in - Return (hm, v) + hashMap_move_elements_loop t ntable slots i (** [hashmap::{hashmap::HashMap}::try_resize]: Source: 'src/hashmap.rs', lines 140:4-140:28 *) @@ -213,9 +209,9 @@ let hashMap_insert (t : Type0) (self : hashMap_t t) (key : usize) (value : t) : result (hashMap_t t) = - let* hm = hashMap_insert_no_resize t self key value in - let* i = hashMap_len t hm in - if i > hm.max_load then hashMap_try_resize t hm else Return hm + let* self1 = hashMap_insert_no_resize t self key value in + let* i = hashMap_len t self1 in + if i > self1.max_load then hashMap_try_resize t self1 else Return self1 (** [hashmap::{hashmap::HashMap}::contains_key_in_list]: loop 0: Source: 'src/hashmap.rs', lines 206:4-219:5 *) 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}::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}::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}::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}::contains_key_in_list]: loop 0: Source: 'src/hashmap.rs', lines 206:4-219:5 *) diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index 6672b523..3ba20022 100644 --- a/tests/fstar/misc/External.Funs.fst +++ b/tests/fstar/misc/External.Funs.fst @@ -33,8 +33,8 @@ let custom_swap (t : Type0) (x : t) (y : t) (st : state) : result (state & (t & (t -> state -> result (state & (t & t))))) = - let* (st1, (x1, x2)) = core_mem_swap t x y st in - let back_'a = fun ret st2 -> Return (st2, (ret, x2)) in + let* (st1, (x1, y1)) = core_mem_swap t x y st in + let back_'a = fun ret st2 -> Return (st2, (ret, y1)) in Return (st1, (x1, back_'a)) (** [external::test_custom_swap]: diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst index c8ed16f4..e43f8170 100644 --- a/tests/fstar/misc/Loops.Clauses.Template.fst +++ b/tests/fstar/misc/Loops.Clauses.Template.fst @@ -13,8 +13,7 @@ unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit () (** [loops::sum_with_mut_borrows]: decreases clause Source: 'src/loops.rs', lines 19:0-31:1 *) unfold -let sum_with_mut_borrows_loop_decreases (max : u32) (mi : u32) (ms : u32) : nat - = +let sum_with_mut_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit () (** [loops::sum_with_shared_borrows]: decreases clause diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index c87f693b..7c099da2 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -25,15 +25,15 @@ let sum (max : u32) : result u32 = (** [loops::sum_with_mut_borrows]: loop 0: Source: 'src/loops.rs', lines 19:0-31:1 *) let rec sum_with_mut_borrows_loop - (max : u32) (mi : u32) (ms : u32) : - Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms)) + (max : u32) (i : u32) (s : u32) : + Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max i s)) = - if mi < max + if i < max then - let* ms1 = u32_add ms mi in - let* mi1 = u32_add mi 1 in - sum_with_mut_borrows_loop max mi1 ms1 - else u32_mul ms 2 + let* ms = u32_add s i in + let* mi = u32_add i 1 in + sum_with_mut_borrows_loop max mi ms + else u32_mul s 2 (** [loops::sum_with_mut_borrows]: Source: 'src/loops.rs', lines 19:0-19:44 *) @@ -185,11 +185,11 @@ let get_elem_mut (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result (usize & (usize -> result (alloc_vec_Vec (list_t usize)))) = - let* (l, index_mut_back) = + let* (ls, index_mut_back) = alloc_vec_Vec_index_mut (list_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in - let* (i, back) = get_elem_mut_loop x l in - let back1 = fun ret -> let* l1 = back ret in index_mut_back l1 in + let* (i, back) = get_elem_mut_loop x ls in + let back1 = fun ret -> let* l = back ret in index_mut_back l in Return (i, back1) (** [loops::get_elem_shared]: loop 0: @@ -207,10 +207,10 @@ let rec get_elem_shared_loop Source: 'src/loops.rs', lines 129:0-129:68 *) let get_elem_shared (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = - let* l = + let* ls = alloc_vec_Vec_index (list_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in - get_elem_shared_loop x l + get_elem_shared_loop x ls (** [loops::id_mut]: Source: 'src/loops.rs', lines 145:0-145:50 *) diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index c71f8dbb..db63eb0d 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -425,8 +425,7 @@ let id_mut_pair1 (t1 t2 : Type0) (x : t1) (y : t2) : result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2))) = - let back_'a = fun ret -> let (x1, x2) = ret in Return (x1, x2) in - Return ((x, y), back_'a) + Return ((x, y), Return) (** [no_nested_borrows::id_mut_pair2]: Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 *) @@ -434,9 +433,7 @@ let id_mut_pair2 (t1 t2 : Type0) (p : (t1 & t2)) : result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2))) = - let (x, x1) = p in - let back_'a = fun ret -> let (x2, x3) = ret in Return (x2, x3) in - Return ((x, x1), back_'a) + let (x, x1) = p in Return ((x, x1), Return) (** [no_nested_borrows::id_mut_pair3]: Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 *) diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst index cf4dc454..ddc5e7a8 100644 --- a/tests/fstar/misc/Paper.fst +++ b/tests/fstar/misc/Paper.fst @@ -13,7 +13,7 @@ let ref_incr (x : i32) : result i32 = (** [paper::test_incr]: Source: 'src/paper.rs', lines 8:0-8:18 *) let test_incr : result unit = - let* i = ref_incr 0 in if not (i = 1) then Fail Failure else Return () + let* x = ref_incr 0 in if not (x = 1) then Fail Failure else Return () (** Unit test for [paper::test_incr] *) let _ = assert_norm (test_incr = Return ()) diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index cd1b6544..207f31b9 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -35,22 +35,19 @@ def array_to_mut_slice_ def array_len (T : Type) (s : Array T 32#usize) : Result Usize := do let s1 ← Array.to_slice T 32#usize s - let i := Slice.len T s1 - Result.ret i + Result.ret (Slice.len T s1) /- [arrays::shared_array_len]: Source: 'src/arrays.rs', lines 29:0-29:48 -/ def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize := do let s1 ← Array.to_slice T 32#usize s - let i := Slice.len T s1 - Result.ret i + Result.ret (Slice.len T s1) /- [arrays::shared_slice_len]: Source: 'src/arrays.rs', lines 33:0-33:44 -/ def shared_slice_len (T : Type) (s : Slice T) : Result Usize := - let i := Slice.len T s - Result.ret i + Result.ret (Slice.len T s) /- [arrays::index_array_shared]: Source: 'src/arrays.rs', lines 37:0-37:57 -/ @@ -305,8 +302,8 @@ def update_all : Result Unit := do let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let a ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize a + let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize x let s1 ← update_mut_slice s let _ ← to_slice_mut_back s1 Result.ret () diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index bd5921a8..ca9b48da 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -168,13 +168,13 @@ def betree.Leaf.split let (content0, content1) := p let p1 ← betree.List.hd (U64 × U64) content1 let (pivot, _) := p1 - let (id0, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt - let (id1, nic1) ← betree.NodeIdCounter.fresh_id nic + let (id0, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt + let (id1, node_id_cnt2) ← betree.NodeIdCounter.fresh_id node_id_cnt1 let (st1, _) ← betree.store_leaf_node id0 content0 st let (st2, _) ← betree.store_leaf_node id1 content1 st1 let n := betree.Node.Leaf { id := id0, size := params.split_size } let n1 := betree.Node.Leaf { id := id1, size := params.split_size } - Result.ret (st2, (betree.Internal.mk self.id pivot n n1, nic1)) + Result.ret (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2)) /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 789:4-792:34 -/ @@ -227,7 +227,7 @@ divergent def betree.Node.apply_upserts if b then do - let (msg, l) ← betree.List.pop_front (U64 × betree.Message) msgs + let (msg, msgs1) ← betree.List.pop_front (U64 × betree.Message) msgs let (_, m) := msg match m with | betree.Message.Insert _ => Result.fail .panic @@ -235,14 +235,14 @@ divergent def betree.Node.apply_upserts | betree.Message.Upsert s => do let v ← betree.upsert_update prev s - betree.Node.apply_upserts l (some v) key st + betree.Node.apply_upserts msgs1 (some v) key st else do let (st1, v) ← core.option.Option.unwrap U64 prev st - let l ← + let msgs1 ← betree.List.push_front (U64 × betree.Message) msgs (key, betree.Message.Insert v) - Result.ret (st1, (v, l)) + Result.ret (st1, (v, msgs1)) /- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 -/ @@ -280,12 +280,12 @@ divergent def betree.Node.lookup if k != key then do - let (st2, (o, i2)) ← + let (st2, (o, node1)) ← betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key st1 let _ ← lookup_first_message_for_key_back (betree.List.Cons (k, msg) l) - Result.ret (st2, (o, betree.Node.Internal i2)) + Result.ret (st2, (o, betree.Node.Internal node1)) else match msg with | betree.Message.Insert v => @@ -304,24 +304,24 @@ divergent def betree.Node.lookup n n1))) | betree.Message.Upsert ufs => do - let (st2, (v, i2)) ← + let (st2, (v, node1)) ← betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key st1 - let (st3, (v1, l1)) ← + let (st3, (v1, pending1)) ← betree.Node.apply_upserts (betree.List.Cons (k, betree.Message.Upsert ufs) l) v key st2 - let ⟨ i3, i4, n2, n3 ⟩ := i2 - let msgs1 ← lookup_first_message_for_key_back l1 - let (st4, _) ← betree.store_internal_node i3 msgs1 st3 + let ⟨ i2, i3, n2, n3 ⟩ := node1 + let msgs1 ← lookup_first_message_for_key_back pending1 + let (st4, _) ← betree.store_internal_node i2 msgs1 st3 Result.ret (st4, (some v1, betree.Node.Internal (betree.Internal.mk - i3 i4 n2 n3))) + i2 i3 n2 n3))) | betree.List.Nil => do - let (st2, (o, i2)) ← + let (st2, (o, node1)) ← betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key st1 let _ ← lookup_first_message_for_key_back betree.List.Nil - Result.ret (st2, (o, betree.Node.Internal i2)) + Result.ret (st2, (o, betree.Node.Internal node1)) | betree.Node.Leaf node => do let (st1, bindings) ← betree.load_leaf_node node.id st @@ -342,10 +342,10 @@ divergent def betree.Node.filter_messages_for_key if k = key then do - let (_, l1) ← + let (_, msgs1) ← betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m) l) - betree.Node.filter_messages_for_key key l1 + betree.Node.filter_messages_for_key key msgs1 else Result.ret (betree.List.Cons (k, m) l) | betree.List.Nil => Result.ret betree.List.Nil @@ -389,18 +389,18 @@ def betree.Node.apply_to_internal match new_msg with | betree.Message.Insert i => do - let l ← betree.Node.filter_messages_for_key key msgs1 - let l1 ← - betree.List.push_front (U64 × betree.Message) l (key, + let msgs2 ← betree.Node.filter_messages_for_key key msgs1 + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, betree.Message.Insert i) - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | betree.Message.Delete => do - let l ← betree.Node.filter_messages_for_key key msgs1 - let l1 ← - betree.List.push_front (U64 × betree.Message) l (key, + let msgs2 ← betree.Node.filter_messages_for_key key msgs1 + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, betree.Message.Delete) - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | betree.Message.Upsert s => do let p ← betree.List.hd (U64 × betree.Message) msgs1 @@ -409,33 +409,33 @@ def betree.Node.apply_to_internal | betree.Message.Insert prev => do let v ← betree.upsert_update (some prev) s - let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1 - let l1 ← - betree.List.push_front (U64 × betree.Message) l (key, + let (_, msgs2) ← betree.List.pop_front (U64 × betree.Message) msgs1 + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, betree.Message.Insert v) - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | betree.Message.Delete => do - let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1 + let (_, msgs2) ← betree.List.pop_front (U64 × betree.Message) msgs1 let v ← betree.upsert_update none s - let l1 ← - betree.List.push_front (U64 × betree.Message) l (key, + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, betree.Message.Insert v) - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | betree.Message.Upsert _ => do let (msgs2, lookup_first_message_after_key_back) ← betree.Node.lookup_first_message_after_key key msgs1 - let l ← + let msgs3 ← betree.List.push_front (U64 × betree.Message) msgs2 (key, betree.Message.Upsert s) - let msgs3 ← lookup_first_message_after_key_back l - lookup_first_message_for_key_back msgs3 + let msgs4 ← lookup_first_message_after_key_back msgs3 + lookup_first_message_for_key_back msgs4 else do - let l ← + let msgs2 ← betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg) - lookup_first_message_for_key_back l + lookup_first_message_for_key_back msgs2 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 -/ @@ -448,8 +448,8 @@ divergent def betree.Node.apply_messages_to_internal | betree.List.Cons new_msg new_msgs_tl => do let (i, m) := new_msg - let l ← betree.Node.apply_to_internal msgs i m - betree.Node.apply_messages_to_internal l new_msgs_tl + let msgs1 ← betree.Node.apply_to_internal msgs i m + betree.Node.apply_messages_to_internal msgs1 new_msgs_tl | betree.List.Nil => Result.ret msgs /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: @@ -490,31 +490,31 @@ def betree.Node.apply_to_leaf if b then do - let (hd, l) ← betree.List.pop_front (U64 × U64) bindings1 + let (hd, bindings2) ← betree.List.pop_front (U64 × U64) bindings1 match new_msg with | betree.Message.Insert v => do - let 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 + let 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 => do let (_, i) := hd let v ← betree.upsert_update (some i) s - let l1 ← betree.List.push_front (U64 × U64) l (key, v) - lookup_mut_in_bindings_back l1 + let bindings3 ← betree.List.push_front (U64 × U64) bindings2 (key, v) + lookup_mut_in_bindings_back bindings3 else match new_msg with | betree.Message.Insert v => do - let l ← betree.List.push_front (U64 × U64) bindings1 (key, v) - lookup_mut_in_bindings_back l + let 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 => do let v ← betree.upsert_update none s - let l ← betree.List.push_front (U64 × U64) bindings1 (key, v) - lookup_mut_in_bindings_back l + let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v) + lookup_mut_in_bindings_back bindings2 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: Source: 'src/betree.rs', lines 444:4-447:5 -/ @@ -527,8 +527,8 @@ divergent def betree.Node.apply_messages_to_leaf | betree.List.Cons new_msg new_msgs_tl => do let (i, m) := new_msg - let l ← betree.Node.apply_to_leaf bindings i m - betree.Node.apply_messages_to_leaf l new_msgs_tl + let bindings1 ← betree.Node.apply_to_leaf bindings i m + betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl | betree.List.Nil => Result.ret bindings /- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: @@ -583,40 +583,40 @@ divergent def betree.Node.apply_messages do let ⟨ i, i1, n, n1 ⟩ := node let (st1, content) ← betree.load_internal_node i st - let l ← betree.Node.apply_messages_to_internal content msgs - let num_msgs ← betree.List.len (U64 × betree.Message) l + let content1 ← betree.Node.apply_messages_to_internal content msgs + let num_msgs ← betree.List.len (U64 × betree.Message) content1 if num_msgs >= params.min_flush_size then do - let (st2, (content1, p)) ← + let (st2, (content2, p)) ← betree.Internal.flush (betree.Internal.mk i i1 n n1) params node_id_cnt - l st1 + content1 st1 let (node1, node_id_cnt1) := p let ⟨ i2, i3, n2, n3 ⟩ := node1 - let (st3, _) ← betree.store_internal_node i2 content1 st2 + let (st3, _) ← betree.store_internal_node i2 content2 st2 Result.ret (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3), node_id_cnt1)) else do - let (st2, _) ← betree.store_internal_node i l st1 + let (st2, _) ← betree.store_internal_node i content1 st1 Result.ret (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1), node_id_cnt)) | betree.Node.Leaf node => do let (st1, content) ← betree.load_leaf_node node.id st - let l ← betree.Node.apply_messages_to_leaf content msgs - let len ← betree.List.len (U64 × U64) l + let content1 ← betree.Node.apply_messages_to_leaf content msgs + let len ← betree.List.len (U64 × U64) content1 let i ← 2#u64 * params.split_size if len >= i then do - let (st2, (new_node, nic)) ← - betree.Leaf.split node l params node_id_cnt st1 + let (st2, (new_node, node_id_cnt1)) ← + betree.Leaf.split node content1 params node_id_cnt st1 let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2 - Result.ret (st3, (betree.Node.Internal new_node, nic)) + Result.ret (st3, (betree.Node.Internal new_node, node_id_cnt1)) else do - let (st2, _) ← betree.store_leaf_node node.id l st1 + let (st2, _) ← betree.store_leaf_node node.id content1 st1 Result.ret (st2, (betree.Node.Leaf { node with size := len }, node_id_cnt)) @@ -645,12 +645,12 @@ def betree.BeTree.new := do let node_id_cnt ← betree.NodeIdCounter.new - let (id, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt + let (id, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt let (st1, _) ← betree.store_leaf_node id betree.List.Nil st Result.ret (st1, { params := { min_flush_size := min_flush_size, split_size := split_size }, - node_id_cnt := nic, + node_id_cnt := node_id_cnt1, root := (betree.Node.Leaf { id := id, size := 0#u64 }) }) diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 09032820..4acc69c8 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -40,9 +40,9 @@ def incr (x : U32) : Result U32 := Source: 'src/demo.rs', lines 25:0-25:17 -/ def use_incr : Result Unit := do - let i ← incr 0#u32 - let i1 ← incr i - let _ ← incr i1 + let x ← incr 0#u32 + let x1 ← incr x + let _ ← incr x1 Result.ret () /- [demo::CList] diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index db15aacc..8b645037 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -38,9 +38,9 @@ def custom_swap Result (State × (T × (T → State → Result (State × (T × T))))) := do - let (st1, (t, t1)) ← core.mem.swap T x y st - let back_'a := fun ret st2 => Result.ret (st2, (ret, t1)) - Result.ret (st1, (t, back_'a)) + let (st1, (x1, y1)) ← core.mem.swap T x y st + let back_'a := fun ret st2 => Result.ret (st2, (ret, y1)) + Result.ret (st1, (x1, back_'a)) /- [external::test_custom_swap]: Source: 'src/external.rs', lines 29:0-29:59 -/ diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index d33b6571..1c95f7c9 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -20,9 +20,9 @@ divergent def HashMap.allocate_slots_loop if n > 0#usize then do - let v ← alloc.vec.Vec.push (List T) slots List.Nil + let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil let n1 ← n - 1#usize - HashMap.allocate_slots_loop T v n1 + HashMap.allocate_slots_loop T slots1 n1 else Result.ret slots /- [hashmap::{hashmap::HashMap}::allocate_slots]: @@ -142,8 +142,8 @@ divergent def HashMap.move_elements_from_list_loop match ls with | List.Cons k v tl => do - let hm ← HashMap.insert_no_resize T ntable k v - HashMap.move_elements_from_list_loop T hm tl + let ntable1 ← HashMap.insert_no_resize T ntable k v + HashMap.move_elements_from_list_loop T ntable1 tl | List.Nil => Result.ret ntable /- [hashmap::{hashmap::HashMap}::move_elements_from_list]: @@ -167,12 +167,10 @@ divergent def HashMap.move_elements_loop alloc.vec.Vec.index_mut (List T) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i let (ls, l1) := core.mem.replace (List T) l List.Nil - let hm ← HashMap.move_elements_from_list T ntable ls + let ntable1 ← HashMap.move_elements_from_list T ntable ls let i2 ← i + 1#usize let slots1 ← index_mut_back l1 - let back_'a ← HashMap.move_elements_loop T hm slots1 i2 - let (hm1, v) := back_'a - Result.ret (hm1, v) + HashMap.move_elements_loop T ntable1 slots1 i2 else Result.ret (ntable, slots) /- [hashmap::{hashmap::HashMap}::move_elements]: @@ -182,10 +180,7 @@ def HashMap.move_elements : Result ((HashMap T) × (alloc.vec.Vec (List T))) := - do - let back_'a ← HashMap.move_elements_loop T ntable slots i - let (hm, v) := back_'a - Result.ret (hm, v) + HashMap.move_elements_loop T ntable slots i /- [hashmap::{hashmap::HashMap}::try_resize]: Source: 'src/hashmap.rs', lines 140:4-140:28 -/ @@ -218,11 +213,11 @@ def HashMap.insert Result (HashMap T) := do - let hm ← HashMap.insert_no_resize T self key value - let i ← HashMap.len T hm - if i > hm.max_load - then HashMap.try_resize T hm - else Result.ret hm + let self1 ← HashMap.insert_no_resize T self key value + let i ← HashMap.len T self1 + if i > self1.max_load + then HashMap.try_resize T self1 + else Result.ret self1 /- [hashmap::{hashmap::HashMap}::contains_key_in_list]: loop 0: Source: 'src/hashmap.rs', lines 206:4-219:5 -/ diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index 8a277700..6a6934b8 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -21,9 +21,9 @@ divergent def hashmap.HashMap.allocate_slots_loop if n > 0#usize then do - let v ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil + let slots1 ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil let n1 ← n - 1#usize - hashmap.HashMap.allocate_slots_loop T v n1 + hashmap.HashMap.allocate_slots_loop T slots1 n1 else Result.ret slots /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: @@ -150,8 +150,8 @@ divergent def hashmap.HashMap.move_elements_from_list_loop match ls with | hashmap.List.Cons k v tl => do - let hm ← hashmap.HashMap.insert_no_resize T ntable k v - hashmap.HashMap.move_elements_from_list_loop T hm tl + let ntable1 ← hashmap.HashMap.insert_no_resize T ntable k v + hashmap.HashMap.move_elements_from_list_loop T ntable1 tl | hashmap.List.Nil => Result.ret ntable /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements_from_list]: @@ -177,12 +177,10 @@ divergent def hashmap.HashMap.move_elements_loop alloc.vec.Vec.index_mut (hashmap.List T) Usize (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) slots i let (ls, l1) := core.mem.replace (hashmap.List T) l hashmap.List.Nil - let hm ← hashmap.HashMap.move_elements_from_list T ntable ls + let ntable1 ← hashmap.HashMap.move_elements_from_list T ntable ls let i2 ← i + 1#usize let slots1 ← index_mut_back l1 - let back_'a ← hashmap.HashMap.move_elements_loop T hm slots1 i2 - let (hm1, v) := back_'a - Result.ret (hm1, v) + hashmap.HashMap.move_elements_loop T ntable1 slots1 i2 else Result.ret (ntable, slots) /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements]: @@ -192,10 +190,7 @@ def hashmap.HashMap.move_elements (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) : Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T))) := - do - let back_'a ← hashmap.HashMap.move_elements_loop T ntable slots i - let (hm, v) := back_'a - Result.ret (hm, v) + hashmap.HashMap.move_elements_loop T ntable slots i /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::try_resize]: Source: 'src/hashmap.rs', lines 140:4-140:28 -/ @@ -229,11 +224,11 @@ def hashmap.HashMap.insert Result (hashmap.HashMap T) := do - let hm ← hashmap.HashMap.insert_no_resize T self key value - let i ← hashmap.HashMap.len T hm - if i > hm.max_load - then hashmap.HashMap.try_resize T hm - else Result.ret hm + let self1 ← hashmap.HashMap.insert_no_resize T self key value + let i ← hashmap.HashMap.len T self1 + if i > self1.max_load + then hashmap.HashMap.try_resize T self1 + else Result.ret self1 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: loop 0: Source: 'src/hashmap.rs', lines 206:4-219:5 -/ diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index 3f075347..0f3d77c2 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -23,14 +23,14 @@ def sum (max : U32) : Result U32 := /- [loops::sum_with_mut_borrows]: loop 0: Source: 'src/loops.rs', lines 19:0-31:1 -/ divergent def sum_with_mut_borrows_loop - (max : U32) (mi : U32) (ms : U32) : Result U32 := - if mi < max + (max : U32) (i : U32) (s : U32) : Result U32 := + if i < max then do - let ms1 ← ms + mi - let mi1 ← mi + 1#u32 - sum_with_mut_borrows_loop max mi1 ms1 - else ms * 2#u32 + let ms ← s + i + let mi ← i + 1#u32 + sum_with_mut_borrows_loop max mi ms + else s * 2#u32 /- [loops::sum_with_mut_borrows]: Source: 'src/loops.rs', lines 19:0-19:44 -/ @@ -187,13 +187,13 @@ def get_elem_mut Result (Usize × (Usize → Result (alloc.vec.Vec (List Usize)))) := do - let (l, index_mut_back) ← + let (ls, index_mut_back) ← alloc.vec.Vec.index_mut (List Usize) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize - let (i, back) ← get_elem_mut_loop x l + let (i, back) ← get_elem_mut_loop x ls let back1 := fun ret => do - let l1 ← back ret - index_mut_back l1 + let l ← back ret + index_mut_back l Result.ret (i, back1) /- [loops::get_elem_shared]: loop 0: @@ -211,10 +211,10 @@ divergent def get_elem_shared_loop def get_elem_shared (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize := do - let l ← + let ls ← alloc.vec.Vec.index (List Usize) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize - get_elem_shared_loop x l + get_elem_shared_loop x ls /- [loops::id_mut]: Source: 'src/loops.rs', lines 145:0-145:50 -/ diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index 2112e282..5f9ec0f2 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -487,9 +487,7 @@ def id_mut_pair1 (T1 T2 : Type) (x : T1) (y : T2) : Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2))) := - let back_'a := fun ret => let (t, t1) := ret - Result.ret (t, t1) - Result.ret ((x, y), back_'a) + Result.ret ((x, y), Result.ret) /- [no_nested_borrows::id_mut_pair2]: Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 -/ @@ -498,9 +496,7 @@ def id_mut_pair2 Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2))) := let (t, t1) := p - let back_'a := fun ret => let (t2, t3) := ret - Result.ret (t2, t3) - Result.ret ((t, t1), back_'a) + Result.ret ((t, t1), Result.ret) /- [no_nested_borrows::id_mut_pair3]: Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 -/ diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index 4930a05c..924ff36c 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -14,8 +14,8 @@ def ref_incr (x : I32) : Result I32 := Source: 'src/paper.rs', lines 8:0-8:18 -/ def test_incr : Result Unit := do - let i ← ref_incr 0#i32 - if ¬ (i = 1#i32) + let x ← ref_incr 0#i32 + if ¬ (x = 1#i32) then Result.fail .panic else Result.ret () -- cgit v1.2.3