diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 14 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsJoinCtxs.ml | 17 |
2 files changed, 18 insertions, 13 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index d48635fc..653dea7c 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -1713,7 +1713,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) let ignored = mk_aignored span child_av.ty in let value = ABorrow (AMutBorrow (pm, bid, ignored)) in push { value; ty } - | ASharedBorrow (pm, _) -> + | ASharedBorrow _ -> (* Nothing specific to do: keep the value as it is *) push av | AIgnoredMutBorrow (opt_bid, child_av) -> @@ -2417,7 +2417,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) *) craise __FILE__ __LINE__ span "Unreachable" | Abstract (ty, bc) -> { value = ABorrow bc; ty }) - | Some bc0, Some bc1 -> + | Some _, Some _ -> (* With markers, the case where the same borrow is duplicated should now be unreachable. Note, this is due to all shared borrows currently taking different ids, this will not be the case anymore when shared loans will take a unique id instead of a set *) @@ -2480,7 +2480,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) craise __FILE__ __LINE__ span "Unreachable")) - | Some lc0, Some lc1 -> + | Some _, Some _ -> (* With projection markers, shared loans should not be duplicated *) craise __FILE__ __LINE__ span "Unreachable" | None, None -> craise __FILE__ __LINE__ span "Unreachable" @@ -2503,7 +2503,13 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) avalues := []; (* We recompute the relevant information on the abstraction after phase 1 *) - let { loans; borrows; borrows_loans; loan_to_content; borrow_to_content } = + let { + loans = _; + borrows = _; + borrows_loans; + loan_to_content; + borrow_to_content; + } = compute_merge_abstraction_info span ctx abs_values in diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 2f2dba41..4b5cfb82 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -190,10 +190,10 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) abs_ids; abs_to_borrows; abs_to_loans = _; - abs_to_borrows_loans; + abs_to_borrows_loans = _; borrow_to_abs = _; loan_to_abs; - borrow_loan_to_abs; + borrow_loan_to_abs = _; } = ids_maps in @@ -306,7 +306,6 @@ let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id) let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in let can_end = true in - let destructure_shared_values = true in let is_fresh_abs_id (id : AbstractionId.id) : bool = not (AbstractionId.Set.mem id old_ids.aids) in @@ -318,10 +317,10 @@ let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id) abs_ids; abs_to_borrows; abs_to_loans; - abs_to_borrows_loans; + abs_to_borrows_loans = _; borrow_to_abs; loan_to_abs; - borrow_loan_to_abs; + borrow_loan_to_abs = _; } = ids_maps in @@ -519,7 +518,7 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) Note that the join matcher doesn't implement match functions for avalues (see the comments in {!MakeJoinMatcher}. *) - let merge_amut_borrows id ty0 pm0 child0 _ty1 pm1 child1 = + let merge_amut_borrows id ty0 _pm0 child0 _ty1 _pm1 child1 = (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; @@ -535,7 +534,7 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) { value; ty } in - let merge_ashared_borrows id ty0 pm0 ty1 pm1 = + let merge_ashared_borrows id ty0 _pm0 ty1 _pm1 = (* Sanity checks *) let _ = let _, ty0, _ = ty_as_ref ty0 in @@ -554,7 +553,7 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) { value; ty } in - let merge_amut_loans id ty0 pm0 child0 _ty1 pm1 child1 = + let merge_amut_loans id ty0 _pm0 child0 _ty1 _pm1 child1 = (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; @@ -565,7 +564,7 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) let value = ALoan (AMutLoan (PNone, id, child)) in { value; ty } in - let merge_ashared_loans ids ty0 pm0 (sv0 : typed_value) child0 _ty1 pm1 + let merge_ashared_loans ids ty0 _pm0 (sv0 : typed_value) child0 _ty1 _pm1 (sv1 : typed_value) child1 = (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; |