Make minor modifications

2 files changed, 40 insertions, 4 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index b968bfa6..fe1c1c6f 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -176,6 +176,42 @@ let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
   | None -> failwith "Unreachable"
   | Some lc -> lc
 
+(*
+TODO: use this
+(** Update a loan content in a value.
+
+    The loan is referred to by a borrow id.
+
+    This is a helper function: it might break invariants.
+ *)
+let update_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id)
+    (nlc : V.loan_content) (v : V.typed_value) : V.typed_value =
+  let obj =
+    object
+      inherit [_] V.map_typed_value as super
+
+      method! visit_MutBorrow env bid mv =
+        if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
+        else V.MutBorrow (bid, mv)
+      (** Control the diving into mutable borrows *)
+
+      method! visit_SharedLoan env bids sv =
+        if V.BorrowId.Set.mem l bids then nlc
+        else if ek.enter_shared_loans then super#visit_SharedLoan env bids sv
+        else V.SharedLoan (bids, sv)
+      (** Shared loan: checks if this is the loan we are looking for, and
+          control the dive.    
+      *)
+
+      method! visit_MutLoan env bid =
+        if bid = l then nlc else super#visit_MutLoan env bid
+      (** Mut loan: checks if this is the loan we are looking for
+      *)
+    end
+  in
+  (* We use exceptions *)
+obj#visit_typed_value () v*)
+
 (** Update a loan content in a value.
 
     The loan is referred to by a borrow id.
diff --git a/src/Values.ml b/src/Values.ml
index 72d5c948..4acce0e6 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -214,10 +214,10 @@ and typed_value =
 (** Override some undefined functions *)
 class ['self] map_typed_value =
   object (self : 'self)
-    inherit [_] map_typed_value_incomplete as super
+    inherit [_] map_typed_value_incomplete
 
     method! visit_typed_value (env : 'env) (tv : typed_value) : typed_value =
-      let value = super#visit_value env tv.value in
+      let value = self#visit_value env tv.value in
       (* Ignore the type *)
       let ty = tv.ty in
       { value; ty }
@@ -320,10 +320,10 @@ and typed_avalue = (region, aproj, aborrow_content, aloan_content) g_typed_value
 (** Override some undefined functions *)
 class ['self] map_typed_avalue =
   object (self : 'self)
-    inherit [_] map_typed_avalue_incomplete as super
+    inherit [_] map_typed_avalue_incomplete
 
     method! visit_typed_avalue (env : 'env) (tv : typed_avalue) : typed_avalue =
-      let value = super#visit_avalue env tv.value in
+      let value = self#visit_avalue env tv.value in
       (* Ignore the type *)
       let ty = tv.ty in
       { value; ty }