summaryrefslogtreecommitdiff
path: root/src/Values.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/Values.ml')
-rw-r--r--src/Values.ml217
1 files changed, 200 insertions, 17 deletions
diff --git a/src/Values.ml b/src/Values.ml
index 969e01d2..58934e03 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -111,7 +111,7 @@ and adt_value = {
and borrow_content =
| SharedBorrow of (BorrowId.id[@opaque]) (** A shared value *)
| MutBorrow of (BorrowId.id[@opaque]) * typed_value
- (** A mutably borrowed value *)
+ (** A mutably borrowed value. *)
| InactivatedMutBorrow of (BorrowId.id[@opaque])
(** An inactivated mut borrow.
@@ -127,6 +127,9 @@ and borrow_content =
and loan_content =
| SharedLoan of (BorrowId.set_t[@opaque]) * typed_value
| MutLoan of (BorrowId.id[@opaque])
+ (** TODO: we might want to add a set of borrow ids (useful for inactivated
+ borrows, and extremely useful when giving shared values to abstractions).
+ *)
and typed_value = { value : value; ty : ety }
[@@deriving
@@ -234,31 +237,123 @@ and adt_avalue = {
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. We keep track of the hierarchy because
- we need it to properly instantiate the backward functions when generating
- the pure translation.
+ 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 (BorrowId.id[@opaque]) * typed_avalue
+ (** A mutable loan owned by an abstraction.
+
+ Example:
+ ========
+ ```
+ fn f<'a>(...) -> &'a mut &'a mut u32;
+
+ let px = f(...);
+ ```
+
+ We get (after some symbolic exansion):
+ ```
+ abs0 {
+ a_mut_loan l0 (a_mut_loan l1)
+ }
+ px -> mut_borrow l0 (mut_borrow @s1)
+ ```
+ *)
| ASharedLoan of (BorrowId.set_t[@opaque]) * typed_value * typed_avalue
+ (** A shared loan owned by an abstraction.
+
+ Example:
+ ========
+ ```
+ fn f<'a>(...) -> &'a u32;
+
+ let px = f(...);
+ ```
+
+ We get:
+ ```
+ abs0 { a_shared_loan {l0} @s0 ⊥ }
+ px -> shared_loan l0
+ ```
+ *)
| AEndedMutLoan of { given_back : typed_avalue; child : typed_avalue }
- (** TODO: in the formalization, given_back was initially a typed value
- (not an avalue). It seems more consistent to use a value, especially
- because then the invariants about the borrows are simpler (otherwise,
- there may be borrow ids duplicated in the context, which is very
- annoying).
- I think the original idea was that using values would make it
- simple to instantiate the backward function (because projecting
- deconstructs a bit the values with which we feed the function).
- *)
+ (** An ended mutable loan in an abstraction.
+ We need it because abstractions must keep track of the values
+ we gave back to them, so that we can correctly instantiate
+ backward functions.
+
+ Example:
+ ========
+ ```
+ abs0 { a_mut_loan l0 ⊥ }
+ x -> mut_borrow l0 (U32 3)
+ ```
+
+ After ending `l0`:
+
+ ```
+ abs0 { a_ended_mut_loan { given_back = U32 3; child = ⊥; }
+ x -> ⊥
+ ```
+
+ TODO: in the formalization, given_back was initially a typed value
+ (not an avalue). It seems more consistent to use a value, especially
+ because then the invariants about the borrows are simpler (otherwise,
+ there may be borrow ids duplicated in the context, which is very
+ annoying).
+ I think the original idea was that using values would make it
+ simple to instantiate the backward function (because projecting
+ deconstructs a bit the values with which we feed the function).
+ *)
| AEndedSharedLoan of typed_value * typed_avalue
+ (** Similar to [AEndedMutLoan] but in this case there are no avalues to
+ give back. Actually, we could probably forget the shared value
+ altogether (and just keep the child avalue).
+ *)
| AIgnoredMutLoan of (BorrowId.id[@opaque]) * typed_avalue
+ (** An ignored mutable loan.
+
+ We need to keep track of ignored mutable loans, because we may have
+ to apply projections on the values given back to those loans (say
+ 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).
+
+ Example:
+ ========
+ ```
+ 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 ⊥) }
+ > x -> mut_borrow l0 (mut_borrow l1 @s1)
+ ```
+ *)
| AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue }
+ (** Similar to [AEndedMutLoan], for ignored loans *)
| AProjSharedLoan of (abstract_shared_borrows[@opaque])
- (** A projected shared loan - TODO: remove? Does it make sense? Maybe
- I should rename that to AIgnoredSharedLoan... *)
+ (** An ignored shared loan.
+ TODO: rename and change fields to: typed_avalue
+
+ Example:
+ ========
+ ```
+ 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 ⊥) }
+ > x -> shared_borrow l0
+ ```
+ *)
-(** Note that when a borrow content is ended, it is replaced by Bottom (while
+(** 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).
@@ -272,10 +367,98 @@ and aloan_content =
*)
and aborrow_content =
| AMutBorrow of (BorrowId.id[@opaque]) * typed_avalue
+ (** A mutable borrow owned by an abstraction.
+
+ Is used when an abstraction "consumes" borrows, when giving borrows
+ as arguments to a function.
+
+ Example:
+ ========
+ ```
+ fn f<'a>(px : &'a mut u32);
+
+ > x -> mut_loan l0
+ > px -> mut_borrow l0 (U32 0)
+
+ f(move px);
+
+ > x -> mut_loan l0
+ > px -> ⊥
+ > abs0 { a_mut_borrow l0 (U32 0) }
+ ```
+ *)
| ASharedBorrow of (BorrowId.id[@opaque])
+ (** A shared borrow owned by an abstraction.
+
+ Example:
+ ========
+ ```
+ fn f<'a>(px : &'a u32);
+
+ > x -> shared_loan {l0} (U32 0)
+ > px -> shared_borrow l0
+
+ f(move px);
+
+ > x -> shared_loan {l0} (U32 0)
+ > px -> ⊥
+ > abs0 { a_shared_bororw l0 }
+ ```
+ *)
| AIgnoredMutBorrow of typed_avalue
+ (** An ignored mutable borrow.
+
+ This is mostly useful for typing concerns: when a borrow doesn't
+ belong to an abstraction, it would be weird to ignore it altogether.
+
+ Example:
+ ========
+ ```
+ fn f<'a,'b>(ppx : &'a mut &'b mut u32);
+
+ > x -> mut_loan l0
+ > px -> mut_loan l1
+ > ppx -> mut_borrow l1 (mut_borrow l0 (U32 0))
+
+ f(move ppx);
+
+ > x -> mut_loan l0
+ > px -> mut_loan l1
+ > ppx -> ⊥
+ > abs'a { a_mut_borrow l1 ⊥ } // TODO: there might be an a_ignored_mut_borrow in the inner value
+ > abs'b { a_ignored_mut_borrow (a_mut_borrow l0 (U32 0)) }
+ ```
+ *)
| AProjSharedBorrow of (abstract_shared_borrows[@opaque])
- (** A projected shared borrow *)
+ (** A projected shared borrow.
+
+ When giving shared borrows as arguments to function calls, we
+ introduce new borrows to keep track of the fact that the function
+ might reborrow values inside.
+
+ Example:
+ ========
+ Below, when calling `f`, we need to introduce one shared borrow per
+ borrow in the argument.
+ ```
+ fn f<'a,'b>(pppx : &'a &'b &'c mut u32);
+
+ > x -> mut_loan l0
+ > px -> shared_loan {l1} (mut_borrow l0 (U32 0))
+ > ppx -> shared_loan {l2} (shared_borrow l1)
+ > pppx -> shared_borrow l2
+
+ f(move pppx);
+
+ > x -> mut_loan l0
+ > 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'b { a_proj_shared_borrow {l3} } // l3 reborrows l1
+ > abs'c { a_proj_shared_borrow {l4} } // l4 reborrows l0
+ ```
+ *)
(* TODO: we may want to merge this with typed_value - would prevent some issues
when accessing fields... *)