summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Assumed.ml36
-rw-r--r--compiler/Extract.ml60
-rw-r--r--compiler/InterpreterStatements.ml8
-rw-r--r--compiler/PrintPure.ml20
-rw-r--r--compiler/PureMicroPasses.ml8
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)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 08:29:04 +0000