Start adding markers

6 files changed, 94 insertions, 50 deletions

diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 2628b26a..3bef7b30 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -255,13 +255,17 @@ let lookup_loan_opt (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
           (because there are no use cases requiring finer control) *)
       method! visit_aloan_content env lc =
         match lc with
-        | AMutLoan (bid, av) ->
+        | AMutLoan (pm, bid, av) ->
+            (* Sanity check: markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then raise (FoundGLoanContent (Abstract lc))
-            else super#visit_AMutLoan env bid av
-        | ASharedLoan (bids, v, av) ->
+            else super#visit_AMutLoan env pm bid av
+        | ASharedLoan (pm, bids, v, av) ->
+            (* Sanity check: markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if BorrowId.Set.mem l bids then
               raise (FoundGLoanContent (Abstract lc))
-            else super#visit_ASharedLoan env bids v av
+            else super#visit_ASharedLoan env pm bids v av
         | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan (_, _)
         | AIgnoredMutLoan (_, _)
@@ -396,11 +400,15 @@ let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
 
       method! visit_aloan_content env lc =
         match lc with
-        | AMutLoan (bid, av) ->
-            if bid = l then update () else super#visit_AMutLoan env bid av
-        | ASharedLoan (bids, v, av) ->
+        | AMutLoan (pm, bid, av) ->
+            (* Sanity check: markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
+            if bid = l then update () else super#visit_AMutLoan env pm bid av
+        | ASharedLoan (pm, bids, v, av) ->
+            (* Sanity check: markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if BorrowId.Set.mem l bids then update ()
-            else super#visit_ASharedLoan env bids v av
+            else super#visit_ASharedLoan env pm bids v av
         | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan (_, _)
         | AIgnoredMutLoan (_, _)
@@ -422,8 +430,8 @@ let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
   ctx
 
 (** Lookup a borrow content from a borrow id. *)
-let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx)
-    : g_borrow_content option =
+let lookup_borrow_opt (span : Meta.span) (ek : exploration_kind)
+    (l : BorrowId.id) (ctx : eval_ctx) : g_borrow_content option =
   let obj =
     object
       inherit [_] iter_eval_ctx as super
@@ -453,12 +461,16 @@ let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx)
 
       method! visit_aborrow_content env bc =
         match bc with
-        | AMutBorrow (bid, av) ->
+        | AMutBorrow (pm, bid, av) ->
+            (* Sanity check: markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then raise (FoundGBorrowContent (Abstract bc))
-            else super#visit_AMutBorrow env bid av
-        | ASharedBorrow bid ->
+            else super#visit_AMutBorrow env pm bid av
+        | ASharedBorrow (pm, bid) ->
+            (* Sanity check: markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then raise (FoundGBorrowContent (Abstract bc))
-            else super#visit_ASharedBorrow env bid
+            else super#visit_ASharedBorrow env pm bid
         | AIgnoredMutBorrow (_, _)
         | AEndedMutBorrow _
         | AEndedIgnoredMutBorrow
@@ -486,7 +498,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx)
 *)
 let lookup_borrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
     (ctx : eval_ctx) : g_borrow_content =
-  match lookup_borrow_opt ek l ctx with
+  match lookup_borrow_opt span ek l ctx with
   | None -> craise __FILE__ __LINE__ span "Unreachable"
   | Some lc -> lc
 
@@ -571,12 +583,16 @@ let update_aborrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
 
       method! visit_ABorrow env bc =
         match bc with
-        | AMutBorrow (bid, av) ->
+        | AMutBorrow (pm, bid, av) ->
+            (* Sanity check: markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then update ()
-            else ABorrow (super#visit_AMutBorrow env bid av)
-        | ASharedBorrow bid ->
+            else ABorrow (super#visit_AMutBorrow env pm bid av)
+        | ASharedBorrow (pm, bid) ->
+            (* Sanity check: markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then update ()
-            else ABorrow (super#visit_ASharedBorrow env bid)
+            else ABorrow (super#visit_ASharedBorrow env pm bid)
         | AIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedSharedBorrow
         | AEndedIgnoredMutBorrow _ ->
             super#visit_ABorrow env bc
@@ -1182,8 +1198,14 @@ let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) :
 
       method! visit_aloan_content env lc =
         match lc with
-        | AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid))
-        | ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids))
+        | AMutLoan (pm, bid, _) ->
+            (* Sanity check: markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
+            raise (FoundBorrowIds (Borrow bid))
+        | ASharedLoan (pm, bids, _, _) ->
+            (* Sanity check: markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
+            raise (FoundBorrowIds (Borrows bids))
         | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan (_, _) ->
             super#visit_aloan_content env lc
@@ -1232,7 +1254,7 @@ let lookup_shared_value_opt (span : Meta.span) (ctx : eval_ctx)
   | None -> None
   | Some (_, lc) -> (
       match lc with
-      | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) ->
+      | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, _, sv, _)) ->
           Some sv
       | _ -> None)
 
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index faba1088..a74017d1 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -187,7 +187,7 @@ let rec access_projection (span : Meta.span) (access : projection_access)
                         Ok (ctx, { res with updated = v }))
                 | ( _,
                     Abstract
-                      ( AMutLoan (_, _)
+                      ( AMutLoan (_, _, _)
                       | AEndedMutLoan
                           { given_back = _; child = _; given_back_span = _ }
                       | AEndedSharedLoan (_, _)
@@ -197,7 +197,9 @@ let rec access_projection (span : Meta.span) (access : projection_access)
                       | AIgnoredSharedLoan _ ) ) ->
                     craise __FILE__ __LINE__ span
                       "Expected a shared (abstraction) loan"
-                | _, Abstract (ASharedLoan (bids, sv, _av)) -> (
+                | _, Abstract (ASharedLoan (pm, bids, sv, _av)) -> (
+                    (* Sanity check: markers can only appear when we're doing a join *)
+                    sanity_check __FILE__ __LINE__ (pm = PNone) span;
                     (* Explore the shared value *)
                     match access_projection span access ctx update p' sv with
                     | Error err -> Error err
@@ -205,14 +207,14 @@ let rec access_projection (span : Meta.span) (access : projection_access)
                         (* Relookup the child avalue *)
                         let av =
                           match lookup_loan span ek bid ctx with
-                          | _, Abstract (ASharedLoan (_, _, av)) -> av
+                          | _, Abstract (ASharedLoan (_, _, _, av)) -> av
                           | _ -> craise __FILE__ __LINE__ span "Unexpected"
                         in
                         (* Update the shared loan with the new value returned
                              by {!access_projection} *)
                         let ctx =
                           update_aloan span ek bid
-                            (ASharedLoan (bids, res.updated, av))
+                            (ASharedLoan (pm, bids, res.updated, av))
                             ctx
                         in
                         (* Return - note that we don't need to update the borrow itself *)
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index a887c44c..0e820982 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -61,7 +61,7 @@ let rec apply_proj_borrows_on_shared_borrow (span : Meta.span) (ctx : eval_ctx)
               let asb =
                 match sv with
                 | _, Concrete (VSharedLoan (_, sv))
-                | _, Abstract (ASharedLoan (_, sv, _)) ->
+                | _, Abstract (ASharedLoan (_, _, sv, _)) ->
                     apply_proj_borrows_on_shared_borrow span ctx fresh_reborrow
                       regions sv ref_ty
                 | _ -> craise __FILE__ __LINE__ span "Unexpected"
@@ -137,7 +137,7 @@ let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool)
                     apply_proj_borrows span check_symbolic_no_ended ctx
                       fresh_reborrow regions ancestors_regions bv ref_ty
                   in
-                  AMutBorrow (bid, bv)
+                  AMutBorrow (PNone, bid, bv)
               | VSharedBorrow bid, RShared ->
                   (* Rem.: we don't need to also apply the projection on the
                      borrowed value, because for as long as the abstraction
@@ -150,7 +150,7 @@ let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool)
                      need to lookup the shared value and project it (see the
                      other branch of the [if then else]).
                   *)
-                  ASharedBorrow bid
+                  ASharedBorrow (PNone, bid)
               | VReservedMutBorrow _, _ ->
                   craise __FILE__ __LINE__ span
                     "Can't apply a proj_borrow over a reserved mutable borrow"
@@ -183,7 +183,7 @@ let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool)
                   let asb =
                     match sv with
                     | _, Concrete (VSharedLoan (_, sv))
-                    | _, Abstract (ASharedLoan (_, sv, _)) ->
+                    | _, Abstract (ASharedLoan (_, _, sv, _)) ->
                         apply_proj_borrows_on_shared_borrow span ctx
                           fresh_reborrow regions sv ref_ty
                     | _ -> craise __FILE__ __LINE__ span "Unexpected"
@@ -288,7 +288,7 @@ let apply_proj_loans_on_symbolic_expansion (span : Meta.span)
          * we never project over static regions) *)
         if region_in_set r regions then
           (* In the set: keep *)
-          (ALoan (AMutLoan (bid, child_av)), ref_ty)
+          (ALoan (AMutLoan (PNone, bid, child_av)), ref_ty)
         else
           (* Not in the set: ignore *)
           (* If the borrow id is in the ancestor's regions, we still need
@@ -307,7 +307,7 @@ let apply_proj_loans_on_symbolic_expansion (span : Meta.span)
         if region_in_set r regions then
           (* In the set: keep *)
           let shared_value = mk_typed_value_from_symbolic_value spc in
-          (ALoan (ASharedLoan (bids, shared_value, child_av)), ref_ty)
+          (ALoan (ASharedLoan (PNone, bids, shared_value, child_av)), ref_ty)
         else
           (* Not in the set: ignore *)
           (ALoan (AIgnoredSharedLoan child_av), ref_ty)
@@ -441,7 +441,7 @@ let apply_reborrows (span : Meta.span)
 
       method! visit_aloan_content env lc =
         match lc with
-        | ASharedLoan (bids, sv, av) ->
+        | ASharedLoan (pm, bids, sv, av) ->
             (* Insert the reborrows *)
             let bids = insert_reborrows bids in
             (* Similarly to the non-abstraction case: check if the shared
@@ -453,9 +453,9 @@ let apply_reborrows (span : Meta.span)
               | Some bid -> insert_reborrows_for_bid bids bid
             in
             (* Update and explore *)
-            super#visit_ASharedLoan env bids sv av
+            super#visit_ASharedLoan env pm bids sv av
         | AIgnoredSharedLoan _
-        | AMutLoan (_, _)
+        | AMutLoan (_, _, _)
         | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan (_, _)
         | AIgnoredMutLoan (_, _)
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 51be02c8..bcf92b25 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -246,8 +246,8 @@ let check_loans_borrows_relation_invariant (span : Meta.span) (ctx : eval_ctx) :
       method! visit_aborrow_content env bc =
         let _ =
           match bc with
-          | AMutBorrow (bid, _) -> register_borrow BMut bid
-          | ASharedBorrow bid -> register_borrow BShared bid
+          | AMutBorrow (_, bid, _) -> register_borrow BMut bid
+          | ASharedBorrow (_, bid) -> register_borrow BShared bid
           | AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow RMut bid
           | AIgnoredMutBorrow (None, _)
           | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow
@@ -341,8 +341,8 @@ let check_borrowed_values_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
         (* Update the info *)
         let info =
           match lc with
-          | AMutLoan (_, _) -> set_outer_mut info
-          | ASharedLoan (_, _, _) -> set_outer_shared info
+          | AMutLoan (_, _, _) -> set_outer_mut info
+          | ASharedLoan (_, _, _, _) -> set_outer_shared info
           | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } ->
               set_outer_mut info
           | AEndedSharedLoan (_, _) -> set_outer_shared info
@@ -359,7 +359,7 @@ let check_borrowed_values_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
         (* Update the info *)
         let info =
           match bc with
-          | AMutBorrow (_, _) -> set_outer_mut info
+          | AMutBorrow (_, _, _) -> set_outer_mut info
           | ASharedBorrow _ | AEndedSharedBorrow -> set_outer_shared info
           | AIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _
             ->
@@ -500,9 +500,11 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
                 (* Lookup the borrowed value to check it has the proper type *)
                 let _, glc = lookup_loan span ek_all bid ctx in
                 match glc with
-                | Concrete (VSharedLoan (_, sv))
-                | Abstract (ASharedLoan (_, sv, _)) ->
+                | Concrete (VSharedLoan (_, sv)) ->
                     sanity_check __FILE__ __LINE__ (sv.ty = ref_ty) span
+                | Abstract (ASharedLoan (pm, _, sv, _)) ->
+                    sanity_check __FILE__ __LINE__ (sv.ty = ref_ty) span;
+                    sanity_check __FILE__ __LINE__ (pm = PNone) span
                 | _ -> craise __FILE__ __LINE__ span "Inconsistent context")
             | VMutBorrow (_, bv), RMut ->
                 sanity_check __FILE__ __LINE__
diff --git a/compiler/Print.ml b/compiler/Print.ml
index f7f1f54b..12506274 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -148,6 +148,12 @@ module Values = struct
     | AEndedProjBorrows _mv -> "_"
     | AIgnoredProjBorrows -> "_"
 
+  let add_proj_marker (pm : proj_marker) (s : string) : string =
+    match pm with
+    | PNone -> s
+    | PLeft -> "|" ^ s ^ "|"
+    | PRight -> "┊" ^ s ^ "┊"
+
   let rec typed_avalue_to_string ?(span : Meta.span option = None)
       (env : fmt_env) (v : typed_avalue) : string =
     match v.value with
@@ -197,17 +203,19 @@ module Values = struct
   and aloan_content_to_string ?(span : Meta.span option = None) (env : fmt_env)
       (lc : aloan_content) : string =
     match lc with
-    | AMutLoan (bid, av) ->
+    | AMutLoan (pm, bid, av) ->
         "@mut_loan(" ^ BorrowId.to_string bid ^ ", "
         ^ typed_avalue_to_string ~span env av
         ^ ")"
-    | ASharedLoan (loans, v, av) ->
+        |> add_proj_marker pm
+    | ASharedLoan (pm, loans, v, av) ->
         let loans = BorrowId.Set.to_string None loans in
         "@shared_loan(" ^ loans ^ ", "
         ^ typed_value_to_string ~span env v
         ^ ", "
         ^ typed_avalue_to_string ~span env av
         ^ ")"
+        |> add_proj_marker pm
     | AEndedMutLoan ml ->
         "@ended_mut_loan{"
         ^ typed_avalue_to_string ~span env ml.child
@@ -238,11 +246,13 @@ module Values = struct
   and aborrow_content_to_string ?(span : Meta.span option = None)
       (env : fmt_env) (bc : aborrow_content) : string =
     match bc with
-    | AMutBorrow (bid, av) ->
+    | AMutBorrow (pm, bid, av) ->
         "mb@" ^ BorrowId.to_string bid ^ " ("
         ^ typed_avalue_to_string ~span env av
         ^ ")"
-    | ASharedBorrow bid -> "sb@" ^ BorrowId.to_string bid
+        |> add_proj_marker pm
+    | ASharedBorrow (pm, bid) ->
+        "sb@" ^ BorrowId.to_string bid |> add_proj_marker pm
     | AIgnoredMutBorrow (opt_bid, av) ->
         "@ignored_mut_borrow("
         ^ option_to_string BorrowId.to_string opt_bid
diff --git a/compiler/Values.ml b/compiler/Values.ml
index e7b96051..96d61f88 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -176,6 +176,10 @@ type region_id_set = RegionId.Set.t [@@deriving show, ord]
 type abstraction_id = AbstractionId.id [@@deriving show, ord]
 type abstraction_id_set = AbstractionId.Set.t [@@deriving show, ord]
 
+(** Projection markers: those are used in the joins.
+    For additional explanations see: https://arxiv.org/pdf/2404.02680#section.5 *)
+type proj_marker = PNone | PLeft | PRight [@@deriving show, ord]
+
 (** Ancestor for {!typed_avalue} iter visitor *)
 class ['self] iter_typed_avalue_base =
   object (self : 'self)
@@ -192,6 +196,8 @@ class ['self] iter_typed_avalue_base =
 
     method visit_abstraction_id_set : 'env -> abstraction_id_set -> unit =
       fun env ids -> AbstractionId.Set.iter (self#visit_abstraction_id env) ids
+
+    method visit_proj_marker : 'env -> proj_marker -> unit = fun _ _ -> ()
   end
 
 (** Ancestor for {!typed_avalue} map visitor *)
@@ -212,6 +218,8 @@ class ['self] map_typed_avalue_base =
     method visit_abstraction_id_set
         : 'env -> abstraction_id_set -> abstraction_id_set =
       fun env ids -> AbstractionId.Set.map (self#visit_abstraction_id env) ids
+
+    method visit_proj_marker : 'env -> proj_marker -> proj_marker = fun _ x -> x
   end
 
 (** When giving shared borrows to functions (i.e., inserting shared borrows inside
@@ -333,7 +341,7 @@ and adt_avalue = {
     contain other, independent loans.
 *)
 and aloan_content =
-  | AMutLoan of loan_id * typed_avalue
+  | AMutLoan of proj_marker * loan_id * typed_avalue
       (** A mutable loan owned by an abstraction.
 
           The avalue is the child avalue.
@@ -354,7 +362,7 @@ and aloan_content =
             px -> mut_borrow l0 (mut_borrow @s1)
           ]}
        *)
-  | ASharedLoan of loan_id_set * typed_value * typed_avalue
+  | ASharedLoan of proj_marker * loan_id_set * typed_value * typed_avalue
       (** A shared loan owned by an abstraction.
 
           The avalue is the child avalue.
@@ -507,7 +515,7 @@ and aloan_content =
     ids)?
 *)
 and aborrow_content =
-  | AMutBorrow of borrow_id * typed_avalue
+  | AMutBorrow of proj_marker * borrow_id * typed_avalue
       (** A mutable borrow owned by an abstraction.
       
           Is used when an abstraction "consumes" borrows, when giving borrows
@@ -528,7 +536,7 @@ and aborrow_content =
             > abs0 { a_mut_borrow l0 (U32 0) _ }
           ]}
      *)
-  | ASharedBorrow of borrow_id
+  | ASharedBorrow of proj_marker * borrow_id
       (** A shared borrow owned by an abstraction.
     
           Example: