summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-09 12:38:29 +0100
committerSon Ho2022-02-09 12:38:29 +0100
commitfa5815de72b983bcbf87b4ec3e57d459632bb0d8 (patch)
treecfc76232ebbe841981e155c46c935bbb1f056e2c
parentb9dd3ed9b70246449ce1c856175d8f6ff28a6049 (diff)
Add logging information
-rw-r--r--src/Translate.ml13
-rw-r--r--src/main.ml33
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 *)