summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterBorrows.ml30
-rw-r--r--compiler/InterpreterExpansion.ml4
-rw-r--r--compiler/InterpreterLoops.ml193
-rw-r--r--compiler/InterpreterProjectors.ml31
-rw-r--r--compiler/InterpreterProjectors.mli12
-rw-r--r--compiler/Invariants.ml8
-rw-r--r--compiler/Print.ml6
-rw-r--r--compiler/Values.ml29
8 files changed, 279 insertions, 34 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index d20a02a2..1b05911b 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -393,10 +393,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
| V.AEndedSharedLoan (_, _) ->
(* Nothing special to do *)
super#visit_ALoan opt_abs lc
- | V.AIgnoredMutLoan (bid', child) ->
+ | V.AIgnoredMutLoan (opt_bid, child) ->
(* This loan is ignored, but we may have to project on a subvalue
* of the value which is given back *)
- if bid' = bid then
+ if opt_bid = Some bid then
(* Remember the given back value as a meta-value *)
let given_back_meta = nv in
(* Note that we replace the ignored mut loan by an *ended* ignored
@@ -557,10 +557,10 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
| V.AEndedSharedLoan (_, _) ->
(* Nothing special to do *)
super#visit_ALoan opt_abs lc
- | V.AIgnoredMutLoan (bid', child) ->
+ | V.AIgnoredMutLoan (bid_opt, child) ->
(* This loan is ignored, but we may have to project on a subvalue
* of the value which is given back *)
- if bid' = bid then (
+ if bid_opt = Some bid then (
(* Note that we replace the ignored mut loan by an *ended* ignored
* mut loan. Also, this is not the loan we are looking for *per se*:
* we don't register the fact that we inserted the value somewhere
@@ -1626,10 +1626,15 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
push { V.value; ty };
(* Explore the child *)
list_avalues false push_fail child_av
+ | V.AIgnoredMutLoan (opt_bid, child_av) ->
+ (* We don't support nested borrows for now *)
+ assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
+ assert (opt_bid = None);
+ (* Simply explore the child *)
+ list_avalues false push_fail child_av
| V.AEndedMutLoan
{ child = child_av; given_back = _; given_back_meta = _ }
| V.AEndedSharedLoan (_, child_av)
- | V.AIgnoredMutLoan (_, child_av)
| V.AEndedIgnoredMutLoan
{ child = child_av; given_back = _; given_back_meta = _ }
| V.AIgnoredSharedLoan child_av ->
@@ -1651,7 +1656,12 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
| V.ASharedBorrow _ ->
(* Nothing specific to do: keep the value as it is *)
push av
- | V.AIgnoredMutBorrow (_, child_av)
+ | V.AIgnoredMutBorrow (opt_bid, child_av) ->
+ (* We don't support nested borrows for now *)
+ assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
+ assert (opt_bid = None);
+ (* Just explore the child *)
+ list_avalues false push_fail child_av
| V.AEndedIgnoredMutBorrow
{ child = child_av; given_back_loans_proj = _; given_back_meta = _ }
->
@@ -1659,9 +1669,11 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
(* Just explore the child *)
list_avalues false push_fail child_av
- | V.AProjSharedBorrow _ ->
- (* Nothing specific to do: keep the value as it is *)
- push_avalue av
+ | V.AProjSharedBorrow asb ->
+ (* We don't support nested borrows *)
+ assert (asb = []);
+ (* Nothing specific to do *)
+ ()
| V.AEndedMutBorrow _ | V.AEndedSharedBorrow ->
(* If we get there it means the abstraction ended: it should not
be in the context anymore (if we end *one* borrow in an abstraction,
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 40c32ccc..8a563351 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -105,8 +105,8 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
assert (given_back = []);
(* Apply the projector *)
let projected_value =
- apply_proj_loans_on_symbolic_expansion proj_regions expansion
- original_sv.V.sv_ty
+ apply_proj_loans_on_symbolic_expansion proj_regions
+ ancestors_regions expansion original_sv.V.sv_ty
in
(* Replace *)
projected_value.V.value)
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index b159ab58..00e6eb01 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -415,7 +415,12 @@ module type Matcher = sig
V.typed_value ->
V.borrow_id * V.typed_value
- (** The shared value is the result of a match *)
+ (** Parameters:
+ [ty]
+ [ids0]
+ [ids1]
+ [v]: the result of matching the shared values coming from the two loans
+ *)
val match_shared_loans :
T.ety ->
V.loan_id_set ->
@@ -438,6 +443,93 @@ module type Matcher = sig
*)
val match_symbolic_with_other :
bool -> V.symbolic_value -> V.typed_value -> V.typed_value
+
+ (** The input ADTs don't have the same variant *)
+ val match_distinct_aadts :
+ T.rty -> V.adt_avalue -> T.rty -> V.adt_avalue -> V.typed_avalue
+
+ (** Parameters:
+ [ty0]
+ [bid0]
+ [ty1]
+ [bid1]
+ *)
+ val match_ashared_borrows :
+ T.rty -> V.borrow_id -> T.rty -> V.borrow_id -> V.typed_avalue
+
+ (** Parameters:
+ [ty0]
+ [mv0]
+ [bid0]
+ [av0]
+ [ty1]
+ [mv1]
+ [bid1]
+ [av1]
+ [mv]: result of matching mv0 and mv1
+ [av]: result of matching av0 and av1
+ *)
+ val match_amut_borrows :
+ T.rty ->
+ V.mvalue ->
+ V.borrow_id ->
+ V.typed_avalue ->
+ T.rty ->
+ V.mvalue ->
+ V.borrow_id ->
+ V.typed_avalue ->
+ V.mvalue ->
+ V.typed_avalue ->
+ V.typed_avalue
+
+ (** Parameters:
+ [ty0]
+ [ids0]
+ [v0]
+ [av0]
+ [ty1]
+ [ids1]
+ [v1]
+ [av1]
+ [v]: result of matching v0 and v1
+ [av]: result of matching av0 and av1
+ *)
+ val match_ashared_loans :
+ T.rty ->
+ V.loan_id_set ->
+ V.typed_value ->
+ V.typed_avalue ->
+ T.rty ->
+ V.loan_id_set ->
+ V.typed_value ->
+ V.typed_avalue ->
+ V.typed_value ->
+ V.typed_avalue ->
+ V.typed_avalue
+
+ (** Parameters:
+ [ty0]
+ [id0]
+ [av0]
+ [ty1]
+ [id1]
+ [av1]
+ [av]: result of matching av0 and av1
+ *)
+ val match_amut_loans :
+ T.rty ->
+ V.borrow_id ->
+ V.typed_avalue ->
+ T.rty ->
+ V.borrow_id ->
+ V.typed_avalue ->
+ V.typed_avalue ->
+ V.typed_avalue
+
+ (** Match two arbitrary avalues whose constructors don't match (this function
+ is typically used to raise the proper exception).
+ *)
+ val match_avalues : V.typed_avalue -> V.typed_avalue -> V.typed_avalue
end
(** Generic functor to implement matching functions between values, environments,
@@ -473,7 +565,7 @@ module Match (M : Matcher) = struct
assert (not (value_has_borrows ctx v1.V.value));
(* Merge *)
M.match_distinct_adts v0.V.ty av0 av1)
- | Bottom, Bottom -> v1
+ | Bottom, Bottom -> v0
| Borrow bc0, Borrow bc1 ->
let bc =
match (bc0, bc1) with
@@ -546,7 +638,83 @@ module Match (M : Matcher) = struct
and match_typed_avalues (ctx : C.eval_ctx) (v0 : V.typed_avalue)
(v1 : V.typed_avalue) : V.typed_avalue =
- raise (Failure "Unreachable")
+ let match_rec = match_typed_values ctx in
+ let match_arec = match_typed_avalues ctx in
+ assert (v0.V.ty = v1.V.ty);
+ match (v0.V.value, v1.V.value) with
+ | V.APrimitive _, V.APrimitive _ ->
+ (* We simply ignore - those are actually not used *)
+ assert (v0.V.ty = v1.V.ty);
+ mk_aignored v0.V.ty
+ | V.AAdt av0, V.AAdt av1 ->
+ if av0.variant_id = av1.variant_id then
+ let fields = List.combine av0.field_values av1.field_values in
+ let field_values =
+ List.map (fun (f0, f1) -> match_arec f0 f1) fields
+ in
+ let value : V.avalue =
+ V.AAdt { variant_id = av0.variant_id; field_values }
+ in
+ { V.value; ty = v1.V.ty }
+ else (* Merge *)
+ M.match_distinct_aadts v0.V.ty av0 v1.V.ty av1
+ | ABottom, ABottom -> v0
+ | ABorrow bc0, ABorrow bc1 -> (
+ match (bc0, bc1) with
+ | ASharedBorrow bid0, ASharedBorrow bid1 ->
+ M.match_ashared_borrows v0.V.ty bid0 v1.V.ty bid1
+ | AMutBorrow (mv0, bid0, av0), AMutBorrow (mv1, bid1, av1) ->
+ (* Not sure what to do with the meta-value *)
+ let mv = match_rec mv0 mv1 in
+ let av = match_arec av0 av1 in
+ M.match_amut_borrows v0.V.ty mv0 bid0 av0 v1.V.ty mv1 bid1 av1 mv av
+ | AIgnoredMutBorrow _, AIgnoredMutBorrow _ ->
+ (* The abstractions are destructured: we shouldn't get there *)
+ raise (Failure "Unexpected")
+ | AProjSharedBorrow asb0, AProjSharedBorrow asb1 -> (
+ match (asb0, asb1) with
+ | [], [] ->
+ (* This case actually stands for ignored shared borrows, when
+ there are no nested borrows *)
+ v0
+ | _ ->
+ (* We should get there only if there are nested borrows *)
+ raise (Failure "Unexpected"))
+ | _ ->
+ (* TODO: getting there is not necessarily inconsistent (it may
+ just be because the environments don't match) so we may want
+ to call a specific function (which could raise the proper
+ exception).
+ Rem.: we shouldn't get to the ended borrow cases, because
+ an abstraction should never contain ended borrows unless
+ we are *currently* ending it, in which case we need
+ to completely end it before continuing.
+ *)
+ raise (Failure "Unexpected"))
+ | ALoan lc0, ALoan lc1 -> (
+ (* TODO: maybe we should enforce that the ids are always exactly the same -
+ without matching *)
+ match (lc0, lc1) with
+ | ASharedLoan (ids0, sv0, av0), ASharedLoan (ids1, sv1, av1) ->
+ let sv = match_rec sv0 sv1 in
+ let av = match_arec av0 av1 in
+ assert (not (value_has_borrows ctx sv.V.value));
+ M.match_ashared_loans v0.V.ty ids0 sv0 av0 v1.V.ty ids1 sv1 av1 sv
+ av
+ | AMutLoan (id0, av0), AMutLoan (id1, av1) ->
+ let av = match_arec av0 av1 in
+ M.match_amut_loans v0.V.ty id0 av0 v1.V.ty id1 av1 av
+ | AIgnoredMutLoan _, AIgnoredMutLoan _
+ | AIgnoredSharedLoan _, AIgnoredSharedLoan _ ->
+ (* Those should have been filtered when destructuring the abstractions -
+ they are necessary only when there are nested borrows *)
+ raise (Failure "Unreachable")
+ | _ -> raise (Failure "Unreachable"))
+ | ASymbolic _, ASymbolic _ ->
+ (* For now, we force all the symbolic values containing borrows to
+ be eagerly expanded, and we don't support nested borrows *)
+ raise (Failure "Unreachable")
+ | _ -> M.match_avalues v0 v1
end
(* Very annoying: functors only take modules as inputs... *)
@@ -709,7 +877,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
(* Return the new borrow *)
(bid2, sv)
- let match_shared_loans (ty : T.ety) (ids0 : V.loan_id_set)
+ let match_shared_loans (_ : T.ety) (ids0 : V.loan_id_set)
(ids1 : V.loan_id_set) (sv : V.typed_value) :
V.loan_id_set * V.typed_value =
(* Check if the ids are the same - Rem.: we forbid the sets of loans
@@ -732,9 +900,13 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
(* Return *)
(ids, sv)
- let match_mut_loans (_ : T.ety) (id0 : V.loan_id) (_ : V.loan_id) : V.loan_id
- =
- id0
+ let match_mut_loans (_ : T.ety) (id0 : V.loan_id) (id1 : V.loan_id) :
+ V.loan_id =
+ if id0 = id1 then id0
+ else
+ (* We forbid this case for now: if we get there, we force to end
+ both borrows *)
+ raise (ValueMatchFailure (LoanInLeft id0))
let match_symbolic_values (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) :
V.symbolic_value =
@@ -771,6 +943,13 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
else raise (ValueMatchFailure (LoanInRight id)));
(* Return a fresh symbolic value *)
mk_fresh_symbolic_typed_value V.LoopJoin sv.sv_ty
+
+ let match_distinct_aadts _ _ _ _ = raise (Failure "Unreachable")
+ let match_ashared_borrows _ _ _ _ = raise (Failure "Unreachable")
+ let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable")
+ let match_ashared_loans _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable")
+ let match_amut_loans _ _ _ _ _ _ _ = raise (Failure "Unreachable")
+ let match_avalues _ _ = raise (Failure "Unreachable")
end
(*
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index d656e158..87522d73 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -69,8 +69,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
| V.ReservedMutBorrow _, _ ->
raise
(Failure
- "Can't apply a proj_borrow over a reserved mutable \
- borrow")
+ "Can't apply a proj_borrow over a reserved mutable borrow")
| _ -> raise (Failure "Unreachable")
in
let asb =
@@ -140,7 +139,19 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
fresh_reborrow regions ancestors_regions bv ref_ty
in
V.AMutBorrow (mv, bid, bv)
- | V.SharedBorrow (_, bid), T.Shared -> V.ASharedBorrow bid
+ | V.SharedBorrow (_, bid), T.Shared ->
+ (* Rem.: we don't need to also apply the projection on the
+ borrowed value, because for as long as the abstraction
+ lives then the shared borrow lives, which means that the
+ whole value is borrowed (and thus immutable).
+ This is not the case if the current borrow is not to be
+ projected to the current abstraction: if this happens,
+ then maybe there are borrows *inside* the shared value
+ which belong to the current abstraction, meaning we
+ need to lookup the shared value and project it (see the
+ other branch of the [if then else]).
+ *)
+ V.ASharedBorrow bid
| V.ReservedMutBorrow _, _ ->
raise
(Failure
@@ -150,7 +161,9 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
in
V.ABorrow bc
else
- (* Not in the set: ignore *)
+ (* Not in the set: ignore the borrow, but project the borrowed
+ value (maybe some borrows *inside* the borrowed value are in
+ the region set) *)
let bc =
match (bc, kind) with
| V.MutBorrow (bid, bv), T.Mut ->
@@ -249,7 +262,8 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value)
TODO: detailed comments. See [apply_proj_borrows]
*)
let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
- (see : V.symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue =
+ (ancestors_regions : T.RegionId.Set.t) (see : V.symbolic_expansion)
+ (original_sv_ty : T.rty) : V.typed_avalue =
(* Sanity check: if we have a proj_loans over a symbolic value, it should
* contain regions which we will project *)
assert (ty_has_regions_in_set regions original_sv_ty);
@@ -278,7 +292,12 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
(V.ALoan (V.AMutLoan (bid, child_av)), ref_ty)
else
(* Not in the set: ignore *)
- (V.ALoan (V.AIgnoredMutLoan (bid, child_av)), ref_ty)
+ (* If the borrow id is in the ancestor's regions, we still need
+ * to remember it *)
+ let opt_bid =
+ if region_in_set r ancestors_regions then Some bid else None
+ in
+ (V.ALoan (V.AIgnoredMutLoan (opt_bid, child_av)), ref_ty)
| SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) ->
(* Sanity check *)
assert (spc.V.sv_ty = ref_ty);
diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
index a6d8bd5c..602125c6 100644
--- a/compiler/InterpreterProjectors.mli
+++ b/compiler/InterpreterProjectors.mli
@@ -11,9 +11,19 @@ open InterpreterBorrowsCore
Apply a proj_borrows on a shared borrow.
Note that when projecting over shared values, we generate
{!V.abstract_shared_borrows}, not {!V.avalue}s.
+
+ Parameters:
+ [regions]
+ [ancestor_regions]
+ [see]
+ [original_sv_ty]
*)
val apply_proj_loans_on_symbolic_expansion :
- T.RegionId.Set.t -> V.symbolic_expansion -> T.rty -> V.typed_avalue
+ T.RegionId.Set.t ->
+ T.RegionId.Set.t ->
+ V.symbolic_expansion ->
+ T.rty ->
+ V.typed_avalue
(** Convert a symbolic expansion *which is not a borrow* to a value *)
val symbolic_expansion_non_borrow_to_value :
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index d9ed9cea..2904289f 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -160,7 +160,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
match lc with
| V.AMutLoan (bid, _) -> register_mut_loan inside_abs bid
| V.ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids
- | V.AIgnoredMutLoan (bid, _) -> register_ignored_loan T.Mut bid
+ | V.AIgnoredMutLoan (Some bid, _) -> register_ignored_loan T.Mut bid
+ | V.AIgnoredMutLoan (None, _)
| V.AIgnoredSharedLoan _
| V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
| V.AEndedSharedLoan (_, _)
@@ -571,7 +572,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| _ -> raise (Failure "Inconsistent context"))
| V.ALoan lc, aty -> (
match lc with
- | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (bid, child_av)
+ | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (Some bid, child_av)
-> (
let borrowed_aty = aloan_get_expected_child_type aty in
assert (child_av.V.ty = borrowed_aty);
@@ -585,6 +586,9 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
Subst.erase_regions sv.V.ty
= Subst.erase_regions borrowed_aty)
| _ -> raise (Failure "Inconsistent context"))
+ | V.AIgnoredMutLoan (None, child_av) ->
+ let borrowed_aty = aloan_get_expected_child_type aty in
+ assert (child_av.V.ty = borrowed_aty)
| V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av)
->
let borrowed_aty = aloan_get_expected_child_type aty in
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 2b2f98f0..6c0c95ad 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -248,8 +248,10 @@ module Values = struct
^ ", "
^ typed_avalue_to_string fmt av
^ ")"
- | AIgnoredMutLoan (bid, av) ->
- "@ignored_mut_loan(" ^ V.BorrowId.to_string bid ^ ", "
+ | AIgnoredMutLoan (opt_bid, av) ->
+ "@ignored_mut_loan("
+ ^ option_to_string V.BorrowId.to_string opt_bid
+ ^ ", "
^ typed_avalue_to_string fmt av
^ ")"
| AEndedIgnoredMutLoan ml ->
diff --git a/compiler/Values.ml b/compiler/Values.ml
index efb0bb67..9c68ad4f 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -524,7 +524,7 @@ and aloan_content =
We get (after some symbolic exansion):
{[
abs0 {
- a_mut_loan l0 (a_mut_loan l1)
+ a_mut_loan l0 (a_mut_loan l1 _)
}
px -> mut_borrow l0 (mut_borrow @s1)
]}
@@ -542,7 +542,7 @@ and aloan_content =
We get:
{[
- abs0 { a_shared_loan {l0} @s0 ⊥ }
+ abs0 { a_shared_loan {l0} @s0 _ }
px -> shared_loan l0
]}
*)
@@ -579,7 +579,7 @@ and aloan_content =
give back. We keep the shared value because it now behaves as a
"regular" value (which contains borrows we might want to end...).
*)
- | AIgnoredMutLoan of loan_id * typed_avalue
+ | AIgnoredMutLoan of loan_id option * typed_avalue
(** An ignored mutable loan.
We need to keep track of ignored mutable loans, because we may have
@@ -588,6 +588,9 @@ and aloan_content =
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).
+
+ Note that we need to do so only for borrows consumed by parent
+ abstractions, hence the optional loan id.
Example:
========
@@ -692,7 +695,11 @@ and aborrow_content =
Note that we need to do so only for borrows consumed by parent
abstractions (hence the optional borrow id).
- TODO: the below explanations are obsolete
+ 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
+ use {!AProjSharedBorrow} to project the shared value).
+
+ TODO: the explanations below are obsolete
Example:
========
@@ -806,10 +813,22 @@ and aborrow_content =
> px -> shared_loan {l1, l3, l4} (mut_borrow l0 (U32 0))
> ppx -> shared_loan {l2} (shared_borrow l1)
> pppx -> ⊥
- > abs'a { a_proj_shared_borrow {l2} }
+ > abs'a { a_shared_borrow {l2} }
> abs'b { a_proj_shared_borrow {l3} } // l3 reborrows l1
> abs'c { a_proj_shared_borrow {l4} } // l4 reborrows l0
]}
+
+ 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.
+
+ TODO: maybe we should factorized [ASharedBorrow] and [AProjSharedBorrow].
*)
(* TODO: the type of avalues doesn't make sense for loan avalues: they currently