Make the micro passes config a parameter of Translate.translate_module

2 files changed, 17 insertions, 12 deletions

diff --git a/src/Translate.ml b/src/Translate.ml
index e79a47c4..30d6d0f8 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -203,7 +203,8 @@ let translate_function_to_pure (config : C.partial_config)
   (* Return *)
   (pure_forward, pure_backwards)
 
-let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
+let translate_module_to_pure (config : C.partial_config)
+    (mp_config : Micro.config) (m : M.cfim_module) :
     trans_ctx * Pure.type_def list * pure_fun_translation list =
   (* Debug *)
   log#ldebug (lazy "translate_module_to_pure");
@@ -243,16 +244,9 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
   in
 
   (* Apply the micro-passes *)
-  (* TODO: move the configuration *)
-  let passes_config =
-    {
-      Micro.unfold_monadic_let_bindings = true;
-      filter_unused_monadic_calls = true;
-    }
-  in
   let pure_translations =
     List.map
-      (Micro.apply_passes_to_pure_fun_translation passes_config trans_ctx)
+      (Micro.apply_passes_to_pure_fun_translation mp_config trans_ctx)
       pure_translations
   in
 
@@ -269,9 +263,12 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
     ```
  *)
 let translate_module (filename : string) (config : C.partial_config)
-    (test_unit_functions : bool) (m : M.cfim_module) : unit =
+    (mp_config : Micro.config) (test_unit_functions : bool) (m : M.cfim_module)
+    : unit =
   (* Translate the module to the pure AST *)
-  let trans_ctx, trans_types, trans_funs = translate_module_to_pure config m in
+  let trans_ctx, trans_types, trans_funs =
+    translate_module_to_pure config mp_config m
+  in
 
   (* Initialize the extraction context - for now we extract only to F* *)
   let names_map =
diff --git a/src/main.ml b/src/main.ml
index bb7b0e06..7f7ed96c 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -6,6 +6,7 @@ module A = CfimAst
 module I = Interpreter
 module EL = Easy_logging.Logging
 module TA = TypesAnalysis
+module Micro = PureMicroPasses
 
 (* This is necessary to have a backtrace when raising exceptions - for some
  * reason, the -g option doesn't work.
@@ -85,4 +86,11 @@ let () =
 
       (* Translate the functions *)
       let test_unit_functions = true in
-      Translate.translate_module !filename config test_unit_functions m
+      let micro_passes_config =
+        {
+          Micro.unfold_monadic_let_bindings = true;
+          filter_unused_monadic_calls = true;
+        }
+      in
+      Translate.translate_module !filename config micro_passes_config
+        test_unit_functions m