diff options
author | Son Ho | 2022-01-03 16:21:42 +0100 |
---|---|---|
committer | Son Ho | 2022-01-03 16:21:42 +0100 |
commit | f371140e5df9210d27af44fd2d21065005b05a9d (patch) | |
tree | f1aa92242fcdcd5e3d0ca7f8c88e53affa8b1e0d /src/Values.ml | |
parent | 2ec3f0ac2834101360fff59c20e91a02dd197760 (diff) |
Make progress on end_abstraction_borrows and start implementing
convert_avalue_to_value
Diffstat (limited to '')
-rw-r--r-- | src/Values.ml | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/src/Values.ml b/src/Values.ml index 3fddc88c..f1b2e0a6 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -424,9 +424,24 @@ and aborrow_content = > 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'a { a_mut_borrow l1 (a_ignored_mut_borrow (U32 0)) } // TODO: duplication > abs'b { a_ignored_mut_borrow (a_mut_borrow l0 (U32 0)) } ``` + 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. *) | AProjSharedBorrow of (abstract_shared_borrows[@opaque]) (** A projected shared borrow. |