diff options
Diffstat (limited to 'tests/lean')
| -rw-r--r-- | tests/lean/Arrays.lean | 41 | ||||
| -rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 144 | ||||
| -rw-r--r-- | tests/lean/Demo/Demo.lean | 51 | ||||
| -rw-r--r-- | tests/lean/Demo/Properties.lean | 16 | ||||
| -rw-r--r-- | tests/lean/External/Funs.lean | 6 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Funs.lean | 33 | ||||
| -rw-r--r-- | tests/lean/HashmapMain/Funs.lean | 36 | ||||
| -rw-r--r-- | tests/lean/Loops.lean | 76 | ||||
| -rw-r--r-- | tests/lean/NoNestedBorrows.lean | 8 | ||||
| -rw-r--r-- | tests/lean/Paper.lean | 4 |
10 files changed, 199 insertions, 216 deletions
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index d637ee13..207f31b9 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -28,31 +28,26 @@ def array_to_mut_slice_ (T : Type) (s : Array T 32#usize) : Result ((Slice T) × (Slice T → Result (Array T 32#usize))) := - do - let (s1, to_slice_mut_back) ← Array.to_slice_mut T 32#usize s - Result.ret (s1, to_slice_mut_back) + Array.to_slice_mut T 32#usize s /- [arrays::array_len]: Source: 'src/arrays.rs', lines 25:0-25:40 -/ 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 -/ @@ -76,9 +71,7 @@ def index_mut_array (T : Type) (s : Array T 32#usize) (i : Usize) : Result (T × (T → Result (Array T 32#usize))) := - do - let (t, index_mut_back) ← Array.index_mut_usize T 32#usize s i - Result.ret (t, index_mut_back) + Array.index_mut_usize T 32#usize s i /- [arrays::index_slice]: Source: 'src/arrays.rs', lines 56:0-56:46 -/ @@ -91,9 +84,7 @@ def index_mut_slice (T : Type) (s : Slice T) (i : Usize) : Result (T × (T → Result (Slice T))) := - do - let (t, index_mut_back) ← Slice.index_mut_usize T s i - Result.ret (t, index_mut_back) + Slice.index_mut_usize T s i /- [arrays::slice_subslice_shared_]: Source: 'src/arrays.rs', lines 64:0-64:70 -/ @@ -127,9 +118,7 @@ def array_to_slice_mut_ (x : Array U32 32#usize) : Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize))) := - do - let (s, to_slice_mut_back) ← Array.to_slice_mut U32 32#usize x - Result.ret (s, to_slice_mut_back) + Array.to_slice_mut U32 32#usize x /- [arrays::array_subslice_shared_]: Source: 'src/arrays.rs', lines 80:0-80:74 -/ @@ -313,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 () @@ -354,9 +343,7 @@ def take_array_t (a : Array AB 2#usize) : Result Unit := /- [arrays::non_copyable_array]: Source: 'src/arrays.rs', lines 229:0-229:27 -/ def non_copyable_array : Result Unit := - do - let _ ← take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) - Result.ret () + take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) /- [arrays::sum]: loop 0: Source: 'src/arrays.rs', lines 242:0-250:1 -/ @@ -496,11 +483,9 @@ def zero_slice (a : Slice U8) : Result (Slice U8) := Source: 'src/arrays.rs', lines 312:0-318:1 -/ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit := if i < len - then - do - let i1 ← i + 1#usize - let _ ← iter_mut_slice_loop len i1 - Result.ret () + then do + let i1 ← i + 1#usize + iter_mut_slice_loop len i1 else Result.ret () /- [arrays::iter_mut_slice]: diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index d6449b37..ca9b48da 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -21,9 +21,7 @@ def betree.store_internal_node (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) : Result (State × Unit) := - do - let (st1, _) ← betree_utils.store_internal_node id content st - Result.ret (st1, ()) + betree_utils.store_internal_node id content st /- [betree_main::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 -/ @@ -37,9 +35,7 @@ def betree.store_leaf_node (id : U64) (content : betree.List (U64 × U64)) (st : State) : Result (State × Unit) := - do - let (st1, _) ← betree_utils.store_leaf_node id content st - Result.ret (st1, ()) + betree_utils.store_leaf_node id content st /- [betree_main::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 -/ @@ -172,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 -/ @@ -231,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 @@ -239,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 -/ @@ -284,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 => @@ -308,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 @@ -346,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 @@ -393,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 @@ -413,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 -/ @@ -452,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]: @@ -494,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 -/ @@ -531,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]: @@ -587,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)) @@ -649,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 854b4853..4acc69c8 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -36,14 +36,23 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 := def incr (x : U32) : Result U32 := x + 1#u32 +/- [demo::use_incr]: + Source: 'src/demo.rs', lines 25:0-25:17 -/ +def use_incr : Result Unit := + do + let x ← incr 0#u32 + let x1 ← incr x + let _ ← incr x1 + Result.ret () + /- [demo::CList] - Source: 'src/demo.rs', lines 27:0-27:17 -/ + Source: 'src/demo.rs', lines 34:0-34:17 -/ inductive CList (T : Type) := | CCons : T → CList T → CList T | CNil : CList T /- [demo::list_nth]: - Source: 'src/demo.rs', lines 32:0-32:56 -/ + Source: 'src/demo.rs', lines 39:0-39:56 -/ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := match l with | CList.CCons x tl => @@ -55,7 +64,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := | CList.CNil => Result.fail .panic /- [demo::list_nth_mut]: - Source: 'src/demo.rs', lines 47:0-47:68 -/ + Source: 'src/demo.rs', lines 54:0-54:68 -/ divergent def list_nth_mut (T : Type) (l : CList T) (i : U32) : Result (T × (T → Result (CList T))) @@ -79,7 +88,7 @@ divergent def list_nth_mut | CList.CNil => Result.fail .panic /- [demo::list_nth_mut1]: loop 0: - Source: 'src/demo.rs', lines 62:0-71:1 -/ + Source: 'src/demo.rs', lines 69:0-78:1 -/ divergent def list_nth_mut1_loop (T : Type) (l : CList T) (i : U32) : Result (T × (T → Result (CList T))) @@ -102,17 +111,15 @@ divergent def list_nth_mut1_loop | CList.CNil => Result.fail .panic /- [demo::list_nth_mut1]: - Source: 'src/demo.rs', lines 62:0-62:77 -/ + Source: 'src/demo.rs', lines 69:0-69:77 -/ def list_nth_mut1 (T : Type) (l : CList T) (i : U32) : Result (T × (T → Result (CList T))) := - do - let (t, back_'a) ← list_nth_mut1_loop T l i - Result.ret (t, back_'a) + list_nth_mut1_loop T l i /- [demo::i32_id]: - Source: 'src/demo.rs', lines 73:0-73:28 -/ + Source: 'src/demo.rs', lines 80:0-80:28 -/ divergent def i32_id (i : I32) : Result I32 := if i = 0#i32 then Result.ret 0#i32 @@ -121,26 +128,44 @@ divergent def i32_id (i : I32) : Result I32 := let i2 ← i32_id i1 i2 + 1#i32 +/- [demo::list_tail]: + Source: 'src/demo.rs', lines 88:0-88:64 -/ +divergent def list_tail + (T : Type) (l : CList T) : + Result ((CList T) × (CList T → Result (CList T))) + := + match l with + | CList.CCons t tl => + do + let (c, list_tail_back) ← list_tail T tl + let back_'a := + fun ret => + do + let tl1 ← list_tail_back ret + Result.ret (CList.CCons t tl1) + Result.ret (c, back_'a) + | CList.CNil => Result.ret (CList.CNil, Result.ret) + /- Trait declaration: [demo::Counter] - Source: 'src/demo.rs', lines 83:0-83:17 -/ + Source: 'src/demo.rs', lines 97:0-97:17 -/ structure Counter (Self : Type) where incr : Self → Result (Usize × Self) /- [demo::{(demo::Counter for usize)}::incr]: - Source: 'src/demo.rs', lines 88:4-88:31 -/ + Source: 'src/demo.rs', lines 102:4-102:31 -/ def CounterUsize.incr (self : Usize) : Result (Usize × Usize) := do let self1 ← self + 1#usize Result.ret (self, self1) /- Trait implementation: [demo::{(demo::Counter for usize)}] - Source: 'src/demo.rs', lines 87:0-87:22 -/ + Source: 'src/demo.rs', lines 101:0-101:22 -/ def CounterUsize : Counter Usize := { incr := CounterUsize.incr } /- [demo::use_counter]: - Source: 'src/demo.rs', lines 95:0-95:59 -/ + Source: 'src/demo.rs', lines 109:0-109:59 -/ def use_counter (T : Type) (CounterInst : Counter T) (cnt : T) : Result (Usize × T) := CounterInst.incr cnt diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean index cdec7332..e514ac3e 100644 --- a/tests/lean/Demo/Properties.lean +++ b/tests/lean/Demo/Properties.lean @@ -65,4 +65,20 @@ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : termination_by x.val.toNat decreasing_by scalar_decr_tac +theorem list_tail_spec {T : Type} [Inhabited T] (l : CList T) : + ∃ back, list_tail T l = ret (CList.CNil, back) ∧ + ∀ tl', ∃ l', back tl' = ret l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by + rw [list_tail] + match l with + | CNil => + simp_all + | CCons hd tl => + simp_all + progress as ⟨ back ⟩ + simp + -- Proving the backward function + intro tl' + progress + simp_all + end demo 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 f0706725..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 -/ @@ -311,9 +306,7 @@ def HashMap.get_mut_in_list (T : Type) (ls : List T) (key : Usize) : Result (T × (T → Result (List T))) := - do - let (t, back_'a) ← HashMap.get_mut_in_list_loop T ls key - Result.ret (t, back_'a) + HashMap.get_mut_in_list_loop T ls key /- [hashmap::{hashmap::HashMap<T>}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 -/ diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index 31441b4a..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 -/ @@ -326,9 +321,7 @@ def hashmap.HashMap.get_mut_in_list (T : Type) (ls : hashmap.List T) (key : Usize) : Result (T × (T → Result (hashmap.List T))) := - do - let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T ls key - Result.ret (t, back_'a) + hashmap.HashMap.get_mut_in_list_loop T ls key /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 -/ @@ -460,8 +453,7 @@ def insert_on_disk do let (st1, hm) ← hashmap_utils.deserialize st let hm1 ← hashmap.HashMap.insert U64 hm key value - let (st2, _) ← hashmap_utils.serialize hm1 st1 - Result.ret (st2, ()) + hashmap_utils.serialize hm1 st1 /- [hashmap_main::main]: Source: 'src/hashmap_main.rs', lines 16:0-16:13 -/ diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index 433ca8f0..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 -/ @@ -138,9 +138,7 @@ divergent def list_nth_mut_loop_loop Source: 'src/loops.rs', lines 88:0-88:71 -/ def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) := - do - let (t, back) ← list_nth_mut_loop_loop T ls i - Result.ret (t, back) + list_nth_mut_loop_loop T ls i /- [loops::list_nth_shared_loop]: loop 0: Source: 'src/loops.rs', lines 101:0-111:1 -/ @@ -189,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: @@ -213,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 -/ @@ -322,9 +320,7 @@ def list_nth_mut_loop_pair (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × (T → Result (List T)) × (T → Result (List T))) := - do - let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T ls0 ls1 i - Result.ret (p, back_'a, back_'b) + list_nth_mut_loop_pair_loop T ls0 ls1 i /- [loops::list_nth_shared_loop_pair]: loop 0: Source: 'src/loops.rs', lines 208:0-229:1 -/ @@ -384,9 +380,7 @@ def list_nth_mut_loop_pair_merge (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × ((T × T) → Result ((List T) × (List T)))) := - do - let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T ls0 ls1 i - Result.ret (p, back_'a) + list_nth_mut_loop_pair_merge_loop T ls0 ls1 i /- [loops::list_nth_shared_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 251:0-266:1 -/ @@ -443,9 +437,7 @@ def list_nth_mut_shared_loop_pair (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × (T → Result (List T))) := - do - let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T ls0 ls1 i - Result.ret (p, back_'a) + list_nth_mut_shared_loop_pair_loop T ls0 ls1 i /- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 288:0-303:1 -/ @@ -480,9 +472,7 @@ def list_nth_mut_shared_loop_pair_merge (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × (T → Result (List T))) := - do - let (p, back_'a) ← list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i - Result.ret (p, back_'a) + list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i /- [loops::list_nth_shared_mut_loop_pair]: loop 0: Source: 'src/loops.rs', lines 307:0-322:1 -/ @@ -516,9 +506,7 @@ def list_nth_shared_mut_loop_pair (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × (T → Result (List T))) := - do - let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T ls0 ls1 i - Result.ret (p, back_'b) + list_nth_shared_mut_loop_pair_loop T ls0 ls1 i /- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 326:0-341:1 -/ @@ -553,19 +541,15 @@ def list_nth_shared_mut_loop_pair_merge (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × (T → Result (List T))) := - do - let (p, back_'a) ← list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i - Result.ret (p, back_'a) + list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i /- [loops::ignore_input_mut_borrow]: loop 0: Source: 'src/loops.rs', lines 345:0-349:1 -/ divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit := if i > 0#u32 - then - do - let i1 ← i - 1#u32 - let _ ← ignore_input_mut_borrow_loop i1 - Result.ret () + then do + let i1 ← i - 1#u32 + ignore_input_mut_borrow_loop i1 else Result.ret () /- [loops::ignore_input_mut_borrow]: @@ -579,11 +563,9 @@ def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 := Source: 'src/loops.rs', lines 353:0-358:1 -/ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit := if i > 0#u32 - then - do - let i1 ← i - 1#u32 - let _ ← incr_ignore_input_mut_borrow_loop i1 - Result.ret () + then do + let i1 ← i - 1#u32 + incr_ignore_input_mut_borrow_loop i1 else Result.ret () /- [loops::incr_ignore_input_mut_borrow]: @@ -598,11 +580,9 @@ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 := Source: 'src/loops.rs', lines 362:0-366:1 -/ divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit := if i > 0#u32 - then - do - let i1 ← i - 1#u32 - let _ ← ignore_input_shared_borrow_loop i1 - Result.ret () + then do + let i1 ← i - 1#u32 + ignore_input_shared_borrow_loop i1 else Result.ret () /- [loops::ignore_input_shared_borrow]: 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 () |