Finish implementing visit_ABorrow for end_borrow_get_borrow_in_env

2 files changed, 36 insertions, 3 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 9a440648..4ea95028 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -701,8 +701,41 @@ let end_borrow_get_borrow_in_env (io : inner_outer)
 
       method! visit_ABorrow outer bc =
         match bc with
-        | V.AMutBorrow (bid, av) -> raise Unimplemented
-        | V.ASharedBorrow bid -> raise Unimplemented
+        | V.AMutBorrow (bid, av) ->
+            (* Check if this is the borrow we are looking for *)
+            if bid = l then (
+              (* When ending a mut borrow, there are two cases:
+               * - in the general case, we have to end the whole abstraction
+               *   (and thus raise an exception to signal that to the caller)
+               * - in some situations, the associated loan is inside the same
+               *   abstraction as the borrow. In this situation, we can end
+               *   the borrow without ending the whole abstraction, and we
+               *   simply move the child avalue around.
+               *)
+              (* Check there are outer borrows, or if we need to end the whole
+               * abstraction *)
+              raise_if_outer outer;
+              (* Register the update *)
+              set_replaced_bc (Abstract bc);
+              (* Update the value - note that we are necessarily in the second
+               * of the two cases described above *)
+              V.ABottom)
+            else
+              (* Update the outer borrows before diving into the child avalue *)
+              let outer_borrows = update_outer_borrows io outer (Borrow bid) in
+              V.ABorrow (super#visit_AMutBorrow outer bid av)
+        | V.ASharedBorrow bid ->
+            (* Check if this is the borrow we are looking for *)
+            if bid = l then (
+              (* Check there are outer borrows, or if we need to end the whole
+               * abstraction *)
+              raise_if_outer outer;
+              (* Register the update *)
+              set_replaced_bc (Abstract bc);
+              (* Update the value - note that we are necessarily in the second
+               * of the two cases described above *)
+              V.ABottom)
+            else V.ABorrow (super#visit_ASharedBorrow outer bid)
         | V.AIgnoredMutBorrow av ->
             (* Nothing special to do *)
             V.ABorrow (super#visit_AIgnoredMutBorrow outer av)
diff --git a/src/Values.ml b/src/Values.ml
index 44c80578..8c4c689c 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -236,7 +236,7 @@ and aloan_content =
 (** Note that when a borrow content is ended, it is replaced by Bottom (while
     we need to track ended loans more precisely, especially because of their
     children values).
-    
+
     Note that contrary to [aloan_content], here the children avalues are
     note independent of the parent avalues. For instance, a value
     `AMutBorrow (_, AMutBorrow (_, ...)` (ignoring the types) really is