diff options
Diffstat (limited to 'tests/lean')
| -rw-r--r-- | tests/lean/Arrays.lean | 13 | ||||
| -rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 136 | ||||
| -rw-r--r-- | tests/lean/Demo/Demo.lean | 6 | ||||
| -rw-r--r-- | tests/lean/External/Funs.lean | 6 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Funs.lean | 29 | ||||
| -rw-r--r-- | tests/lean/HashmapMain/Funs.lean | 29 | ||||
| -rw-r--r-- | tests/lean/Loops.lean | 24 | ||||
| -rw-r--r-- | tests/lean/NoNestedBorrows.lean | 8 | ||||
| -rw-r--r-- | tests/lean/Paper.lean | 4 |
9 files changed, 119 insertions, 136 deletions
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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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 () |