Change some fun id names to use "Mut"/"Shared" as a suffix

5 files changed, 66 insertions, 66 deletions

diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index 572b0a24..11cd5666 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -416,44 +416,44 @@ let assumed_infos : assumed_info list =
       true,
       to_name (index_pre @ [ "IndexMut"; "index_mut" ]) );
     (* Array Index *)
-    ( ArraySharedIndex,
+    ( ArrayIndexShared,
       Sig.array_index_sig false,
       true,
-      to_name [ "@ArraySharedIndex" ] );
-    (ArrayMutIndex, Sig.array_index_sig true, true, to_name [ "@ArrayMutIndex" ]);
+      to_name [ "@ArrayIndexShared" ] );
+    (ArrayIndexMut, Sig.array_index_sig true, true, to_name [ "@ArrayIndexMut" ]);
     (* Array to slice*)
-    ( ArrayToSharedSlice,
+    ( ArrayToSliceShared,
       Sig.array_to_slice_sig false,
       true,
-      to_name [ "@ArrayToSharedSlice" ] );
-    ( ArrayToMutSlice,
+      to_name [ "@ArrayToSliceShared" ] );
+    ( ArrayToSliceMut,
       Sig.array_to_slice_sig true,
       true,
-      to_name [ "@ArrayToMutSlice" ] );
+      to_name [ "@ArrayToSliceMut" ] );
     (* Array Subslice *)
-    ( ArraySharedSubslice,
+    ( ArraySubsliceShared,
       Sig.array_subslice_sig false,
       true,
-      to_name [ "@ArraySharedSubslice" ] );
-    ( ArrayMutSubslice,
+      to_name [ "@ArraySubsliceShared" ] );
+    ( ArraySubsliceMut,
       Sig.array_subslice_sig true,
       true,
-      to_name [ "@ArrayMutSubslice" ] );
+      to_name [ "@ArraySubsliceMut" ] );
     (* Slice Index *)
-    ( SliceSharedIndex,
+    ( SliceIndexShared,
       Sig.slice_index_sig false,
       true,
-      to_name [ "@SliceSharedIndex" ] );
-    (SliceMutIndex, Sig.slice_index_sig true, true, to_name [ "@SliceMutIndex" ]);
+      to_name [ "@SliceIndexShared" ] );
+    (SliceIndexMut, Sig.slice_index_sig true, true, to_name [ "@SliceIndexMut" ]);
     (* Slice Subslice *)
-    ( SliceSharedSubslice,
+    ( SliceSubsliceShared,
       Sig.slice_subslice_sig false,
       true,
-      to_name [ "@SliceSharedSubslice" ] );
-    ( SliceMutSubslice,
+      to_name [ "@SliceSubsliceShared" ] );
+    ( SliceSubsliceMut,
       Sig.slice_subslice_sig true,
       true,
-      to_name [ "@SliceMutSubslice" ] );
+      to_name [ "@SliceSubsliceMut" ] );
     (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ]);
   ]
 
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 297c182a..c4238d83 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -329,21 +329,21 @@ let assumed_llbc_functions () :
         (VecIndex, rg0, "vec_index_back") (* shouldn't be used *);
         (VecIndexMut, None, "vec_index_mut_fwd");
         (VecIndexMut, rg0, "vec_index_mut_back");
-        (ArraySharedIndex, None, "array_index_shared");
-        (ArrayMutIndex, None, "array_index_mut_fwd");
-        (ArrayMutIndex, rg0, "array_index_mut_back");
-        (ArrayToSharedSlice, None, "array_to_slice_shared");
-        (ArrayToMutSlice, None, "array_to_slice_mut_fwd");
-        (ArrayToMutSlice, rg0, "array_to_slice_mut_back");
-        (ArraySharedSubslice, None, "array_subslice_shared");
-        (ArrayMutSubslice, None, "array_subslice_mut_fwd");
-        (ArrayMutSubslice, rg0, "array_subslice_mut_back");
-        (SliceSharedIndex, None, "slice_index_shared");
-        (SliceMutIndex, None, "slice_index_mut_fwd");
-        (SliceMutIndex, rg0, "slice_index_mut_back");
-        (SliceSharedSubslice, None, "slice_subslice_shared");
-        (SliceMutSubslice, None, "slice_subslice_mut_fwd");
-        (SliceMutSubslice, rg0, "slice_subslice_mut_back");
+        (ArrayIndexShared, None, "array_index_shared");
+        (ArrayIndexMut, None, "array_index_mut_fwd");
+        (ArrayIndexMut, rg0, "array_index_mut_back");
+        (ArrayToSliceShared, None, "array_to_slice_shared");
+        (ArrayToSliceMut, None, "array_to_slice_mut_fwd");
+        (ArrayToSliceMut, rg0, "array_to_slice_mut_back");
+        (ArraySubsliceShared, None, "array_subslice_shared");
+        (ArraySubsliceMut, None, "array_subslice_mut_fwd");
+        (ArraySubsliceMut, rg0, "array_subslice_mut_back");
+        (SliceIndexShared, None, "slice_index_shared");
+        (SliceIndexMut, None, "slice_index_mut_fwd");
+        (SliceIndexMut, rg0, "slice_index_mut_back");
+        (SliceSubsliceShared, None, "slice_subslice_shared");
+        (SliceSubsliceMut, None, "slice_subslice_mut_fwd");
+        (SliceSubsliceMut, rg0, "slice_subslice_mut_back");
         (SliceLen, None, "slice_len");
       ]
   | Lean ->
@@ -360,21 +360,21 @@ let assumed_llbc_functions () :
         (VecIndex, rg0, "Vec.index_shared_back") (* shouldn't be used *);
         (VecIndexMut, None, "Vec.index_mut");
         (VecIndexMut, rg0, "Vec.index_mut_back");
-        (ArraySharedIndex, None, "Array.index_shared");
-        (ArrayMutIndex, None, "Array.index_mut");
-        (ArrayMutIndex, rg0, "Array.index_mut_back");
-        (ArrayToSharedSlice, None, "Array.to_slice_shared");
-        (ArrayToMutSlice, None, "Array.to_slice_mut");
-        (ArrayToMutSlice, rg0, "Array.to_slice_mut_back");
-        (ArraySharedSubslice, None, "Array.subslice_shared");
-        (ArrayMutSubslice, None, "Array.subslice_mut");
-        (ArrayMutSubslice, rg0, "Array.subslice_mut_back");
-        (SliceSharedIndex, None, "Slice.index_shared");
-        (SliceMutIndex, None, "Slice.index_mut");
-        (SliceMutIndex, rg0, "Slice.index_mut_back");
-        (SliceSharedSubslice, None, "Slice.subslice_shared");
-        (SliceMutSubslice, None, "Slice.subslice_mut");
-        (SliceMutSubslice, rg0, "Slice.subslice_mut_back");
+        (ArrayIndexShared, None, "Array.index_shared");
+        (ArrayIndexMut, None, "Array.index_mut");
+        (ArrayIndexMut, rg0, "Array.index_mut_back");
+        (ArrayToSliceShared, None, "Array.to_slice_shared");
+        (ArrayToSliceMut, None, "Array.to_slice_mut");
+        (ArrayToSliceMut, rg0, "Array.to_slice_mut_back");
+        (ArraySubsliceShared, None, "Array.subslice_shared");
+        (ArraySubsliceMut, None, "Array.subslice_mut");
+        (ArraySubsliceMut, rg0, "Array.subslice_mut_back");
+        (SliceIndexShared, None, "Slice.index_shared");
+        (SliceIndexMut, None, "Slice.index_mut");
+        (SliceIndexMut, rg0, "Slice.index_mut_back");
+        (SliceSubsliceShared, None, "Slice.subslice_shared");
+        (SliceSubsliceMut, None, "Slice.subslice_mut");
+        (SliceSubsliceMut, rg0, "Slice.subslice_mut_back");
         (SliceLen, None, "Slice.len");
       ]
 
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 157cca38..045c4484 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -644,10 +644,10 @@ let eval_non_local_function_call_concrete (config : C.config)
           | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut ->
               eval_vec_function_concrete config fid region_params type_params
                 cg_params
-          | ArraySharedIndex | ArrayMutIndex | ArrayToSharedSlice
-          | ArrayToMutSlice | ArraySharedSubslice | ArrayMutSubslice
-          | SliceSharedIndex | SliceMutIndex | SliceSharedSubslice
-          | SliceMutSubslice | SliceLen ->
+          | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared
+          | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut
+          | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
+          | SliceSubsliceMut | SliceLen ->
               raise (Failure "Unimplemented")
         in
 
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index ad7ab05f..cfb63ec2 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -506,17 +506,17 @@ let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string =
   | A.VecLen -> "alloc::vec::Vec::len"
   | A.VecIndex -> "core::ops::index::Index<alloc::vec::Vec>::index"
   | A.VecIndexMut -> "core::ops::index::IndexMut<alloc::vec::Vec>::index_mut"
-  | ArraySharedIndex -> "@ArraySharedIndex"
-  | ArrayMutIndex -> "@ArrayMutIndex"
-  | ArrayToSharedSlice -> "@ArrayToSharedSlice"
-  | ArrayToMutSlice -> "@ArrayToMutSlice"
-  | ArraySharedSubslice -> "@ArraySharedSubslice"
-  | ArrayMutSubslice -> "@ArrayMutSubslice"
+  | ArrayIndexShared -> "@ArrayIndexShared"
+  | ArrayIndexMut -> "@ArrayIndexMut"
+  | ArrayToSliceShared -> "@ArrayToSliceShared"
+  | ArrayToSliceMut -> "@ArrayToSliceMut"
+  | ArraySubsliceShared -> "@ArraySubsliceShared"
+  | ArraySubsliceMut -> "@ArraySubsliceMut"
   | SliceLen -> "@SliceLen"
-  | SliceSharedIndex -> "@SliceSharedIndex"
-  | SliceMutIndex -> "@SliceMutIndex"
-  | SliceSharedSubslice -> "@SliceSharedSubslice"
-  | SliceMutSubslice -> "@SliceMutSubslice"
+  | SliceIndexShared -> "@SliceIndexShared"
+  | SliceIndexMut -> "@SliceIndexMut"
+  | SliceSubsliceShared -> "@SliceSubsliceShared"
+  | SliceSubsliceMut -> "@SliceSubsliceMut"
 
 let pure_assumed_fun_id_to_string (fid : pure_assumed_fun_id) : string =
   match fid with
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 52eeee26..b6025df4 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1564,10 +1564,10 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     assert (args = []);
                     mk_unit_rvalue
                 | ( ( A.Replace | VecNew | VecPush | VecInsert | VecLen
-                    | VecIndex | VecIndexMut | ArraySharedSubslice
-                    | ArrayMutSubslice | SliceSharedIndex | SliceMutIndex
-                    | SliceSharedSubslice | SliceMutSubslice | ArraySharedIndex
-                    | ArrayMutIndex | ArrayToSharedSlice | ArrayToMutSlice
+                    | VecIndex | VecIndexMut | ArraySubsliceShared
+                    | ArraySubsliceMut | SliceIndexShared | SliceIndexMut
+                    | SliceSubsliceShared | SliceSubsliceMut | ArrayIndexShared
+                    | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
                     | SliceLen ),
                     _ ) ->
                     super#visit_texpression env e)