Cleanup a bit

1 files changed, 18 insertions, 59 deletions

diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 1c1ae0bc..d5d6fa7e 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -2659,7 +2659,6 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
      environments upon loop *reentry*, and synthesize nothing by
      returning [None]
   *)
-  let ctx_upon_entry = ref None in
   let ctxs = ref [] in
   let register_ctx ctx = ctxs := ctx :: !ctxs in
 
@@ -2708,7 +2707,6 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
   (* Join the contexts at the loop entry - ctx1 is the current joined
      context (the context at the loop entry, after we called
      {!prepare_ashared_loans}, if this is the first iteration) *)
-  (* TODO: ctx_upon_entry is useless, it should be ctx0? *)
   let join_ctxs (ctx1 : C.eval_ctx) : C.eval_ctx =
     (* If this is the first iteration, end the borrows/loans/abs which
        appear in ctx1 and not in the other contexts, then compute the
@@ -2747,33 +2745,33 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
     in
 
     let fixed_ids = Option.get !fixed_ids in
-    let (ctx1', _), ctx2 =
+    let (_, _), ctx2 =
       loop_join_origin_with_continue_ctxs config loop_id fixed_ids ctx1 !ctxs
     in
     ctxs := [];
-    if !ctx_upon_entry = None then ctx_upon_entry := Some ctx1';
     ctx2
   in
-  (* Check if two contexts are equivalent - modulo alpha conversion on the
-     existentially quantified borrows/abstractions/symbolic values.
-  *)
-  let compute_fixed_ids (ctx1 : C.eval_ctx) (ctx2 : C.eval_ctx) : ids_sets =
-    (* Compute the set of fixed ids - for the symbolic ids, we compute the
-       intersection of ids between the original environment and [ctx1]
-       and [ctx2] *)
+  (* Compute the set of fixed ids - for the symbolic ids, we compute the
+     intersection of ids between the original environment and the list
+     of new environments *)
+  let compute_fixed_ids (ctxl : C.eval_ctx list) : ids_sets =
     let fixed_ids, _ = compute_context_ids ctx0 in
     let { aids; blids; borrow_ids; loan_ids; dids; rids; sids } = fixed_ids in
-    let fixed_ids1, _ = compute_context_ids ctx1 in
-    let fixed_ids2, _ = compute_context_ids ctx2 in
-    let sids =
-      V.SymbolicValueId.Set.inter sids
-        (V.SymbolicValueId.Set.inter fixed_ids1.sids fixed_ids2.sids)
-    in
+    let sids = ref sids in
+    List.iter
+      (fun ctx ->
+        let fixed_ids, _ = compute_context_ids ctx in
+        sids := V.SymbolicValueId.Set.inter !sids fixed_ids.sids)
+      ctxl;
+    let sids = !sids in
     let fixed_ids = { aids; blids; borrow_ids; loan_ids; dids; rids; sids } in
     fixed_ids
   in
+  (* Check if two contexts are equivalent - modulo alpha conversion on the
+     existentially quantified borrows/abstractions/symbolic values.
+  *)
   let equiv_ctxs (ctx1 : C.eval_ctx) (ctx2 : C.eval_ctx) : bool =
-    let fixed_ids = compute_fixed_ids ctx1 ctx2 in
+    let fixed_ids = compute_fixed_ids [ ctx1; ctx2 ] in
     let check_equivalent = true in
     let lookup_shared_value _ = raise (Failure "Unreachable") in
     Option.is_some
@@ -3025,7 +3023,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
     (* Return *)
     fp
   in
-  let fixed_ids = compute_fixed_ids (Option.get !ctx_upon_entry) fp in
+  let fixed_ids = compute_fixed_ids [ fp ] in
 
   (* Return *)
   (fp, fixed_ids)
@@ -3461,44 +3459,6 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
      context, which results from joins during which we ended the loans which
      were introduced during the loop iterations)
   *)
-  (* End the borrows in the dummy values - TODO: is this useful? *)
-  let rec cf_reorganize_dummy_tgt : cm_fun =
-   fun cf tgt_ctx ->
-    (* Collect the dummy values in the target context *)
-    let _, _, tgt_dummies = ctx_split_fixed_new fixed_ids tgt_ctx in
-
-    (* Whenever we find a borrow which can be ended (doesn't contain loans)
-       we end it *)
-    let bid = ref None in
-    try
-      let visitor =
-        object
-          inherit [_] V.iter_typed_value
-
-          method! visit_SharedBorrow _ l =
-            bid := Some l;
-            raise Utils.Found
-
-          method! visit_MutBorrow _ l v =
-            if not (value_has_loans v.value) then (
-              bid := Some l;
-              raise Utils.Found)
-            else ()
-        end
-      in
-      List.iter (visitor#visit_typed_value ()) tgt_dummies;
-
-      log#ldebug
-        (lazy
-          ("match_ctx_with_target: after reorganizing dummies:\n"
-         ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- tgt_ctx: "
-         ^ eval_ctx_to_string tgt_ctx));
-
-      cf tgt_ctx
-    with Utils.Found ->
-      let cc = InterpreterBorrows.end_borrow config (Option.get !bid) in
-      comp cc cf_reorganize_dummy_tgt cf tgt_ctx
-  in
   (* End the loans which lead to mismatches when joining *)
   let rec cf_reorganize_join_tgt : cm_fun =
    fun cf tgt_ctx ->
@@ -3803,8 +3763,7 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
   in
 
   (* Compose and continue *)
-  comp cf_reorganize_dummy_tgt cf_reorganize_join_tgt cf_introduce_loop_fp_abs
-    tgt_ctx
+  cf_reorganize_join_tgt cf_introduce_loop_fp_abs tgt_ctx
 
 (** Evaluate a loop in concrete mode *)
 let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun =