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

1 files changed, 21 insertions, 63 deletions

diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 6f0e8074..304d0f2f 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -1,6 +1,5 @@
 open Aeneas.LlbcOfJson
 open Aeneas.Logging
-open Aeneas.Print
 module T = Aeneas.Types
 module A = Aeneas.LlbcAst
 module I = Aeneas.Interpreter
@@ -10,6 +9,7 @@ module Micro = Aeneas.PureMicroPasses
 module Print = Aeneas.Print
 module PrePasses = Aeneas.PrePasses
 module Translate = Aeneas.Translate
+open Aeneas.Config
 
 (* This is necessary to have a backtrace when raising exceptions - for some
  * reason, the -g option doesn't work.
@@ -30,25 +30,12 @@ let () =
 
   (* Read the command line arguments *)
   let dest_dir = ref "" in
-  let decompose_monads = ref false in
-  let unfold_monads = ref true in
-  let filter_useless_calls = ref true in
-  let filter_useless_functions = ref true in
-  let test_units = ref false in
-  let test_trans_units = ref false in
-  let no_decreases_clauses = ref false in
-  let no_state = ref false in
-  (* [backward_no_state_update]: see the comment for {!Translate.config.backward_no_state_update} *)
-  let backward_no_state_update = ref false in
-  let template_decreases_clauses = ref false in
-  let no_split_files = ref false in
-  let no_check_inv = ref false in
 
   let spec =
     [
       ("-dest", Arg.Set_string dest_dir, " Specify the output directory");
       ( "-decompose-monads",
-        Arg.Set decompose_monads,
+        Arg.Set decompose_monadic_let_bindings,
         " Decompose the monadic let-bindings.\n\n\
         \         Introduces a temporary variable which is later decomposed,\n\
         \         when the pattern on the left of the monadic let is not a \n\
@@ -59,49 +46,49 @@ let () =
         \         `tmp <-- f (); let (x, y) = tmp in ...`\n\
         \        " );
       ( "-unfold-monads",
-        Arg.Set unfold_monads,
+        Arg.Set unfold_monadic_let_bindings,
         " Unfold the monadic let-bindings to matches" );
-      ( "-filter-useless-calls",
-        Arg.Set filter_useless_calls,
-        " Filter the useless function calls, when possible" );
-      ( "-filter-useless-funs",
-        Arg.Set filter_useless_functions,
-        " Filter the useless forward/backward functions" );
+      ( "-no-filter-useless-calls",
+        Arg.Clear filter_useless_monadic_calls,
+        " Do not filter the useless function calls, when possible" );
+      ( "-no-filter-useless-funs",
+        Arg.Clear filter_useless_functions,
+        " Do not filter the useless forward/backward functions" );
       ( "-test-units",
-        Arg.Set test_units,
+        Arg.Set test_unit_functions,
         " Test the unit functions with the concrete interpreter" );
       ( "-test-trans-units",
-        Arg.Set test_trans_units,
+        Arg.Set test_trans_unit_functions,
         " Test the translated unit functions with the target theorem\n\
         \                         prover's normalizer" );
       ( "-no-decreases-clauses",
-        Arg.Set no_decreases_clauses,
+        Arg.Clear extract_decreases_clauses,
         " Do not add decrease clauses to the recursive definitions" );
       ( "-no-state",
-        Arg.Set no_state,
+        Arg.Clear use_state,
         " Do not use state-error monads, simply use error monads" );
       ( "-backward-no-state-update",
         Arg.Set backward_no_state_update,
         " Forbid backward functions from updating the state" );
       ( "-template-clauses",
-        Arg.Set template_decreases_clauses,
+        Arg.Set extract_template_decreases_clauses,
         " Generate templates for the required decreases clauses, in a\n\
         \                         dedicated file. Incompatible with \
          -no-decreases-clauses" );
       ( "-no-split-files",
-        Arg.Set no_split_files,
+        Arg.Clear split_files,
         " Don't split the definitions between different files for types,\n\
         \                         functions, etc." );
       ( "-no-check-inv",
-        Arg.Set no_check_inv,
+        Arg.Clear check_invariants,
         " Deactivate the invariant sanity checks performed at every step of\n\
         \                         evaluation. Dramatically saves speed." );
     ]
   in
   (* Sanity check: -template-clauses ==> not -no-decrease-clauses *)
-  assert ((not !no_decreases_clauses) || not !template_decreases_clauses);
+  assert (!extract_decreases_clauses || not !extract_template_decreases_clauses);
   (* Sanity check: -backward-no-state-update ==> not -no-state *)
-  assert ((not !backward_no_state_update) || not !no_state);
+  assert ((not !backward_no_state_update) || !use_state);
 
   let spec = Arg.align spec in
   let filenames = ref [] in
@@ -169,46 +156,17 @@ let () =
       let m = PrePasses.apply_passes m in
 
       (* Some options for the execution *)
-      let eval_config =
-        {
-          C.check_invariants = not !no_check_inv;
-          greedy_expand_symbolics_with_borrows = true;
-          allow_bottom_below_borrow = true;
-          return_unit_end_abs_with_no_loans = true;
-        }
-      in
 
       (* Test the unit functions with the concrete interpreter *)
-      if !test_units then I.Test.test_unit_functions eval_config m;
+      if !test_unit_functions then I.Test.test_unit_functions 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 eval_config synthesize m;
+      I.Test.test_functions_symbolic synthesize m;
 
       (* Translate the functions *)
-      let test_unit_functions = !test_trans_units in
-      let micro_passes_config =
-        {
-          Micro.decompose_monadic_let_bindings = !decompose_monads;
-          unfold_monadic_let_bindings = !unfold_monads;
-          filter_useless_monadic_calls = !filter_useless_calls;
-          filter_useless_functions = !filter_useless_functions;
-        }
-      in
-      let trans_config =
-        {
-          Translate.eval_config;
-          mp_config = micro_passes_config;
-          split_files = not !no_split_files;
-          test_unit_functions;
-          extract_decreases_clauses = not !no_decreases_clauses;
-          extract_template_decreases_clauses = !template_decreases_clauses;
-          use_state = not !no_state;
-          backward_no_state_update = !backward_no_state_update;
-        }
-      in
-      Translate.translate_module filename dest_dir trans_config m;
+      Translate.translate_module filename dest_dir m;
 
       (* Print total elapsed time *)
       log#linfo