Use msymbolic_value instead of mvalue in some places in Values.aproj

4 files changed, 8 insertions, 12 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index ccd41747..bc5341c5 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -432,7 +432,7 @@ let give_back_symbolic_value (_config : C.config)
   | V.SynthInputGivenBack | V.SynthRetGivenBack | V.FunCallGivenBack -> ()
   | V.FunCallRet | V.SynthInput -> failwith "Unrechable");
   (* Store the given-back value as a meta-value for synthesis purposes *)
-  let mv = mk_typed_value_from_symbolic_value nsv in
+  let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
   let subst (_abs : V.abs) local_given_back =
     (* Compute the projection over the given back value *)
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 57e47df0..81f9d0d3 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -901,7 +901,7 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t)
  *)
 let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
     (proj_ty : T.rty) (sv : V.symbolic_value)
-    (subst : V.abs -> (V.typed_value * V.aproj) list -> V.aproj)
+    (subst : V.abs -> (V.msymbolic_value * V.aproj) list -> V.aproj)
     (ctx : C.eval_ctx) : C.eval_ctx =
   (* Small helpers for sanity checks *)
   let updated = ref false in
@@ -952,7 +952,7 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
     to the couple (abstraction id, symbolic value).
  *)
 let lookup_aproj_loans (abs_id : V.AbstractionId.id) (sv : V.symbolic_value)
-    (ctx : C.eval_ctx) : (V.mvalue * V.aproj) list =
+    (ctx : C.eval_ctx) : (V.msymbolic_value * V.aproj) list =
   (* Small helpers for sanity checks *)
   let found = ref None in
   let set_found x =
diff --git a/src/SymbolicAstUtils.ml b/src/SymbolicAstUtils.ml
index 264f9cad..5a329c8d 100644
--- a/src/SymbolicAstUtils.ml
+++ b/src/SymbolicAstUtils.ml
@@ -9,9 +9,9 @@ open InterpreterUtils
 
 type ('c, 's) ended = EndedConcrete of 'c | EndedSymbolic of 's
 
-type ended_loan = (V.mvalue, V.mvalue list) ended
+type ended_loan = (V.typed_value, V.msymbolic_value list) ended
 
-type ended_borrow = (V.mvalue, V.mvalue) ended
+type ended_borrow = (V.typed_value, V.typed_value) ended
 
 type ended_loan_or_borrow =
   | EndedLoan of ended_loan
@@ -45,7 +45,7 @@ let get_top_owned_ended_loans_borrows (abs : V.abs) : ended_loan_or_borrow list
         match aproj with
         | AEndedProjLoans (msv, []) ->
             (* The symbolic value was left unchanged *)
-            add_sloan [ mk_typed_value_from_symbolic_value msv ]
+            add_sloan [ msv ]
         | AEndedProjLoans (_, mvl) -> add_sloan (List.map fst mvl)
         | AEndedProjBorrows mv -> add_sborrow mv
         | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
diff --git a/src/Values.ml b/src/Values.ml
index fe8daf30..6ab81f6b 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -252,7 +252,7 @@ class ['self] map_aproj_base =
   end
 
 type aproj =
-  | AProjLoans of symbolic_value * (mvalue * aproj) list
+  | AProjLoans of symbolic_value * (msymbolic_value * aproj) list
       (** A projector of loans over a symbolic value.
       
           Note that the borrows of a symbolic value may be spread between
@@ -285,8 +285,6 @@ type aproj =
           We can later end the projector of loans if `s@0` is not referenced
           anywhere in the context below a projector of borrows which intersects
           this projector of loans.
-          
-          TODO: we should use an msymbolic_value, not an mvalue
        *)
   | AProjBorrows of symbolic_value * rty
       (** Note that an AProjBorrows only operates on a value which is not below
@@ -296,14 +294,12 @@ type aproj =
           can't get updated/expanded: this means that we don't need to save
           any meta-value here.
        *)
-  | AEndedProjLoans of msymbolic_value * (mvalue * aproj) list
+  | AEndedProjLoans of msymbolic_value * (msymbolic_value * aproj) list
       (** An ended projector of loans over a symbolic value.
       
           See the explanations for [AProjLoans]
           
           Note that we keep the original symbolic value as a meta-value.
-
-          TODO: we should use an msymbolic_value, not an mvalue
        *)
   | AEndedProjBorrows of mvalue
       (** The only purpose of [AEndedProjBorrows] is to store, for synthesis