1 files changed, 22 insertions, 0 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml
index fd11f30b..0e05e5b9 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -5,6 +5,28 @@
     happens that we move a value out of a box before freeing this box).
     Semantically speaking, we thus handle `Box::free` as a value drop and
     not as a function call, and thus never need its signature.
+    
+    TODO: implementing the concrete evaluation functions for the assumed
+    functions is really annoying (see
+    [InterpreterStatements.eval_non_local_function_call_concrete]).
+    I think it should be possible, in most situations, to write bodies which
+    model the behaviour of those unsafe functions. For instance, `Box::deref_mut`
+    should simply be:
+    ```
+    fn deref_mut<'a, T>(x : &'a mut Box<T>) -> &'a mut T {
+      &mut ( *x ) // box dereferencement is a primitive operation
+    }
+    ```
+    
+    For vectors, we could "cheat" by using the index as a field index (vectors
+    would be encoded as ADTs with a variable number of fields). Of course, it
+    would require a bit of engineering, but it would probably be quite lightweight
+    in the end.
+    ```
+    Vec::get_mut<'a,T>(v : &'a mut Vec<T>, i : usize) -> &'a mut T {
+      &mut ( ( *x ).i )
+    }
+    ```
  *)
 
 module T = Types