diff options
Diffstat (limited to 'tests/lean')
| -rw-r--r-- | tests/lean/hashmap/Hashmap/Funs.lean | 14 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 14 | ||||
| -rw-r--r-- | tests/lean/misc/loops/Loops/Funs.lean | 52 | ||||
| -rw-r--r-- | tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean | 32 | ||||
| -rw-r--r-- | tests/lean/misc/paper/Paper.lean | 11 |
5 files changed, 33 insertions, 90 deletions
diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean index 78ed970a..3bdd9dd2 100644 --- a/tests/lean/hashmap/Hashmap/Funs.lean +++ b/tests/lean/hashmap/Hashmap/Funs.lean @@ -98,7 +98,6 @@ def hash_map_insert_in_list_loop_fwd then result.ret false else hash_map_insert_in_list_loop_fwd T key value tl | list_t.ListNil => result.ret true - termination_by hash_map_insert_in_list_loop_fwd key value ls => hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hash_map_insert_in_list_loop_decreases key value ls @@ -122,7 +121,6 @@ def hash_map_insert_in_list_loop_back | list_t.ListNil => let l := list_t.ListNil result.ret (list_t.ListCons key value l) - termination_by hash_map_insert_in_list_loop_back key value ls => hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hash_map_insert_in_list_loop_decreases key value ls @@ -185,7 +183,6 @@ def hash_map_move_elements_from_list_loop_fwd_back let ntable0 <- hash_map_insert_no_resize_fwd_back T ntable k v hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl | list_t.ListNil => result.ret ntable - termination_by hash_map_move_elements_from_list_loop_fwd_back ntable ls => hash_map_move_elements_from_list_loop_terminates T ntable ls decreasing_by hash_map_move_elements_from_list_loop_decreases ntable ls @@ -277,7 +274,6 @@ def hash_map_contains_key_in_list_loop_fwd then result.ret true else hash_map_contains_key_in_list_loop_fwd T key tl | list_t.ListNil => result.ret false - termination_by hash_map_contains_key_in_list_loop_fwd key ls => hash_map_contains_key_in_list_loop_terminates T key ls decreasing_by hash_map_contains_key_in_list_loop_decreases key ls @@ -306,7 +302,6 @@ def hash_map_get_in_list_loop_fwd then result.ret cvalue else hash_map_get_in_list_loop_fwd T key tl | list_t.ListNil => result.fail error.panic - termination_by hash_map_get_in_list_loop_fwd key ls => hash_map_get_in_list_loop_terminates T key ls decreasing_by hash_map_get_in_list_loop_decreases key ls @@ -335,7 +330,6 @@ def hash_map_get_mut_in_list_loop_fwd then result.ret cvalue else hash_map_get_mut_in_list_loop_fwd T tl key | list_t.ListNil => result.fail error.panic - termination_by hash_map_get_mut_in_list_loop_fwd ls key => hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hash_map_get_mut_in_list_loop_decreases ls key @@ -357,7 +351,6 @@ def hash_map_get_mut_in_list_loop_back let tl0 <- hash_map_get_mut_in_list_loop_back T tl key ret0 result.ret (list_t.ListCons ckey cvalue tl0) | list_t.ListNil => result.fail error.panic - termination_by hash_map_get_mut_in_list_loop_back ls key ret0 => hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hash_map_get_mut_in_list_loop_decreases ls key @@ -409,10 +402,8 @@ def hash_map_remove_from_list_loop_fwd match mv_ls with | list_t.ListCons i cvalue tl0 => result.ret (Option.some cvalue) | list_t.ListNil => result.fail error.panic - else hash_map_remove_from_list_loop_fwd T key tl | list_t.ListNil => result.ret Option.none - termination_by hash_map_remove_from_list_loop_fwd key ls => hash_map_remove_from_list_loop_terminates T key ls decreasing_by hash_map_remove_from_list_loop_decreases key ls @@ -434,13 +425,11 @@ def hash_map_remove_from_list_loop_back match mv_ls with | list_t.ListCons i cvalue tl0 => result.ret tl0 | list_t.ListNil => result.fail error.panic - else do let tl0 <- hash_map_remove_from_list_loop_back T key tl result.ret (list_t.ListCons ckey t tl0) | list_t.ListNil => result.ret list_t.ListNil - termination_by hash_map_remove_from_list_loop_back key ls => hash_map_remove_from_list_loop_terminates T key ls decreasing_by hash_map_remove_from_list_loop_decreases key ls @@ -466,7 +455,6 @@ def hash_map_remove_fwd let _ <- USize.checked_sub self.hash_map_num_entries (USize.ofNatCore 1 (by intlit)) result.ret (Option.some x0) - /- [hashmap::HashMap::{0}::remove] -/ def hash_map_remove_back @@ -502,7 +490,6 @@ def hash_map_remove_back hash_map_max_load := self.hash_map_max_load, hash_map_slots := v } - /- [hashmap::test1] -/ def test1_fwd : result Unit := @@ -565,7 +552,6 @@ def test1_fwd : result Unit := if not (i3 = (UInt64.ofNatCore 256 (by intlit))) then result.fail error.panic else result.ret () - /- Unit test for [hashmap::test1] -/ #assert (test1_fwd = .ret ()) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 5b7d6f46..1abc9f8d 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -110,7 +110,6 @@ def hashmap_hash_map_insert_in_list_loop_fwd then result.ret false else hashmap_hash_map_insert_in_list_loop_fwd T key value tl | hashmap_list_t.HashmapListNil => result.ret true - termination_by hashmap_hash_map_insert_in_list_loop_fwd key value ls => hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls @@ -136,7 +135,6 @@ def hashmap_hash_map_insert_in_list_loop_back | hashmap_list_t.HashmapListNil => let l := hashmap_list_t.HashmapListNil result.ret (hashmap_list_t.HashmapListCons key value l) - termination_by hashmap_hash_map_insert_in_list_loop_back key value ls => hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls @@ -206,7 +204,6 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl | hashmap_list_t.HashmapListNil => result.ret ntable - termination_by hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls => hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls @@ -306,7 +303,6 @@ def hashmap_hash_map_contains_key_in_list_loop_fwd then result.ret true else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl | hashmap_list_t.HashmapListNil => result.ret false - termination_by hashmap_hash_map_contains_key_in_list_loop_fwd key ls => hashmap_hash_map_contains_key_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_contains_key_in_list_loop_decreases key ls @@ -336,7 +332,6 @@ def hashmap_hash_map_get_in_list_loop_fwd then result.ret cvalue else hashmap_hash_map_get_in_list_loop_fwd T key tl | hashmap_list_t.HashmapListNil => result.fail error.panic - termination_by hashmap_hash_map_get_in_list_loop_fwd key ls => hashmap_hash_map_get_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls @@ -366,7 +361,6 @@ def hashmap_hash_map_get_mut_in_list_loop_fwd then result.ret cvalue else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key | hashmap_list_t.HashmapListNil => result.fail error.panic - termination_by hashmap_hash_map_get_mut_in_list_loop_fwd ls key => hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key @@ -390,7 +384,6 @@ def hashmap_hash_map_get_mut_in_list_loop_back let tl0 <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0) | hashmap_list_t.HashmapListNil => result.fail error.panic - termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 => hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key @@ -450,10 +443,8 @@ def hashmap_hash_map_remove_from_list_loop_fwd | hashmap_list_t.HashmapListCons i cvalue tl0 => result.ret (Option.some cvalue) | hashmap_list_t.HashmapListNil => result.fail error.panic - else hashmap_hash_map_remove_from_list_loop_fwd T key tl | hashmap_list_t.HashmapListNil => result.ret Option.none - termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls => hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls @@ -478,13 +469,11 @@ def hashmap_hash_map_remove_from_list_loop_back match mv_ls with | hashmap_list_t.HashmapListCons i cvalue tl0 => result.ret tl0 | hashmap_list_t.HashmapListNil => result.fail error.panic - else do let tl0 <- hashmap_hash_map_remove_from_list_loop_back T key tl result.ret (hashmap_list_t.HashmapListCons ckey t tl0) | hashmap_list_t.HashmapListNil => result.ret hashmap_list_t.HashmapListNil - termination_by hashmap_hash_map_remove_from_list_loop_back key ls => hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls @@ -513,7 +502,6 @@ def hashmap_hash_map_remove_fwd let _ <- USize.checked_sub self.hashmap_hash_map_num_entries (USize.ofNatCore 1 (by intlit)) result.ret (Option.some x0) - /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ def hashmap_hash_map_remove_back @@ -556,7 +544,6 @@ def hashmap_hash_map_remove_back hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, hashmap_hash_map_slots := v } - /- [hashmap_main::hashmap::test1] -/ def hashmap_test1_fwd : result Unit := @@ -624,7 +611,6 @@ def hashmap_test1_fwd : result Unit := if not (i3 = (UInt64.ofNatCore 256 (by intlit))) then result.fail error.panic else result.ret () - /- Unit test for [hashmap_main::hashmap::test1] -/ #assert (hashmap_test1_fwd = .ret ()) diff --git a/tests/lean/misc/loops/Loops/Funs.lean b/tests/lean/misc/loops/Loops/Funs.lean index 8b7e8a1f..55f0c87d 100644 --- a/tests/lean/misc/loops/Loops/Funs.lean +++ b/tests/lean/misc/loops/Loops/Funs.lean @@ -80,9 +80,10 @@ def clear_fwd_back (v : vec UInt32) : result (vec UInt32) := def list_mem_loop_fwd (x : UInt32) (ls : list_t UInt32) : (result Bool) := match ls with | list_t.ListCons y tl => - if y = x then result.ret true else list_mem_loop_fwd x tl + if y = x + then result.ret true + else list_mem_loop_fwd x tl | list_t.ListNil => result.ret false - termination_by list_mem_loop_fwd x ls => list_mem_loop_terminates x ls decreasing_by list_mem_loop_decreases x ls @@ -102,7 +103,6 @@ def list_nth_mut_loop_loop_fwd let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_loop_loop_fwd T tl i0 | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_loop_loop_fwd ls i => list_nth_mut_loop_loop_terminates T ls i decreasing_by list_nth_mut_loop_loop_decreases ls i @@ -124,7 +124,6 @@ def list_nth_mut_loop_loop_back let tl0 <- list_nth_mut_loop_loop_back T tl i0 ret0 result.ret (list_t.ListCons x tl0) | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_loop_loop_back ls i ret0 => list_nth_mut_loop_loop_terminates T ls i decreasing_by list_nth_mut_loop_loop_decreases ls i @@ -146,7 +145,6 @@ def list_nth_shared_loop_loop_fwd let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_loop_loop_fwd T tl i0 | list_t.ListNil => result.fail error.panic - termination_by list_nth_shared_loop_loop_fwd ls i => list_nth_shared_loop_loop_terminates T ls i decreasing_by list_nth_shared_loop_loop_decreases ls i @@ -160,9 +158,10 @@ def list_nth_shared_loop_fwd def get_elem_mut_loop_fwd (x : USize) (ls : list_t USize) : (result USize) := match ls with | list_t.ListCons y tl => - if y = x then result.ret y else get_elem_mut_loop_fwd x tl + if y = x + then result.ret y + else get_elem_mut_loop_fwd x tl | list_t.ListNil => result.fail error.panic - termination_by get_elem_mut_loop_fwd x ls => get_elem_mut_loop_terminates x ls decreasing_by get_elem_mut_loop_decreases x ls @@ -185,7 +184,6 @@ def get_elem_mut_loop_back let tl0 <- get_elem_mut_loop_back x tl ret0 result.ret (list_t.ListCons y tl0) | list_t.ListNil => result.fail error.panic - termination_by get_elem_mut_loop_back x ls ret0 => get_elem_mut_loop_terminates x ls decreasing_by get_elem_mut_loop_decreases x ls @@ -206,9 +204,10 @@ def get_elem_shared_loop_fwd (x : USize) (ls : list_t USize) : (result USize) := match ls with | list_t.ListCons y tl => - if y = x then result.ret y else get_elem_shared_loop_fwd x tl + if y = x + then result.ret y + else get_elem_shared_loop_fwd x tl | list_t.ListNil => result.fail error.panic - termination_by get_elem_shared_loop_fwd x ls => get_elem_shared_loop_terminates x ls decreasing_by get_elem_shared_loop_decreases x ls @@ -245,7 +244,6 @@ def list_nth_mut_loop_with_id_loop_fwd let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_loop_with_id_loop_fwd T i0 tl | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_loop_with_id_loop_fwd i ls => list_nth_mut_loop_with_id_loop_terminates T i ls decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls @@ -270,7 +268,6 @@ def list_nth_mut_loop_with_id_loop_back let tl0 <- list_nth_mut_loop_with_id_loop_back T i0 tl ret0 result.ret (list_t.ListCons x tl0) | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_loop_with_id_loop_back i ls ret0 => list_nth_mut_loop_with_id_loop_terminates T i ls decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls @@ -295,7 +292,6 @@ def list_nth_shared_loop_with_id_loop_fwd let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_loop_with_id_loop_fwd T i0 tl | list_t.ListNil => result.fail error.panic - termination_by list_nth_shared_loop_with_id_loop_fwd i ls => list_nth_shared_loop_with_id_loop_terminates T i ls decreasing_by list_nth_shared_loop_with_id_loop_decreases i ls @@ -323,9 +319,7 @@ def list_nth_mut_loop_pair_loop_fwd let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_loop_pair_loop_fwd T tl0 tl1 i0 | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_loop_pair_loop_fwd ls0 ls1 i => list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i @@ -354,9 +348,7 @@ def list_nth_mut_loop_pair_loop_back'a let tl00 <- list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0 result.ret (list_t.ListCons x0 tl00) | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret0 => list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i @@ -385,9 +377,7 @@ def list_nth_mut_loop_pair_loop_back'b let tl10 <- list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0 result.ret (list_t.ListCons x1 tl10) | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret0 => list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i @@ -415,9 +405,7 @@ def list_nth_shared_loop_pair_loop_fwd let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_loop_pair_loop_fwd T tl0 tl1 i0 | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_shared_loop_pair_loop_fwd ls0 ls1 i => list_nth_shared_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_loop_pair_loop_decreases ls0 ls1 i @@ -445,9 +433,7 @@ def list_nth_mut_loop_pair_merge_loop_fwd let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0 | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i => list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_merge_loop_decreases ls0 ls1 i @@ -479,9 +465,7 @@ def list_nth_mut_loop_pair_merge_loop_back list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 result.ret (list_t.ListCons x0 tl00, list_t.ListCons x1 tl10) | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret0 => list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_merge_loop_decreases ls0 ls1 i @@ -509,9 +493,7 @@ def list_nth_shared_loop_pair_merge_loop_fwd let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0 | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i => list_nth_shared_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_loop_pair_merge_loop_decreases ls0 ls1 i @@ -539,9 +521,7 @@ def list_nth_mut_shared_loop_pair_loop_fwd let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_shared_loop_pair_loop_fwd T tl0 tl1 i0 | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i => list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_shared_loop_pair_loop_decreases ls0 ls1 i @@ -570,9 +550,7 @@ def list_nth_mut_shared_loop_pair_loop_back let tl00 <- list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0 result.ret (list_t.ListCons x0 tl00) | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret0 => list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_shared_loop_pair_loop_decreases ls0 ls1 i @@ -600,9 +578,7 @@ def list_nth_mut_shared_loop_pair_merge_loop_fwd let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0 | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i => list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_shared_loop_pair_merge_loop_decreases ls0 ls1 i @@ -632,9 +608,7 @@ def list_nth_mut_shared_loop_pair_merge_loop_back list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 result.ret (list_t.ListCons x0 tl00) | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret0 => list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_shared_loop_pair_merge_loop_decreases ls0 ls1 i @@ -662,9 +636,7 @@ def list_nth_shared_mut_loop_pair_loop_fwd let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_mut_loop_pair_loop_fwd T tl0 tl1 i0 | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i => list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_mut_loop_pair_loop_decreases ls0 ls1 i @@ -693,9 +665,7 @@ def list_nth_shared_mut_loop_pair_loop_back let tl10 <- list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0 result.ret (list_t.ListCons x1 tl10) | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret0 => list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_mut_loop_pair_loop_decreases ls0 ls1 i @@ -723,9 +693,7 @@ def list_nth_shared_mut_loop_pair_merge_loop_fwd let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0 | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i => list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_mut_loop_pair_merge_loop_decreases ls0 ls1 i @@ -755,9 +723,7 @@ def list_nth_shared_mut_loop_pair_merge_loop_back list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 result.ret (list_t.ListCons x1 tl10) | list_t.ListNil => result.fail error.panic - | list_t.ListNil => result.fail error.panic - termination_by list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret0 => list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_mut_loop_pair_merge_loop_decreases ls0 ls1 i diff --git a/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean index 53093519..608aabc1 100644 --- a/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean +++ b/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean @@ -69,7 +69,9 @@ structure OpaqueDefs where /- [no_nested_borrows::get_max] -/ def get_max_fwd (x : UInt32) (y : UInt32) : result UInt32 := - if x >= y then result.ret x else result.ret y + if x >= y + then result.ret x + else result.ret y /- [no_nested_borrows::test3] -/ def test3_fwd : result Unit := @@ -153,11 +155,15 @@ structure OpaqueDefs where /- [no_nested_borrows::test_unreachable] -/ def test_unreachable_fwd (b : Bool) : result Unit := - if b then result.fail error.panic else result.ret () + if b + then result.fail error.panic + else result.ret () /- [no_nested_borrows::test_panic] -/ def test_panic_fwd (b : Bool) : result Unit := - if b then result.fail error.panic else result.ret () + if b + then result.fail error.panic + else result.ret () /- [no_nested_borrows::test_copy_int] -/ def test_copy_int_fwd : result Unit := @@ -175,7 +181,6 @@ structure OpaqueDefs where match l with | list_t.ListCons t l0 => result.ret true | list_t.ListNil => result.ret false - /- [no_nested_borrows::test_is_cons] -/ def test_is_cons_fwd : result Unit := @@ -183,7 +188,9 @@ structure OpaqueDefs where let l := list_t.ListNil let b <- is_cons_fwd Int32 (list_t.ListCons (Int32.ofNatCore 0 (by intlit)) l) - if not b then result.fail error.panic else result.ret () + if not b + then result.fail error.panic + else result.ret () /- Unit test for [no_nested_borrows::test_is_cons] -/ #assert (test_is_cons_fwd = .ret ()) @@ -193,7 +200,6 @@ structure OpaqueDefs where match l with | list_t.ListCons hd tl => result.ret (hd, tl) | list_t.ListNil => result.fail error.panic - /- [no_nested_borrows::test_split_list] -/ def test_split_list_fwd : result Unit := @@ -212,12 +218,16 @@ structure OpaqueDefs where /- [no_nested_borrows::choose] -/ def choose_fwd (T : Type) (b : Bool) (x : T) (y : T) : result T := - if b then result.ret x else result.ret y + if b + then result.ret x + else result.ret y /- [no_nested_borrows::choose] -/ def choose_back (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : result (T × T) := - if b then result.ret (ret0, y) else result.ret (x, ret0) + if b + then result.ret (ret0, y) + else result.ret (x, ret0) /- [no_nested_borrows::choose_test] -/ def choose_test_fwd : result Unit := @@ -265,7 +275,6 @@ structure OpaqueDefs where let i <- list_length_fwd T l1 UInt32.checked_add (UInt32.ofNatCore 1 (by intlit)) i | list_t.ListNil => result.ret (UInt32.ofNatCore 0 (by intlit)) - /- [no_nested_borrows::list_nth_shared] -/ def list_nth_shared_fwd (T : Type) (l : list_t T) (i : UInt32) : result T := @@ -278,7 +287,6 @@ structure OpaqueDefs where let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_fwd T tl i0 | list_t.ListNil => result.fail error.panic - /- [no_nested_borrows::list_nth_mut] -/ def list_nth_mut_fwd (T : Type) (l : list_t T) (i : UInt32) : result T := @@ -291,7 +299,6 @@ structure OpaqueDefs where let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_fwd T tl i0 | list_t.ListNil => result.fail error.panic - /- [no_nested_borrows::list_nth_mut] -/ def list_nth_mut_back @@ -306,7 +313,6 @@ structure OpaqueDefs where let tl0 <- list_nth_mut_back T tl i0 ret0 result.ret (list_t.ListCons x tl0) | list_t.ListNil => result.fail error.panic - /- [no_nested_borrows::list_rev_aux] -/ def list_rev_aux_fwd @@ -314,7 +320,6 @@ structure OpaqueDefs where match li with | list_t.ListCons hd tl => list_rev_aux_fwd T tl (list_t.ListCons hd lo) | list_t.ListNil => result.ret lo - /- [no_nested_borrows::list_rev] -/ def list_rev_fwd_back (T : Type) (l : list_t T) : result (list_t T) := @@ -542,7 +547,6 @@ structure OpaqueDefs where match l with | list_t.ListCons i l0 => result.ret (UInt32.ofNatCore 1 (by intlit)) | list_t.ListNil => result.ret (UInt32.ofNatCore 0 (by intlit)) - /- [no_nested_borrows::test_shared_borrow_enum2] -/ def test_shared_borrow_enum2_fwd : result UInt32 := diff --git a/tests/lean/misc/paper/Paper.lean b/tests/lean/misc/paper/Paper.lean index 2d23f394..adcd1eae 100644 --- a/tests/lean/misc/paper/Paper.lean +++ b/tests/lean/misc/paper/Paper.lean @@ -21,12 +21,16 @@ structure OpaqueDefs where /- [paper::choose] -/ def choose_fwd (T : Type) (b : Bool) (x : T) (y : T) : result T := - if b then result.ret x else result.ret y + if b + then result.ret x + else result.ret y /- [paper::choose] -/ def choose_back (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : result (T × T) := - if b then result.ret (ret0, y) else result.ret (x, ret0) + if b + then result.ret (ret0, y) + else result.ret (x, ret0) /- [paper::test_choose] -/ def test_choose_fwd : result Unit := @@ -68,7 +72,6 @@ structure OpaqueDefs where let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_fwd T tl i0 | list_t.ListNil => result.fail error.panic - /- [paper::list_nth_mut] -/ def list_nth_mut_back @@ -83,7 +86,6 @@ structure OpaqueDefs where let tl0 <- list_nth_mut_back T tl i0 ret0 result.ret (list_t.ListCons x tl0) | list_t.ListNil => result.fail error.panic - /- [paper::sum] -/ def sum_fwd (l : list_t Int32) : result Int32 := @@ -92,7 +94,6 @@ structure OpaqueDefs where let i <- sum_fwd tl Int32.checked_add x i | list_t.ListNil => result.ret (Int32.ofNatCore 0 (by intlit)) - /- [paper::test_nth] -/ def test_nth_fwd : result Unit := |