diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/hashmap/Hashmap/Funs.lean | 34 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 32 |
2 files changed, 25 insertions, 41 deletions
diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean index 030b335a..1b03b7a2 100644 --- a/tests/lean/hashmap/Hashmap/Funs.lean +++ b/tests/lean/hashmap/Hashmap/Funs.lean @@ -20,8 +20,7 @@ def hash_map_allocate_slots_loop_fwd hash_map_allocate_slots_loop_fwd T slots0 n0 else result.ret slots termination_by hash_map_allocate_slots_loop_fwd slots n => - hash_map_allocate_slots_loop_terminates - T slots n + hash_map_allocate_slots_loop_terminates T slots n decreasing_by hash_map_allocate_slots_loop_decreases slots n /- [hashmap::HashMap::{0}::allocate_slots] -/ @@ -67,8 +66,7 @@ def hash_map_clear_loop_fwd_back hash_map_clear_loop_fwd_back T slots0 i1 else result.ret slots termination_by hash_map_clear_loop_fwd_back slots i => - hash_map_clear_loop_terminates - T slots i + hash_map_clear_loop_terminates T slots i decreasing_by hash_map_clear_loop_decreases slots i /- [hashmap::HashMap::{0}::clear] -/ @@ -101,8 +99,7 @@ def hash_map_insert_in_list_loop_fwd | 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 + hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hash_map_insert_in_list_loop_decreases key value ls /- [hashmap::HashMap::{0}::insert_in_list] -/ @@ -125,8 +122,7 @@ def hash_map_insert_in_list_loop_back 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 + hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hash_map_insert_in_list_loop_decreases key value ls /- [hashmap::HashMap::{0}::insert_in_list] -/ @@ -189,7 +185,7 @@ def hash_map_move_elements_from_list_loop_fwd_back | 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 + hash_map_move_elements_from_list_loop_terminates T ntable ls decreasing_by hash_map_move_elements_from_list_loop_decreases ntable ls /- [hashmap::HashMap::{0}::move_elements_from_list] -/ @@ -215,7 +211,7 @@ def hash_map_move_elements_loop_fwd_back hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 else result.ret (ntable, slots) termination_by hash_map_move_elements_loop_fwd_back ntable slots i => - hash_map_move_elements_loop_terminates T ntable slots i + hash_map_move_elements_loop_terminates T ntable slots i decreasing_by hash_map_move_elements_loop_decreases ntable slots i /- [hashmap::HashMap::{0}::move_elements] -/ @@ -281,8 +277,7 @@ def hash_map_contains_key_in_list_loop_fwd | 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 + hash_map_contains_key_in_list_loop_terminates T key ls decreasing_by hash_map_contains_key_in_list_loop_decreases key ls /- [hashmap::HashMap::{0}::contains_key_in_list] -/ @@ -311,8 +306,7 @@ def hash_map_get_in_list_loop_fwd | 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 + hash_map_get_in_list_loop_terminates T key ls decreasing_by hash_map_get_in_list_loop_decreases key ls /- [hashmap::HashMap::{0}::get_in_list] -/ @@ -341,8 +335,7 @@ def hash_map_get_mut_in_list_loop_fwd | 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 + hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hash_map_get_mut_in_list_loop_decreases ls key /- [hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -364,8 +357,7 @@ def hash_map_get_mut_in_list_loop_back | 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 + hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hash_map_get_mut_in_list_loop_decreases ls key /- [hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -420,8 +412,7 @@ def hash_map_remove_from_list_loop_fwd | 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 + hash_map_remove_from_list_loop_terminates T key ls decreasing_by hash_map_remove_from_list_loop_decreases key ls /- [hashmap::HashMap::{0}::remove_from_list] -/ @@ -449,8 +440,7 @@ def hash_map_remove_from_list_loop_back | 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 + hash_map_remove_from_list_loop_terminates T key ls decreasing_by hash_map_remove_from_list_loop_decreases key ls /- [hashmap::HashMap::{0}::remove_from_list] -/ diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 5134f483..2795ecfa 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -24,8 +24,7 @@ def hashmap_hash_map_allocate_slots_loop_fwd hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 else result.ret slots termination_by hashmap_hash_map_allocate_slots_loop_fwd slots n => - hashmap_hash_map_allocate_slots_loop_terminates - T slots n + hashmap_hash_map_allocate_slots_loop_terminates T slots n decreasing_by hashmap_hash_map_allocate_slots_loop_decreases slots n /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ @@ -76,8 +75,7 @@ def hashmap_hash_map_clear_loop_fwd_back hashmap_hash_map_clear_loop_fwd_back T slots0 i1 else result.ret slots termination_by hashmap_hash_map_clear_loop_fwd_back slots i => - hashmap_hash_map_clear_loop_terminates - T slots i + hashmap_hash_map_clear_loop_terminates T slots i decreasing_by hashmap_hash_map_clear_loop_decreases slots i /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ @@ -113,7 +111,7 @@ def hashmap_hash_map_insert_in_list_loop_fwd | 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 + 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 /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ @@ -139,7 +137,7 @@ def hashmap_hash_map_insert_in_list_loop_back 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 + 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 /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ @@ -209,8 +207,8 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back | 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 + => + hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls decreasing_by hashmap_hash_map_move_elements_from_list_loop_decreases ntable ls /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ @@ -242,7 +240,7 @@ def hashmap_hash_map_move_elements_loop_fwd_back hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 else result.ret (ntable, slots) termination_by hashmap_hash_map_move_elements_loop_fwd_back ntable slots i => - hashmap_hash_map_move_elements_loop_terminates T ntable slots i + hashmap_hash_map_move_elements_loop_terminates T ntable slots i decreasing_by hashmap_hash_map_move_elements_loop_decreases ntable slots i /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ @@ -309,7 +307,7 @@ def hashmap_hash_map_contains_key_in_list_loop_fwd | 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 + 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 /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ @@ -339,8 +337,7 @@ def hashmap_hash_map_get_in_list_loop_fwd | 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 + hashmap_hash_map_get_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ @@ -370,8 +367,7 @@ def hashmap_hash_map_get_mut_in_list_loop_fwd | 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 + 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 /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -395,7 +391,7 @@ def hashmap_hash_map_get_mut_in_list_loop_back | 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 + 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 /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -458,8 +454,7 @@ def hashmap_hash_map_remove_from_list_loop_fwd | 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 + hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ @@ -490,8 +485,7 @@ def hashmap_hash_map_remove_from_list_loop_back | 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 + hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ |