summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2024-06-17 07:15:26 +0200
committerSon Ho2024-06-17 07:15:26 +0200
commit1021cdea98043dd935dbc8dbe633b90fda68047d (patch)
treedc2f420cf5167690da9dfebe358ba56bf05e1b1e /tests
parentf4739fba4be95818ca01776837c8d610e443a45b (diff)
Update the tests
Diffstat (limited to 'tests')
-rw-r--r--tests/lean/Betree/Funs.lean8
-rw-r--r--tests/lean/Demo/Demo.lean1
-rw-r--r--tests/lean/Hashmap/Funs.lean8
-rw-r--r--tests/lean/Hashmap/Properties.lean3
-rw-r--r--tests/lean/InfiniteLoop.lean4
-rw-r--r--tests/lean/Loops.lean11
6 files changed, 31 insertions, 4 deletions
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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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)))