summaryrefslogtreecommitdiff
path: root/TODO.md
diff options
context:
space:
mode:
authorSon Ho2022-01-27 10:12:08 +0100
committerSon Ho2022-01-27 10:12:08 +0100
commit708c8582b3ac9065256a2763f4175ac3a1205e7f (patch)
tree94170f7a5387454eefc98a59aebfc27524ffd5a2 /TODO.md
parente8643f79704e06a6211bf4b594255ed70026a5dc (diff)
Make minor modifications and add comments
Diffstat (limited to '')
-rw-r--r--TODO.md7
1 files changed, 7 insertions, 0 deletions
diff --git a/TODO.md b/TODO.md
index 8edb8fe6..46ef183b 100644
--- a/TODO.md
+++ b/TODO.md
@@ -15,6 +15,11 @@
backward calls (because they may panic!)
- calls which don't take inputs (can happen with backward functions - for
instance, if a rust function only returns shared borrows)
+ - monadic lets to matches
+ - no tuple deconstruction on returned monadic values (introduce intermediate
+ variables to deconstruct in two times)
+ - matching on values (ex.: `let Cons hd tl = ls in` ~~>
+ `match ls with | Nil -> Panic | Cons hd tl -> ...`)
1. reorder the branches of matches
@@ -64,6 +69,8 @@
while in the case of `s1` we should ignore the outer borrow (what we give
back actually has type `T`...)
+10. Write "bodies" for the assumed functions.
+
* write a function to check that the code we are about to synthesize is in the proper
subset. In particular:
* borrow overwrites