From 47e0291dd840cfc59ee6c5bc3ac2c7edd1610ab7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 7 Nov 2022 09:55:04 +0100
Subject: Rename "inactivated borrows" to "reserved borrows"

---
 compiler/InterpreterBorrows.ml     | 53 ++++++++++++++++++--------------------
 compiler/InterpreterBorrows.mli    | 12 +++++++--
 compiler/InterpreterBorrowsCore.ml | 12 ++++-----
 compiler/InterpreterExpressions.ml | 14 +++++-----
 compiler/InterpreterPaths.ml       | 19 ++++++--------
 compiler/InterpreterProjectors.ml  | 14 +++++-----
 compiler/InterpreterStatements.ml  |  2 +-
 compiler/Invariants.ml             | 16 ++++++------
 compiler/Print.ml                  |  4 +--
 compiler/SymbolicToPure.ml         |  6 ++---
 compiler/Values.ml                 | 22 ++++++++--------
 compiler/ValuesUtils.ml            |  6 ++---
 12 files changed, 91 insertions(+), 89 deletions(-)

(limited to 'compiler')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 1b4907ac..585db0eb 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -93,7 +93,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
 
       method! visit_Borrow outer bc =
         match bc with
-        | SharedBorrow (_, l') | InactivatedMutBorrow (_, l') ->
+        | SharedBorrow (_, l') | ReservedMutBorrow (_, l') ->
             (* Check if this is the borrow we are looking for *)
             if l = l' then (
               (* Check if there are outer borrows or if we are inside an abstraction *)
@@ -731,7 +731,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
       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')) ->
+  | Concrete (V.SharedBorrow (_, l') | V.ReservedMutBorrow (_, l')) ->
       (* Sanity check *)
       assert (l' = l);
       (* Check that the borrow is somewhere - purely a sanity check *)
@@ -1120,7 +1120,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
         match bc with
         | V.SharedBorrow (_, _) | V.MutBorrow (_, _) ->
             raise (FoundBorrowContent bc)
-        | V.InactivatedMutBorrow _ -> raise (Failure "Unreachable")
+        | V.ReservedMutBorrow _ -> raise (Failure "Unreachable")
     end
   in
   (* Lookup the abstraction *)
@@ -1224,7 +1224,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
                 (* Give the value back - note that the mut borrow was below a
                  * shared borrow: the value is thus unchanged *)
                 give_back_value config bid v ctx)
-        | V.InactivatedMutBorrow _ -> raise (Failure "Unreachable")
+        | V.ReservedMutBorrow _ -> raise (Failure "Unreachable")
       in
       (* Reexplore *)
       end_abstraction_borrows config chain abs_id cf ctx
@@ -1403,7 +1403,7 @@ let end_borrows config : V.BorrowId.Set.t -> cm_fun =
 let end_abstraction config = end_abstraction_aux config []
 let end_abstractions config = end_abstractions_aux config []
 
-(** Helper function: see {!activate_inactivated_mut_borrow}.
+(** Helper function: see {!activate_reserved_mut_borrow}.
 
     This function updates the shared loan to a mutable loan (we then update
     the borrow with another helper). Of course, the shared loan must contain
@@ -1413,7 +1413,7 @@ let end_abstractions config = end_abstractions_aux config []
     The returned value (previously shared) is checked:
     - it mustn't contain loans
     - it mustn't contain {!V.Bottom}
-    - it mustn't contain inactivated borrows
+    - it mustn't contain reserved borrows
     TODO: this kind of checks should be put in an auxiliary helper, because
     they are redundant.
 
@@ -1446,8 +1446,8 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id)
       assert (not (loans_in_value sv));
       (* Check there isn't {!Bottom} (this is actually an invariant *)
       assert (not (bottom_in_value ctx.ended_regions sv));
-      (* Check there aren't inactivated borrows *)
-      assert (not (inactivated_in_value sv));
+      (* Check there aren't reserved borrows *)
+      assert (not (reserved_in_value sv));
       (* Update the loan content *)
       let ctx = update_loan ek l (V.MutLoan l) ctx in
       (* Continue *)
@@ -1460,15 +1460,16 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id)
            "Can't promote a shared loan to a mutable loan if the loan is \
             inside an abstraction")
 
-(** Helper function: see {!activate_inactivated_mut_borrow}.
+(** Helper function: see {!activate_reserved_mut_borrow}.
 
-    This function updates a shared borrow to a mutable borrow.
+    This function updates a shared borrow to a mutable borrow (and that is
+    all: it doesn't touch the corresponding loan).
  *)
-let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id) (cf : m_fun)
+let replace_reserved_borrow_with_mut_borrow (l : V.BorrowId.id) (cf : m_fun)
     (borrowed_value : V.typed_value) : m_fun =
  fun ctx ->
-  (* Lookup the inactivated borrow - note that we don't go inside borrows/loans:
-     there can't be inactivated borrows inside other borrows/loans
+  (* Lookup the reserved borrow - note that we don't go inside borrows/loans:
+     there can't be reserved borrows inside other borrows/loans
   *)
   let ek =
     { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false }
@@ -1476,8 +1477,8 @@ let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id) (cf : m_fun)
   let ctx =
     match lookup_borrow ek l ctx with
     | Concrete (V.SharedBorrow _ | V.MutBorrow (_, _)) ->
-        raise (Failure "Expected an inactivated mutable borrow")
-    | Concrete (V.InactivatedMutBorrow _) ->
+        raise (Failure "Expected a reserved mutable borrow")
+    | Concrete (V.ReservedMutBorrow _) ->
         (* Update it *)
         update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx
     | Abstract _ ->
@@ -1490,12 +1491,9 @@ let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id) (cf : m_fun)
   (* Continue *)
   cf ctx
 
-(** Promote an inactivated mut borrow to a mut borrow.
-
-    The borrow must point to a shared value which is borrowed exactly once.
- *)
-let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
-    : cm_fun =
+(** Promote a reserved mut borrow to a mut borrow. *)
+let rec promote_reserved_mut_borrow (config : C.config) (l : V.BorrowId.id) :
+    cm_fun =
  fun cf ctx ->
   (* Lookup the value *)
   let ek =
@@ -1505,7 +1503,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
   | _, Concrete (V.MutLoan _) -> raise (Failure "Unreachable")
   | _, Concrete (V.SharedLoan (bids, sv)) -> (
       (* If there are loans inside the value, end them. Note that there can't be
-         inactivated borrows inside the value.
+         reserved borrows inside the value.
          If we perform an update, do a recursive call to lookup the updated value *)
       match get_first_loan_in_value sv with
       | Some lc ->
@@ -1516,7 +1514,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
             | V.MutLoan bid -> end_borrow config bid
           in
           (* Recursive call *)
-          let cc = comp cc (activate_inactivated_mut_borrow config l) in
+          let cc = comp cc (promote_reserved_mut_borrow config l) in
           (* Continue *)
           cc cf ctx
       | None ->
@@ -1524,11 +1522,11 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
           (* Some sanity checks *)
           log#ldebug
             (lazy
-              ("activate_inactivated_mut_borrow: resulting value:\n"
+              ("activate_reserved_mut_borrow: resulting value:\n"
               ^ typed_value_to_string ctx sv));
           assert (not (loans_in_value sv));
           assert (not (bottom_in_value ctx.ended_regions sv));
-          assert (not (inactivated_in_value sv));
+          assert (not (reserved_in_value sv));
           (* End the borrows which borrow from the value, at the exception of
              the borrow we want to promote *)
           let bids = V.BorrowId.Set.remove l bids in
@@ -1543,7 +1541,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
           *)
           let cc =
             comp cc (fun cf borrowed_value ->
-                promote_inactivated_borrow_to_mut_borrow l cf borrowed_value)
+                replace_reserved_borrow_with_mut_borrow l cf borrowed_value)
           in
           (* Continue *)
           cc cf ctx)
@@ -1552,6 +1550,5 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
        * returned by abstractions. I'm not sure how we could handle that anyway. *)
       raise
         (Failure
-           "Can't activate an inactivated mutable borrow referencing a loan \
-            inside\n\
+           "Can't activate a reserved mutable borrow referencing a loan inside\n\
            \         an abstraction")
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 0733a15b..f21fdcd5 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -30,5 +30,13 @@ val end_abstraction : C.config -> V.AbstractionId.id -> cm_fun
 (** End a set of abstractions while preserving the invariants. *)
 val end_abstractions : C.config -> V.AbstractionId.Set.t -> cm_fun
 
-(** Activate a reserved borrow into a mutable borrow, while preserving the invariants. *)
-val activate_inactivated_mut_borrow : C.config -> V.BorrowId.id -> cm_fun
+(** 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
+    then promoted to mutable borrows upon their first use.
+
+    This function replaces the reserved borrow with a mutable borrow, then replaces
+    the corresponding shared loan with a mutable loan (after having ended the
+    other shared borrows which point to this loan).
+ *)
+val promote_reserved_mut_borrow : C.config -> V.BorrowId.id -> cm_fun
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 7cd447c3..d3be1bed 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -204,9 +204,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
         | V.SharedBorrow (mv, bid) ->
             (* Nothing specific to do *)
             super#visit_SharedBorrow env mv bid
-        | V.InactivatedMutBorrow (mv, bid) ->
+        | V.ReservedMutBorrow (mv, bid) ->
             (* Nothing specific to do *)
-            super#visit_InactivatedMutBorrow env mv bid
+            super#visit_ReservedMutBorrow env mv bid
         | V.MutBorrow (bid, mv) ->
             (* Control the dive *)
             if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
@@ -314,7 +314,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
 
       method! visit_borrow_content env bc =
         match bc with
-        | V.SharedBorrow (_, _) | V.InactivatedMutBorrow _ ->
+        | V.SharedBorrow (_, _) | V.ReservedMutBorrow _ ->
             (* Nothing specific to do *)
             super#visit_borrow_content env bc
         | V.MutBorrow (bid, mv) ->
@@ -419,7 +419,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
         | V.SharedBorrow (_, bid) ->
             (* Check the borrow id *)
             if bid = l then raise (FoundGBorrowContent (Concrete bc)) else ()
-        | V.InactivatedMutBorrow (_, bid) ->
+        | V.ReservedMutBorrow (_, bid) ->
             (* Check the borrow id *)
             if bid = l then raise (FoundGBorrowContent (Concrete bc)) else ()
 
@@ -503,10 +503,10 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
         | V.SharedBorrow (mv, bid) ->
             (* Check the id *)
             if bid = l then update () else super#visit_SharedBorrow env mv bid
-        | V.InactivatedMutBorrow (mv, bid) ->
+        | V.ReservedMutBorrow (mv, bid) ->
             (* Check the id *)
             if bid = l then update ()
-            else super#visit_InactivatedMutBorrow env mv bid
+            else super#visit_ReservedMutBorrow env mv bid
 
       method! visit_loan_content env lc =
         match lc with
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index a7c17a45..ea0e1aa9 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -52,7 +52,7 @@ let expand_primitively_copyable_at_place (config : C.config)
 
 (** Read a place (CPS-style function).
 
-    We also check that the value *doesn't contain bottoms or inactivated
+    We also check that the value *doesn't contain bottoms or reserved
     borrows*.
  *)
 let read_place (config : C.config) (access : access_kind) (p : E.place)
@@ -61,8 +61,8 @@ let read_place (config : C.config) (access : access_kind) (p : E.place)
   let v = read_place config access p ctx in
   (* Check that there are no bottoms in the value *)
   assert (not (bottom_in_value ctx.ended_regions v));
-  (* Check that there are no inactivated borrows in the value *)
-  assert (not (inactivated_in_value v));
+  (* Check that there are no reserved borrows in the value *)
+  assert (not (reserved_in_value v));
   (* Call the continuation *)
   cf v ctx
 
@@ -77,7 +77,7 @@ let read_place (config : C.config) (access : access_kind) (p : E.place)
       controls whether we only end mutable loans, or also shared loans).
 
     We also check, after the reorganization, that the value at the place
-    *doesn't contain any bottom nor inactivated borrows*.
+    *doesn't contain any bottom nor reserved borrows*.
 
     [expand_prim_copy]: if [true], expand the symbolic values which are
     primitively copyable and contain borrows.
@@ -180,8 +180,8 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
           let ctx = InterpreterBorrows.reborrow_shared bid bid' ctx in
           (ctx, { v with V.value = V.Borrow (SharedBorrow (mv, bid')) })
       | MutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow")
-      | V.InactivatedMutBorrow _ ->
-          raise (Failure "Can't copy an inactivated mut borrow"))
+      | V.ReservedMutBorrow _ ->
+          raise (Failure "Can't copy a reserved mut borrow"))
   | V.Loan lc -> (
       (* We can only copy shared loans *)
       match lc with
@@ -673,7 +673,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
         in
         let bc =
           if bkind = E.Shared then V.SharedBorrow (shared_mvalue, bid)
-          else V.InactivatedMutBorrow (shared_mvalue, bid)
+          else V.ReservedMutBorrow (shared_mvalue, bid)
         in
         let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
         (* Continue *)
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 73b446da..3d0c69e8 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -28,8 +28,8 @@ type path_fail_kind =
       (** Failure because we couldn't go inside a shared loan *)
   | FailMutLoan of V.BorrowId.id
       (** Failure because we couldn't go inside a mutable loan *)
-  | FailInactivatedMutBorrow of V.BorrowId.id
-      (** Failure because we couldn't go inside an inactivated mutable borrow
+  | FailReservedMutBorrow of V.BorrowId.id
+      (** Failure because we couldn't go inside a reserved mutable borrow
           (which should get activated) *)
   | FailSymbolic of int * V.symbolic_value
       (** Failure because we need to enter a symbolic value (and thus need to
@@ -216,8 +216,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
                         (* Return - note that we don't need to update the borrow itself *)
                         Ok (ctx, { res with updated = v }))
               else Error (FailBorrow bc)
-          | V.InactivatedMutBorrow (_, bid) ->
-              Error (FailInactivatedMutBorrow bid)
+          | V.ReservedMutBorrow (_, bid) -> Error (FailReservedMutBorrow bid)
           | V.MutBorrow (bid, bv) ->
               if access.enter_mut_borrows then
                 match access_projection access ctx update p' bv with
@@ -480,8 +479,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
         match err with
         | FailSharedLoan bids -> end_borrows config bids
         | FailMutLoan bid -> end_borrow config bid
-        | FailInactivatedMutBorrow bid ->
-            activate_inactivated_mut_borrow config bid
+        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow config bid
         | FailSymbolic (i, sp) ->
             (* Expand the symbolic value *)
             let proj, _ =
@@ -511,8 +509,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
         match err with
         | FailSharedLoan bids -> end_borrows config bids
         | FailMutLoan bid -> end_borrow config bid
-        | FailInactivatedMutBorrow bid ->
-            activate_inactivated_mut_borrow config bid
+        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow config bid
         | FailSymbolic (_pe, sp) ->
             (* Expand the symbolic value *)
             expand_symbolic_value_no_branching config sp
@@ -549,9 +546,9 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
         match bc with
         | V.SharedBorrow _ | V.MutBorrow (_, _) ->
             (* Nothing special to do *) super#visit_borrow_content env bc
-        | V.InactivatedMutBorrow (_, bid) ->
-            (* We need to activate inactivated borrows *)
-            let cc = activate_inactivated_mut_borrow config bid in
+        | V.ReservedMutBorrow (_, bid) ->
+            (* We need to activate reserved borrows *)
+            let cc = promote_reserved_mut_borrow config bid in
             raise (UpdateCtx cc)
 
       method! visit_loan_content env lc =
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 67bbe21f..d656e158 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -66,10 +66,10 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
                 | _ -> raise (Failure "Unexpected")
               in
               (bid, asb)
-          | V.InactivatedMutBorrow _, _ ->
+          | V.ReservedMutBorrow _, _ ->
               raise
                 (Failure
-                   "Can't apply a proj_borrow over an inactivated mutable \
+                   "Can't apply a proj_borrow over a reserved mutable \
                     borrow")
           | _ -> raise (Failure "Unreachable")
         in
@@ -141,10 +141,10 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
                   in
                   V.AMutBorrow (mv, bid, bv)
               | V.SharedBorrow (_, bid), T.Shared -> V.ASharedBorrow bid
-              | V.InactivatedMutBorrow _, _ ->
+              | V.ReservedMutBorrow _, _ ->
                   raise
                     (Failure
-                       "Can't apply a proj_borrow over an inactivated mutable \
+                       "Can't apply a proj_borrow over a reserved mutable \
                         borrow")
               | _ -> raise (Failure "Unreachable")
             in
@@ -179,10 +179,10 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
                     | _ -> raise (Failure "Unexpected")
                   in
                   V.AProjSharedBorrow asb
-              | V.InactivatedMutBorrow _, _ ->
+              | V.ReservedMutBorrow _, _ ->
                   raise
                     (Failure
-                       "Can't apply a proj_borrow over an inactivated mutable \
+                       "Can't apply a proj_borrow over a reserved mutable \
                         borrow")
               | _ -> raise (Failure "Unreachable")
             in
@@ -333,7 +333,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
     match v.V.value with
     | V.Borrow lc -> (
         match lc with
-        | V.SharedBorrow (_, _) | V.InactivatedMutBorrow _ -> None
+        | V.SharedBorrow (_, _) | V.ReservedMutBorrow _ -> None
         | V.MutBorrow (id, _) -> Some id)
     | _ -> None
   in
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 66196349..08a03885 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -809,7 +809,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
                   (* Update the synthesized AST - here we store meta-information.
                    * We do it only in specific cases (it is not always useful, and
                    * also it can lead to issues - for instance, if we borrow an
-                   * inactivated borrow, we later can't translate it to pure values...) *)
+                   * reserved borrow, we later can't translate it to pure values...) *)
                   match rvalue with
                   | E.Global _ -> raise (Failure "Unreachable")
                   | E.Use _
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 18a1c835..ff7fa1fc 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -46,7 +46,7 @@ let borrows_infos_to_string (indent : string)
     (infos : borrow_info V.BorrowId.Map.t) : string =
   V.BorrowId.Map.to_string (Some indent) show_borrow_info infos
 
-type borrow_kind = Mut | Shared | Inactivated
+type borrow_kind = Mut | Shared | Reserved
 
 (** Check that:
     - loans and borrows are correctly related
@@ -217,10 +217,10 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
     let info = find_info bid in
     (* Check that the borrow kind is consistent *)
     (match (info.loan_kind, kind) with
-    | T.Shared, (Shared | Inactivated) | T.Mut, Mut -> ()
+    | T.Shared, (Shared | Reserved) | T.Mut, Mut -> ()
     | _ -> raise (Failure "Invariant not satisfied"));
-    (* An inactivated borrow can't point to a value inside an abstraction *)
-    assert (kind <> Inactivated || not info.loan_in_abs);
+    (* An reserved borrow can't point to a value inside an abstraction *)
+    assert (kind <> Reserved || not info.loan_in_abs);
     (* Insert the borrow id *)
     let borrow_ids = info.borrow_ids in
     assert (not (V.BorrowId.Set.mem bid borrow_ids));
@@ -247,7 +247,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
           match bc with
           | V.SharedBorrow (_, bid) -> register_borrow Shared bid
           | V.MutBorrow (bid, _) -> register_borrow Mut bid
-          | V.InactivatedMutBorrow (_, bid) -> register_borrow Inactivated bid
+          | V.ReservedMutBorrow (_, bid) -> register_borrow Reserved bid
         in
         (* Continue exploring *)
         super#visit_borrow_content env bc
@@ -298,7 +298,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
     !borrows_infos
 
 (** Check that:
-    - borrows/loans can't contain ⊥ or inactivated mut borrows
+    - borrows/loans can't contain ⊥ or reserved mut borrows
     - shared loans can't contain mutable loans
  *)
 let check_borrowed_values_invariant (config : C.config) (ctx : C.eval_ctx) :
@@ -333,7 +333,7 @@ let check_borrowed_values_invariant (config : C.config) (ctx : C.eval_ctx) :
         let info =
           match bc with
           | V.SharedBorrow _ -> set_outer_shared info
-          | V.InactivatedMutBorrow _ ->
+          | V.ReservedMutBorrow _ ->
               assert (not info.outer_borrow);
               set_outer_shared info
           | V.MutBorrow (_, _) -> set_outer_mut info
@@ -463,7 +463,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
             match (bc, rkind) with
             | V.SharedBorrow (_, bid), T.Shared
-            | V.InactivatedMutBorrow (_, bid), T.Mut -> (
+            | V.ReservedMutBorrow (_, bid), T.Mut -> (
                 (* Lookup the borrowed value to check it has the proper type *)
                 let _, glc = lookup_loan ek_all bid ctx in
                 match glc with
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 53bba8c7..2b2f98f0 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -127,8 +127,8 @@ module Values = struct
         "&mut@" ^ V.BorrowId.to_string bid ^ " ("
         ^ typed_value_to_string fmt tv
         ^ ")"
-    | InactivatedMutBorrow (_, bid) ->
-        "⌊inactivated_mut@" ^ V.BorrowId.to_string bid ^ "⌋"
+    | ReservedMutBorrow (_, bid) ->
+        "⌊reserved_mut@" ^ V.BorrowId.to_string bid ^ "⌋"
 
   and loan_content_to_string (fmt : value_formatter) (lc : V.loan_content) :
       string =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 54f14d30..3636d4b8 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -772,10 +772,10 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (v : V.typed_value) :
             (* The meta-value stored in the shared borrow was added especially
              * for this case (because we can't use the borrow id for lookups) *)
             translate mv
-        | V.InactivatedMutBorrow (mv, _) ->
-            (* Same as for shared borrows. However, note that we use inactivated borrows
+        | V.ReservedMutBorrow (mv, _) ->
+            (* Same as for shared borrows. However, note that we use reserved borrows
              * only in meta-data: a value actually *used in the translation* can't come
-             * from an unpromoted inactivated borrow *)
+             * from an unpromoted reserved borrow *)
             translate mv
         | V.MutBorrow (_, v) ->
             (* Borrows are the identity in the extraction *)
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 6245608d..071f5e0f 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -112,15 +112,15 @@ and borrow_content =
        *)
   | MutBorrow of (BorrowId.id[@opaque]) * typed_value
       (** A mutably borrowed value. *)
-  | InactivatedMutBorrow of mvalue * (BorrowId.id[@opaque])
-      (** An inactivated mut borrow.
+  | ReservedMutBorrow of mvalue * (BorrowId.id[@opaque])
+      (** An reserved mut borrow.
 
           This is used to model {{: https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html} two-phase borrows}.
-          When evaluating a two-phase mutable borrow, we first introduce an inactivated
+          When evaluating a two-phase mutable borrow, we first introduce a reserved
           borrow which behaves like a shared borrow, until the moment we actually *use*
-          the borrow: at this point, we end all the other shared borrows (or inactivated
-          borrows - though there shouldn't be any other inactivated borrows if the program
-          is well typed) of this value and replace the inactivated borrow with a
+          the borrow: at this point, we end all the other shared borrows (or reserved
+          borrows - though there shouldn't be any other reserved borrows if the program
+          is well typed) of this value and replace the reserved borrow with a
           mutable borrow.
           
           A simple use case of two-phase borrows:
@@ -139,24 +139,24 @@ and borrow_content =
           ]}
           
           The meta-value is used for the same purposes as with shared borrows,
-          at the exception that in case of inactivated borrows it is not
+          at the exception that in case of reserved borrows it is not
           *necessary* for the synthesis: we keep it only as meta-information.
           To be more precise:
           - when generating the synthesized program, we may need to convert
             shared borrows to pure values
-          - we never need to do so for inactivated borrows: such borrows must
+          - we never need to do so for reserved borrows: such borrows must
             be activated at the moment we use them (meaning we convert a *mutable*
             borrow to a pure value). However, we save meta-data about the assignments,
             which is used to make the code cleaner: when generating this meta-data,
-            we may need to convert inactivated borrows to pure values, in which
-            situation we convert the meta-value we stored in the inactivated
+            we may need to convert reserved borrows to pure values, in which
+            situation we convert the meta-value we stored in the reserved
             borrow.
        *)
 
 and loan_content =
   | SharedLoan of (BorrowId.Set.t[@opaque]) * typed_value
   | MutLoan of (BorrowId.id[@opaque])
-      (** TODO: we might want to add a set of borrow ids (useful for inactivated
+      (** TODO: we might want to add a set of borrow ids (useful for reserved
           borrows, and extremely useful when giving shared values to abstractions).
        *)
 
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 0e1714a8..524f86a4 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -46,12 +46,12 @@ let borrows_in_value (v : typed_value) : bool =
     false
   with Found -> true
 
-(** Check if a value contains inactivated mutable borrows *)
-let inactivated_in_value (v : typed_value) : bool =
+(** Check if a value contains reserved mutable borrows *)
+let reserved_in_value (v : typed_value) : bool =
   let obj =
     object
       inherit [_] iter_typed_value
-      method! visit_InactivatedMutBorrow _env _ = raise Found
+      method! visit_ReservedMutBorrow _env _ = raise Found
     end
   in
   (* We use exceptions *)
-- 
cgit v1.2.3