diff options
| -rw-r--r-- | src/Translate.ml | 51 |
1 files changed, 19 insertions, 32 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index 5a00db64..ab9ed216 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -433,45 +433,32 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) let out = open_out filename in let fmt = Format.formatter_of_out_channel out in - (* TODO: we actually don't want to use the formatter for the headers, - * because we want to make sure we introduce proper line breaks (it is - * as long as we end with a line break, so that the formatter is - * not lost in its count *) + (* Print the headers. + * Note that we don't use the OCaml formatter for purpose: we want to control + * line insertion (we have to make sure that some instructions like `open MODULE` + * are printed on one line!). + * This is ok as long as we end up with a line break, so that the formatter's + * internal count is consistent with the state of the file. + *) + (* Create the header *) + Printf.fprintf out "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n"; + Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg; + Printf.fprintf out "module %s\n" module_name; + Printf.fprintf out "open Primitives\n"; + (* Add the custom imports *) + List.iter (fun m -> Printf.fprintf out "open %s\n" m) custom_imports; + (* Add the custom includes *) + List.iter (fun m -> Printf.fprintf out "include %s\n" m) custom_includes; + (* Z3 options *) + Printf.fprintf out "\n#set-options \"--z3rlimit 50 --fuel 0 --ifuel 1\"\n"; + (* From now onwards, we use the formatter *) (* Set the margin *) Format.pp_set_margin fmt 80; (* Create a vertical box *) Format.pp_open_vbox fmt 0; - (* Create the header *) - Format.pp_print_string fmt - "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)"; - Format.pp_print_break fmt 0 0; - Format.pp_print_string fmt - ("(** [" ^ rust_module_name ^ "]" ^ custom_msg ^ " *)"); - Format.pp_print_break fmt 0 0; - Format.pp_print_string fmt ("module " ^ module_name); - Format.pp_print_break fmt 0 0; - Format.pp_print_string fmt "open Primitives"; - (* Add the custom imports *) - List.iter - (fun m -> - Format.pp_print_break fmt 0 0; - Format.pp_print_string fmt ("open " ^ m)) - custom_imports; - (* Add the custom includes *) - List.iter - (fun m -> - Format.pp_print_break fmt 0 0; - Format.pp_print_string fmt ("include " ^ m)) - custom_includes; - (* Z3 options *) - Format.pp_print_break fmt 0 0; - Format.pp_print_break fmt 0 0; - Format.pp_print_string fmt "#set-options \"--z3rlimit 50 --fuel 0 --ifuel 1\""; - Format.pp_print_break fmt 0 0; - (* Extract the definitions *) extract_definitions fmt config ctx; |