Start updating the assignment semantics

1 files changed, 24 insertions, 16 deletions

diff --git a/TODO.md b/TODO.md
index c317a8b1..62463d6a 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,34 +1,23 @@
+# TODO
+
 * write an interesting example to study with Jonathan
 
 * update the assignment to move the destination value (which will be overriden)
   to a dummy variable, and end all the outer borrows.
-  update pop_frame
+  Also update pop_frame.
 
 * add option for: `allow_borrow_overwrites_on_input_values`
+  (rather: `will_overwrite_input_borrows`)
   (but always disallow borrow overwrites on returned values)
   at the level of abstractions (not at the level of loans!)
 
 * set of types with mutable borrows (what to do when type variables appear under
   shared borrows?)
-
-* split `apply_proj_borrows` into two:
-  * `apply_proj_borrows_on_input_values` : ... -> value -> rty -> avalue
-  * `apply_proj_borrows_on_given_back_values` : ... -> value -> avalue -> avalue
-  TODO: actually not sure
-
-* remove the rule which says that we can end a borrow under an abstraction if
-  the corresponding loan is in the same abstraction.
+  necessary to know what to return.
 
 * Check what happens when symbolic borrows are not expanded (when looking for
   borrows/abstractions to end).
 
-* Reduce projectors to `_` (ignored) when there are no region intersections
-
-* update end_borrow_get_borrow to keep track of the ignored borrows/loans as
-  outer borrows, and track the ids of the ignored shared loans?
-  or: make sure there are no parent abstractions when ending inner loans in
-  abstractions.
-
 * expand symbolic values which are primitively copyable upon using them as
   function arguments or putting them in the return value, in order to deduplicate
   those values.
@@ -45,6 +34,22 @@
   case we will need to split the value given back - for now: disallow this
   behaviour?).
 
+* split `apply_proj_borrows` into two:
+  * `apply_proj_borrows_on_input_values` : ... -> value -> rty -> avalue
+  * `apply_proj_borrows_on_given_back_values` : ... -> value -> avalue -> avalue
+  TODO: actually not sure
+
+* remove the rule which says that we can end a borrow under an abstraction if
+  the corresponding loan is in the same abstraction.
+  Actually: update the rule, rather.
+* Reduce projectors to `_` (ignored) when there are no region intersections
+
+* update end_borrow_get_borrow to keep track of the ignored borrows/loans as
+  outer borrows, and track the ids of the ignored shared loans?
+  or: make sure there are no parent abstractions when ending inner loans in
+  abstractions.
+
+
 * `ended_proj_loans` (with ghost value)
 
 * add a check in function inputs: ok to take as parameters symbolic values with
@@ -65,3 +70,6 @@
 
 * Some variables have the same name. It might be good to also print their id
   to disambiguate?
+
+
+# DONE