Update the functions to activate inactivated borrows

2 files changed, 37 insertions, 8 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 17dd14a4..ee64ec29 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2118,7 +2118,12 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) :
       let ctx = update_loan ek l (V.MutLoan l) ctx in
       (* Return *)
       (ctx, sv)
-  | _, Abstract _ -> raise Unimplemented
+  | _, Abstract _ ->
+      (* I don't think it is possible to have two-phase borrows involving borrows
+       * returned by abstractions. I'm not sure how we could handle that anyway. *)
+      failwith
+        "Can't promote a shared loan to a mutable loan if the loan is inside \
+         an abstraction"
 
 (** Helper function: see [activate_inactivated_mut_borrow].
 
@@ -2138,7 +2143,11 @@ let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id)
   | Concrete (V.InactivatedMutBorrow _) ->
       (* Update it *)
       update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx
-  | Abstract _ -> raise Unimplemented
+  | Abstract _ ->
+      (* This can't happen for sure *)
+      failwith
+        "Can't promote a shared borrow to a mutable borrow if the borrow is \
+         inside an abstraction"
 
 (** Promote an inactivated mut borrow to a mut borrow.
 
@@ -2187,7 +2196,12 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer)
              [promote_shared_loan_to_mut_loan]
           *)
           promote_inactivated_borrow_to_mut_borrow l borrowed_value ctx)
-  | _, Abstract _ -> raise Unimplemented
+  | _, Abstract _ ->
+      (* I don't think it is possible to have two-phase borrows involving borrows
+       * returned by abstractions. I'm not sure how we could handle that anyway. *)
+      failwith
+        "Can't activate an inactivated mutable borrow referencing a loan inside\n\
+        \         an abstraction"
 
 (** Paths *)
 
diff --git a/src/Values.ml b/src/Values.ml
index f1b2e0a6..b6866621 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -115,13 +115,28 @@ and borrow_content =
   | InactivatedMutBorrow of (BorrowId.id[@opaque])
       (** An inactivated mut borrow.
 
-          This is used to model two-phase borrows. When evaluating a two-phase
-          mutable borrow, we first introduce an inactivated 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
+          This is used to model [two-phase borrows](https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html).
+          When evaluating a two-phase mutable borrow, we first introduce an inactivated
+          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
           mutable borrow.
+          
+          A simple use case of two-phase borrows:
+          ```
+          let mut v = Vec::new();
+          v.push(v.len());
+          ```
+          
+          This gets desugared to (something similar to) the following MIR:
+          ```
+          v = Vec::new();
+          v1 = &mut v;
+          v2 = &v; // We need this borrow, but v has already been mutably borrowed!
+          l = Vec::len(move v2);
+          Vec::push(move v1, move l); // In practice, v1 gets activated only here
+          ```
        *)
 
 and loan_content =