diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Translate.ml | 13 | ||||
| -rw-r--r-- | src/main.ml | 33 |
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 *) |