summaryrefslogtreecommitdiff
path: root/tests/hol4/hashmap_on_disk
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml10
-rw-r--r--tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig12
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;