Change the definition of abstract_shared_borrows

3 files changed, 30 insertions, 24 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 708b1632..2a9db410 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -673,9 +673,8 @@ let rec apply_proj_borrows (regions : T.RegionId.set_t) (v : V.typed_value)
                 let bv = apply_proj_borrows regions bv ref_ty in
                 V.AIgnoredMutBorrow bv
             | V.SharedBorrow bid, T.Shared ->
-                (* TODO *)
+                (* TODO: we need the context to lookup the value *)
                 raise Unimplemented
-            (*              V.AIgnoredSharedBorrow bid*)
             | V.InactivatedMutBorrow _, _ ->
                 failwith
                   "Can't apply a proj_borrow over an inactivated mutable borrow"
diff --git a/src/Print.ml b/src/Print.ml
index bf07e57e..6b4c3c4f 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -297,16 +297,18 @@ module Values = struct
         "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ")"
     | MutLoan bid -> "⌊mut@" ^ V.BorrowId.to_string bid ^ "⌋"
 
-  let rec abstract_shared_borrows_to_string (fmt : value_formatter)
-      (abs : V.abstract_shared_borrows) : string =
+  let rec abstract_shared_borrow_to_string (fmt : value_formatter)
+      (abs : V.abstract_shared_borrow) : string =
     match abs with
-    | AsbSet bs -> V.BorrowId.set_to_string bs
+    | AsbBorrow bid -> V.BorrowId.to_string bid
     | AsbProjReborrows (sv, rty) ->
         "{" ^ symbolic_value_proj_to_string fmt sv rty ^ "}"
-    | AsbUnion (asb1, asb2) ->
-        abstract_shared_borrows_to_string fmt asb1
-        ^ " U "
-        ^ abstract_shared_borrows_to_string fmt asb2
+
+  let rec abstract_shared_borrows_to_string (fmt : value_formatter)
+      (abs : V.abstract_shared_borrows) : string =
+    "{"
+    ^ String.concat "," (List.map (abstract_shared_borrow_to_string fmt) abs)
+    ^ "}"
 
   let aproj_to_string (fmt : value_formatter) (pv : V.aproj) : string =
     match pv with
diff --git a/src/Values.ml b/src/Values.ml
index 96feb814..1a61f296 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -149,13 +149,25 @@ and typed_value = { value : value; ty : ety }
       }]
 (** "Regular" typed value (we map variables to typed values) *)
 
-type abstract_shared_borrows =
-  | AsbSet of BorrowId.set_t
-  | AsbProjReborrows of symbolic_value * rty
-  | AsbUnion of abstract_shared_borrows * abstract_shared_borrows
-      (** TODO: explanations *)
+(** When giving shared borrows to functions (i.e., inserting shared borrows inside
+    abstractions) we need to reborrow the shared values. When doing so, we lookup
+    the shared values and apply some special projections to the shared value
+    (until we can't go further, i.e., we find symbolic values which may get
+    expanded upon reading them later), which don't generate avalues but
+    sets of borrow ids and symbolic values.
+    
+    Note that as shared values can't get modified it is ok to forget the
+    structure of the values we projected, and only keep the set of borrows
+    (and symbolic values).
+*)
+type abstract_shared_borrow =
+  | AsbBorrow of (BorrowId.id[@opaque])
+  | AsbProjReborrows of (symbolic_value[@opaque]) * (rty[@opaque])
 [@@deriving show]
 
+type abstract_shared_borrows = abstract_shared_borrow list
+(** A set of abstract shared borrows *)
+
 type aproj =
   | AProjLoans of symbolic_value
   | AProjBorrows of symbolic_value * rty
@@ -172,10 +184,6 @@ class ['self] iter_typed_avalue_base =
 
     method visit_aproj : 'env -> aproj -> unit = fun _ _ -> ()
 
-    method visit_abstract_shared_borrows
-        : 'env -> abstract_shared_borrows -> unit =
-      fun _ _ -> ()
-
     method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
   end
 
@@ -188,10 +196,6 @@ class ['self] map_typed_avalue_base =
 
     method visit_aproj : 'env -> aproj -> aproj = fun _ p -> p
 
-    method visit_abstract_shared_borrows
-        : 'env -> abstract_shared_borrows -> abstract_shared_borrows =
-      fun _ asb -> asb
-
     method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
   end
 
@@ -247,7 +251,8 @@ and aloan_content =
   | AEndedSharedLoan of typed_value * typed_avalue
   | AIgnoredMutLoan of (BorrowId.id[@opaque]) * typed_avalue
   | AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue }
-  | AIgnoredSharedLoan of abstract_shared_borrows
+  | AIgnoredSharedLoan of (abstract_shared_borrows[@opaque])
+      (** TODO: remove this one? *)
 
 (** 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
@@ -265,7 +270,7 @@ and aborrow_content =
   | AMutBorrow of (BorrowId.id[@opaque]) * typed_avalue
   | ASharedBorrow of (BorrowId.id[@opaque])
   | AIgnoredMutBorrow of typed_avalue
-  | AIgnoredSharedBorrow of abstract_shared_borrows
+  | AIgnoredSharedBorrow of (abstract_shared_borrows[@opaque])
 
 (* TODO: we may want to merge this with typed_value - would prevent some issues
    when accessing fields... *)