From 0cee9e0dbbb804350722f8fb87be5a128d1a8a54 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 8 Dec 2021 14:58:50 +0100
Subject: Cleanup a bit

---
 src/Interpreter.ml | 90 ------------------------------------------------------
 1 file changed, 90 deletions(-)

(limited to 'src')

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 2b6193a4..ca011bf0 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1481,96 +1481,6 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
         ctx
       with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p ctx)
 
-(* (* Explore the value to check if we need to update the environment.
-
-            Note that we can end the borrows which are inside the value (while the
-            value itself might be inside a borrow/loan: we are thus ending inner
-            borrows). Because a loan inside the value may be linked to a borrow
-            somewhere else *also inside* the value (it's possible with adts),
-            we first end all the borrows we find - by using [Inner] to allow
-            ending inner borrows - then end all the loans we find. It is really
-            important to do this in two steps: the borrow linked to a loan may
-            be inside the value at place p, in which case this borrow may be
-            an inner borrow that we *can* end, but it may also be outside this
-            value, in which case we need to end all the outer borrows first...
-            Also, whenever the environment is updated, we need to re-inspect
-            the value at place p *in two steps* again (end borrows, then end loans).
-
-            We use exceptions to make it handy.
-         *)
-         let rec inspect_update (end_loans : bool) (v : V.typed_value) : unit =
-           match v.V.value with
-           | V.Concrete _ -> ()
-           | V.Bottom ->
-               (* Note that we are going to *write* to the value: it is ok if this
-                  value contains [Bottom] - and actually we introduce some
-                  occurrences of [Bottom] by ending borrows *)
-               ()
-           | V.Symbolic _ ->
-               (* Nothing to do for symbolic values - TODO: not sure *)
-               raise Unimplemented
-           | V.Adt adt -> List.iter (inspect_update end_loans) adt.field_values
-           | V.Borrow bc -> (
-               assert (not end_loans);
-
-               (* Sanity check *)
-               (* We need to end all borrows. Note that we ignore the outer borrows
-                  when ending the borrows we find here (we call [end_inner_borrow(s)]:
-                  the value at place p might be below a borrow/loan. Note however
-                  that the borrow we found here is an outer borrow, if we restrain
-                  ourselves at the value at place p.
-               *)
-               match bc with
-               | V.SharedBorrow bid | V.MutBorrow (bid, _) ->
-                   L.log#ldebug
-                     (lazy
-                       ("drop_borrows_loans_at_lplace: dropping "
-                      ^ V.BorrowId.to_string bid));
-                   raise (UpdateCtx (end_inner_borrow config bid ctx))
-               | V.InactivatedMutBorrow bid ->
-                   L.log#ldebug
-                     (lazy
-                       ("drop_borrows_loans_at_lplace: activating "
-                      ^ V.BorrowId.to_string bid));
-                   (* We need to activate ithe nactivated borrow - later, we will
-                    * actually end it *)
-                   let ctx =
-                     activate_inactivated_mut_borrow config Inner bid ctx
-                   in
-                   raise (UpdateCtx ctx))
-           | V.Loan lc ->
-               if
-                 (* If we can, end the loans, otherwise ignore: keep for later *)
-                 end_loans
-               then
-                 (* We need to end all loans. Note that as all the borrows inside
-                    the value at place p should already have ended, the borrows
-                    associated to the loans we find here should be borrows from
-                    outside this value: we need to call [end_outer_borrow(s)]
-                    (we can't ignore outer borrows this time).
-                 *)
-                 match lc with
-                 | V.SharedLoan (bids, _) ->
-                     raise (UpdateCtx (end_outer_borrows config bids ctx))
-                 | V.MutLoan bid ->
-                     raise (UpdateCtx (end_outer_borrow config bid ctx))
-               else ()
-         in
-         (* Inspect the value and update the context while doing so.
-            If the context gets updated: perform a recursive call (many things
-            may have been updated in the context: first we need to retrieve the
-            proper updated value - and this value may actually not be accessible
-            anymore
-         *)
-         try
-           (* Inspect the value: end the borrows only *)
-           inspect_update false v;
-           (* Inspect the value: end the loans *)
-           inspect_update true v;
-           (* No context update required: return the current context *)
-           ctx
-   with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p ctx)*)
-
 (** Copy a value, and return the resulting value.
 
     Note that copying values might update the context. For instance, when
-- 
cgit v1.2.3