From 1021cdea98043dd935dbc8dbe633b90fda68047d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 17 Jun 2024 07:15:26 +0200 Subject: Update the tests --- tests/lean/Betree/Funs.lean | 8 ++++++++ tests/lean/Demo/Demo.lean | 1 + tests/lean/Hashmap/Funs.lean | 8 ++++++++ tests/lean/Hashmap/Properties.lean | 3 +-- tests/lean/InfiniteLoop.lean | 4 ++-- tests/lean/Loops.lean | 11 +++++++++++ 6 files changed, 31 insertions(+), 4 deletions(-) (limited to 'tests') diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean index 7d8b4714..05341b31 100644 --- a/tests/lean/Betree/Funs.lean +++ b/tests/lean/Betree/Funs.lean @@ -248,6 +248,7 @@ divergent def betree.Node.lookup_first_message_for_key_loop /- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 792:4-795:34 -/ +@[reducible] def betree.Node.lookup_first_message_for_key (key : U64) (msgs : betree.List (U64 × betree.Message)) : Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × @@ -272,6 +273,7 @@ divergent def betree.Node.lookup_in_bindings_loop /- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: Source: 'src/betree.rs', lines 649:4-649:84 -/ +@[reducible] def betree.Node.lookup_in_bindings (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := betree.Node.lookup_in_bindings_loop key bindings @@ -307,6 +309,7 @@ divergent def betree.Node.apply_upserts_loop /- [betree::betree::{betree::betree::Node#5}::apply_upserts]: Source: 'src/betree.rs', lines 820:4-820:94 -/ +@[reducible] def betree.Node.apply_upserts (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) : @@ -411,6 +414,7 @@ divergent def betree.Node.filter_messages_for_key_loop /- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: Source: 'src/betree.rs', lines 683:4-683:77 -/ +@[reducible] def betree.Node.filter_messages_for_key (key : U64) (msgs : betree.List (U64 × betree.Message)) : Result (betree.List (U64 × betree.Message)) @@ -443,6 +447,7 @@ divergent def betree.Node.lookup_first_message_after_key_loop /- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: Source: 'src/betree.rs', lines 694:4-697:34 -/ +@[reducible] def betree.Node.lookup_first_message_after_key (key : U64) (msgs : betree.List (U64 × betree.Message)) : Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × @@ -531,6 +536,7 @@ divergent def betree.Node.apply_messages_to_internal_loop /- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 518:4-521:5 -/ +@[reducible] def betree.Node.apply_messages_to_internal (msgs : betree.List (U64 × betree.Message)) (new_msgs : betree.List (U64 × betree.Message)) : @@ -563,6 +569,7 @@ divergent def betree.Node.lookup_mut_in_bindings_loop /- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: Source: 'src/betree.rs', lines 664:4-667:32 -/ +@[reducible] def betree.Node.lookup_mut_in_bindings (key : U64) (bindings : betree.List (U64 × U64)) : Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result @@ -627,6 +634,7 @@ divergent def betree.Node.apply_messages_to_leaf_loop /- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: Source: 'src/betree.rs', lines 463:4-466:5 -/ +@[reducible] def betree.Node.apply_messages_to_leaf (bindings : betree.List (U64 × U64)) (new_msgs : betree.List (U64 × betree.Message)) : diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 48ac2062..2bbc385d 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -112,6 +112,7 @@ divergent def list_nth_mut1_loop /- [demo::list_nth_mut1]: Source: 'tests/src/demo.rs', lines 71:0-71:77 -/ +@[reducible] def list_nth_mut1 (T : Type) (l : CList T) (i : U32) : Result (T × (T → Result (CList T))) diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 7d8f73a7..f5d028db 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -28,6 +28,7 @@ divergent def HashMap.allocate_slots_loop /- [hashmap::{hashmap::HashMap}::allocate_slots]: Source: 'tests/src/hashmap.rs', lines 61:4-61:78 -/ +@[reducible] def HashMap.allocate_slots (T : Type) (slots : alloc.vec.Vec (AList T)) (n : Usize) : Result (alloc.vec.Vec (AList T)) @@ -106,6 +107,7 @@ divergent def HashMap.insert_in_list_loop /- [hashmap::{hashmap::HashMap}::insert_in_list]: Source: 'tests/src/hashmap.rs', lines 108:4-108:72 -/ +@[reducible] def HashMap.insert_in_list (T : Type) (key : Usize) (value : T) (ls : AList T) : Result (Bool × (AList T)) @@ -150,6 +152,7 @@ divergent def HashMap.move_elements_from_list_loop /- [hashmap::{hashmap::HashMap}::move_elements_from_list]: Source: 'tests/src/hashmap.rs', lines 194:4-194:73 -/ +@[reducible] def HashMap.move_elements_from_list (T : Type) (ntable : HashMap T) (ls : AList T) : Result (HashMap T) := HashMap.move_elements_from_list_loop T ntable ls @@ -177,6 +180,7 @@ divergent def HashMap.move_elements_loop /- [hashmap::{hashmap::HashMap}::move_elements]: Source: 'tests/src/hashmap.rs', lines 182:4-182:96 -/ +@[reducible] def HashMap.move_elements (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (AList T)) (i : Usize) : @@ -234,6 +238,7 @@ divergent def HashMap.contains_key_in_list_loop /- [hashmap::{hashmap::HashMap}::contains_key_in_list]: Source: 'tests/src/hashmap.rs', lines 217:4-217:69 -/ +@[reducible] def HashMap.contains_key_in_list (T : Type) (key : Usize) (ls : AList T) : Result Bool := HashMap.contains_key_in_list_loop T key ls @@ -265,6 +270,7 @@ divergent def HashMap.get_in_list_loop /- [hashmap::{hashmap::HashMap}::get_in_list]: Source: 'tests/src/hashmap.rs', lines 235:4-235:71 -/ +@[reducible] def HashMap.get_in_list (T : Type) (key : Usize) (ls : AList T) : Result T := HashMap.get_in_list_loop T key ls @@ -306,6 +312,7 @@ divergent def HashMap.get_mut_in_list_loop /- [hashmap::{hashmap::HashMap}::get_mut_in_list]: Source: 'tests/src/hashmap.rs', lines 256:4-256:87 -/ +@[reducible] def HashMap.get_mut_in_list (T : Type) (ls : AList T) (key : Usize) : Result (T × (T → Result (AList T))) @@ -356,6 +363,7 @@ divergent def HashMap.remove_from_list_loop /- [hashmap::{hashmap::HashMap}::remove_from_list]: Source: 'tests/src/hashmap.rs', lines 276:4-276:70 -/ +@[reducible] def HashMap.remove_from_list (T : Type) (key : Usize) (ls : AList T) : Result ((Option T) × (AList T)) := HashMap.remove_from_list_loop T key ls diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index a2fa0d7d..29b5834b 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -165,8 +165,7 @@ theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) ( have : distinct_keys (AList.v tl0) := by simp [distinct_keys] at hdk simp [hdk, distinct_keys] - progress keep heq as ⟨ b, tl1 .. ⟩ - simp only [insert_in_list] at heq + progress as ⟨ b, tl1 .. ⟩ have : slot_s_inv_hash l (hash_mod_key key l) (AList.v (AList.Cons k v tl1)) := by simp [AList.v, slot_s_inv_hash] at * simp [*] diff --git a/tests/lean/InfiniteLoop.lean b/tests/lean/InfiniteLoop.lean index 9eb8e22c..b8c2343e 100644 --- a/tests/lean/InfiniteLoop.lean +++ b/tests/lean/InfiniteLoop.lean @@ -19,7 +19,7 @@ divergent def foo_loop : Result Unit := /- [infinite_loop::foo]: Source: 'tests/src/infinite-loop.rs', lines 6:0-6:8 -/ -def foo : Result Unit := - foo_loop +@[reducible] def foo : Result Unit := + foo_loop end infinite_loop diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index 199605d5..a9e5a499 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -110,6 +110,7 @@ divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool := /- [loops::list_mem]: Source: 'tests/src/loops.rs', lines 80:0-80:52 -/ +@[reducible] def list_mem (x : U32) (ls : List U32) : Result Bool := list_mem_loop x ls @@ -136,6 +137,7 @@ divergent def list_nth_mut_loop_loop /- [loops::list_nth_mut_loop]: Source: 'tests/src/loops.rs', lines 92:0-92:71 -/ +@[reducible] def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) := list_nth_mut_loop_loop T ls i @@ -155,6 +157,7 @@ divergent def list_nth_shared_loop_loop /- [loops::list_nth_shared_loop]: Source: 'tests/src/loops.rs', lines 105:0-105:66 -/ +@[reducible] def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T := list_nth_shared_loop_loop T ls i @@ -316,6 +319,7 @@ divergent def list_nth_mut_loop_pair_loop /- [loops::list_nth_mut_loop_pair]: Source: 'tests/src/loops.rs', lines 188:0-192:27 -/ +@[reducible] 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))) @@ -340,6 +344,7 @@ divergent def list_nth_shared_loop_pair_loop /- [loops::list_nth_shared_loop_pair]: Source: 'tests/src/loops.rs', lines 212:0-216:19 -/ +@[reducible] def list_nth_shared_loop_pair (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := list_nth_shared_loop_pair_loop T ls0 ls1 i @@ -376,6 +381,7 @@ divergent def list_nth_mut_loop_pair_merge_loop /- [loops::list_nth_mut_loop_pair_merge]: Source: 'tests/src/loops.rs', lines 237:0-241:27 -/ +@[reducible] 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)))) @@ -401,6 +407,7 @@ divergent def list_nth_shared_loop_pair_merge_loop /- [loops::list_nth_shared_loop_pair_merge]: Source: 'tests/src/loops.rs', lines 255:0-259:19 -/ +@[reducible] def list_nth_shared_loop_pair_merge (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := list_nth_shared_loop_pair_merge_loop T ls0 ls1 i @@ -433,6 +440,7 @@ divergent def list_nth_mut_shared_loop_pair_loop /- [loops::list_nth_mut_shared_loop_pair]: Source: 'tests/src/loops.rs', lines 273:0-277:23 -/ +@[reducible] def list_nth_mut_shared_loop_pair (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × (T → Result (List T))) @@ -467,6 +475,7 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop /- [loops::list_nth_mut_shared_loop_pair_merge]: Source: 'tests/src/loops.rs', lines 292:0-296:23 -/ +@[reducible] 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))) @@ -501,6 +510,7 @@ divergent def list_nth_shared_mut_loop_pair_loop /- [loops::list_nth_shared_mut_loop_pair]: Source: 'tests/src/loops.rs', lines 311:0-315:23 -/ +@[reducible] def list_nth_shared_mut_loop_pair (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × (T → Result (List T))) @@ -535,6 +545,7 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop /- [loops::list_nth_shared_mut_loop_pair_merge]: Source: 'tests/src/loops.rs', lines 330:0-334:23 -/ +@[reducible] 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))) -- cgit v1.2.3