Update the comments in Values and make minor modifications

7 files changed, 213 insertions, 120 deletions

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index ab3fb7ea..208918af 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -163,6 +163,8 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
         | V.AMutBorrow (bid, _) ->
             (* Check if this is the borrow we are looking for *)
             if bid = l then (
+              (* TODO: treat this case differently. We should not introduce
+                 a bottom value. *)
               (* When ending a mut borrow, there are two cases:
                * - in the general case, we have to end the whole abstraction
                *   (and thus raise an exception to signal that to the caller)
@@ -181,7 +183,8 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
                * Also note that, as we are moving the borrowed value inside the
                * abstraction (and not really giving the value back to the context)
                * we do not insert {!AEndedMutBorrow} but rather {!ABottom} *)
-              V.ABottom)
+              raise (Failure "Unimplemented")
+              (* V.ABottom *))
             else
               (* Update the outer borrows before diving into the child avalue *)
               let outer = update_outer_borrows outer (Borrow bid) in
@@ -201,7 +204,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
         | V.AIgnoredMutBorrow (_, _)
         | V.AEndedMutBorrow _
         | V.AEndedIgnoredMutBorrow
-            { given_back_loans_proj = _; child = _; given_back_meta = _ }
+            { given_back = _; child = _; given_back_meta = _ }
         | V.AEndedSharedBorrow ->
             (* Nothing special to do *)
             super#visit_ABorrow outer bc
@@ -337,7 +340,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
                    * the value... Think about a more elegant way. *)
                   let given_back_meta = as_symbolic nv.value in
                   (* The loan projector *)
-                  let given_back_loans_proj =
+                  let given_back =
                     mk_aproj_loans_value_from_symbolic_value abs.regions sv
                   in
                   (* Continue giving back in the child value *)
@@ -345,7 +348,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
                   (* Return *)
                   V.ABorrow
                     (V.AEndedIgnoredMutBorrow
-                       { given_back_loans_proj; child; given_back_meta })
+                       { given_back; child; given_back_meta })
               | _ -> raise (Failure "Unreachable")
             else
               (* Continue exploring *)
@@ -1708,8 +1711,7 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
             (* Just explore the child *)
             list_avalues false push_fail child_av
         | V.AEndedIgnoredMutBorrow
-            { child = child_av; given_back_loans_proj = _; given_back_meta = _ }
-          ->
+            { child = child_av; given_back = _; given_back_meta = _ } ->
             (* We don't support nested borrows for now *)
             assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
             (* Just explore the child *)
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 6a8fb87c..a2a1cfde 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -215,14 +215,23 @@ type merge_duplicates_funcs = {
       abs'01 { mut_borrow l0, mut_borrow l2 }
     ]}
 
+    Also, we merge all their regions together. For instance, if [abs'0] projects
+    region [r0] and [abs'1] projects region [r1], we pick one of the two, say [r0]
+    (the one with the smallest index in practice) and substitute [r1] with [r0]
+    in the whole context.
+
     Parameters:
     - [kind]
     - [can_end]
-    - [merge_funs]: in the case it can happen that a loan or a borrow appears in
-      both abstractions, we use those functions to merge the different occurrences
-      (such things can happen when joining environments: we might temporarily
-      duplicate borrows during the join, before merging those borrows together).
-      For instance, this happens for the following abstractions is forbidden:
+    - [merge_funs]: Those functions are used to merge borrows/loans with the
+      *same ids*. For instance, when performing environment joins we may introduce
+      abstractions which both contain loans/borrows with the same ids. When we
+      later merge those abstractions together, we need to call a merge function
+      to reconcile the borrows/loans. For instance, if both abstractions contain
+      the same shared loan [l0], we will call {!merge_ashared_borrows} to derive
+      a shared value for the merged shared loans.
+
+      For instance, this happens for the following abstractions:
       {[
         abs'0 { mut_borrow l0, mut_loan l1 } // mut_borrow l0 !
         abs'1 { mut_borrow l0, mut_loan l2 } // mut_borrow l0 !
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index f4116b75..e3ad26f9 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -445,7 +445,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
         | V.AIgnoredMutBorrow (_, _)
         | V.AEndedMutBorrow _
         | V.AEndedIgnoredMutBorrow
-            { given_back_loans_proj = _; child = _; given_back_meta = _ }
+            { given_back = _; child = _; given_back_meta = _ }
         | V.AEndedSharedBorrow ->
             super#visit_aborrow_content env bc
         | V.AProjSharedBorrow asb ->
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 1228ae99..6c574a94 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -145,8 +145,8 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool)
             (* Process those normally *)
             super#visit_aborrow_content abs_id bc
         | AIgnoredMutBorrow (_, child)
-        | AEndedIgnoredMutBorrow
-            { child; given_back_loans_proj = _; given_back_meta = _ } ->
+        | AEndedIgnoredMutBorrow { child; given_back = _; given_back_meta = _ }
+          ->
             (* Ignore the id of the borrow, if there is *)
             self#visit_typed_avalue abs_id child
         | AEndedMutBorrow _ | AEndedSharedBorrow ->
@@ -390,7 +390,11 @@ let rec match_types (match_distinct_types : 'r T.ty -> 'r T.ty -> 'r T.ty)
       Ref (r, ty, k)
   | _ -> match_distinct_types ty0 ty1
 
-(** See {!Match} *)
+(** See {!Match}.
+
+    This module contains specialized match functions to instantiate the generic
+    {!Match} functor.
+  *)
 module type Matcher = sig
   val match_etys : T.ety -> T.ety -> T.ety
   val match_rtys : T.rty -> T.rty -> T.rty
@@ -553,6 +557,14 @@ end
     etc.
 
     We use it for joins, to check if two environments are convertible, etc.
+
+    The functor is parameterized by a {!Matcher}, which implements the
+    non-generic part of the match. More precisely, the role of {!Match} is two
+    provide generic functions which recursively match two values (by recursively
+    matching the fields of ADT values for instance). When it does need to match
+    values in a non-trivial manner (if two ADT values don't have the same
+    variant for instance) it calls the corresponding specialized function from
+    {!Matcher}.
  *)
 module Match (M : Matcher) = struct
   (** Match two values.
@@ -750,6 +762,20 @@ module type MatchJoinState = sig
   val nabs : V.abs list ref
 end
 
+(** A matcher for loop joins (we use loop joins to compute fixed points).
+
+    See the explanations for {!Match}.
+
+    In case of loop joins:
+    - we match *concrete* values
+    - we check that the "fixed" abstractions (the abstractions to be framed
+      - i.e., the abstractions which are the same in the two environments to
+      join) are equal
+    - we keep the abstractions which are not in the frame, then merge those
+      together (if they have borrows/loans in common) later
+    The join matcher is used to match the *concrete* values only. For this
+    reason, we fail on the functions which match avalues.
+ *)
 module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
   (** Small utility *)
   let push_abs (abs : V.abs) : unit = S.nabs := abs :: !S.nabs
@@ -1011,6 +1037,9 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
         (* Return [Bottom] *)
         mk_bottom v.V.ty
 
+  (* As explained in comments: we don't use the join matcher to join avalues,
+     only concrete values *)
+
   let match_distinct_aadts _ _ _ _ _ = raise (Failure "Unreachable")
   let match_ashared_borrows _ _ _ _ = raise (Failure "Unreachable")
   let match_amut_borrows _ _ _ _ _ _ _ _ = raise (Failure "Unreachable")
@@ -1038,14 +1067,26 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets)
   end in
   let module JM = MakeJoinMatcher (S) in
   let module M = Match (JM) in
-  (* TODO: why not simply call: M.match_type_avalues? (or move this code to
-     MakeJoinMatcher?) *)
+  (* Functions to match avalues (see {!merge_duplicates_funcs}).
+
+     Those functions are used to merge borrows/loans with the *same ids*.
+
+     They will always be called on destructured avalues (whose children are
+     [AIgnored] - we enforce that through sanity checks). We rely on the join
+     matcher [JM] to match the concrete values (for shared loans for instance).
+     Note that the join matcher doesn't implement match functions for avalues
+     (see the comments in {!MakeJoinMatcher}.
+  *)
   let merge_amut_borrows id ty0 child0 _ty1 child1 =
     (* Sanity checks *)
     assert (is_aignored child0.V.value);
     assert (is_aignored child1.V.value);
 
-    (* Same remarks as for [merge_amut_loans] *)
+    (* We need to pick a type for the avalue. The types on the left and on the
+       right may use different regions: it doesn't really matter (here, we pick
+       the one from the left), because we will merge those regions together
+       anyway (see the comments for {!merge_abstractions}).
+    *)
     let ty = ty0 in
     let child = child0 in
     let value = V.ABorrow (V.AMutBorrow (id, child)) in
@@ -1057,7 +1098,7 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets)
     assert (not (ty_has_borrows ctx.type_context.type_infos ty0));
     assert (not (ty_has_borrows ctx.type_context.type_infos ty1));
 
-    (* Same remarks as for [merge_amut_loans] *)
+    (* Same remarks as for [merge_amut_borrows] *)
     let ty = ty0 in
     let value = V.ABorrow (V.ASharedBorrow id) in
     { V.value; ty }
@@ -1067,12 +1108,7 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets)
     (* Sanity checks *)
     assert (is_aignored child0.V.value);
     assert (is_aignored child1.V.value);
-    (* We simply need to introduce an [AMutLoan]. Some remarks:
-       - the child is [AIgnored]
-       - we need to pick some types. The types on the left and on the right
-         may use different regions: it doesn't really matter (here, we pick
-         the ones from the left).
-    *)
+    (* Same remarks as for [merge_amut_borrows] *)
     let ty = ty0 in
     let child = child0 in
     let value = V.ALoan (V.AMutLoan (id, child)) in
@@ -1083,9 +1119,10 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets)
     (* Sanity checks *)
     assert (is_aignored child0.V.value);
     assert (is_aignored child1.V.value);
-    (* Same remarks as for [merge_amut_loans].
+    (* Same remarks as for [merge_amut_borrows].
 
-       This time, however, we need to merge the shared values.
+       This time we need to also merge the shared values. We rely on the
+       join matcher [JM] to do so.
     *)
     assert (not (value_has_loans_or_borrows ctx sv0.V.value));
     assert (not (value_has_loans_or_borrows ctx sv1.V.value));
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 5b81cc02..27dcb330 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -561,9 +561,9 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
             | V.AIgnoredMutBorrow (_opt_bid, av), T.Mut ->
                 assert (av.V.ty = ref_ty)
             | ( V.AEndedIgnoredMutBorrow
-                  { given_back_loans_proj; child; given_back_meta = _ },
+                  { given_back; child; given_back_meta = _ },
                 T.Mut ) ->
-                assert (given_back_loans_proj.V.ty = ref_ty);
+                assert (given_back.V.ty = ref_ty);
                 assert (child.V.ty = ref_ty)
             | V.AProjSharedBorrow _, T.Shared -> ()
             | _ -> raise (Failure "Inconsistent context"))
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 393f80c2..a4a8b1d4 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -277,12 +277,11 @@ module Values = struct
         ^ ")"
     | AEndedMutBorrow (_mv, child) ->
         "@ended_mut_borrow(" ^ typed_avalue_to_string fmt child ^ ")"
-    | AEndedIgnoredMutBorrow
-        { child; given_back_loans_proj; given_back_meta = _ } ->
+    | AEndedIgnoredMutBorrow { child; given_back; given_back_meta = _ } ->
         "@ended_ignored_mut_borrow{ "
         ^ typed_avalue_to_string fmt child
         ^ "; "
-        ^ typed_avalue_to_string fmt given_back_loans_proj
+        ^ typed_avalue_to_string fmt given_back
         ^ ")"
     | AEndedSharedBorrow -> "@ended_shared_borrow"
     | AProjSharedBorrow sb ->
diff --git a/compiler/Values.ml b/compiler/Values.ml
index a57c589b..6af59087 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -175,12 +175,12 @@ and borrow_content =
       (** A reserved mut borrow.
 
           This is used to model {{: https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html} two-phase borrows}.
-          When evaluating a two-phase mutable borrow, we first introduce a reserved
-          borrow which behaves like a shared borrow, until the moment we actually *use*
-          the borrow: at this point, we end all the other shared borrows (or reserved
-          borrows - though there shouldn't be any other reserved borrows) of this value
-          and replace the reserved borrow with a mutable borrow (as well as the shared
-          loan with a mutable loan).
+          When evaluating a two-phase mutable borrow we first introduce a reserved
+          borrow which behaves like a shared borrow until the moment we actually *use*
+          the borrow: at this point, we end all the other shared borrows (and reserved
+          borrows - though there shouldn't be any other reserved borrows in practice)
+          of this value and replace the reserved borrow with a mutable borrow (as well as
+          the shared loan with a mutable loan).
           
           A simple use case of two-phase borrows:
           {[
@@ -188,22 +188,29 @@ and borrow_content =
             v.push(v.len());
           ]}
           
-          This gets desugared to (something similar to) the following MIR:
+          Without two-phase borrows, this gets desugared to (something similar to)
+          the following MIR:
           {[
             v = Vec::new();
             v1 = &mut v;
             v2 = &v; // We need this borrow, but v has already been mutably borrowed!
             l = Vec::len(move v2); // We need v2 here, and v1 *below*
-            Vec::push(move v1, move l); // In practice, v1 gets promoted only here
+            Vec::push(move v1, move l);
+          ]}
+
+          With two-phase borrows we get this:
+          {[
+            v = Vec::new();
+            v1 = &two-phase mut v; // v1 is a reserved borrow, and v is *shared*
+            v2 = &v; // v is shared, so we can (immutably) borrow through v2
+            l = Vec::len(move v2); // We use v2 here
+            Vec::push(move v1, move l); // v1 gets promoted to a mutable borrow here
           ]}
        *)
 
 and loan_content =
   | SharedLoan of loan_id_set * typed_value
   | MutLoan of loan_id
-      (** TODO: we might want to add a set of borrow ids (useful for reserved
-          borrows, and extremely useful when giving shared values to abstractions).
-       *)
 
 (** "Meta"-value: information we store for the synthesis.
 
@@ -346,9 +353,15 @@ type aproj =
   | 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
-          different abstractions, meaning that the projector of loans might
-          receive *several* (symbolic) given back values.
+          Whenever we call a function, we introduce a symbolic value for
+          the returned value. We insert projectors of loans over this
+          symbolic value in the abstractions introduced by this function
+          call: those projectors allow to insert the proper loans in the
+          various abstractions whenever symbolic borrows get expanded.
+
+          The borrows of a symbolic value may be spread between different
+          abstractions, meaning that *one* projector of loans might receive
+          *several* (symbolic) given back values.
           
           This is the case in the following example:
           {[
@@ -483,13 +496,16 @@ class ['self] map_typed_avalue_base =
 *)
 type avalue =
   | AAdt of adt_avalue
-  | ABottom
+  | ABottom (* TODO: remove once we change the way internal borrows are ended *)
   | ALoan of aloan_content
   | ABorrow of aborrow_content
   | ASymbolic of aproj
   | AIgnored
       (** A value which doesn't contain borrows, or which borrows we
-          don't own and thus ignore *)
+          don't own and thus ignore.
+
+          In the comments, we display it as [_].
+       *)
 
 and adt_avalue = {
   variant_id : (VariantId.id option[@opaque]);
@@ -498,17 +514,19 @@ and adt_avalue = {
 
 (** A loan content as stored in an abstraction.
 
+    We use the children avalues for synthesis purposes: though not necessary
+    to maintain the borrow graph, we maintain a structured representation of
+    the avalues to synthesize values for the backward functions in the translation.
+
     Note that the children avalues are independent of the parent avalues.
     For instance, the child avalue contained in an {!AMutLoan} will likely
     contain other, independent loans.
-    Keeping track of the hierarchy is not necessary to maintain the borrow graph
-    (which is the primary role of the abstractions), but it is necessary
-    to properly instantiate the backward functions when generating the pure
-    translation.
 *)
 and aloan_content =
   | AMutLoan of loan_id * typed_avalue
       (** A mutable loan owned by an abstraction.
+
+          The avalue is the child avalue.
          
           Example:
           ========
@@ -529,6 +547,8 @@ and aloan_content =
   | ASharedLoan of loan_id_set * typed_value * typed_avalue
       (** A shared loan owned by an abstraction.
 
+          The avalue is the child avalue.
+
           Example:
           ========
           {[
@@ -553,28 +573,55 @@ and aloan_content =
           we gave back to them, so that we can correctly instantiate
           backward functions.
           
+          [given_back]: stores the projected given back value (useful when
+          there are nested borrows: ending a loan might consume borrows which
+          need to be projected in the abstraction).
+
           Rk.: *DO NOT* use [visit_AEndedMutLoan]. If we update the order of
           the arguments and you forget to swap them at the level of
           [visit_AEndedMutLoan], you will not notice it.          
       
-          Example:
-          ========
+          Example 1:
+          ==========
           {[
-            abs0 { a_mut_loan l0 ⊥ }
+            abs0 { a_mut_loan l0 _ }
             x -> mut_borrow l0 (U32 3)
           ]}
           
           After ending [l0]:
           
           {[
-            abs0 { a_ended_mut_loan { given_back = U32 3; child = ⊥; }
+            abs0 { a_ended_mut_loan { child = _; given_back = _; given_back_meta = U32 3; }
+            x -> ⊥
+          ]}
+
+          Example 2 (nested borrows):
+          ===========================
+          {[
+            abs0 { a_mut_loan l0 _ }
+            ... // abstraction containing a_mut_loan l1
+            x -> mut_borrow l0 (mut_borrow l1 (U32 3))
+          ]}
+
+          After ending [l0]:
+
+          {[
+            abs0 {
+              a_ended_mut_loan {
+                child = _;
+                given_back = a_mut_borrow l1 _;
+                given_back_meta = (mut_borrow l1 (U32 3));
+              }
+            }
+            ...
             x -> ⊥
           ]}
        *)
   | AEndedSharedLoan of typed_value * typed_avalue
-      (** Similar to {!AEndedMutLoan} but in this case there are no avalues to
-          give back. We keep the shared value because it now behaves as a
-          "regular" value (which contains borrows we might want to end...).
+      (** Similar to {!AEndedMutLoan} but in this case we don't consume given
+          back values when the loan ends. We remember the shared value because
+          it now behaves as a "regular" value (which might contain borrows we need
+          to keep track of...).
        *)
   | AIgnoredMutLoan of loan_id option * typed_avalue
       (** An ignored mutable loan.
@@ -584,7 +631,7 @@ and aloan_content =
           you have a borrow of type [&'a mut &'b mut], in the abstraction 'b,
           the outer loan is ignored, however you need to keep track of it so
           that when ending the borrow corresponding to 'a you can correctly
-          project on the inner value).
+          project on the inner given back value).
 
           Note that we need to do so only for borrows consumed by parent
           abstractions, hence the optional loan id.
@@ -595,10 +642,24 @@ and aloan_content =
             fn f<'a,'b>(...) -> &'a mut &'b mut u32;
             let x = f(...);
 
-            > abs'a { a_mut_loan l0 (a_ignored_mut_loan l1 ⊥) }
-            > abs'b { a_ignored_mut_loan l0 (a_mut_loan l1 ⊥) }
+            > abs'a { a_mut_loan l0 (a_ignored_mut_loan None _) _ }
+            > abs'b { a_ignored_mut_loan (Some l0) (a_mut_loan l1 _) }
             > x -> mut_borrow l0 (mut_borrow l1 @s1)
           ]}
+
+          If we end [l0]:
+          {[
+            abs'a { ... }
+            abs'b {
+              a_ended_ignored_mut_loan {
+                child = a_mut_loan l1 _;
+                given_back = a_mut_borrow l1 _;
+                given_back_meta = mut_borrow l1 @s1
+              }
+            }
+            x -> ⊥
+          ]}
+
        *)
   | AEndedIgnoredMutLoan of {
       child : typed_avalue;
@@ -606,9 +667,10 @@ and aloan_content =
       given_back_meta : mvalue;
     }
       (** Similar to {!AEndedMutLoan}, for ignored loans.
+          See the comments for {!AIgnoredMutLoan}.
 
-           Rk.: *DO NOT* use [visit_AEndedIgnoredMutLoan].
-           See the comment for {!AEndedMutLoan}.
+          Rk.: *DO NOT* use [visit_AEndedIgnoredMutLoan] (for the reason why,
+          see the comments for {!AEndedMutLoan}).
        *)
   | AIgnoredSharedLoan of typed_avalue
       (** An ignored shared loan.
@@ -619,20 +681,17 @@ and aloan_content =
             fn f<'a,'b>(...) -> &'a &'b u32;
             let x = f(...);
 
-            > abs'a { a_shared_loan {l0} (shared_borrow l1) (a_ignored_shared_loan ⊥) }
-            > abs'b { a_ignored_shared_loan (a_shared_loan {l1} @s1 ⊥) }
+            > abs'a { a_shared_loan {l0} (shared_borrow l1) (a_ignored_shared_loan _) }
+            > abs'b { a_ignored_shared_loan (a_shared_loan {l1} @s1 _) }
             > x -> shared_borrow l0
           ]}
        *)
 
-(** Note that when a borrow content is ended, it is replaced by ⊥ (while
-    we need to track ended loans more precisely, especially because of their
-    children values).
-
-    Note that contrary to {!aloan_content}, here the children avalues are
+(** Note that contrary to {!aloan_content}, here the children avalues are
     not independent of the parent avalues. For instance, a value
     [AMutBorrow (_, AMutBorrow (_, ...)] (ignoring the types) really is
-    to be seen like a [mut_borrow ... (mut_borrow ...)].
+    to be seen like a [mut_borrow ... (mut_borrow ...)] (i.e., it is a nested
+    borrow).
     
     TODO: be more precise about the ignored borrows (keep track of the borrow
     ids)?
@@ -656,7 +715,7 @@ and aborrow_content =
 
             > x -> mut_loan l0
             > px -> ⊥
-            > abs0 { a_mut_borrow l0 (U32 0) }
+            > abs0 { a_mut_borrow l0 (U32 0) _ }
           ]}
      *)
   | ASharedBorrow of borrow_id
@@ -674,7 +733,7 @@ and aborrow_content =
 
             > x -> shared_loan {l0} (U32 0)
             > px -> ⊥
-            > abs0 { a_shared_borrow l0 }
+            > abs0 { a_shared_borrow l0 _ }
           ]}
      *)
   | AIgnoredMutBorrow of borrow_id option * typed_avalue
@@ -688,7 +747,7 @@ and aborrow_content =
           abstractions (hence the optional borrow id).
           
           Rem.: we don't have an equivalent for shared borrows because if
-          we ignore a shared borrow we don't need keep track it (we directly
+          we ignore a shared borrow we don't need to keep track it (we directly
           use {!AProjSharedBorrow} to project the shared value).
 
           TODO: the explanations below are obsolete
@@ -707,8 +766,8 @@ and aborrow_content =
             > x -> mut_loan l0
             > px -> mut_loan l1
             > ppx -> ⊥
-            > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow None (U32 0)) } // TODO: duplication
-            > abs'b {parents={abs'a}} { a_ignored_mut_borrow (Some l1) (a_mut_borrow l0 (U32 0)) }
+            > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow None _) }
+            > abs'b {parents={abs'a}} { a_ignored_mut_borrow (Some l1) (a_mut_borrow l0 _) }
 
             ... // abs'a ends
 
@@ -716,8 +775,10 @@ and aborrow_content =
             > px -> @s0
             > ppx -> ⊥
             > abs'b {
-            >   a_ended_ignored_mut_borrow (a_proj_loans (@s0 <: &'b mut u32)) // <-- loan projector
-            >                              (a_mut_borrow l0 (U32 0))
+            >   a_ended_ignored_mut_borrow {
+            >     child = a_mut_borrow l0 _;
+            >     given_back = a_proj_loans (@s0 <: &'b mut u32) // <-- loan projector
+            >   }
             > }
 
             ... // [@s0] gets expanded to [&mut l2 @s1]
@@ -726,43 +787,23 @@ and aborrow_content =
             > px -> &mut l2 @s1
             > ppx -> ⊥
             > abs'b {
-            >   a_ended_ignored_mut_borrow (a_mut_loan l2) // <-- loan l2 is here
-            >                              (a_mut_borrow l0 (U32 0))
+            >   a_ended_ignored_mut_borrow {
+            >     child = a_mut_borrow l0 _;
+            >     given_back = a_mut_loan l2 _;
+            >   }
             > }
 
           ]}
 
-          Note that we could use AIgnoredMutLoan in the case the borrow id is not
-          None, which would allow us to simplify the rules (to not have rules
+          Note that we could use [AIgnoredMutLoan] in the case the borrow id is not
+          [None], which would allow us to simplify the rules (to not have rules
           to specifically handle the case of AIgnoredMutBorrow with Some borrow
           id) and also remove the AEndedIgnoredMutBorrow variant.
-          For now, the rules are implemented and it allows us to make the avalues
-          more precise and clearer, so we will keep it that way.
-   
-          TODO: this is annoying, we are duplicating information. Maybe we
-          could introduce an "Ignored" value? We have to pay attention to
-          two things:
-          - introducing ⊥ when ignoring a value is not always possible, because
-            we check whether the borrowed value contains ⊥ when giving back a
-            borrowed value (if it is the case we give back ⊥, otherwise we
-            introduce a symbolic value). This is necessary when ending nested
-            borrows with the same lifetime: when ending the inner borrow we
-            actually give back a value, however when ending the outer borrow
-            we need to give back ⊥.
-            TODO: actually we don't do that anymore, we check if the borrowed
-            avalue contains ended regions (which is cleaner and more robust).
-          - we may need to remember the precise values given to the
-            abstraction so that we can properly call the backward functions
-            when generating the pure translation.
+          For now, we prefer to be more precise that required.
        *)
   | AEndedMutBorrow of msymbolic_value * typed_avalue
       (** The sole purpose of {!AEndedMutBorrow} is to store the (symbolic) value
           that we gave back as a meta-value, to help with the synthesis.
-
-          We also remember the child {!avalue} because this structural information
-          is useful for the synthesis (but not for the symbolic execution):
-          in practice the child value should only contain ended borrows, ignored
-          values, bottom values, etc.
        *)
   | AEndedSharedBorrow
       (** We don't really need {!AEndedSharedBorrow}: we simply want to be
@@ -770,14 +811,14 @@ and aborrow_content =
        *)
   | AEndedIgnoredMutBorrow of {
       child : typed_avalue;
-      given_back_loans_proj : typed_avalue;
+      given_back : typed_avalue;
       given_back_meta : msymbolic_value;
           (** [given_back_meta] is used to store the (symbolic) value we gave back
               upon ending the borrow.
 
               Rk.: *DO NOT* use [visit_AEndedIgnoredMutLoan].
               See the comment for {!AEndedMutLoan}.
-          *)
+           *)
     }  (** See the explanations for {!AIgnoredMutBorrow} *)
   | AProjSharedBorrow of abstract_shared_borrows
       (** A projected shared borrow.
@@ -789,8 +830,11 @@ and aborrow_content =
 
           Example:
           ========
-          Below, when calling [f], we need to introduce one shared borrow per
-          borrow in the argument.
+          Below, when calling [f], we need to introduce one shared re-borrow per
+          *inner* borrow (the borrows for 'b and 'c but not 'a) consumed by the
+          function. Those reborrows are introduced by projecting over the shared
+          value. For each one of those, we introduce an [abstract_shared_borrow]
+          in the abstraction.
           {[
             fn f<'a,'b>(pppx : &'a &'b &'c mut u32);
 
@@ -812,20 +856,22 @@ and aborrow_content =
 
           Rem.: we introduce {!AProjSharedBorrow} only when we project a shared
           borrow *which is ignored* (i.e., the shared borrow doesn't belong to
-          the current abstraction). The reason is that if the shared borrow
-          belongs to the abstraction, then by introducing a shared borrow inside
-          the abstraction we make sure the whole value is shared (and thus immutable)
-          for as long as the abstraction lives, meaning reborrowing subvalues
-          is redundant. However, if the borrow doesn't belong to the abstraction,
-          we need to project the shared values because it may contain some
-          borrows which *do* belong to the current abstraction.
+          the current abstraction, in which case we still project the shared
+          value). The reason is that if the shared borrow belongs to the
+          abstraction, then by introducing a shared borrow inside the
+          abstraction we make sure the whole value is shared (and thus
+          immutable) for as long as the abstraction lives, meaning reborrowing
+          subvalues is redundant. However, if the borrow doesn't belong to the
+          abstraction, we need to project the shared values because it may
+          contain some borrows which *do* belong to the current abstraction.
 
           TODO: maybe we should factorized [ASharedBorrow] and [AProjSharedBorrow].
        *)
 
-(* TODO: the type of avalues doesn't make sense for loan avalues: they currently
-   are typed as [& (mut) T] instead of [T]...
-*)
+(** Rem.: the of avalues is not to be understood in the same manner as for values.
+    To be more precise, shared aloans have the borrow type (i.e., a shared aloan
+    has type [& (mut) T] instead of [T]).
+ *)
 and typed_avalue = { value : avalue; ty : rty }
 [@@deriving
   show,