Introduce a translation config in Translate.ml

2 files changed, 30 insertions, 19 deletions

diff --git a/src/Translate.ml b/src/Translate.ml
index c6db9f19..ba3effc5 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -12,6 +12,20 @@ open TranslateCore
 (** The local logger *)
 let log = TranslateCore.log
 
+type config = {
+  eval_config : Contexts.partial_config;
+  mp_config : Micro.config;
+  test_unit_functions : bool;
+      (** If true, insert tests in the generated files to check that the
+          unit functions normalize to `Success _`.
+          
+          For instance, in F* it generates code like this:
+          ```
+          let _ = assert_norm (FUNCTION () = Success ())
+          ```
+       *)
+}
+
 type symbolic_fun_translation = V.symbolic_value list * SA.expression
 (** The result of running the symbolic interpreter on a function:
     - the list of symbolic values used for the input values
@@ -272,21 +286,12 @@ let translate_module_to_pure (config : C.partial_config)
   (* Return *)
   (trans_ctx, type_defs, pure_translations)
 
-(** Translate a module and write the synthesized code to an output file.
-
-    [test_unit_functions]: if true, insert tests in the generated files to
-    check that the unit functions normalize to `Success _`. For instance,
-    in F* it generates code like this:
-    ```
-    let _ = assert_norm (FUNCTION () = Success ())
-    ```
- *)
-let translate_module (filename : string) (dest_dir : string)
-    (config : C.partial_config) (mp_config : Micro.config)
-    (test_unit_functions : bool) (m : M.cfim_module) : unit =
+(** Translate a module and write the synthesized code to an output file. *)
+let translate_module (filename : string) (dest_dir : string) (config : config)
+    (m : M.cfim_module) : unit =
   (* Translate the module to the pure AST *)
   let trans_ctx, trans_types, trans_funs =
-    translate_module_to_pure config mp_config m
+    translate_module_to_pure config.eval_config config.mp_config m
   in
 
   (* Initialize the extraction context - for now we extract only to F* *)
@@ -413,7 +418,7 @@ let translate_module (filename : string) (dest_dir : string)
         ExtractToFStar.extract_fun_def extract_ctx fmt qualif def)
       fls;
     (* Insert unit tests if necessary *)
-    if test_unit_functions then
+    if config.test_unit_functions then
       List.iter
         (fun (keep_fwd, (fwd, _)) ->
           if keep_fwd then
diff --git a/src/main.ml b/src/main.ml
index ba677361..38cb339a 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -123,7 +123,7 @@ let () =
       let m = PrePasses.apply_passes m in
 
       (* Some options for the execution *)
-      let config =
+      let eval_config =
         {
           C.check_invariants = true;
           greedy_expand_symbolics_with_borrows = true;
@@ -132,12 +132,12 @@ let () =
       in
 
       (* Test the unit functions with the concrete interpreter *)
-      if !test_units then I.Test.test_unit_functions config m;
+      if !test_units then I.Test.test_unit_functions eval_config m;
 
       (* 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;
+      I.Test.test_functions_symbolic eval_config synthesize m;
 
       (* Translate the functions *)
       let test_unit_functions = !test_trans_units in
@@ -150,5 +150,11 @@ let () =
           add_unit_args = false;
         }
       in
-      Translate.translate_module filename dest_dir config micro_passes_config
-        test_unit_functions m
+      let trans_config =
+        {
+          Translate.eval_config;
+          mp_config = micro_passes_config;
+          test_unit_functions;
+        }
+      in
+      Translate.translate_module filename dest_dir trans_config m