diff options
author | Son Ho | 2021-12-17 13:28:51 +0100 |
---|---|---|
committer | Son Ho | 2021-12-17 13:28:51 +0100 |
commit | 2e1903b951b496dd3f0bde08d9b5d524659a3bac (patch) | |
tree | 1e9933c5b979b021d6bb41dc0b9a5b4e31c9f555 /src/Values.ml | |
parent | 4c498a62391624425b05b99197b40fd992626ed5 (diff) |
Implement the avalue cases of give_back_value
Diffstat (limited to '')
-rw-r--r-- | src/Values.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/Values.ml b/src/Values.ml index e0b0b59d..09cf8aa6 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -227,7 +227,16 @@ and adt_avalue = { and aloan_content = | AMutLoan of (BorrowId.id[@opaque]) * typed_avalue | ASharedLoan of (BorrowId.set_t[@opaque]) * typed_value * typed_avalue - | AEndedMutLoan of { given_back : typed_value; child : typed_avalue } + | 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). + *) | AEndedSharedLoan of typed_value * typed_avalue | AIgnoredMutLoan of (BorrowId.id[@opaque]) * typed_avalue | AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue } |