summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-12-17 10:13:39 +0100
committerSon Ho2021-12-17 10:13:39 +0100
commit2e784a2cd8162bdc08b7533ab73ffec9bcd52147 (patch)
tree0be3e1fb98e68c3183509c5fb8170aba38a23ac6 /src
parentaba244a99d95938e495ff513ff021c81603b28f1 (diff)
Finish implementing visit_ABorrow for end_borrow_get_borrow_in_env
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml37
-rw-r--r--src/Values.ml2
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