From 0e14dadbfcc0dc11c899fb81fec759fa4cb634b0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 10 Feb 2022 10:51:16 +0100
Subject: Print the generated file headers with Printf rather than the
 formatter

---
 src/Translate.ml | 51 +++++++++++++++++++--------------------------------
 1 file 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;
 
-- 
cgit v1.2.3