Use eval_ctx instead of env in many functions of the interpreter

2 files changed, 163 insertions, 173 deletions

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 0dc18952..001ebf19 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -244,3 +244,23 @@ class ['self] map_frame_concrete =
             let env = self#visit_env acc env in
             em :: env
   end
+
+(** Visitor to iterate over the values in a context *)
+class ['self] iter_eval_ctx =
+  object (self : 'self)
+    inherit [_] iter_env as super
+
+    method visit_eval_ctx : 'acc -> eval_ctx -> unit =
+      fun acc ctx -> super#visit_env acc ctx.env
+  end
+
+(** Visitor to map the values in a context *)
+class ['self] map_eval_ctx =
+  object (self : 'self)
+    inherit [_] map_env as super
+
+    method visit_eval_ctx : 'acc -> eval_ctx -> eval_ctx =
+      fun acc ctx ->
+        let env = super#visit_env acc ctx.env in
+        { ctx with env }
+  end
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index b3fcc9f5..9634067d 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -176,8 +176,8 @@ let loans_in_value (v : V.typed_value) : bool =
 
     TODO: group abs_or_var_id and g_loan_content. 
  *)
-let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
-    (abs_or_var_id * g_loan_content) option =
+let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
+    (ctx : C.eval_ctx) : (abs_or_var_id * g_loan_content) option =
   (* We store here whether we are inside an abstraction or a value - note that we
    * could also track that with the environment, it would probably be more idiomatic
    * and cleaner *)
@@ -185,7 +185,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
 
   let obj =
     object
-      inherit [_] C.iter_env as super
+      inherit [_] C.iter_eval_ctx as super
 
       method! visit_borrow_content env bc =
         match bc with
@@ -258,7 +258,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
   in
   (* We use exceptions *)
   try
-    obj#visit_env () env;
+    obj#visit_eval_ctx () ctx;
     None
   with FoundGLoanContent lc -> (
     match !abs_or_var with
@@ -270,9 +270,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
     The loan is referred to by a borrow id.
     Raises an exception if no loan was found.
  *)
-let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
+let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (ctx : C.eval_ctx) :
     abs_or_var_id * g_loan_content =
-  match lookup_loan_opt ek l env with
+  match lookup_loan_opt ek l ctx with
   | None -> failwith "Unreachable"
   | Some res -> res
 
@@ -283,7 +283,7 @@ let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
     This is a helper function: it might break invariants.
  *)
 let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
-    (nlc : V.loan_content) (env : C.env) : C.env =
+    (nlc : V.loan_content) (ctx : C.eval_ctx) : C.eval_ctx =
   (* We use a reference to check that we update exactly one loan: when updating
    * inside values, we check we don't update more than one loan. Then, upon
    * returning we check that we updated at least once. *)
@@ -296,7 +296,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
 
   let obj =
     object
-      inherit [_] C.map_env as super
+      inherit [_] C.map_eval_ctx as super
 
       method! visit_borrow_content env bc =
         match bc with
@@ -334,10 +334,10 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
     end
   in
 
-  let env = obj#visit_env () env in
+  let ctx = obj#visit_eval_ctx () ctx in
   (* Check that we updated at least one loan *)
   assert !r;
-  env
+  ctx
 
 (** Update a abstraction loan content.
 
@@ -346,7 +346,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
     This is a helper function: it might break invariants.
  *)
 let update_aloan (ek : exploration_kind) (l : V.BorrowId.id)
-    (nlc : V.aloan_content) (env : C.env) : C.env =
+    (nlc : V.aloan_content) (ctx : C.eval_ctx) : C.eval_ctx =
   (* We use a reference to check that we update exactly one loan: when updating
    * inside values, we check we don't update more than one loan. Then, upon
    * returning we check that we updated at least once. *)
@@ -359,7 +359,7 @@ let update_aloan (ek : exploration_kind) (l : V.BorrowId.id)
 
   let obj =
     object
-      inherit [_] C.map_env as super
+      inherit [_] C.map_eval_ctx as super
 
       method! visit_aloan_content env lc =
         match lc with
@@ -385,17 +385,17 @@ let update_aloan (ek : exploration_kind) (l : V.BorrowId.id)
     end
   in
 
-  let env = obj#visit_env () env in
+  let ctx = obj#visit_eval_ctx () ctx in
   (* Check that we updated at least one loan *)
   assert !r;
-  env
+  ctx
 
 (** Lookup a borrow content from a borrow id. *)
-let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env)
-    : g_borrow_content option =
+let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
+    (ctx : C.eval_ctx) : g_borrow_content option =
   let obj =
     object
-      inherit [_] C.iter_env as super
+      inherit [_] C.iter_eval_ctx as super
 
       method! visit_borrow_content env bc =
         match bc with
@@ -440,7 +440,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env)
   in
   (* We use exceptions *)
   try
-    obj#visit_env () env;
+    obj#visit_eval_ctx () ctx;
     None
   with FoundGBorrowContent lc -> Some lc
 
@@ -448,9 +448,9 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env)
 
     Raise an exception if no loan was found
 *)
-let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
-    g_borrow_content =
-  match lookup_borrow_opt ek l env with
+let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (ctx : C.eval_ctx)
+    : g_borrow_content =
+  match lookup_borrow_opt ek l ctx with
   | None -> failwith "Unreachable"
   | Some lc -> lc
 
@@ -461,7 +461,7 @@ let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
     This is a helper function: it might break invariants.   
  *)
 let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
-    (nbc : V.borrow_content) (env : C.env) : C.env =
+    (nbc : V.borrow_content) (ctx : C.eval_ctx) : C.eval_ctx =
   (* We use a reference to check that we update exactly one borrow: when updating
    * inside values, we check we don't update more than one borrow. Then, upon
    * returning we check that we updated at least once. *)
@@ -474,7 +474,7 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
 
   let obj =
     object
-      inherit [_] C.map_env as super
+      inherit [_] C.map_eval_ctx as super
 
       method! visit_borrow_content env bc =
         match bc with
@@ -506,10 +506,10 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
     end
   in
 
-  let env = obj#visit_env () env in
+  let ctx = obj#visit_eval_ctx () ctx in
   (* Check that we updated at least one borrow *)
   assert !r;
-  env
+  ctx
 
 (** Update an abstraction borrow content.
 
@@ -518,7 +518,7 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
     This is a helper function: it might break invariants.     
  *)
 let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id)
-    (nbc : V.aborrow_content) (env : C.env) : C.env =
+    (nbc : V.aborrow_content) (ctx : C.eval_ctx) : C.eval_ctx =
   (* We use a reference to check that we update exactly one borrow: when updating
    * inside values, we check we don't update more than one borrow. Then, upon
    * returning we check that we updated at least once. *)
@@ -531,7 +531,7 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id)
 
   let obj =
     object
-      inherit [_] C.map_env as super
+      inherit [_] C.map_eval_ctx as super
 
       method! visit_aborrow_content env bc =
         match bc with
@@ -549,10 +549,10 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id)
     end
   in
 
-  let env = obj#visit_env () env in
+  let ctx = obj#visit_eval_ctx () ctx in
   (* Check that we updated at least one borrow *)
   assert !r;
-  env
+  ctx
 
 (** The following type identifies the relative position of expressions (in
     particular borrows) in other expressions.
@@ -669,6 +669,8 @@ let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t)
     - [ty]: the type with regions which we use for the projection (to
       map borrows to regions - or to interpret the borrows as belonging
       to some regions...)
+
+    TODO: we need a context
 *)
 let rec apply_proj_borrows (regions : T.RegionId.set_t) (v : V.typed_value)
     (ty : T.rty) : V.typed_avalue =
@@ -682,6 +684,7 @@ let rec apply_proj_borrows (regions : T.RegionId.set_t) (v : V.typed_value)
     | V.Concrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AConcrete cv
     | V.Adt adt, T.Adt (id, regions, tys) ->
         (* Retrieve the types of the fields *)
+
         (* Explore the field values *)
         raise Unimplemented
     | V.Bottom, _ -> failwith "Unreachable"
@@ -747,9 +750,10 @@ let rec apply_proj_borrows (regions : T.RegionId.set_t) (v : V.typed_value)
     as well. The [allowed_abs] parameter controls whether we allow to end borrows
     in an abstraction or not, and in which abstraction.
 *)
-let end_borrow_get_borrow_in_env (io : inner_outer)
-    (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) (env : C.env)
-    : (C.env * g_borrow_content option, outer_borrows_or_abs) result =
+let end_borrow_get_borrow (io : inner_outer)
+    (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id)
+    (ctx : C.eval_ctx) :
+    (C.eval_ctx * g_borrow_content option, outer_borrows_or_abs) result =
   (* We use a reference to communicate the kind of borrow we found, if we
    * find one *)
   let replaced_bc : g_borrow_content option ref = ref None in
@@ -780,7 +784,7 @@ let end_borrow_get_borrow_in_env (io : inner_outer)
   (* The environment is used to keep track of the outer loans *)
   let obj =
     object
-      inherit [_] C.map_env as super
+      inherit [_] C.map_eval_ctx as super
 
       method! visit_Loan (outer : V.AbstractionId.id option * borrow_ids option)
           lc =
@@ -922,8 +926,8 @@ let end_borrow_get_borrow_in_env (io : inner_outer)
   in
   (* Catch the exceptions - raised if there are outer borrows *)
   try
-    let env = obj#visit_env (None, None) env in
-    Ok (env, !replaced_bc)
+    let ctx = obj#visit_eval_ctx (None, None) ctx in
+    Ok (ctx, !replaced_bc)
   with FoundOuter outers -> Error outers
 
 (** Auxiliary function to end borrows. See [give_back_in_env].
@@ -936,7 +940,7 @@ let end_borrow_get_borrow_in_env (io : inner_outer)
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
 let give_back_value (config : C.config) (bid : V.BorrowId.id)
-    (nv : V.typed_value) (env : C.env) : C.env =
+    (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
@@ -945,7 +949,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
   in
   let obj =
     object (self)
-      inherit [_] C.map_env as super
+      inherit [_] C.map_eval_ctx as super
 
       method! visit_Loan opt_abs lc =
         match lc with
@@ -1034,11 +1038,11 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
   in
 
   (* Explore the environment *)
-  let env = obj#visit_env None env in
+  let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
   assert !replaced;
   (* Return *)
-  env
+  ctx
 
 (** Auxiliary function to end borrows. See [give_back_in_env].
 
@@ -1050,7 +1054,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
     abstraction).
  *)
 let give_back_avalue (config : C.config) (bid : V.BorrowId.id)
-    (nv : V.typed_avalue) (env : C.env) : C.env =
+    (nv : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
@@ -1059,7 +1063,7 @@ let give_back_avalue (config : C.config) (bid : V.BorrowId.id)
   in
   let obj =
     object (self)
-      inherit [_] C.map_env as super
+      inherit [_] C.map_eval_ctx as super
 
       method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue
           =
@@ -1123,11 +1127,11 @@ let give_back_avalue (config : C.config) (bid : V.BorrowId.id)
   in
 
   (* Explore the environment *)
-  let env = obj#visit_env None env in
+  let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
   assert !replaced;
   (* Return *)
-  env
+  ctx
 
 (** Auxiliary function to end borrows. See [give_back_in_env].
     
@@ -1138,7 +1142,8 @@ let give_back_avalue (config : C.config) (bid : V.BorrowId.id)
     we update.
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
-let give_back_shared config (bid : V.BorrowId.id) (env : C.env) : C.env =
+let give_back_shared config (bid : V.BorrowId.id) (ctx : C.eval_ctx) :
+    C.eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
@@ -1147,7 +1152,7 @@ let give_back_shared config (bid : V.BorrowId.id) (env : C.env) : C.env =
   in
   let obj =
     object (self)
-      inherit [_] C.map_env as super
+      inherit [_] C.map_eval_ctx as super
 
       method! visit_Loan opt_abs lc =
         match lc with
@@ -1216,11 +1221,11 @@ let give_back_shared config (bid : V.BorrowId.id) (env : C.env) : C.env =
   in
 
   (* Explore the environment *)
-  let env = obj#visit_env None env in
+  let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
   assert !replaced;
   (* Return *)
-  env
+  ctx
 
 (** When copying values, we duplicate the shared borrows. This is tantamount
     to reborrowing the shared value. The following function applies this change
@@ -1268,8 +1273,8 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id)
   { ctx with env }
 
 (** Auxiliary function: see [end_borrow_in_env] *)
-let give_back_in_env (config : C.config) (l : V.BorrowId.id)
-    (bc : g_borrow_content) (env : C.env) : C.env =
+let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
+    (ctx : C.eval_ctx) : C.eval_ctx =
   (* This is used for sanity checks *)
   let sanity_ek =
     { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
@@ -1279,39 +1284,39 @@ let give_back_in_env (config : C.config) (l : V.BorrowId.id)
       (* Sanity check *)
       assert (l' = l);
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
-      assert (Option.is_some (lookup_loan_opt sanity_ek l env));
-      (* Update the environment *)
-      give_back_value config l tv env
+      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      (* Update the context *)
+      give_back_value config l tv ctx
   | Concrete (V.SharedBorrow l' | V.InactivatedMutBorrow l') ->
       (* Sanity check *)
       assert (l' = l);
       (* Check that the borrow is somewhere - purely a sanity check *)
-      assert (Option.is_some (lookup_loan_opt sanity_ek l env));
-      (* Update the environment *)
-      give_back_shared config l env
+      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      (* Update the context *)
+      give_back_shared config l ctx
   | Abstract (V.AMutBorrow (l', av)) ->
       (* Sanity check *)
       assert (l' = l);
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
-      assert (Option.is_some (lookup_loan_opt sanity_ek l env));
-      (* Update the environment *)
-      give_back_avalue config l av env
+      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      (* Update the context *)
+      give_back_avalue config l av ctx
   | Abstract (V.ASharedBorrow l') ->
       (* Sanity check *)
       assert (l' = l);
       (* Check that the borrow is somewhere - purely a sanity check *)
-      assert (Option.is_some (lookup_loan_opt sanity_ek l env));
-      (* Update the environment *)
-      give_back_shared config l env
+      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      (* Update the context *)
+      give_back_shared config l ctx
   | Abstract (V.AIgnoredSharedBorrow _) -> raise Unimplemented
   | Abstract (V.AIgnoredMutBorrow _) -> failwith "Unreachable"
 
-(** End a borrow identified by its borrow id in an environment
+(** End a borrow identified by its borrow id in a context
     
-    First lookup the borrow in the environment and replace it with [Bottom].
-    Then, check that there is an associated loan in the environment. When moving
+    First lookup the borrow in the context and replace it with [Bottom].
+    Then, check that there is an associated loan in the context. When moving
     values, before putting the value in its destination, we get an
-    intermediate state where some values are "outside" the environment and thus
+    intermediate state where some values are "outside" the context and thus
     inaccessible. As [give_back_value] just performs a map for instance (TODO:
     not the case anymore), we need to check independently that there is indeed a
     loan ready to receive the value we give back (note that we also have other
@@ -1332,15 +1337,15 @@ let give_back_in_env (config : C.config) (l : V.BorrowId.id)
     if it is not `None`, we allow ending a borrow if it is inside the given
     abstraction. In practice, if the value is `Some abs_id`, we should have
     checked that the corresponding loan is inside the abstraction given by
-    `abs_id` before. In practice, only [end_borrow_in_env] should call itself
+    `abs_id` before. In practice, only [end_borrow] should call itself
     with `allowed_abs = Some ...`, all the other calls should use `allowed_abs = None`:
-    if you look ath the implementation details, `end_borrow_in_env` performs
+    if you look ath the implementation details, `end_borrow` performs
     all tne necessary checks in case a borrow is inside an abstraction.
  *)
-let rec end_borrow_in_env (config : C.config) (io : inner_outer)
-    (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) (env : C.env)
-    : C.env =
-  match end_borrow_get_borrow_in_env io allowed_abs l env with
+let rec end_borrow (config : C.config) (io : inner_outer)
+    (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  match end_borrow_get_borrow io allowed_abs l ctx with
   (* Two cases:
    * - error: we found outer borrows (end them first)
    * - success: we didn't find outer borrows when updating (but maybe we actually
@@ -1359,16 +1364,16 @@ let rec end_borrow_in_env (config : C.config) (io : inner_outer)
            * be trying to end a borrow inside an abstraction, but which is actually
            * inside another borrow *)
           let allowed_abs' = None in
-          let env = end_borrows_in_env config io allowed_abs' bids env in
+          let ctx = end_borrows config io allowed_abs' bids ctx in
           (* Retry to end the borrow *)
-          end_borrow_in_env config io allowed_abs l env
+          end_borrow config io allowed_abs l ctx
       | OuterBorrows (Borrow bid) ->
           (* See the comments for the previous case *)
           assert (io = Outer);
           let allowed_abs' = None in
-          let env = end_borrow_in_env config io allowed_abs' bid env in
+          let ctx = end_borrow config io allowed_abs' bid ctx in
           (* Retry to end the borrow *)
-          end_borrow_in_env config io allowed_abs l env
+          end_borrow config io allowed_abs l ctx
       | OuterAbs abs_id -> (
           (* The borrow is inside an asbtraction: check if the corresponding
            * loan is inside the same abstraction. If this is the case, we end
@@ -1382,81 +1387,47 @@ let rec end_borrow_in_env (config : C.config) (io : inner_outer)
               enter_abs = true;
             }
           in
-          match lookup_loan ek l env with
+          match lookup_loan ek l ctx with
           | AbsId loan_abs_id, _ ->
               if loan_abs_id = abs_id then (
                 (* Same abstraction! We can end the borrow *)
-                let env = end_borrow_in_env config io (Some abs_id) l env in
+                let ctx = end_borrow config io (Some abs_id) l ctx in
                 (* Sanity check *)
-                assert (Option.is_none (lookup_borrow_opt ek l env));
-                env)
+                assert (Option.is_none (lookup_borrow_opt ek l ctx));
+                ctx)
               else
                 (* Not the same abstraction: we need to end the whole abstraction.
                  * By doing that we should have ended the target borrow (see the
                  * below sanity check) *)
-                let env = end_abstraction_in_env config abs_id env in
+                let ctx = end_abstraction config abs_id ctx in
                 (* Sanity check: we ended the target borrow *)
-                assert (Option.is_none (lookup_borrow_opt ek l env));
-                env
+                assert (Option.is_none (lookup_borrow_opt ek l ctx));
+                ctx
           | VarId _, _ ->
               (* The loan is not inside the same abstraction (actually inside
                * a non-abstraction value): we need to end the whole abstraction *)
-              let env = end_abstraction_in_env config abs_id env in
+              let ctx = end_abstraction config abs_id ctx in
               (* Sanity check: we ended the target borrow *)
-              assert (Option.is_none (lookup_borrow_opt ek l env));
-              env))
-  | Ok (env, None) ->
+              assert (Option.is_none (lookup_borrow_opt ek l ctx));
+              ctx))
+  | Ok (ctx, None) ->
       (* It is possible that we can't find a borrow in symbolic mode (ending
        * an abstraction may end several borrows at once *)
       assert (config.mode = SymbolicMode);
-      env
+      ctx
   (* We found a borrow: give the value back (i.e., update the corresponding loan) *)
-  | Ok (env, Some bc) -> give_back_in_env config l bc env
+  | Ok (ctx, Some bc) -> give_back config l bc ctx
 
-and end_borrows_in_env (config : C.config) (io : inner_outer)
+and end_borrows (config : C.config) (io : inner_outer)
     (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t)
-    (env : C.env) : C.env =
-  V.BorrowId.Set.fold
-    (fun id env -> end_borrow_in_env config io allowed_abs id env)
-    lset env
-
-and end_abstraction_in_env (config : C.config) (abs : V.AbstractionId.id)
-    (env : C.env) : C.env =
-  raise Unimplemented
-
-(** Same as [end_borrow_in_env], but operating on evaluation contexts *)
-let end_borrow (config : C.config) (io : inner_outer)
-    (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id)
     (ctx : C.eval_ctx) : C.eval_ctx =
-  L.log#ldebug
-    (lazy
-      ("end_borrow " ^ V.BorrowId.to_string l ^ ": context before:\n"
-     ^ eval_ctx_to_string ctx));
-  let env = end_borrow_in_env config io allowed_abs l ctx.env in
-  let ctx = { ctx with env } in
-  L.log#ldebug
-    (lazy
-      ("end_borrow " ^ V.BorrowId.to_string l ^ ": context after:\n"
-     ^ eval_ctx_to_string ctx));
-  ctx
+  V.BorrowId.Set.fold
+    (fun id ctx -> end_borrow config io allowed_abs id ctx)
+    lset ctx
 
-(** Same as [end_borrows_in_env], but operating on evaluation contexts *)
-let end_borrows (config : C.config) (io : inner_outer)
-    (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t)
+and end_abstraction (config : C.config) (abs : V.AbstractionId.id)
     (ctx : C.eval_ctx) : C.eval_ctx =
-  L.log#ldebug
-    (lazy
-      ("end_borrows "
-      ^ V.BorrowId.set_to_string lset
-      ^ ": context before:\n" ^ eval_ctx_to_string ctx));
-  let env = end_borrows_in_env config io allowed_abs lset ctx.env in
-  let ctx = { ctx with env } in
-  L.log#ldebug
-    (lazy
-      ("end_borrows "
-      ^ V.BorrowId.set_to_string lset
-      ^ ": context after:\n" ^ eval_ctx_to_string ctx));
-  ctx
+  raise Unimplemented
 
 let end_outer_borrow config = end_borrow config Outer None
 
@@ -1486,7 +1457,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) :
   let ek =
     { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
   in
-  match lookup_loan ek l ctx.env with
+  match lookup_loan ek l ctx with
   | _, Concrete (V.MutLoan _) ->
       failwith "Expected a shared loan, found a mut loan"
   | _, Concrete (V.SharedLoan (bids, sv)) ->
@@ -1501,8 +1472,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) :
       (* Check there aren't inactivated borrows *)
       assert (not (inactivated_in_value sv));
       (* Update the loan content *)
-      let env = update_loan ek l (V.MutLoan l) ctx.env in
-      let ctx = { ctx with env } in
+      let ctx = update_loan ek l (V.MutLoan l) ctx in
       (* Return *)
       (ctx, sv)
   | _, Abstract _ -> raise Unimplemented
@@ -1519,13 +1489,12 @@ let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id)
   let ek =
     { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false }
   in
-  match lookup_borrow ek l ctx.env with
+  match lookup_borrow ek l ctx with
   | Concrete (V.SharedBorrow _ | V.MutBorrow (_, _)) ->
       failwith "Expected an inactivated mutable borrow"
   | Concrete (V.InactivatedMutBorrow _) ->
       (* Update it *)
-      let env = update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx.env in
-      { ctx with env }
+      update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx
   | Abstract _ -> raise Unimplemented
 
 (** Promote an inactivated mut borrow to a mut borrow.
@@ -1538,7 +1507,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer)
   let ek =
     { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
   in
-  match lookup_loan ek l ctx.env with
+  match lookup_loan ek l ctx with
   | _, Concrete (V.MutLoan _) -> failwith "Unreachable"
   | _, Concrete (V.SharedLoan (bids, sv)) -> (
       (* If there are loans inside the value, end them. Note that there can't be
@@ -1626,10 +1595,10 @@ type projection_access = {
     We return the (eventually) updated value, the value we read at the end of
     the place and the (eventually) updated environment.
  *)
-let rec access_projection (access : projection_access) (env : C.env)
+let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
     (* Function to (eventually) update the value we find *)
       (update : V.typed_value -> V.typed_value) (p : E.projection)
-    (v : V.typed_value) : (C.env * updated_read_value) path_access_result =
+    (v : V.typed_value) : (C.eval_ctx * updated_read_value) path_access_result =
   (* For looking up/updating shared loans *)
   let ek : exploration_kind =
     { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
@@ -1646,7 +1615,7 @@ let rec access_projection (access : projection_access) (env : C.env)
         failwith
           "Assertion failed: new value doesn't have the same type as its \
            destination");
-      Ok (env, { read = v; updated = nv })
+      Ok (ctx, { read = v; updated = nv })
   | pe :: p' -> (
       (* Match on the projection element and the value *)
       match (pe, v.V.value, v.V.ty) with
@@ -1662,31 +1631,31 @@ let rec access_projection (access : projection_access) (env : C.env)
           | _ -> failwith "Unreachable");
           (* Actually project *)
           let fv = T.FieldId.nth adt.field_values field_id in
-          match access_projection access env update p' fv with
+          match access_projection access ctx update p' fv with
           | Error err -> Error err
-          | Ok (env, res) ->
+          | Ok (ctx, res) ->
               (* Update the field value *)
               let nvalues =
                 T.FieldId.update_nth adt.field_values field_id res.updated
               in
               let nadt = V.Adt { adt with V.field_values = nvalues } in
               let updated = { v with value = nadt } in
-              Ok (env, { res with updated }))
+              Ok (ctx, { res with updated }))
       (* Tuples *)
       | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _, _) -> (
           assert (arity = List.length adt.field_values);
           let fv = T.FieldId.nth adt.field_values field_id in
           (* Project *)
-          match access_projection access env update p' fv with
+          match access_projection access ctx update p' fv with
           | Error err -> Error err
-          | Ok (env, res) ->
+          | Ok (ctx, res) ->
               (* Update the field value *)
               let nvalues =
                 T.FieldId.update_nth adt.field_values field_id res.updated
               in
               let ntuple = V.Adt { adt with field_values = nvalues } in
               let updated = { v with value = ntuple } in
-              Ok (env, { res with updated })
+              Ok (ctx, { res with updated })
           (* If we reach Bottom, it may mean we need to expand an uninitialized
            * enumeration value *))
       | Field (ProjAdt (_, _), _), V.Bottom, _ ->
@@ -1706,9 +1675,9 @@ let rec access_projection (access : projection_access) (env : C.env)
            * it shouldn't happen due to user code, and we leverage it
            * when implementing box dereferencement for the concrete
            * interpreter *)
-          match access_projection access env update p' bv with
+          match access_projection access ctx update p' bv with
           | Error err -> Error err
-          | Ok (env, res) ->
+          | Ok (ctx, res) ->
               let nv =
                 {
                   v with
@@ -1716,44 +1685,44 @@ let rec access_projection (access : projection_access) (env : C.env)
                     V.Adt { variant_id = None; field_values = [ res.updated ] };
                 }
               in
-              Ok (env, { res with updated = nv }))
+              Ok (ctx, { res with updated = nv }))
       (* Borrows *)
       | Deref, V.Borrow bc, _ -> (
           match bc with
           | V.SharedBorrow bid ->
               (* Lookup the loan content, and explore from there *)
               if access.lookup_shared_borrows then
-                match lookup_loan ek bid env with
+                match lookup_loan ek bid ctx with
                 | _, Concrete (V.MutLoan _) -> failwith "Expected a shared loan"
                 | _, Concrete (V.SharedLoan (bids, sv)) -> (
                     (* Explore the shared value *)
-                    match access_projection access env update p' sv with
+                    match access_projection access ctx update p' sv with
                     | Error err -> Error err
-                    | Ok (env, res) ->
+                    | Ok (ctx, res) ->
                         (* Update the shared loan with the new value returned
                            by [access_projection] *)
-                        let env =
+                        let ctx =
                           update_loan ek bid
                             (V.SharedLoan (bids, res.updated))
-                            env
+                            ctx
                         in
                         (* Return - note that we don't need to update the borrow itself *)
-                        Ok (env, { res with updated = v }))
+                        Ok (ctx, { res with updated = v }))
                 | _, Abstract _ -> raise Unimplemented
               else Error (FailBorrow bc)
           | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid)
           | V.MutBorrow (bid, bv) ->
               if access.enter_mut_borrows then
-                match access_projection access env update p' bv with
+                match access_projection access ctx update p' bv with
                 | Error err -> Error err
-                | Ok (env, res) ->
+                | Ok (ctx, res) ->
                     let nv =
                       {
                         v with
                         value = V.Borrow (V.MutBorrow (bid, res.updated));
                       }
                     in
-                    Ok (env, { res with updated = nv })
+                    Ok (ctx, { res with updated = nv })
               else Error (FailBorrow bc))
       | _, V.Loan lc, _ -> (
           match lc with
@@ -1763,16 +1732,16 @@ let rec access_projection (access : projection_access) (env : C.env)
                  to the fact that we need to reexplore the *whole* place (i.e,
                  we mustn't ignore the current projection element *)
               if access.enter_shared_loans then
-                match access_projection access env update (pe :: p') sv with
+                match access_projection access ctx update (pe :: p') sv with
                 | Error err -> Error err
-                | Ok (env, res) ->
+                | Ok (ctx, res) ->
                     let nv =
                       {
                         v with
                         value = V.Loan (V.SharedLoan (bids, res.updated));
                       }
                     in
-                    Ok (env, { res with updated = nv })
+                    Ok (ctx, { res with updated = nv })
               else Error (FailSharedLoan bids))
       | (_, (V.Concrete _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r ->
           let pe, v, ty = r in
@@ -1790,18 +1759,18 @@ let rec access_projection (access : projection_access) (env : C.env)
  *)
 let access_place (access : projection_access)
     (* Function to (eventually) update the value we find *)
-      (update : V.typed_value -> V.typed_value) (p : E.place) (env : C.env) :
-    (C.env * V.typed_value) path_access_result =
+      (update : V.typed_value -> V.typed_value) (p : E.place) (ctx : C.eval_ctx)
+    : (C.eval_ctx * V.typed_value) path_access_result =
   (* Lookup the variable's value *)
-  let value = C.env_lookup_var_value env p.var_id in
+  let value = C.ctx_lookup_var_value ctx p.var_id in
   (* Apply the projection *)
-  match access_projection access env update p.projection value with
+  match access_projection access ctx update p.projection value with
   | Error err -> Error err
-  | Ok (env, res) ->
+  | Ok (ctx, res) ->
       (* Update the value *)
-      let env = C.env_update_var_value env p.var_id res.updated in
+      let ctx = C.ctx_update_var_value ctx p.var_id res.updated in
       (* Return *)
-      Ok (env, res.read)
+      Ok (ctx, res.read)
 
 type access_kind =
   | Read  (** We can go inside borrows and loans *)
@@ -1836,17 +1805,18 @@ let read_place (config : C.config) (access : access_kind) (p : E.place)
   let access = access_kind_to_projection_access access in
   (* The update function is the identity *)
   let update v = v in
-  match access_place access update p ctx.env with
+  match access_place access update p ctx with
   | Error err -> Error err
-  | Ok (env1, read_value) ->
+  | Ok (ctx1, read_value) ->
       (* Note that we ignore the new environment: it should be the same as the
          original one.
       *)
       if config.check_invariants then
-        if env1 <> ctx.env then (
+        if ctx1 <> ctx then (
           let msg =
             "Unexpected environment update:\nNew environment:\n"
-            ^ C.show_env env1 ^ "\n\nOld environment:\n" ^ C.show_env ctx.env
+            ^ C.show_env ctx1.env ^ "\n\nOld environment:\n"
+            ^ C.show_env ctx.env
           in
           L.log#serror msg;
           failwith "Unexpected environment update");
@@ -1864,11 +1834,11 @@ let write_place (_config : C.config) (access : access_kind) (p : E.place)
   let access = access_kind_to_projection_access access in
   (* The update function substitutes the value with the new value *)
   let update _ = nv in
-  match access_place access update p ctx.env with
+  match access_place access update p ctx with
   | Error err -> Error err
-  | Ok (env, _) ->
+  | Ok (ctx, _) ->
       (* We ignore the read value *)
-      Ok { ctx with env }
+      Ok ctx
 
 let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
     (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx =