diff options
Diffstat (limited to 'tests/hol4/hashmap/hashmap_FunsScript.sml')
| -rw-r--r-- | tests/hol4/hashmap/hashmap_FunsScript.sml | 85 |
1 files changed, 47 insertions, 38 deletions
diff --git a/tests/hol4/hashmap/hashmap_FunsScript.sml b/tests/hol4/hashmap/hashmap_FunsScript.sml index 9ad497f5..1ed57080 100644 --- a/tests/hol4/hashmap/hashmap_FunsScript.sml +++ b/tests/hol4/hashmap/hashmap_FunsScript.sml @@ -7,13 +7,13 @@ val _ = new_theory "hashmap_Funs" val hash_key_fwd_def = Define ‘ - (** [hashmap::hash_key] *) + (** [hashmap::hash_key]: forward function *) hash_key_fwd (k : usize) : usize result = Return k ’ val [hash_map_allocate_slots_loop_fwd_def] = DefineDiv ‘ - (** [hashmap::HashMap::{0}::allocate_slots] *) + (** [hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *) hash_map_allocate_slots_loop_fwd (slots : 't list_t vec) (n : usize) : 't list_t vec result = if usize_gt n (int_to_usize 0) @@ -27,14 +27,14 @@ val [hash_map_allocate_slots_loop_fwd_def] = DefineDiv ‘ ’ val hash_map_allocate_slots_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::allocate_slots] *) + (** [hashmap::HashMap::{0}::allocate_slots]: forward function *) hash_map_allocate_slots_fwd (slots : 't list_t vec) (n : usize) : 't list_t vec result = hash_map_allocate_slots_loop_fwd slots n ’ val hash_map_new_with_capacity_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::new_with_capacity] *) + (** [hashmap::HashMap::{0}::new_with_capacity]: forward function *) hash_map_new_with_capacity_fwd (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) : 't hash_map_t result @@ -55,14 +55,15 @@ val hash_map_new_with_capacity_fwd_def = Define ‘ ’ val hash_map_new_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::new] *) + (** [hashmap::HashMap::{0}::new]: forward function *) hash_map_new_fwd : 't hash_map_t result = hash_map_new_with_capacity_fwd (int_to_usize 32) (int_to_usize 4) (int_to_usize 5) ’ val [hash_map_clear_loop_fwd_back_def] = DefineDiv ‘ - (** [hashmap::HashMap::{0}::clear] *) + (** [hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) hash_map_clear_loop_fwd_back (slots : 't list_t vec) (i : usize) : 't list_t vec result = let i0 = vec_len slots in @@ -77,7 +78,8 @@ val [hash_map_clear_loop_fwd_back_def] = DefineDiv ‘ ’ val hash_map_clear_fwd_back_def = Define ‘ - (** [hashmap::HashMap::{0}::clear] *) + (** [hashmap::HashMap::{0}::clear]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) hash_map_clear_fwd_back (self : 't hash_map_t) : 't hash_map_t result = do v <- hash_map_clear_loop_fwd_back self.hash_map_slots (int_to_usize 0); @@ -91,13 +93,13 @@ val hash_map_clear_fwd_back_def = Define ‘ ’ val hash_map_len_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::len] *) + (** [hashmap::HashMap::{0}::len]: forward function *) hash_map_len_fwd (self : 't hash_map_t) : usize result = Return self.hash_map_num_entries ’ val [hash_map_insert_in_list_loop_fwd_def] = DefineDiv ‘ - (** [hashmap::HashMap::{0}::insert_in_list] *) + (** [hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *) hash_map_insert_in_list_loop_fwd (key : usize) (value : 't) (ls : 't list_t) : bool result = (case ls of @@ -109,14 +111,14 @@ val [hash_map_insert_in_list_loop_fwd_def] = DefineDiv ‘ ’ val hash_map_insert_in_list_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::insert_in_list] *) + (** [hashmap::HashMap::{0}::insert_in_list]: forward function *) hash_map_insert_in_list_fwd (key : usize) (value : 't) (ls : 't list_t) : bool result = hash_map_insert_in_list_loop_fwd key value ls ’ val [hash_map_insert_in_list_loop_back_def] = DefineDiv ‘ - (** [hashmap::HashMap::{0}::insert_in_list] *) + (** [hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *) hash_map_insert_in_list_loop_back (key : usize) (value : 't) (ls : 't list_t) : 't list_t result = (case ls of @@ -132,14 +134,15 @@ val [hash_map_insert_in_list_loop_back_def] = DefineDiv ‘ ’ val hash_map_insert_in_list_back_def = Define ‘ - (** [hashmap::HashMap::{0}::insert_in_list] *) + (** [hashmap::HashMap::{0}::insert_in_list]: backward function 0 *) hash_map_insert_in_list_back (key : usize) (value : 't) (ls : 't list_t) : 't list_t result = hash_map_insert_in_list_loop_back key value ls ’ val hash_map_insert_no_resize_fwd_back_def = Define ‘ - (** [hashmap::HashMap::{0}::insert_no_resize] *) + (** [hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) hash_map_insert_no_resize_fwd_back (self : 't hash_map_t) (key : usize) (value : 't) : 't hash_map_t result = do @@ -176,7 +179,8 @@ Definition core_num_u32_max_c_def: End val [hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘ - (** [hashmap::HashMap::{0}::move_elements_from_list] *) + (** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) hash_map_move_elements_from_list_loop_fwd_back (ntable : 't hash_map_t) (ls : 't list_t) : 't hash_map_t result = (case ls of @@ -189,14 +193,16 @@ val [hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘ ’ val hash_map_move_elements_from_list_fwd_back_def = Define ‘ - (** [hashmap::HashMap::{0}::move_elements_from_list] *) + (** [hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) hash_map_move_elements_from_list_fwd_back (ntable : 't hash_map_t) (ls : 't list_t) : 't hash_map_t result = hash_map_move_elements_from_list_loop_fwd_back ntable ls ’ val [hash_map_move_elements_loop_fwd_back_def] = DefineDiv ‘ - (** [hashmap::HashMap::{0}::move_elements] *) + (** [hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) hash_map_move_elements_loop_fwd_back (ntable : 't hash_map_t) (slots : 't list_t vec) (i : usize) : ('t hash_map_t # 't list_t vec) result @@ -221,7 +227,8 @@ val [hash_map_move_elements_loop_fwd_back_def] = DefineDiv ‘ ’ val hash_map_move_elements_fwd_back_def = Define ‘ - (** [hashmap::HashMap::{0}::move_elements] *) + (** [hashmap::HashMap::{0}::move_elements]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) hash_map_move_elements_fwd_back (ntable : 't hash_map_t) (slots : 't list_t vec) (i : usize) : ('t hash_map_t # 't list_t vec) result @@ -230,7 +237,8 @@ val hash_map_move_elements_fwd_back_def = Define ‘ ’ val hash_map_try_resize_fwd_back_def = Define ‘ - (** [hashmap::HashMap::{0}::try_resize] *) + (** [hashmap::HashMap::{0}::try_resize]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) hash_map_try_resize_fwd_back (self : 't hash_map_t) : 't hash_map_t result = do max_usize <- mk_usize (u32_to_int core_num_u32_max_c); @@ -263,7 +271,8 @@ val hash_map_try_resize_fwd_back_def = Define ‘ ’ val hash_map_insert_fwd_back_def = Define ‘ - (** [hashmap::HashMap::{0}::insert] *) + (** [hashmap::HashMap::{0}::insert]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) hash_map_insert_fwd_back (self : 't hash_map_t) (key : usize) (value : 't) : 't hash_map_t result = do @@ -276,7 +285,7 @@ val hash_map_insert_fwd_back_def = Define ‘ ’ val [hash_map_contains_key_in_list_loop_fwd_def] = DefineDiv ‘ - (** [hashmap::HashMap::{0}::contains_key_in_list] *) + (** [hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *) hash_map_contains_key_in_list_loop_fwd (key : usize) (ls : 't list_t) : bool result = (case ls of @@ -288,14 +297,14 @@ val [hash_map_contains_key_in_list_loop_fwd_def] = DefineDiv ‘ ’ val hash_map_contains_key_in_list_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::contains_key_in_list] *) + (** [hashmap::HashMap::{0}::contains_key_in_list]: forward function *) hash_map_contains_key_in_list_fwd (key : usize) (ls : 't list_t) : bool result = hash_map_contains_key_in_list_loop_fwd key ls ’ val hash_map_contains_key_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::contains_key] *) + (** [hashmap::HashMap::{0}::contains_key]: forward function *) hash_map_contains_key_fwd (self : 't hash_map_t) (key : usize) : bool result = do @@ -310,7 +319,7 @@ val hash_map_contains_key_fwd_def = Define ‘ ’ val [hash_map_get_in_list_loop_fwd_def] = DefineDiv ‘ - (** [hashmap::HashMap::{0}::get_in_list] *) + (** [hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *) hash_map_get_in_list_loop_fwd (key : usize) (ls : 't list_t) : 't result = (case ls of | ListCons ckey cvalue tl => @@ -321,13 +330,13 @@ val [hash_map_get_in_list_loop_fwd_def] = DefineDiv ‘ ’ val hash_map_get_in_list_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::get_in_list] *) + (** [hashmap::HashMap::{0}::get_in_list]: forward function *) hash_map_get_in_list_fwd (key : usize) (ls : 't list_t) : 't result = hash_map_get_in_list_loop_fwd key ls ’ val hash_map_get_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::get] *) + (** [hashmap::HashMap::{0}::get]: forward function *) hash_map_get_fwd (self : 't hash_map_t) (key : usize) : 't result = do hash <- hash_key_fwd key; @@ -341,7 +350,7 @@ val hash_map_get_fwd_def = Define ‘ ’ val [hash_map_get_mut_in_list_loop_fwd_def] = DefineDiv ‘ - (** [hashmap::HashMap::{0}::get_mut_in_list] *) + (** [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *) hash_map_get_mut_in_list_loop_fwd (ls : 't list_t) (key : usize) : 't result = (case ls of @@ -353,13 +362,13 @@ val [hash_map_get_mut_in_list_loop_fwd_def] = DefineDiv ‘ ’ val hash_map_get_mut_in_list_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::get_mut_in_list] *) + (** [hashmap::HashMap::{0}::get_mut_in_list]: forward function *) hash_map_get_mut_in_list_fwd (ls : 't list_t) (key : usize) : 't result = hash_map_get_mut_in_list_loop_fwd ls key ’ val [hash_map_get_mut_in_list_loop_back_def] = DefineDiv ‘ - (** [hashmap::HashMap::{0}::get_mut_in_list] *) + (** [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *) hash_map_get_mut_in_list_loop_back (ls : 't list_t) (key : usize) (ret : 't) : 't list_t result = (case ls of @@ -375,14 +384,14 @@ val [hash_map_get_mut_in_list_loop_back_def] = DefineDiv ‘ ’ val hash_map_get_mut_in_list_back_def = Define ‘ - (** [hashmap::HashMap::{0}::get_mut_in_list] *) + (** [hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *) hash_map_get_mut_in_list_back (ls : 't list_t) (key : usize) (ret : 't) : 't list_t result = hash_map_get_mut_in_list_loop_back ls key ret ’ val hash_map_get_mut_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::get_mut] *) + (** [hashmap::HashMap::{0}::get_mut]: forward function *) hash_map_get_mut_fwd (self : 't hash_map_t) (key : usize) : 't result = do hash <- hash_key_fwd key; @@ -396,7 +405,7 @@ val hash_map_get_mut_fwd_def = Define ‘ ’ val hash_map_get_mut_back_def = Define ‘ - (** [hashmap::HashMap::{0}::get_mut] *) + (** [hashmap::HashMap::{0}::get_mut]: backward function 0 *) hash_map_get_mut_back (self : 't hash_map_t) (key : usize) (ret : 't) : 't hash_map_t result = do @@ -413,7 +422,7 @@ val hash_map_get_mut_back_def = Define ‘ ’ val [hash_map_remove_from_list_loop_fwd_def] = DefineDiv ‘ - (** [hashmap::HashMap::{0}::remove_from_list] *) + (** [hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *) hash_map_remove_from_list_loop_fwd (key : usize) (ls : 't list_t) : 't option result = (case ls of @@ -429,14 +438,14 @@ val [hash_map_remove_from_list_loop_fwd_def] = DefineDiv ‘ ’ val hash_map_remove_from_list_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::remove_from_list] *) + (** [hashmap::HashMap::{0}::remove_from_list]: forward function *) hash_map_remove_from_list_fwd (key : usize) (ls : 't list_t) : 't option result = hash_map_remove_from_list_loop_fwd key ls ’ val [hash_map_remove_from_list_loop_back_def] = DefineDiv ‘ - (** [hashmap::HashMap::{0}::remove_from_list] *) + (** [hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *) hash_map_remove_from_list_loop_back (key : usize) (ls : 't list_t) : 't list_t result = (case ls of @@ -456,14 +465,14 @@ val [hash_map_remove_from_list_loop_back_def] = DefineDiv ‘ ’ val hash_map_remove_from_list_back_def = Define ‘ - (** [hashmap::HashMap::{0}::remove_from_list] *) + (** [hashmap::HashMap::{0}::remove_from_list]: backward function 1 *) hash_map_remove_from_list_back (key : usize) (ls : 't list_t) : 't list_t result = hash_map_remove_from_list_loop_back key ls ’ val hash_map_remove_fwd_def = Define ‘ - (** [hashmap::HashMap::{0}::remove] *) + (** [hashmap::HashMap::{0}::remove]: forward function *) hash_map_remove_fwd (self : 't hash_map_t) (key : usize) : 't option result = do hash <- hash_key_fwd key; @@ -484,7 +493,7 @@ val hash_map_remove_fwd_def = Define ‘ ’ val hash_map_remove_back_def = Define ‘ - (** [hashmap::HashMap::{0}::remove] *) + (** [hashmap::HashMap::{0}::remove]: backward function 0 *) hash_map_remove_back (self : 't hash_map_t) (key : usize) : 't hash_map_t result = do @@ -513,7 +522,7 @@ val hash_map_remove_back_def = Define ‘ ’ val test1_fwd_def = Define ‘ - (** [hashmap::test1] *) + (** [hashmap::test1]: forward function *) test1_fwd : unit result = do hm <- hash_map_new_fwd; |