From f3e16bb43a8ff27a5184d9fa452277cc6a59410f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 19 Mar 2024 05:29:29 +0100 Subject: Regenerate the tests --- tests/lean/Arrays.lean | 28 +++++++--------------- tests/lean/BetreeMain/Funs.lean | 8 ++----- tests/lean/Demo/Demo.lean | 4 +--- tests/lean/Hashmap/Funs.lean | 4 +--- tests/lean/HashmapMain/Funs.lean | 7 ++---- tests/lean/Loops.lean | 52 +++++++++++++--------------------------- 6 files changed, 30 insertions(+), 73 deletions(-) (limited to 'tests/lean') diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index d637ee13..cd1b6544 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -28,9 +28,7 @@ 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 -/ @@ -76,9 +74,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 +87,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 +121,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 -/ @@ -354,9 +346,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 +486,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..bd5921a8 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 -/ diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index f38b5cd3..09032820 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -116,9 +116,7 @@ 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 80:0-80:28 -/ diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index f0706725..d33b6571 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -311,9 +311,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}::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..8a277700 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -326,9 +326,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}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 -/ @@ -460,8 +458,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..3f075347 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -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 -/ @@ -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]: -- cgit v1.2.3