Factor out some code and update some comments

1 files changed, 8 insertions, 68 deletions

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 26505902..033deebb 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -126,70 +126,6 @@ let cleanup_fresh_values_and_abs (config : config) (span : Meta.span)
   let ctx = cleanup_fresh_values fixed_ids ctx in
   (ctx, cc)
 
-(** Reorder the loans and borrows in the fresh abstractions.
-
-    We do this in order to enforce some structure in the environments: this
-    allows us to find fixed-points. Note that this function needs to be
-    called typically after we merge abstractions together (see {!collapse_ctx}
-    and {!reduce_ctx} for instance).
- *)
-let reorder_loans_borrows_in_fresh_abs (span : Meta.span)
-    (old_abs_ids : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx =
-  let reorder_in_fresh_abs (abs : abs) : abs =
-    (* Split between the loans and borrows *)
-    let is_borrow (av : typed_avalue) : bool =
-      match av.value with
-      | ABorrow _ -> true
-      | ALoan _ -> false
-      | _ -> craise __FILE__ __LINE__ span "Unexpected"
-    in
-    let aborrows, aloans = List.partition is_borrow abs.avalues in
-
-    (* Reoder the borrows, and the loans.
-
-       After experimenting, it seems that a good way of reordering the loans
-       and the borrows to find fixed points is simply to sort them by increasing
-       order of id (taking the smallest id of a set of ids, in case of sets).
-    *)
-    let get_borrow_id (av : typed_avalue) : BorrowId.id =
-      match av.value with
-      | ABorrow (AMutBorrow (pm, bid, _) | ASharedBorrow (pm, bid)) ->
-          sanity_check __FILE__ __LINE__ (pm = PNone) span;
-          bid
-      | _ -> craise __FILE__ __LINE__ span "Unexpected"
-    in
-    let get_loan_id (av : typed_avalue) : BorrowId.id =
-      match av.value with
-      | ALoan (AMutLoan (pm, lid, _)) ->
-          sanity_check __FILE__ __LINE__ (pm = PNone) span;
-          lid
-      | ALoan (ASharedLoan (pm, lids, _, _)) ->
-          sanity_check __FILE__ __LINE__ (pm = PNone) span;
-          BorrowId.Set.min_elt lids
-      | _ -> craise __FILE__ __LINE__ span "Unexpected"
-    in
-    (* We use ordered maps to reorder the borrows and loans *)
-    let reorder (get_bid : typed_avalue -> BorrowId.id)
-        (values : typed_avalue list) : typed_avalue list =
-      List.map snd
-        (BorrowId.Map.bindings
-           (BorrowId.Map.of_list (List.map (fun v -> (get_bid v, v)) values)))
-    in
-    let aborrows = reorder get_borrow_id aborrows in
-    let aloans = reorder get_loan_id aloans in
-    let avalues = List.append aborrows aloans in
-    { abs with avalues }
-  in
-
-  let reorder_in_abs (abs : abs) =
-    if AbstractionId.Set.mem abs.abs_id old_abs_ids then abs
-    else reorder_in_fresh_abs abs
-  in
-
-  let env = env_map_abs reorder_in_abs ctx.env in
-
-  { ctx with env }
-
 let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
     cm_fun =
  fun ctx0 ->
@@ -251,11 +187,14 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
        SL {l0, l1} s0
      ]}
 
-     and introduce the corresponding abstraction for the borrow l0
-     (and we do something similar for l1):
+     and introduce the corresponding abstractions for the borrows l0 and l1:
      {[
-       abs'2 { SB l0, SL {l2} s2 }
+       abs'2 { SB l0, SL {l0'} s1 } // Reborrow for l0
+       abs'3 { SB l1, SL {l1'} s2 } // Reborrow for l1
      ]}
+
+     Remark: of course we also need to replace the [SB l0] and the [SB l1]
+     values we find in the environments with [SB l0'] and [SB l1'].
   *)
   let push_abs_for_shared_value (abs : abs) (sv : typed_value)
       (lid : BorrowId.id) : unit =
@@ -821,7 +760,8 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
 
     (* Reorder the loans and borrows in the fresh abstractions in the fixed-point *)
     let fp =
-      reorder_loans_borrows_in_fresh_abs span (Option.get !fixed_ids).aids !fp
+      reorder_loans_borrows_in_fresh_abs span false (Option.get !fixed_ids).aids
+        !fp
     in
 
     (* Update the abstraction's [can_end] field and their kinds.