Implement a Config.ml file which groups all the global options in references

1 files changed, 13 insertions, 15 deletions

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index e752594e..f776c7ff 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -208,7 +208,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
       for the synthesis)
     - the symbolic AST generated by the symbolic execution
  *)
-let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
+let evaluate_function_symbolic (synthesize : bool)
     (type_context : C.type_context) (fun_context : C.fun_context)
     (global_context : C.global_context) (fdef : A.fun_decl)
     (back_id : T.RegionGroupId.id option) :
@@ -229,7 +229,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
   in
 
   (* Create the continuation to finish the evaluation *)
-  let config = C.config_of_partial C.SymbolicMode config in
+  let config = C.mk_config C.SymbolicMode in
   let cf_finish res ctx =
     match res with
     | Return ->
@@ -284,8 +284,7 @@ module Test = struct
   (** Test a unit function (taking no arguments) by evaluating it in an empty
       environment.
    *)
-  let test_unit_function (config : C.partial_config) (crate : A.crate)
-      (fid : A.FunDeclId.id) : unit =
+  let test_unit_function (crate : A.crate) (fid : A.FunDeclId.id) : unit =
     (* Retrieve the function declaration *)
     let fdef = A.FunDeclId.nth crate.functions fid in
     let body = Option.get fdef.body in
@@ -311,7 +310,7 @@ module Test = struct
     let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in
 
     (* Create the continuation to check the function's result *)
-    let config = C.config_of_partial C.ConcreteMode config in
+    let config = C.mk_config C.ConcreteMode in
     let cf_check res ctx =
       match res with
       | Return ->
@@ -340,24 +339,24 @@ module Test = struct
         && List.length def.A.signature.inputs = 0
 
   (** Test all the unit functions in a list of function definitions *)
-  let test_unit_functions (config : C.partial_config) (crate : A.crate) : unit =
+  let test_unit_functions (crate : A.crate) : unit =
     let unit_funs = List.filter fun_decl_is_transparent_unit crate.functions in
     let test_unit_fun (def : A.fun_decl) : unit =
-      test_unit_function config crate def.A.def_id
+      test_unit_function crate def.A.def_id
     in
     List.iter test_unit_fun unit_funs
 
   (** Execute the symbolic interpreter on a function. *)
-  let test_function_symbolic (config : C.partial_config) (synthesize : bool)
-      (type_context : C.type_context) (fun_context : C.fun_context)
-      (global_context : C.global_context) (fdef : A.fun_decl) : unit =
+  let test_function_symbolic (synthesize : bool) (type_context : C.type_context)
+      (fun_context : C.fun_context) (global_context : C.global_context)
+      (fdef : A.fun_decl) : unit =
     (* Debug *)
     log#ldebug
       (lazy ("test_function_symbolic: " ^ Print.fun_name_to_string fdef.A.name));
 
     (* Evaluate *)
     let evaluate =
-      evaluate_function_symbolic config synthesize type_context fun_context
+      evaluate_function_symbolic synthesize type_context fun_context
         global_context fdef
     in
     (* Execute the forward function *)
@@ -380,8 +379,7 @@ module Test = struct
       TODO: for now we ignore the functions which contain loops, because
       they are not supported by the symbolic interpreter.
    *)
-  let test_functions_symbolic (config : C.partial_config) (synthesize : bool)
-      (crate : A.crate) : unit =
+  let test_functions_symbolic (synthesize : bool) (crate : A.crate) : unit =
     (* Filter the functions which contain loops *)
     let no_loop_funs =
       List.filter
@@ -397,8 +395,8 @@ module Test = struct
       (* Execute the function - note that as the symbolic interpreter explores
        * all the path, some executions are expected to "panic": we thus don't
        * check the return value *)
-      test_function_symbolic config synthesize type_context fun_context
-        global_context def
+      test_function_symbolic synthesize type_context fun_context global_context
+        def
     in
     List.iter test_fun no_loop_funs
 end