summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-02-10 10:51:16 +0100
committerSon Ho2022-02-10 10:51:16 +0100
commit0e14dadbfcc0dc11c899fb81fec759fa4cb634b0 (patch)
treec8443aaada3454a58b256aca651ae3b0b4b6cfbf /src
parentaa307d8b11de93a65dd6e67c12dc7418078b8eca (diff)
Print the generated file headers with Printf rather than the formatter
Diffstat (limited to 'src')
-rw-r--r--src/Translate.ml51
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;