diff options
| author | Son HO | 2023-11-10 18:21:06 +0100 |
|---|---|---|
| committer | GitHub | 2023-11-10 18:21:06 +0100 |
| commit | 587f1ebc0178acb19029d3fc9a729c197082aba7 (patch) | |
| tree | f29805e5426f9f3fabe12d3fdadda96a1e987880 /tests/hol4/hashmap_on_disk | |
| parent | 7fc7c82aa61d782b335e7cf37231fd9998cd0d89 (diff) | |
| parent | d300be95c28ff3147bb6f6a65992df5b9b571bdf (diff) | |
Merge pull request #44 from AeneasVerif/son_traits_types
Add support for traits
Diffstat (limited to 'tests/hol4/hashmap_on_disk')
| -rw-r--r-- | tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml | 10 | ||||
| -rw-r--r-- | tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig | 12 |
2 files changed, 2 insertions, 20 deletions
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml index b21c4f58..c1e30aa6 100644 --- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml +++ b/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml @@ -193,14 +193,6 @@ val hashmap_hash_map_insert_no_resize_fwd_back_def = Define ‘ od ’ -(** [core::num::u32::{8}::MAX] *) -Definition core_num_u32_max_body_def: - core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295) -End -Definition core_num_u32_max_c_def: - core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body -End - val [hashmap_hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘ (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) @@ -271,7 +263,7 @@ val hashmap_hash_map_try_resize_fwd_back_def = Define ‘ hashmap_hash_map_try_resize_fwd_back (self : 't hashmap_hash_map_t) : 't hashmap_hash_map_t result = do - max_usize <- mk_usize (u32_to_int core_num_u32_max_c); + max_usize <- mk_usize (u32_to_int core_u32_max); let capacity = vec_len self.hashmap_hash_map_slots in do n1 <- usize_div max_usize (int_to_usize 2); diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig index 1d24cb26..d4e43d9a 100644 --- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig +++ b/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig @@ -3,8 +3,6 @@ sig type thm = Thm.thm (* Definitions *) - val core_num_u32_max_body_def : thm - val core_num_u32_max_c_def : thm val hashmap_hash_key_fwd_def : thm val hashmap_hash_map_allocate_slots_fwd_def : thm val hashmap_hash_map_allocate_slots_loop_fwd_def : thm @@ -50,14 +48,6 @@ sig (* [hashmapMain_Opaque] Parent theory of "hashmapMain_Funs" - [core_num_u32_max_body_def] Definition - - ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295) - - [core_num_u32_max_c_def] Definition - - ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body - [hashmap_hash_key_fwd_def] Definition ⊢ ∀k. hashmap_hash_key_fwd k = Return k @@ -506,7 +496,7 @@ sig ⊢ ∀self. hashmap_hash_map_try_resize_fwd_back self = do - max_usize <- mk_usize (u32_to_int core_num_u32_max_c); + max_usize <- mk_usize (u32_to_int core_u32_max); capacity <<- vec_len self.hashmap_hash_map_slots; n1 <- usize_div max_usize (int_to_usize 2); (i,i0) <<- self.hashmap_hash_map_max_load_factor; |