summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-20 00:31:24 +0100
committerSon Ho2022-01-20 00:31:24 +0100
commit437cf6d3571f6bdaa7222ea937d019390c6217cf (patch)
tree941a03eda6117bc18de90506e4ee49d942bd0ce4
parent15201d05ab21baa67191d6f5c4c6b54effef6642 (diff)
Update the TODO
-rw-r--r--TODO.md18
1 files changed, 18 insertions, 0 deletions
diff --git a/TODO.md b/TODO.md
index 60211c32..3b868d10 100644
--- a/TODO.md
+++ b/TODO.md
@@ -33,6 +33,24 @@
7. fix the static regions (with projectors)
Before that, introduce a sanity check to make sure we don't use static regions.
+8. The following doesn't work:
+ ```
+ fn f1<'c, T>(p : (&'c mut T, &'c mut T)) -> (&'c mut T, &'c mut T)
+
+ fn f2<'a, 'b, T>(p: (&'a mut T, &'b mut T)) -> (&'a mut T, &'b mut T)
+
+ let p1 = f1<'c>(p0);
+ let p2 = f2<'a, 'b>(p1);
+ ```
+ (end borrows)
+ I think we should change the proj_loans to:
+ `AProjLoans of symbolic_value * (mvalue * aproj) list`
+ (to accumulate the given back values)
+ Then, once we collected all the borrows, we would convert it to:
+ `AEndedProjLoans of (mvalue * aproj) list`
+ If the list is empty, it means the value was not modified.
+
+
* write a function to check that the code we are about to synthesize is in the proper
subset. In particular:
* borrow overwrites