2 files changed, 62 insertions, 27 deletions

diff --git a/src/Translate.ml b/src/Translate.ml
index 30d6d0f8..ba975c60 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -262,9 +262,9 @@ let translate_module_to_pure (config : C.partial_config)
     let _ = assert_norm (FUNCTION () = Success ())
     ```
  *)
-let translate_module (filename : string) (config : C.partial_config)
-    (mp_config : Micro.config) (test_unit_functions : bool) (m : M.cfim_module)
-    : unit =
+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 the module to the pure AST *)
   let trans_ctx, trans_types, trans_funs =
     translate_module_to_pure config mp_config m
@@ -309,13 +309,12 @@ let translate_module (filename : string) (config : C.partial_config)
         (* Note that we already checked the suffix upon opening the file *)
         failwith "Unreachable"
     | Some filename ->
-        (* Split between basename and dirname *)
-        let dirname = Filename.dirname filename in
+        (* Retrieve the file basename *)
         let basename = Filename.basename filename in
         (* Convert the case *)
         let module_name = StringUtils.to_camel_case basename in
         (* We add the extension for F* *)
-        (module_name, Filename.concat dirname (module_name ^ ".fst"))
+        (module_name, Filename.concat dest_dir (module_name ^ ".fst"))
   in
   let out = open_out extract_filename in
   let fmt = Format.formatter_of_out_channel out in
diff --git a/src/main.ml b/src/main.ml
index 0eaff02d..95bebf39 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -15,7 +15,7 @@ let () = Printexc.record_backtrace true
 
 let usage =
   Printf.sprintf
-    {|Aeneas: verification of Rust programs by translation
+    {|Aeneas: verification of Rust programs by translation to pure lambda calculus
 
 Usage: %s [OPTIONS] FILE
 |}
@@ -23,26 +23,62 @@ Usage: %s [OPTIONS] FILE
 
 let () =
   (* Read the command line arguments *)
-  let spec = [] in
+  let dest_dir = ref "" in
+  let decompose_monads = ref false in
+  let unfold_monads = ref true in
+  let filter_unused_calls = ref true in
+
+  let spec =
+    [
+      ("-dest", Arg.Set_string dest_dir, " Specify the output directory");
+      ( "-decompose-monads",
+        Arg.Set decompose_monads,
+        " 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\
+        \         variable.\n\
+        \         \n\
+        \         Example:\n\
+        \         `(x, y) <-- f (); ...` ~~>\n\
+        \         `tmp <-- f (); let (x, y) = tmp in ...`\n\
+        \        " );
+      ( "-unfold-monads",
+        Arg.Set unfold_monads,
+        " Unfold the monadic let-bindings to matches" );
+      ( "-filter-unused-calls",
+        Arg.Set filter_unused_calls,
+        " Filter the unused function calls, when possible" );
+    ]
+  in
   let spec = Arg.align spec in
-  let filename = ref "" in
+  let filenames = ref [] in
+  let add_filename f = filenames := f :: !filenames in
+  Arg.parse spec add_filename usage;
   let fail () =
     print_string usage;
     exit 1
   in
-  Arg.parse spec
-    (fun f ->
-      if not (Filename.check_suffix f ".cfim") then (
-        print_string "Unrecognized file extension";
-        fail ())
-      else if not (Sys.file_exists f) then (
-        print_string "File not found";
-        fail ())
-      else filename := f)
-    usage;
-  if !filename = "" then (
-    print_string usage;
-    exit 1);
+  (* Retrieve and check the filename *)
+  let filename =
+    match !filenames with
+    | [ f ] ->
+        if not (Filename.check_suffix f ".cfim") then (
+          print_string "Unrecognized file extension";
+          fail ())
+        else if not (Sys.file_exists f) then (
+          print_string "File not found";
+          fail ())
+        else f
+    | _ ->
+        (* For now, we only process one file at a time *)
+        print_string usage;
+        exit 1
+  in
+  (* Check the destination directory *)
+  let dest_dir =
+    if !dest_dir = "" then Filename.dirname filename else !dest_dir
+  in
+
   (* Set up the logging - for now we use default values - TODO: use the
    * command-line arguments *)
   Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
@@ -59,7 +95,7 @@ let () =
   pure_to_extract_log#set_level EL.Debug;
   translate_log#set_level EL.Debug;
   (* Load the module *)
-  let json = Yojson.Basic.from_file !filename in
+  let json = Yojson.Basic.from_file filename in
   match cfim_module_of_json json with
   | Error s ->
       main_log#error "error: %s\n" s;
@@ -88,10 +124,10 @@ let () =
       let test_unit_functions = true in
       let micro_passes_config =
         {
-          Micro.decompose_monadic_let_bindings = false;
-          unfold_monadic_let_bindings = true;
-          filter_unused_monadic_calls = true;
+          Micro.decompose_monadic_let_bindings = !decompose_monads;
+          unfold_monadic_let_bindings = !unfold_monads;
+          filter_unused_monadic_calls = !filter_unused_calls;
         }
       in
-      Translate.translate_module !filename config micro_passes_config
+      Translate.translate_module filename dest_dir config micro_passes_config
         test_unit_functions m