diff options
| -rw-r--r-- | src/Interpreter.ml | 37 | ||||
| -rw-r--r-- | src/Values.ml | 2 |
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 |