Make progress on the fixed point computation

6 files changed, 381 insertions, 400 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 3e882365..b37d4a84 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -82,7 +82,7 @@ let return_unit_end_abs_with_no_loans = true
     thus use this bound to detect a loop, fail and report the case to the
     user.
  *)
-let loop_fixed_point_max_num_iters = 100
+let loop_fixed_point_max_num_iters = 2
 
 (** {1 Translation} *)
 
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index be758ffe..cb6a092f 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -439,22 +439,9 @@ let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
 (** Visitor to iterate over the values in the *current* frame *)
 class ['self] iter_frame =
   object (self : 'self)
-    inherit [_] V.iter_abs
+    inherit [_] iter_env
 
-    method visit_Var : 'acc -> binder -> typed_value -> unit =
-      fun acc _ v -> self#visit_typed_value acc v
-
-    method visit_Abs : 'acc -> abs -> unit =
-      fun acc abs -> self#visit_abs acc abs
-
-    method visit_env_elem : 'acc -> env_elem -> unit =
-      fun acc em ->
-        match em with
-        | Var (vid, v) -> self#visit_Var acc vid v
-        | Abs abs -> self#visit_Abs acc abs
-        | Frame -> raise (Failure "Unreachable")
-
-    method visit_env : 'acc -> env -> unit =
+    method! visit_env : 'acc -> env -> unit =
       fun acc env ->
         match env with
         | [] -> ()
@@ -467,24 +454,9 @@ class ['self] iter_frame =
 (** Visitor to map over the values in the *current* frame *)
 class ['self] map_frame_concrete =
   object (self : 'self)
-    inherit [_] V.map_abs
-
-    method visit_Var : 'acc -> binder -> typed_value -> env_elem =
-      fun acc b v ->
-        let v = self#visit_typed_value acc v in
-        Var (b, v)
-
-    method visit_Abs : 'acc -> abs -> env_elem =
-      fun acc abs -> Abs (self#visit_abs acc abs)
-
-    method visit_env_elem : 'acc -> env_elem -> env_elem =
-      fun acc em ->
-        match em with
-        | Var (vid, v) -> self#visit_Var acc vid v
-        | Abs abs -> self#visit_Abs acc abs
-        | Frame -> raise (Failure "Unreachable")
+    inherit [_] map_env
 
-    method visit_env : 'acc -> env -> env =
+    method! visit_env : 'acc -> env -> env =
       fun acc env ->
         match env with
         | [] -> []
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 1b05911b..a8d50720 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1423,6 +1423,9 @@ let end_borrows_no_synth config ids ctx =
 let end_abstraction_no_synth config id ctx =
   get_cf_ctx_no_synth (end_abstraction config id) ctx
 
+let end_abstractions_no_synth config ids ctx =
+  get_cf_ctx_no_synth (end_abstractions config ids) ctx
+
 (** Helper function: see {!activate_reserved_mut_borrow}.
 
     This function updates the shared loan to a mutable loan (we then update
@@ -1923,8 +1926,7 @@ type merge_abstraction_info = {
     - all the borrows are destructured (for instance, shared loans can't
       contain shared loans).
  *)
-let compute_merge_abstractions_info (ctx : C.eval_ctx) (abs : V.abs) :
-    merge_abstraction_info =
+let compute_merge_abstractions_info (abs : V.abs) : merge_abstraction_info =
   let loans : V.loan_id_set ref = ref V.BorrowId.Set.empty in
   let borrows : V.borrow_id_set ref = ref V.BorrowId.Set.empty in
   let borrows_loans : borrow_or_loan_id list ref = ref [] in
@@ -2060,7 +2062,23 @@ type merge_duplicates_funcs = {
     V.mvalue ->
     V.typed_avalue ->
     V.typed_avalue;
+      (** Parameters:
+          - [id]
+          - [ty0]
+          - [mv0]
+          - [child0]
+          - [ty1]
+          - [mv1]
+          - [child1]
+
+          The children should be [AIgnored].
+       *)
   merge_ashared_borrows : V.borrow_id -> T.rty -> T.rty -> V.typed_avalue;
+      (** Parameters:
+          - [id]
+          - [ty0]
+          - [ty1]
+       *)
   merge_amut_loans :
     V.loan_id ->
     T.rty ->
@@ -2068,13 +2086,33 @@ type merge_duplicates_funcs = {
     T.rty ->
     V.typed_avalue ->
     V.typed_avalue;
+      (** Parameters:
+          - [id]
+          - [ty0]
+          - [child0]
+          - [ty1]
+          - [child1]
+
+          The children should be [AIgnored].
+       *)
   merge_ashared_loans :
     V.loan_id_set ->
     T.rty ->
     V.typed_value ->
+    V.typed_avalue ->
     T.rty ->
     V.typed_value ->
+    V.typed_avalue ->
     V.typed_avalue;
+      (** Parameters:
+          - [ids]
+          - [ty0]
+          - [sv0]
+          - [child0]
+          - [ty1]
+          - [sv1]
+          - [child1]
+       *)
 }
 
 let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
@@ -2094,7 +2132,7 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
     loan_to_content = loan_to_content0;
     borrow_to_content = borrow_to_content0;
   } =
-    compute_merge_abstractions_info ctx abs0
+    compute_merge_abstractions_info abs0
   in
 
   let {
@@ -2104,7 +2142,7 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
     loan_to_content = loan_to_content1;
     borrow_to_content = borrow_to_content1;
   } =
-    compute_merge_abstractions_info ctx abs1
+    compute_merge_abstractions_info abs1
   in
 
   (* Sanity check: there is no loan/borrows which appears in both abstractions,
@@ -2181,7 +2219,7 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
   let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty)
       (bc1 : g_borrow_content_with_ty) : V.typed_avalue =
     match (bc0, bc1) with
-    | Concrete (ty0, bc0), Concrete (ty1, bc1) ->
+    | Concrete _, Concrete _ ->
         (* This can happen only in case of nested borrows *)
         raise (Failure "Unreachable")
     | Abstract (ty0, bc0), Abstract (ty1, bc1) ->
@@ -2212,7 +2250,8 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
         (* Register the loan ids *)
         V.BorrowId.Set.iter set_loan_as_merged ids;
         (* Merge *)
-        (Option.get merge_funs).merge_ashared_loans ids ty0 sv0 ty1 sv1
+        (Option.get merge_funs).merge_ashared_loans ids ty0 sv0 child0 ty1 sv1
+          child1
     | _ ->
         (* Unreachable because those cases are ignored (ended/ignored borrows)
            or inconsistent *)
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 8b8b76d9..01ce206a 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -41,6 +41,10 @@ val end_borrows_no_synth :
 val end_abstraction_no_synth :
   C.config -> V.AbstractionId.id -> C.eval_ctx -> C.eval_ctx
 
+(** End a set of abstractions and return the resulting environment, ignoring synthesis *)
+val end_abstractions_no_synth :
+  C.config -> V.AbstractionId.Set.t -> C.eval_ctx -> C.eval_ctx
+
 (** Promote a reserved mut borrow to a mut borrow, while preserving the invariants.
 
     Reserved borrows are special mutable borrows which are created as shared borrows
@@ -133,6 +137,7 @@ val convert_value_to_abstractions :
     Rem.: it may be more idiomatic to have a functor, but this seems a bit
     heavyweight, though.
   *)
+
 type merge_duplicates_funcs = {
   merge_amut_borrows :
     V.borrow_id ->
@@ -143,7 +148,23 @@ type merge_duplicates_funcs = {
     V.mvalue ->
     V.typed_avalue ->
     V.typed_avalue;
+      (** Parameters:
+          - [id]
+          - [ty0]
+          - [mv0]
+          - [child0]
+          - [ty1]
+          - [mv1]
+          - [child1]
+
+          The children should be [AIgnored].
+       *)
   merge_ashared_borrows : V.borrow_id -> T.rty -> T.rty -> V.typed_avalue;
+      (** Parameters:
+          - [id]
+          - [ty0]
+          - [ty1]
+       *)
   merge_amut_loans :
     V.loan_id ->
     T.rty ->
@@ -151,13 +172,33 @@ type merge_duplicates_funcs = {
     T.rty ->
     V.typed_avalue ->
     V.typed_avalue;
+      (** Parameters:
+          - [id]
+          - [ty0]
+          - [child0]
+          - [ty1]
+          - [child1]
+
+          The children should be [AIgnored].
+       *)
   merge_ashared_loans :
     V.loan_id_set ->
     T.rty ->
     V.typed_value ->
+    V.typed_avalue ->
     T.rty ->
     V.typed_value ->
+    V.typed_avalue ->
     V.typed_avalue;
+      (** Parameters:
+          - [ids]
+          - [ty0]
+          - [sv0]
+          - [child0]
+          - [ty1]
+          - [sv1]
+          - [child1]
+       *)
 }
 
 (** Merge two abstractions together.
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 54949d3f..6db23cc4 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -182,14 +182,29 @@ let projection_contains (ty1 : T.rty) (rset1 : T.RegionId.Set.t) (ty2 : T.rty)
   in
   compare_rtys default combine compare_regions ty1 ty2
 
-(** Compute the set of borrow ids, loan ids and abstraction ids in a context. *)
-let compute_borrow_abs_ids_in_context (ctx : C.eval_ctx) :
-    V.BorrowId.Set.t * V.AbstractionId.Set.t =
+(* TODO: there misses fields *)
+type ctx_ids = {
+  aids : V.AbstractionId.Set.t;
+  bids : V.BorrowId.Set.t;
+  dids : C.DummyVarId.Set.t;
+}
+
+(* TODO: move *)
+
+(** Compute the sets of ids found in a list of contexts. *)
+let compute_contexts_ids (ctxl : C.eval_ctx list) : ctx_ids =
   let bids = ref V.BorrowId.Set.empty in
   let aids = ref V.AbstractionId.Set.empty in
+  let dids = ref C.DummyVarId.Set.empty in
   let obj =
     object
       inherit [_] C.iter_eval_ctx
+
+      method! visit_binder _ bv =
+        match bv with
+        | VarBinder _ -> ()
+        | DummyBinder bid -> dids := C.DummyVarId.Set.add bid !dids
+
       method! visit_borrow_id _ id = bids := V.BorrowId.Set.add id !bids
 
       method! visit_loan_id _ id =
@@ -201,8 +216,12 @@ let compute_borrow_abs_ids_in_context (ctx : C.eval_ctx) :
         aids := V.AbstractionId.Set.add id !aids
     end
   in
-  obj#visit_eval_ctx () ctx;
-  (!bids, !aids)
+  List.iter (obj#visit_eval_ctx ()) ctxl;
+  { aids = !aids; bids = !bids; dids = !dids }
+
+(** Compute the sets of ids found in a context. *)
+let compute_context_ids (ctx : C.eval_ctx) : ctx_ids =
+  compute_contexts_ids [ ctx ]
 
 (** Lookup a loan content.
 
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 00e6eb01..85174aaf 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -15,14 +15,12 @@ open Utils
 open Cps
 open InterpreterUtils
 open InterpreterBorrows
-open InterpreterProjectors
-open InterpreterExpansion
-open InterpreterPaths
 open InterpreterExpressions
 
 (** The local logger *)
 let log = L.loops_log
 
+(* TODO: some fields are actually useless *)
 type cnt_thresholds = {
   aid : V.AbstractionId.id;
   sid : V.SymbolicValueId.id;
@@ -31,34 +29,18 @@ type cnt_thresholds = {
   rid : T.RegionId.id;
 }
 
-(* TODO: document.
-   TODO: we might not use the bounds properly, use sets instead.
-   TODO: actually, bounds are good
-*)
-type match_ctx = {
-  ctx : C.eval_ctx;
-  aids : V.AbstractionId.Set.t;
-  sids : V.SymbolicValueId.Set.t;
-  bids : V.BorrowId.Set.t;
-}
-
-let mk_match_ctx (ctx : C.eval_ctx) : match_ctx =
-  let aids = V.AbstractionId.Set.empty in
-  let sids = V.SymbolicValueId.Set.empty in
-  let bids = V.BorrowId.Set.empty in
-  { ctx; aids; sids; bids }
-
 type updt_env_kind =
   | AbsInLeft of V.AbstractionId.id
   | LoanInLeft of V.BorrowId.id
   | LoansInLeft of V.BorrowId.Set.t
+  | AbsInRight of V.AbstractionId.id
   | LoanInRight of V.BorrowId.id
   | LoansInRight of V.BorrowId.Set.t
 
 (** Utility exception *)
 exception ValueMatchFailure of updt_env_kind
 
-type joined_ctx_or_update = (match_ctx, updt_env_kind) result
+type ctx_or_update = (C.eval_ctx, updt_env_kind) result
 
 (** Union Find *)
 module UnionFind = UF.Make (UF.StoreMap)
@@ -209,16 +191,40 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool)
     borrow_loan_to_abs = !borrow_loan_to_abs;
   }
 
+(** Destructure all the new abstractions *)
+let destructure_new_abs (loop_id : V.LoopId.id)
+    (old_abs_ids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx =
+  let abs_kind = V.Loop loop_id in
+  let can_end = false in
+  let destructure_shared_values = true in
+  let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
+    not (V.AbstractionId.Set.mem id old_abs_ids)
+  in
+  let env =
+    List.map
+      (fun ee ->
+        match ee with
+        | C.Var _ | C.Frame -> ee
+        | C.Abs abs ->
+            if is_fresh_abs_id abs.abs_id then
+              let abs =
+                destructure_abs abs_kind can_end destructure_shared_values ctx
+                  abs
+              in
+              C.Abs abs
+            else ee)
+      ctx.env
+  in
+  { ctx with env }
+
 (** Collapse an environment.
 
     We do this to simplify an environment, for the purpose of finding a loop
     fixed point.
 
     We do the following:
-    - we look for all the *new* dummy values (we use id thresholds to decide
-      wether a value is new or not - the ids generated by our counters are
-      monotonic), and we convert to abstractions (if they contain loans or
-      borrows)
+    - we look for all the *new* dummy values (we use sets of old ids to decide
+      wether a value is new or not)
     - whenever there is a new abstraction in the context, and some of its
       its borrows are associated to loans in another new abstraction, we
       merge them.
@@ -232,18 +238,21 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool)
     they become well formed again after collapsing).
  *)
 let collapse_ctx (loop_id : V.LoopId.id)
-    (merge_funs : merge_duplicates_funcs option) (thresh : cnt_thresholds)
-    (ctx0 : C.eval_ctx) : C.eval_ctx =
+    (merge_funs : merge_duplicates_funcs option)
+    (old_ids : InterpreterBorrowsCore.ctx_ids) (ctx0 : C.eval_ctx) : C.eval_ctx
+    =
   let abs_kind = V.Loop loop_id in
   let can_end = false in
   let destructure_shared_values = true in
   let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
-    V.AbstractionId.Ord.compare thresh.aid id >= 0
+    not (V.AbstractionId.Set.mem id old_ids.aids)
   in
   let is_fresh_did (id : C.DummyVarId.id) : bool =
-    C.DummyVarId.Ord.compare thresh.did id >= 0
+    not (C.DummyVarId.Set.mem id old_ids.dids)
   in
-  (* Convert the dummy values to abstractions *)
+  (* Convert the dummy values to abstractions, and destructure all the new
+     abstractions at the same time (note that when we convert values to
+     abstractions, the resulting abstraction should be destructured) *)
   (* Note that we preserve the order of the dummy values: we replace them with
      abstractions in place - this makes matching easier *)
   let env =
@@ -538,7 +547,10 @@ end
     We use it for joins, to check if two environments are convertible, etc.
  *)
 module Match (M : Matcher) = struct
-  (** Match two values *)
+  (** Match two values.
+
+      Rem.: this function raises exceptions of type {!ValueMatchFailure}.
+   *)
   let rec match_typed_values (ctx : C.eval_ctx) (v0 : V.typed_value)
       (v1 : V.typed_value) : V.typed_value =
     let match_rec = match_typed_values ctx in
@@ -636,6 +648,10 @@ module Match (M : Matcher) = struct
     | _, Symbolic sv -> M.match_symbolic_with_other false sv v0
     | _ -> raise (Failure "Unreachable")
 
+  (** Match two avalues.
+
+      Rem.: this function raises exceptions of type {!ValueMatchFailure}.
+   *)
   and match_typed_avalues (ctx : C.eval_ctx) (v0 : V.typed_avalue)
       (v1 : V.typed_avalue) : V.typed_avalue =
     let match_rec = match_typed_values ctx in
@@ -952,267 +968,93 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
   let match_avalues _ _ = raise (Failure "Unreachable")
 end
 
-(*
-(** This function raises exceptions of kind {!ValueMatchFailue}.
+(** Collapse an environment, merging the duplicated borrows/loans.
 
-    [convertible]: the function updates it to [false] if the result of the
-    merge is not the result of an alpha-conversion. For instance, if we
-    match two primitive values which are not equal, and thus introduce a
-    symbolic value for the result:
-    {[
-      0 : u32, 1 : u32 ~~> s : u32     where s fresh
-    ]}
+    This function simply calls {!collapse_ctx} with the proper merging functions.
  *)
-let rec match_typed_values (config : C.config) (thresh : cnt_thresholds)
-    (convertible : bool ref) (rid_map : T.RegionId.InjSubst.t ref)
-    (bid_map : V.BorrowId.InjSubst.t ref)
-    (sid_map : V.SymbolicValueId.InjSubst.t ref) (ctx : C.eval_ctx)
-    (v0 : V.typed_value) (v1 : V.typed_value) : V.typed_value =
-  let match_rec =
-    match_typed_values config thresh convertible rid_map bid_map sid_map ctx
-  in
-  let lookup_bid (id : V.BorrowId.id) : V.BorrowId.id =
-    V.BorrowId.InjSubst.find_with_default id id !bid_map
-  in
-  let lookup_bids (ids : V.BorrowId.Set.t) : V.BorrowId.Set.t =
-    V.BorrowId.Set.map lookup_bid ids
+let collapse_ctx_with_merge (loop_id : V.LoopId.id)
+    (old_ids : InterpreterBorrowsCore.ctx_ids) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* When we join environments, we may introduce duplicated *loans*: we thus
+      don't implement merge functions for the borrows, only for the loans.
+
+      For instance:
+      {[
+        // If we have:
+        env0 = {
+          abs0 { ML l0 }
+          l -> MB l0 s0
+        }
+
+        env1 = {
+          abs0 { ML l0 }
+          abs1 { MB l0, ML l1 }
+          l -> MB l1 s1
+        }
+
+        // Then:
+        join env0 env1 = {
+          abs0 { ML l0 }
+          abs1 { MB l0, ML l1 }
+          abs2 { MB l0, MB l1, ML l2 } // Introduced when merging the "l" binding
+          l -> MB l2 s2
+        }
+      ]}
+
+     Rem.: the merge functions raise exceptions (that we catch).
+  *)
+  let module S : MatchJoinState = struct
+    let ctx = ctx
+    let loop_id = loop_id
+    let nabs = ref []
+  end in
+  let module JM = MakeJoinMatcher (S) in
+  let module M = Match (JM) in
+  let merge_amut_borrows _ _ _ _ _ _ _ = raise (Failure "Unexpected") in
+  let merge_ashared_borrows _ _ _ = raise (Failure "Unexpected") in
+  let merge_amut_loans id ty0 child0 _ty1 child1 =
+    (* Sanity checks *)
+    assert (is_aignored child0.V.value);
+    assert (is_aignored child1.V.value);
+    (* We simply need to introduce an [AMutLoan]. Some remarks:
+       - the child is [AIgnored]
+       - we need to pick some types. The types on the left and on the right
+         may use different regions: it doesn't really matter (here, we pick
+         the ones from the left).
+    *)
+    let ty = ty0 in
+    let child = child0 in
+    let value = V.ALoan (V.AMutLoan (id, child)) in
+    { V.value; ty }
   in
-  let map_bid (id0 : V.BorrowId.id) (id1 : V.BorrowId.id) : V.BorrowId.id =
-    assert (V.BorrowId.Ord.compare id0 thresh.bid >= 0);
-    assert (V.BorrowId.Ord.compare id1 thresh.bid >= 0);
-    assert (not (V.BorrowId.InjSubst.mem id0 !bid_map));
-    bid_map := V.BorrowId.InjSubst.add id0 id1 !bid_map;
-    id1
+  let merge_ashared_loans ids ty0 (sv0 : V.typed_value) child0 _ty1
+      (sv1 : V.typed_value) child1 =
+    (* Sanity checks *)
+    assert (is_aignored child0.V.value);
+    assert (is_aignored child1.V.value);
+    (* Same remarks as for [merge_amut_loans].
+
+       This time, however, we need to merge the shared values.
+    *)
+    assert (not (value_has_loans_or_borrows ctx sv0.V.value));
+    assert (not (value_has_loans_or_borrows ctx sv1.V.value));
+    let ty = ty0 in
+    let child = child0 in
+    let sv = M.match_typed_values ctx sv0 sv1 in
+    let value = V.ALoan (V.ASharedLoan (ids, sv, child)) in
+    { V.value; ty }
   in
-  let lookup_sid (id : V.SymbolicValueId.id) : V.SymbolicValueId.id =
-    match V.SymbolicValueId.InjSubst.find_opt id !sid_map with
-    | None -> id
-    | Some id -> id
+  let merge_funcs =
+    {
+      merge_amut_borrows;
+      merge_ashared_borrows;
+      merge_amut_loans;
+      merge_ashared_loans;
+    }
   in
-  assert (v0.V.ty = v1.V.ty);
-  match (v0.V.value, v1.V.value) with
-  | V.Primitive pv0, V.Primitive pv1 ->
-      if pv0 = pv1 then v1 else raise (Failure "Unimplemented")
-  | V.Adt av0, V.Adt av1 ->
-      if av0.variant_id = av1.variant_id then
-        let fields = List.combine av0.field_values av1.field_values in
-        let field_values = List.map (fun (f0, f1) -> match_rec f0 f1) fields in
-        let value : V.value =
-          V.Adt { variant_id = av0.variant_id; field_values }
-        in
-        { V.value; ty = v1.V.ty }
-      else (
-        convertible := false;
-        (* For now, we don't merge values which contain borrows *)
-        (* TODO: *)
-        raise (Failure "Unimplemented"))
-  | Bottom, Bottom -> v1
-  | Borrow bc0, Borrow bc1 ->
-      let bc =
-        match (bc0, bc1) with
-        | SharedBorrow (mv0, bid0), SharedBorrow (mv1, bid1) ->
-            let bid0 = lookup_bid bid0 in
-            (* Not completely sure what to do with the meta-value. If a shared
-               symbolic value gets expanded in a branch, it may be simplified
-               (by being folded back to a symbolic value) upon doing the join,
-               which as a result would lead to code where it is considered as
-               mutable (which is sound). On the other hand, if we access a
-               symbolic value in a loop, the translated loop should take it as
-               input anyway, so maybe this actually leads to equivalent
-               code.
-            *)
-            let mv = match_rec mv0 mv1 in
-            let bid = if bid0 = bid1 then bid1 else map_bid bid0 bid1 in
-            V.SharedBorrow (mv, bid)
-        | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) ->
-            let bid0 = lookup_bid bid0 in
-            let bv = match_rec bv0 bv1 in
-            let bid = if bid0 = bid1 then bid1 else map_bid bid0 bid1 in
-            V.MutBorrow (bid, bv)
-        | ReservedMutBorrow _, _
-        | _, ReservedMutBorrow _
-        | SharedBorrow _, MutBorrow _
-        | MutBorrow _, SharedBorrow _ ->
-            (* If we get here, either there is a typing inconsistency, or we are
-               trying to match a reserved borrow, which shouldn't happen because
-               reserved borrow should be eliminated very quickly - they are introduced
-               just before function calls which activate them *)
-            raise (Failure "Unexpected")
-      in
-      { V.value = V.Borrow bc; V.ty = v1.V.ty }
-  | Loan lc0, Loan lc1 ->
-      (* TODO: maybe we should enforce that the ids are always exactly the same -
-         without matching *)
-      let lc =
-        match (lc0, lc1) with
-        | SharedLoan (ids0, sv0), SharedLoan (ids1, sv1) ->
-            let ids0 = lookup_bids ids0 in
-            (* Not sure what to do if the ids don't match *)
-            let ids =
-              if ids0 = ids1 then ids1 else raise (Failure "Unimplemented")
-            in
-            let sv = match_rec sv0 sv1 in
-            V.SharedLoan (ids, sv)
-        | MutLoan id0, MutLoan id1 ->
-            let id0 = lookup_bid id0 in
-            let id = if id0 = id1 then id1 else map_bid id0 id1 in
-            V.MutLoan id
-        | SharedLoan _, MutLoan _ | MutLoan _, SharedLoan _ ->
-            raise (Failure "Unreachable")
-      in
-      { V.value = Loan lc; ty = v1.V.ty }
-  | Symbolic sv0, Symbolic sv1 ->
-      (* TODO: id check mapping *)
-      let id0 = lookup_sid sv0.sv_id in
-      let id1 = sv1.sv_id in
-      if id0 = id1 then (
-        assert (sv0.sv_kind = sv1.sv_kind);
-        (* Sanity check: the types should be the same *)
-        match_rtypes rid_map ctx sv0.sv_ty sv1.sv_ty;
-        (* Return *)
-        v1)
-      else (
-        (* For now, we force all the symbolic values containing borrows to
-           be eagerly expanded, and we don't support nested borrows *)
-        assert (not (value_has_borrows ctx v0.V.value));
-        assert (not (value_has_borrows ctx v1.V.value));
-        raise (Failure "Unimplemented"))
-  | Loan lc, _ -> (
-      match lc with
-      | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids))
-      | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id)))
-  | _, Loan lc -> (
-      match lc with
-      | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids))
-      | MutLoan id -> raise (ValueMatchFailure (LoanInRight id)))
-  | Symbolic _, _ -> raise (Failure "Unimplemented")
-  | _, Symbolic _ -> raise (Failure "Unimplemented")
-  | _ -> raise (Failure "Unreachable")
- *)
+  try collapse_ctx loop_id (Some merge_funcs) old_ids ctx
+  with ValueMatchFailure _ -> raise (Failure "Unexpected")
 
-(*(** This function raises exceptions of kind {!ValueMatchFailue} *)
-  let rec match_typed_avalues (config : C.config) (thresh : cnt_thresholds)
-      (rid_map : T.RegionId.InjSubst.t ref) (bid_map : V.BorrowId.InjSubst.t ref)
-      (sid_map : V.SymbolicValueId.InjSubst.t ref)
-      (aid_map : V.AbstractionId.InjSubst.t ref) (ctx : C.eval_ctx)
-      (v0 : V.typed_avalue) (v1 : V.typed_avalue) : V.typed_avalue =
-    let match_rec =
-      match_typed_avalues config thresh rid_map bid_map sid_map ctx
-    in
-    (* TODO: factorize those helpers with [match_typed_values] (write a functor?) *)
-    let lookup_bid (id : V.BorrowId.id) : V.BorrowId.id =
-      V.BorrowId.InjSubst.find_with_default id id !bid_map
-    in
-    let lookup_bids (ids : V.BorrowId.Set.t) : V.BorrowId.Set.t =
-      V.BorrowId.Set.map lookup_bid ids
-    in
-    let map_bid (id0 : V.BorrowId.id) (id1 : V.BorrowId.id) : V.BorrowId.id =
-      assert (V.BorrowId.Ord.compare id0 thresh.bid >= 0);
-      assert (V.BorrowId.Ord.compare id1 thresh.bid >= 0);
-      assert (not (V.BorrowId.InjSubst.mem id0 !bid_map));
-      bid_map := V.BorrowId.InjSubst.add id0 id1 !bid_map;
-      id1
-    in
-    let lookup_sid (id : V.SymbolicValueId.id) : V.SymbolicValueId.id =
-      match V.SymbolicValueId.InjSubst.find_opt id !sid_map with
-      | None -> id
-      | Some id -> id
-    in
-    assert (v0.V.ty = v1.V.ty);
-    match (v0.V.value, v1.V.value) with
-    | V.APrimitive pv0, V.APrimitive pv1 ->
-        if pv0 = pv1 then v1 else raise (Failure "Unimplemented")
-    | V.AAdt av0, V.AAdt av1 ->
-        if av0.variant_id = av1.variant_id then
-          let fields = List.combine av0.field_values av1.field_values in
-          let field_values = List.map (fun (f0, f1) -> match_rec f0 f1) fields in
-          let value : V.value =
-            V.Adt { variant_id = av0.variant_id; field_values }
-          in
-          { V.value; ty = v1.V.ty }
-        else raise (Failure "Unimplemented")
-    | Bottom, Bottom -> v1
-    | Borrow bc0, Borrow bc1 ->
-        let bc =
-          match (bc0, bc1) with
-          | SharedBorrow (mv0, bid0), SharedBorrow (mv1, bid1) ->
-              let bid0 = lookup_bid bid0 in
-              (* Not completely sure what to do with the meta-value. If a shared
-                 symbolic value gets expanded in a branch, it may be simplified
-                 (by being folded back to a symbolic value) upon doing the join,
-                 which as a result would lead to code where it is considered as
-                 mutable (which is sound). On the other hand, if we access a
-                 symbolic value in a loop, the translated loop should take it as
-                 input anyway, so maybe this actually leads to equivalent
-                 code.
-              *)
-              let mv = match_rec mv0 mv1 in
-              let bid = if bid0 = bid1 then bid1 else map_bid bid0 bid1 in
-              V.SharedBorrow (mv, bid)
-          | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) ->
-              let bid0 = lookup_bid bid0 in
-              let bv = match_rec bv0 bv1 in
-              let bid = if bid0 = bid1 then bid1 else map_bid bid0 bid1 in
-              V.MutBorrow (bid, bv)
-          | ReservedMutBorrow _, _
-          | _, ReservedMutBorrow _
-          | SharedBorrow _, MutBorrow _
-          | MutBorrow _, SharedBorrow _ ->
-              (* If we get here, either there is a typing inconsistency, or we are
-                 trying to match a reserved borrow, which shouldn't happen because
-                 reserved borrow should be eliminated very quickly - they are introduced
-                 just before function calls which activate them *)
-              raise (Failure "Unexpected")
-        in
-        { V.value = V.Borrow bc; V.ty = v1.V.ty }
-    | Loan lc0, Loan lc1 ->
-        (* TODO: maybe we should enforce that the ids are always exactly the same -
-           without matching *)
-        let lc =
-          match (lc0, lc1) with
-          | SharedLoan (ids0, sv0), SharedLoan (ids1, sv1) ->
-              let ids0 = lookup_bids ids0 in
-              (* Not sure what to do if the ids don't match *)
-              let ids =
-                if ids0 = ids1 then ids1 else raise (Failure "Unimplemented")
-              in
-              let sv = match_rec sv0 sv1 in
-              V.SharedLoan (ids, sv)
-          | MutLoan id0, MutLoan id1 ->
-              let id0 = lookup_bid id0 in
-              let id = if id0 = id1 then id1 else map_bid id0 id1 in
-              V.MutLoan id
-          | SharedLoan _, MutLoan _ | MutLoan _, SharedLoan _ ->
-              raise (Failure "Unreachable")
-        in
-        { V.value = Loan lc; ty = v1.V.ty }
-    | Symbolic sv0, Symbolic sv1 ->
-        (* TODO: id check mapping *)
-        let id0 = lookup_sid sv0.sv_id in
-        let id1 = sv1.sv_id in
-        if id0 = id1 then (
-          assert (sv0.sv_kind = sv1.sv_kind);
-          (* Sanity check: the types should be the same *)
-          match_rtypes rid_map ctx sv0.sv_ty sv1.sv_ty;
-          (* Return *)
-          v1)
-        else (
-          (* For now, we force all the symbolic values containing borrows to
-             be eagerly expanded, and we don't support nested borrows *)
-          assert (not (value_has_borrows ctx v0.V.value));
-          assert (not (value_has_borrows ctx v1.V.value));
-          raise (Failure "Unimplemented"))
-    | Loan lc, _ -> (
-        match lc with
-        | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids))
-        | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id)))
-    | _, Loan lc -> (
-        match lc with
-        | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids))
-        | MutLoan id -> raise (ValueMatchFailure (LoanInRight id)))
-  | _ -> raise (Failure "Unreachable")*)
-
-(** Apply substitutions in the first abstraction, then join the abstractions together.
+(*(** Apply substitutions in the first abstraction, then join the abstractions together.
 
     TODO: remove?
  *)
@@ -1243,8 +1085,9 @@ let subst_join_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
   (* Merge the two abstractions *)
   let abs_kind = V.Loop loop_id in
   let can_end = false in
-  merge_abstractions abs_kind can_end None ctx abs0 abs1
+merge_abstractions abs_kind can_end None ctx abs0 abs1*)
 
+(*
 (** Merge a borrow with the abstraction containing the associated loan, where
     the abstraction must be a *loop abstraction* (we don't synthesize code during
     the operation).
@@ -1279,25 +1122,23 @@ let rec merge_borrows_with_parent_loop_abs (config : C.config)
   V.BorrowId.Set.fold
     (fun id ctx -> merge_borrow_with_parent_loop_abs config id ctx)
     bids ctx
+ *)
 
+(*
 (* TODO: we probably don't need an [match_ctx], and actually we might not use
    the bounds propertly.
    TODO: remove
 *)
-let match_ctx_with_target_old (config : C.config) (tgt_mctx : match_ctx) :
+let match_ctx_with_target_old (config : C.config) (tgt_ctx : C.eval_ctx) :
     cm_fun =
  fun cf src_ctx ->
-  (* We first reorganize [ctx] so that we can match it with [tgt_mctx] *)
+  (* We first reorganize [ctx] so that we can match it with [tgt_ctx] *)
   (* First, collect all the borrows and abstractions which are in [ctx]
-     and not in [tgt_mctx]: we need to end them *)
-  let src_bids, src_aids =
-    InterpreterBorrowsCore.compute_borrow_abs_ids_in_context src_ctx
-  in
-  let tgt_bids, tgt_aids =
-    InterpreterBorrowsCore.compute_borrow_abs_ids_in_context tgt_mctx.ctx
-  in
-  let bids = V.BorrowId.Set.diff src_bids tgt_bids in
-  let aids = V.AbstractionId.Set.diff src_aids tgt_aids in
+     and not in [tgt_ctx]: we need to end them *)
+  let src_ids = InterpreterBorrowsCore.compute_context_ids src_ctx in
+  let tgt_ids = InterpreterBorrowsCore.compute_context_ids tgt_ctx in
+  let bids = V.BorrowId.Set.diff src_ids.bids tgt_ids.bids in
+  let aids = V.AbstractionId.Set.diff src_ids.aids tgt_ids.aids in
   (* End those borrows and abstractions *)
   let cc = InterpreterBorrows.end_borrows config bids in
   let cc = comp cc (InterpreterBorrows.end_abstractions config aids) in
@@ -1306,8 +1147,8 @@ let match_ctx_with_target_old (config : C.config) (tgt_mctx : match_ctx) :
   *)
   let tgt_ctx =
     merge_borrows_with_parent_loop_abs config
-      (V.BorrowId.Set.diff tgt_bids src_bids)
-      tgt_mctx.ctx
+      (V.BorrowId.Set.diff tgt_ids.bids src_ids.bids)
+      tgt_ctx
   in
   (* Replace the source context with the target context - TODO: explain
      why this works *)
@@ -1317,29 +1158,104 @@ let match_ctx_with_target_old (config : C.config) (tgt_mctx : match_ctx) :
   let cc = comp_check_ctx cc Inv.check_invariants in
   (* Apply and continue *)
   cc cf src_ctx
+*)
 
+(** Join two contexts *)
+let join_ctxs (_config : C.config) (_old_ids : InterpreterBorrowsCore.ctx_ids)
+    (_ctx0 : C.eval_ctx) (_ctx1 : C.eval_ctx) : ctx_or_update =
+  raise (Failure "Unimplemented")
+
+(** Join the context at the entry of the loop with the contexts upon reentry
+    (upon reaching the [Continue] statement - the goal is to compute a fixed
+    point for the loop entry).
+ *)
+let loop_join_origin_with_continue_ctxs (config : C.config)
+    (loop_id : V.LoopId.id) (old_ctx : C.eval_ctx) (ctxl : C.eval_ctx list) :
+    C.eval_ctx =
+  (* # Look for borrows and abstractions that exist in [old_ctx] and not in [ctxl]:
+   * we need to end those *)
+  (* Compute the sets of borrows and abstractions *)
+  let old_ids = InterpreterBorrowsCore.compute_context_ids old_ctx in
+  let new_ids = InterpreterBorrowsCore.compute_contexts_ids ctxl in
+  let bids = V.BorrowId.Set.diff old_ids.bids new_ids.bids in
+  let aids = V.AbstractionId.Set.diff old_ids.aids new_ids.aids in
+  (* End those borrows and abstractions *)
+  let old_ctx = InterpreterBorrows.end_borrows_no_synth config bids old_ctx in
+  let old_ctx =
+    InterpreterBorrows.end_abstractions_no_synth config aids old_ctx
+  in
+
+  (* # Join with the new contexts, one by one
+
+     For every context, we repeteadly attempt to join it with the current
+     result of the join: if we fail (because we need to end loans for instance),
+     we update the context and retry.
+     Rem.: we should never have to end loans in the aggregated context, only
+     in the one we are trying to add to the join.
+  *)
+  let joined_ctx = ref old_ctx in
+  let rec join_one_aux (ctx : C.eval_ctx) : unit =
+    match join_ctxs config old_ids !joined_ctx ctx with
+    | Ok nctx -> joined_ctx := nctx
+    | Error err ->
+        let ctx =
+          match err with
+          | LoanInRight bid ->
+              InterpreterBorrows.end_borrow_no_synth config bid ctx
+          | LoansInRight bids ->
+              InterpreterBorrows.end_borrows_no_synth config bids ctx
+          | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ ->
+              raise (Failure "Unexpected")
+        in
+        join_one_aux ctx
+  in
+  let join_one (ctx : C.eval_ctx) : unit =
+    (* Destructure the abstractions introduced in the new context *)
+    let ctx = destructure_new_abs loop_id old_ids.aids ctx in
+    (* Collapse the context we want to add to the join *)
+    let ctx = collapse_ctx loop_id None old_ids ctx in
+    (* Join the two contexts  *)
+    join_one_aux ctx;
+    (* Collapse again - the join might have introduce abstractions we want
+       to merge with the others (note that those abstractions may actually
+       lead to borrows/loans duplications) *)
+    joined_ctx := collapse_ctx_with_merge loop_id old_ids !joined_ctx;
+    (* Sanity check *)
+    if !Config.check_invariants then Invariants.check_invariants !joined_ctx
+  in
+
+  List.iter join_one ctxl;
+
+  (* # Return *)
+  !joined_ctx
+
+(*
 (** Join a context at the entry of a loop with a context upon reaching
     a continue in this loop.
  *)
-let loop_join_entry_ctx_with_continue_ctx (ctx0 : match_ctx) (ctx1 : C.eval_ctx)
-    : joined_ctx_or_update =
+let loop_join_entry_ctx_with_continue_ctx (_ctx0 : C.eval_ctx)
+    (_ctx1 : C.eval_ctx) : ctx_or_update =
   failwith "Unimplemented"
 
 (** See {!loop_join_entry_ctx_with_continue_ctx} *)
-let rec loop_join_entry_ctx_with_continue_ctxs (ctx0 : match_ctx)
-    (ctxs : C.eval_ctx list) : joined_ctx_or_update =
+let rec loop_join_entry_ctx_with_continue_ctxs (ctx0 : C.eval_ctx)
+    (ctxs : C.eval_ctx list) : ctx_or_update =
   match ctxs with
   | [] -> Ok ctx0
   | ctx1 :: ctxs -> (
       let res = loop_join_entry_ctx_with_continue_ctx ctx0 ctx1 in
       match res with
-      | Error _ -> res
+      | Error _ ->
+          (* TODO: apply the error *)
+          raise (Failure "Unimplemented")
       | Ok ctx0 -> loop_join_entry_ctx_with_continue_ctxs ctx0 ctxs)
+ *)
 
-let compute_loop_entry_fixed_point (config : C.config)
-    (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : match_ctx =
-  (* The continuation for when we exit the loop - we use it to register the
-     environments upon loop *reentry*
+let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
+    (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : C.eval_ctx =
+  (* The continuation for when we exit the loop - we register the
+     environments upon loop *reentry*, and synthesize nothing by
+     returning [None]
   *)
   let ctxs = ref [] in
   let register_ctx ctx = ctxs := ctx :: !ctxs in
@@ -1367,64 +1283,51 @@ let compute_loop_entry_fixed_point (config : C.config)
    * TODO: the returned env is an eval_ctx or smth else?
    * Maybe simply keep track of existentially quantified variables?
    *)
-  let join_ctxs (ctx0 : match_ctx) : joined_ctx_or_update =
-    let ctx1 = loop_join_entry_ctx_with_continue_ctxs ctx0 !ctxs in
+  let join_ctxs (ctx0 : C.eval_ctx) : C.eval_ctx =
+    let ctx1 = loop_join_origin_with_continue_ctxs config loop_id ctx0 !ctxs in
     ctxs := [];
     ctx1
   in
   (* Check if two contexts are equivalent - modulo alpha conversion on the
      existentially quantified borrows/abstractions/symbolic values *)
-  let equiv_ctxs (_ctx1 : match_ctx) (_ctx2 : match_ctx) : bool =
+  let equiv_ctxs (_ctx1 : C.eval_ctx) (_ctx2 : C.eval_ctx) : bool =
     failwith "Unimplemented"
   in
   let max_num_iter = Config.loop_fixed_point_max_num_iters in
-  let rec compute_fixed_point (mctx : match_ctx) (i : int) : match_ctx =
+  let rec compute_fixed_point (ctx : C.eval_ctx) (i : int) : C.eval_ctx =
     if i = 0 then
       raise
         (Failure
            ("Could not compute a loop fixed point in "
           ^ string_of_int max_num_iter ^ " iterations"))
     else
-      (* The join on the environments may fail if we need to end some borrows/abstractions
-         in the original context first: reorganize the original environment for as
-         long as we need to *)
-      let rec eval_iteration_then_join (mctx : match_ctx) =
-        (* Evaluate the loop body *)
-        let _ = eval_loop_body cf_exit_loop_body mctx.ctx in
-        (* Check if the join succeeded, or if we need to end abstractions/borrows
-           in the original environment first *)
-        match join_ctxs mctx with
-        | Error (AbsInLeft id) ->
-            let ctx1 =
-              InterpreterBorrows.end_abstraction_no_synth config id mctx.ctx
-            in
-            eval_iteration_then_join { mctx with ctx = ctx1 }
-        | Error (LoanInLeft id) ->
-            let ctx1 =
-              InterpreterBorrows.end_borrow_no_synth config id mctx.ctx
-            in
-            eval_iteration_then_join { mctx with ctx = ctx1 }
-        | Error (LoansInLeft ids) ->
-            let ctx1 =
-              InterpreterBorrows.end_borrows_no_synth config ids mctx.ctx
-            in
-            eval_iteration_then_join { mctx with ctx = ctx1 }
-        | Error (LoanInRight _ | LoansInRight _) ->
-            (* Shouldn't happen here *)
-            raise (Failure "Unreachable")
-        | Ok mctx1 ->
-            (* The join succeeded: check if we reached a fixed point, otherwise
-               iterate *)
-            if equiv_ctxs mctx mctx1 then mctx1
-            else compute_fixed_point mctx1 (i - 1)
-      in
-      eval_iteration_then_join mctx
+      (* Evaluate the loop body to register the different contexts upon reentry *)
+      let _ = eval_loop_body cf_exit_loop_body ctx in
+      (* Compute the join between the original contexts and the contexts computed
+         upon reentry *)
+      let ctx1 = join_ctxs ctx0 in
+      (* Check if we reached a fixed point: if not, iterate *)
+      if equiv_ctxs ctx0 ctx1 then ctx1 else compute_fixed_point ctx1 (i - 1)
   in
-  compute_fixed_point (mk_match_ctx ctx0) max_num_iter
+  compute_fixed_point ctx0 max_num_iter
+
+let match_ctx_with_target (config : C.config) (tgt_ctx : C.eval_ctx) : cm_fun =
+ fun cf src_ctx ->
+  (* We first reorganize [src_ctx] so that we can match it with [tgt_ctx] *)
+  (* First, collect all the borrows and abstractions which are in [ctx]
+     and not in [tgt_ctx]: we need to end them *)
+  let src_ids = InterpreterBorrowsCore.compute_context_ids src_ctx in
+  let tgt_ids = InterpreterBorrowsCore.compute_context_ids tgt_ctx in
+  let bids = V.BorrowId.Set.diff src_ids.bids tgt_ids.bids in
+  let aids = V.AbstractionId.Set.diff src_ids.aids tgt_ids.aids in
+  (* End those borrows and abstractions *)
+  let cc = InterpreterBorrows.end_borrows config bids in
+  let cc = comp cc (InterpreterBorrows.end_abstractions config aids) in
+  (* TODO *)
+  raise (Failure "Unimplemented")
 
 (** Evaluate a loop in concrete mode *)
-let eval_loop_concrete (config : C.config) (eval_loop_body : st_cm_fun) :
-    st_cm_fun =
+let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun =
  fun cf ctx ->
   (* Continuation for after we evaluate the loop body: depending the result
      of doing one loop iteration:
@@ -1470,10 +1373,17 @@ let eval_loop_concrete (config : C.config) (eval_loop_body : st_cm_fun) :
 let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
     st_cm_fun =
  fun cf ctx ->
+  (* Compute a fresh loop id *)
+  let loop_id = C.fresh_loop_id () in
   (* Compute the fixed point at the loop entrance *)
-  let mctx = compute_loop_entry_fixed_point config eval_loop_body ctx in
-  (* Synthesize the end of the function *)
-  let end_expr = match_ctx_with_target_old config mctx (cf EndEnterLoop) ctx in
+  let fp_ctx =
+    compute_loop_entry_fixed_point config loop_id eval_loop_body ctx
+  in
+  (* Synthesize the end of the function - we simply match the context at the
+     loop entry with the fixed point: in the synthesized code, the function
+     will end with a call to the loop translation
+  *)
+  let end_expr = match_ctx_with_target config fp_ctx (cf EndEnterLoop) ctx in
   (* Synthesize the loop body by evaluating it, with the continuation for
      after the loop starting at the *fixed point*, but with a special
      treatment for the [Break] and [Continue] cases *)
@@ -1488,14 +1398,14 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
     | Continue i ->
         (* We don't support nested loops for now *)
         assert (i = 0);
-        match_ctx_with_target_old config mctx (cf EndContinue) ctx
+        match_ctx_with_target config fp_ctx (cf EndContinue) ctx
     | Unit | EndEnterLoop | EndContinue ->
         (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}.
            For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now.
         *)
         raise (Failure "Unreachable")
   in
-  let loop_expr = eval_loop_body cf_loop mctx.ctx in
+  let loop_expr = eval_loop_body cf_loop fp_ctx in
   (* Put together *)
   S.synthesize_loop end_expr loop_expr
 
@@ -1503,5 +1413,5 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
 let eval_loop (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun =
  fun cf ctx ->
   match config.C.mode with
-  | ConcreteMode -> eval_loop_concrete config eval_loop_body cf ctx
+  | ConcreteMode -> eval_loop_concrete eval_loop_body cf ctx
   | SymbolicMode -> eval_loop_symbolic config eval_loop_body cf ctx