summaryrefslogtreecommitdiff
path: root/src/Interpreter.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/Interpreter.ml')
-rw-r--r--src/Interpreter.ml43
1 files changed, 41 insertions, 2 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 *)