diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/hashmap/Hashmap/Funs.lean | 14 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 14 |
2 files changed, 0 insertions, 28 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 ()) |