summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-12-17 13:45:38 +0100
committerSon Ho2021-12-17 13:45:38 +0100
commit238e82bf5542304fb38825b9cb15114bacaa28a6 (patch)
tree90cd7412d2a056d71ceb4dcac281554aa8e3629e /src
parent3c07db54b2763c9da72aa8105a6f188360b0b641 (diff)
Implement the avalue cases of give_back_shared
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml41
1 files changed, 34 insertions, 7 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 7d0a2ef0..0bf1825d 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -921,13 +921,40 @@ let give_back_shared config (bid : V.BorrowId.id) (env : C.env) : C.env =
method! visit_ALoan opt_abs lc =
match lc with
- | V.AMutLoan (bid, av) -> raise Unimplemented
- | V.ASharedLoan (bids, v, av) -> raise Unimplemented
- | V.AEndedMutLoan { given_back; child } -> raise Unimplemented
- | V.AEndedSharedLoan (v, av) -> raise Unimplemented
- | V.AIgnoredMutLoan (bid, av) -> raise Unimplemented
- | V.AEndedIgnoredMutLoan { given_back; child } -> raise Unimplemented
- | V.AIgnoredSharedLoan asb -> raise Unimplemented
+ | V.AMutLoan (bid, av) ->
+ (* Nothing special to do (we are giving back a *shared* borrow) *)
+ V.ALoan (super#visit_AMutLoan opt_abs bid av)
+ | V.ASharedLoan (bids, shared_value, child) ->
+ if V.BorrowId.Set.mem bid bids then (
+ (* This is the loan we are looking for *)
+ set_replaced ();
+ (* If there remains exactly one borrow identifier, we need
+ * to end the loan. Otherwise, we just remove the current
+ * loan identifier *)
+ if V.BorrowId.Set.cardinal bids = 1 then
+ V.ALoan (V.AEndedSharedLoan (shared_value, child))
+ else
+ V.ALoan
+ (V.ASharedLoan
+ (V.BorrowId.Set.remove bid bids, shared_value, child)))
+ else
+ (* Not the loan we are looking for: continue exploring *)
+ V.ALoan (super#visit_ASharedLoan opt_abs bids shared_value child)
+ | V.AEndedMutLoan { given_back; child } ->
+ (* Nothing special to do (the loan has ended) *)
+ V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child)
+ | V.AEndedSharedLoan (v, av) ->
+ (* Nothing special to do (the loan has ended) *)
+ V.ALoan (super#visit_AEndedSharedLoan opt_abs v av)
+ | V.AIgnoredMutLoan (bid, av) ->
+ (* Nothing special to do (we are giving back a *shared* borrow) *)
+ V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid av)
+ | V.AEndedIgnoredMutLoan { given_back; child } ->
+ (* Nothing special to do *)
+ V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child)
+ | V.AIgnoredSharedLoan asb ->
+ (* Nothing special to do (the loan is ignored) *)
+ V.ALoan (super#visit_AIgnoredSharedLoan opt_abs asb)
end
in