Make minor modifications and add comments

4 files changed, 45 insertions, 6 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
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
diff --git a/src/Translate.ml b/src/Translate.ml
index 043ed375..ecc97ed1 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -1,4 +1,3 @@
-open Errors
 open InterpreterStatements
 open Interpreter
 module L = Logging
@@ -41,10 +40,14 @@ let translate_function_to_symbolics (config : C.partial_config)
   (forward, backwards)
 
 (** Translate a function, by generating its forward and backward translations. *)
-let translate_function (config : C.partial_config)
+let translate_function_to_pure (config : C.partial_config)
     (type_context : C.type_context) (fun_context : C.fun_context)
     (fun_sigs : Pure.fun_sig SymbolicToPure.RegularFunIdMap.t)
     (fdef : A.fun_def) : pure_fun_translation =
+  (* Debug *)
+  log#ldebug
+    (lazy ("translate_function_to_pure: " ^ Print.name_to_string fdef.A.name));
+
   let def_id = fdef.def_id in
 
   (* Compute the symbolic ASTs *)
@@ -144,6 +147,9 @@ let translate_function (config : C.partial_config)
 
 let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
     Pure.type_def T.TypeDefId.Map.t * pure_fun_translation A.FunDefId.Map.t =
+  (* Debug *)
+  log#ldebug (lazy "translate_module_to_pure");
+
   (* Compute the type and function contexts *)
   let type_context, fun_context = compute_type_fun_contexts m in
 
@@ -165,11 +171,12 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
   in
 
   (* Translate all the functions *)
-  let translations =
+  let pure_translations =
     List.map
       (fun (fdef : A.fun_def) ->
         ( fdef.def_id,
-          translate_function config type_context fun_context fun_sigs fdef ))
+          translate_function_to_pure config type_context fun_context fun_sigs
+            fdef ))
       m.functions
   in
 
@@ -177,7 +184,7 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
   let fun_defs =
     List.fold_left
       (fun m (def_id, trans) -> A.FunDefId.Map.add def_id trans m)
-      A.FunDefId.Map.empty translations
+      A.FunDefId.Map.empty pure_translations
   in
 
   (* Return *)
diff --git a/src/main.ml b/src/main.ml
index aca1978c..46b54d55 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -54,6 +54,8 @@ let () =
   expansion_log#set_level EL.Debug;
   borrows_log#set_level EL.Debug;
   invariants_log#set_level EL.Warning;
+  symbolic_to_pure_log#set_level EL.Debug;
+  translate_log#set_level EL.Debug;
   (* Load the module *)
   let json = Yojson.Basic.from_file !filename in
   match cfim_module_of_json json with
@@ -73,7 +75,8 @@ let () =
       (* Test the unit functions with the concrete interpreter *)
       I.Test.test_unit_functions config m;
 
-      (* Evaluate the symbolic interpreter on the functions - TODO: remove *)
+      (* Evaluate the symbolic interpreter on the functions, ignoring the
+       * functions which contain loops - TODO: remove *)
       let synthesize = true in
       I.Test.test_functions_symbolic config synthesize m;