Implement the visit_ALoan case for end_borrow_get_borrow_in_env

2 files changed, 56 insertions, 3 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 4b2a303c..baf433c2 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -663,9 +663,48 @@ let end_borrow_get_borrow_in_env (io : inner_outer)
               let outer_borrows = update_outer_borrows io outer (Borrow l') in
               V.Borrow (super#visit_MutBorrow outer l' bv)
 
-      method! visit_ALoan outer bc = raise Unimplemented
+      method! visit_ALoan outer lc =
+        (* Note that the children avalues are just other, independent loans,
+         * so we don't need to update the outer borrows when diving in.
+         * We keep track of the parents/children relationship only because we
+         * need it to properly instantiate the backward functions when generating
+         * the pure translation. *)
+        match lc with
+        | V.AMutLoan (bid, av) ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AMutLoan outer bid av)
+        | V.ASharedLoan (bids, v, av) ->
+            (* Explore the shared value - we need to update the outer borrows *)
+            let souter = update_outer_borrows io outer (Borrows bids) in
+            let v = super#visit_typed_value souter v in
+            (* Explore the child avalue - we keep the same outer borrows *)
+            let av = super#visit_typed_avalue outer av in
+            (* Reconstruct *)
+            V.ALoan (V.ASharedLoan (bids, v, av))
+        | V.AEndedMutLoan { given_back; child } ->
+            (* The loan has ended, so no need to update the outer borrows *)
+            V.ALoan (super#visit_AEndedMutLoan outer given_back child)
+        | V.AEndedSharedLoan (v, av) ->
+            (* The loan has ended, so no need to update the outer borrows *)
+            V.ALoan (super#visit_AEndedSharedLoan outer v av)
+        | V.AIgnoredMutLoan (bid, av) ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AIgnoredMutLoan outer bid av)
+        | V.AEndedIgnoredMutLoan { given_back; child } ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AEndedIgnoredMutLoan outer given_back child)
+        | V.AIgnoredSharedLoan asb ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AIgnoredSharedLoan outer asb)
+      (** We reimplement [visit_ALoan] because we may have to update the
+          outer borrows *)
 
-      method! visit_ABorrow outer bc = raise Unimplemented
+      method! visit_ABorrow outer bc =
+        match bc with
+        | V.AMutBorrow (bid, av) -> raise Unimplemented
+        | V.ASharedBorrow bid -> raise Unimplemented
+        | V.AIgnoredMutBorrow av -> raise Unimplemented
+        | V.AIgnoredSharedBorrow asb -> raise Unimplemented
 
       method! visit_abs outer abs =
         (* Update the outer abs *)
diff --git a/src/Values.ml b/src/Values.ml
index f2f2274d..44c80578 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -216,6 +216,14 @@ and adt_avalue = {
   field_values : typed_avalue list;
 }
 
+(** A loan content as stored in an abstraction.
+
+    Note that the children avalues are independent of the parent avalues.
+    For instance, the child avalue contained in an [AMutLoan] will likely
+    contain other, independent loans. We keep track of the hierarchy because
+    we need it to properly instantiate the backward functions when generating
+    the pure translation.
+*)
 and aloan_content =
   | AMutLoan of (BorrowId.id[@opaque]) * typed_avalue
   | ASharedLoan of (BorrowId.set_t[@opaque]) * typed_value * typed_avalue
@@ -227,7 +235,13 @@ 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) *)
+    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
+    to be seen like a `mut_borrow ... (mut_borrow ...)`.
+*)
 and aborrow_content =
   | AMutBorrow of (BorrowId.id[@opaque]) * typed_avalue
   | ASharedBorrow of (BorrowId.id[@opaque])