summaryrefslogtreecommitdiff
path: root/tests/hol4/hashmap_main
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hol4/hashmap_main')
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_FunsScript.sml4
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig4
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml4
3 files changed, 6 insertions, 6 deletions
diff --git a/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
index c1e30aa6..2a17d185 100644
--- a/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
@@ -628,9 +628,9 @@ val insert_on_disk_fwd_def = Define ‘
insert_on_disk_fwd
(key : usize) (value : u64) (st : state) : (state # unit) result =
do
- (st0, hm) <- hashmap_utils_deserialize_fwd st;
+ (st0, hm) <- utils_deserialize_fwd st;
hm0 <- hashmap_hash_map_insert_fwd_back hm key value;
- (st1, _) <- hashmap_utils_serialize_fwd hm0 st0;
+ (st1, _) <- utils_serialize_fwd hm0 st0;
Return (st1, ())
od
diff --git a/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
index d4e43d9a..c19673bb 100644
--- a/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
@@ -583,9 +583,9 @@ sig
⊢ ∀key value st.
insert_on_disk_fwd key value st =
do
- (st0,hm) <- hashmap_utils_deserialize_fwd st;
+ (st0,hm) <- utils_deserialize_fwd st;
hm0 <- hashmap_hash_map_insert_fwd_back hm key value;
- (st1,_) <- hashmap_utils_serialize_fwd hm0 st0;
+ (st1,_) <- utils_serialize_fwd hm0 st0;
Return (st1,())
od
diff --git a/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
index f7221d92..9c29c0e0 100644
--- a/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
@@ -6,10 +6,10 @@ open hashmapMain_TypesTheory
val _ = new_theory "hashmapMain_Opaque"
-(** [hashmap_main::hashmap_utils::deserialize]: forward function *)val _ = new_constant ("hashmap_utils_deserialize_fwd",
+(** [hashmap_main::utils::deserialize]: forward function *)val _ = new_constant ("utils_deserialize_fwd",
“:state -> (state # u64 hashmap_hash_map_t) result”)
-(** [hashmap_main::hashmap_utils::serialize]: forward function *)val _ = new_constant ("hashmap_utils_serialize_fwd",
+(** [hashmap_main::utils::serialize]: forward function *)val _ = new_constant ("utils_serialize_fwd",
“:u64 hashmap_hash_map_t -> state -> (state # unit) result”)
val _ = export_theory ()