Start working on Collections.ml

7 files changed, 17 insertions, 26 deletions

diff --git a/TODO.md b/TODO.md
index fd950d7b..7e6648cd 100644
--- a/TODO.md
+++ b/TODO.md
@@ -11,6 +11,8 @@
 
 3. fix the static regions (with projectors)
 
+4. Add a `Collections.ml` file, with `Map` and `Set`
+
 * write an interesting example to study with Jonathan
 
 * add option for: `allow_borrow_overwrites_on_input_values`
@@ -58,6 +60,15 @@
 * Some variables have the same name. It might be good to also print their id
   to disambiguate?
 
+* it would be good to find a "core", which implements the rules (like
+  "end_borrow") and on top of which we build more complex functions which
+  chose in which order to apply the rules, etc. This way we would make very
+  explicit where we need to insert sanity checks, what the preconditions are,
+  where invariants might be broken, etc.
+
+* intensively test with PLT-redex
+
+* remove the config parameters when they are useless
 
 # DONE
 
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 56edc238..4ec5aab7 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -1,3 +1,5 @@
+open Collections
+
 (** Signature for a module describing an identifier.
     
     We often need identifiers (for definitions, variables, etc.) and in
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index c998214b..2f0f52af 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2,15 +2,10 @@ module L = Logging
 module T = Types
 module A = CfimAst
 module M = Modules
-open Utils
 open InterpreterUtils
 open InterpreterExpressions
 open InterpreterStatements
 
-(* TODO: check that the value types are correct when evaluating *)
-(* TODO: for debugging purposes, we might want to put use eval_ctx everywhere
-   (rather than only env) *)
-
 (* TODO: it would be good to find a "core", which implements the rules (like
    "end_borrow") and on top of which we build more complex functions which
    chose in which order to apply the rules, etc. This way we would make very
@@ -98,7 +93,7 @@ module Test = struct
     (* Split the variables between return var, inputs and remaining locals *)
     let ret_var = List.hd fdef.locals in
     let input_vars, local_vars =
-      list_split_at (List.tl fdef.locals) fdef.arg_count
+      Collections.List.split_at (List.tl fdef.locals) fdef.arg_count
     in
     (* Push the return variable (initialized with ⊥) *)
     let ctx = C.ctx_push_uninitialized_var ctx ret_var in
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 8cf2b747..4482a507 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -413,7 +413,7 @@ let expand_bottom_value_from_projection (config : C.config)
      during whose evaluation we got stuck *)
   let projection' =
     fst
-      (Utils.list_split_at p.projection
+      (Collections.List.split_at p.projection
          (List.length p.projection - remaining_pes))
   in
   let p' = { p with projection = projection' } in
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 885d1bdc..1b06dd7f 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -829,7 +829,7 @@ and eval_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
   let ctx = C.ctx_push_var ctx ret_var (mk_bottom ret_var.var_ty) in
 
   (* 2. Push the input values *)
-  let input_locals, locals = Utils.list_split_at locals def.A.arg_count in
+  let input_locals, locals = Collections.List.split_at locals def.A.arg_count in
   let inputs = List.combine input_locals args in
   (* Note that this function checks that the variables and their values
      have the same type (this is important) *)
diff --git a/src/Print.ml b/src/Print.ml
index 8067eae3..000874fe 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -863,7 +863,7 @@ module CfimAst = struct
 
     (* Arguments *)
     let inputs = List.tl def.locals in
-    let inputs, _aux_locals = Utils.list_split_at inputs def.arg_count in
+    let inputs, _aux_locals = Collections.List.split_at inputs def.arg_count in
     let args = List.combine inputs sg.inputs in
     let args =
       List.map
diff --git a/src/Utils.ml b/src/Utils.ml
index 16ee7252..a285e869 100644
--- a/src/Utils.ml
+++ b/src/Utils.ml
@@ -1,20 +1,3 @@
-(* Split a list at a given index [i] (the first list contains all the elements
-   up to element of index [i], not included, the second one contains the remaining
-   elements. Note that the first returned list has length [i].
-*)
-let rec list_split_at (ls : 'a list) (i : int) =
-  if i < 0 then raise (Invalid_argument "list_split_at take positive integers")
-  else if i = 0 then ([], ls)
-  else
-    match ls with
-    | [] ->
-        raise
-          (Failure
-             "The int given to list_split_at should be <= the list's length")
-    | x :: ls' ->
-        let ls1, ls2 = list_split_at ls' (i - 1) in
-        (x :: ls1, ls2)
-
 exception Found
 (** Utility exception