Add logging information

2 files changed, 26 insertions, 20 deletions

diff --git a/src/Translate.ml b/src/Translate.ml
index 8d9c0270..7dab7a90 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -342,7 +342,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   (* Open the output file *)
   (* First compute the filename by replacing the extension and converting the
    * case (rust module names are snake case) *)
-  let module_name, extract_filename =
+  let module_name, extract_filebasename =
     match Filename.chop_suffix_opt ~suffix:".cfim" filename with
     | None ->
         (* Note that we already checked the suffix upon opening the file *)
@@ -352,9 +352,11 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
         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 dest_dir (module_name ^ ".fst"))
+        (* Concatenate *)
+        (module_name, Filename.concat dest_dir module_name)
   in
+  (* Add the extension for F* *)
+  let extract_filename = extract_filebasename ^ ".fst" in
   let out = open_out extract_filename in
   let fmt = Format.formatter_of_out_channel out in
 
@@ -471,4 +473,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
 
   (* Close the box and end the formatting *)
   Format.pp_close_box fmt ();
-  Format.pp_print_newline fmt ()
+  Format.pp_print_newline fmt ();
+
+  (* Some logging *)
+  log#linfo (lazy ("Generated: " ^ extract_filename))
diff --git a/src/main.ml b/src/main.ml
index 38cb339a..2297f106 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -94,21 +94,21 @@ let () =
 
   (* 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.Warning;
-  main_log#set_level EL.Warning;
-  pre_passes_log#set_level EL.Warning;
-  interpreter_log#set_level EL.Warning;
-  statements_log#set_level EL.Warning;
-  paths_log#set_level EL.Warning;
-  expressions_log#set_level EL.Warning;
-  expansion_log#set_level EL.Warning;
-  borrows_log#set_level EL.Warning;
-  invariants_log#set_level EL.Warning;
-  pure_utils_log#set_level EL.Warning;
-  symbolic_to_pure_log#set_level EL.Warning;
-  pure_micro_passes_log#set_level EL.Warning;
-  pure_to_extract_log#set_level EL.Warning;
-  translate_log#set_level EL.Warning;
+  Easy_logging.Handlers.set_level main_logger_handler EL.Info;
+  main_log#set_level EL.Info;
+  pre_passes_log#set_level EL.Info;
+  interpreter_log#set_level EL.Info;
+  statements_log#set_level EL.Info;
+  paths_log#set_level EL.Info;
+  expressions_log#set_level EL.Info;
+  expansion_log#set_level EL.Info;
+  borrows_log#set_level EL.Info;
+  invariants_log#set_level EL.Info;
+  pure_utils_log#set_level EL.Info;
+  symbolic_to_pure_log#set_level EL.Info;
+  pure_micro_passes_log#set_level EL.Info;
+  pure_to_extract_log#set_level EL.Info;
+  translate_log#set_level EL.Info;
   (* Load the module *)
   let json = Yojson.Basic.from_file filename in
   match cfim_module_of_json json with
@@ -116,7 +116,8 @@ let () =
       main_log#error "error: %s\n" s;
       exit 1
   | Ok m ->
-      (* Print the module *)
+      (* Logging *)
+      main_log#linfo (lazy ("Imported: " ^ filename));
       main_log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
 
       (* Apply the pre-passes *)