From c4d2af051c18c4c81b1e57a45210c37c89c8330f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 28 May 2024 11:18:35 +0200
Subject: tests: Rename hashmap_utils -> utils

---
 tests/hol4/hashmap_main/hashmapMain_FunsScript.sml   | 4 ++--
 tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig   | 4 ++--
 tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'tests/hol4/hashmap_main')

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 ()
-- 
cgit v1.2.3