improving support for pprinting Ail/Core to files.

the `fout` pp_annot is removed, instead the user can now use `--pp_core_out=FILE` and `--pp_ail_out=FILE`
to tell the pprinters (which are still enabled with `--pp`) to output in files instead of stdout.

the logic for disabling colours when outputing to files has also been fixed

backend/bmc/main.ml

@@ -101,7 +101,7 @@ let cerberus debug_level progress core_obj
   Bmc_globals.set bmc_max_depth bmc_seq bmc_conc bmc_fn bmc_debug
       bmc_all_execs bmc_output_model bmc_cat bmc_mode;
   set_cerb_conf "Bmc" exec exec_mode concurrency QuoteStd defacto false false false bmc;
-  let conf = { astprints; pprints; ppflags; debug_level; typecheck_core;
+  let conf = { astprints; pprints; ppflags; ppouts=[]; debug_level; typecheck_core;
                rewrite_core; sequentialise_core; cpp_cmd; cpp_stderr = true } in
   let prelude =
     (* Looking for and parsing the core standard library *)
@@ -403,9 +403,8 @@ let fs =
 
 let ppflags =
   let open Pipeline in
-  let doc = "Pretty print flags [annot: include location and ISO annotations,\
-             fout: output in a file]." in
-  Arg.(value & opt (list (enum ["annot", Annot; "fout", FOut])) [] &
+  let doc = "Pretty print flags [annot: include location and ISO annotations]." in
+  Arg.(value & opt (list (enum ["annot", Annot])) [] &
        info ["pp_flags"] ~doc)
 
 let files =

backend/cn/setup.ml

@@ -47,6 +47,7 @@ let conf incl_dirs incl_files astprints =
   ; pprints = []
   ; astprints = astprints
   ; ppflags = []
+  ; ppouts = []
   ; typecheck_core = true
   ; rewrite_core = true
   ; sequentialise_core = true

backend/common/pipeline.ml

@@ -8,18 +8,11 @@ let (>>=) = Exception.except_bind
 let (<$>)  = Exception.except_fmap
 let return = Exception.except_return
 
-let run_pp ?(remove_path = true) with_ext doc =
+let run_pp fout_opt doc =
   let (is_fout, oc) =
-    match with_ext with
-      | Some (filename, ext_str) ->
-         let open Filename in
-         let filename = 
-           if remove_path then remove_extension (basename filename) ^ "." ^ ext_str 
-           else remove_extension filename ^ "." ^ ext_str 
-         in
-         (true, Stdlib.open_out filename)
-      | None ->
-          (false, Stdlib.stdout) in
+    match fout_opt with
+      | Some filename -> true, Stdlib.open_out filename
+      | None -> false, Stdlib.stdout in
   let saved = !Cerb_colour.do_colour in
   Cerb_colour.do_colour := not is_fout;
   let term_col = match Cerb_util.terminal_size () with
@@ -73,13 +66,14 @@ type language =
   | Cabs | Ail | Core | Types
 
 type pp_flag =
-  | Annot | FOut
+  | Annot
 
 type configuration = {
   debug_level: int;
   pprints: language list;
   astprints: language list;
   ppflags: pp_flag list;
+  ppouts: (language * string) list;
   typecheck_core: bool;
   rewrite_core: bool;
   sequentialise_core: bool;
@@ -90,7 +84,7 @@ type configuration = {
 type io_helpers = {
   pass_message: string -> (unit, Errors.error) Exception.exceptM;
   set_progress: string -> (unit, Errors.error) Exception.exceptM;
-  run_pp: (string * string) option -> PPrint.document -> (unit, Errors.error) Exception.exceptM;
+  run_pp: string option -> PPrint.document -> (unit, Errors.error) Exception.exceptM;
   print_endline: string -> (unit, Errors.error) Exception.exceptM;
   print_debug: int -> (unit -> string) -> (unit, Errors.error) Exception.exceptM;
   warn: ?always:bool -> (unit -> string) -> (unit, Errors.error) Exception.exceptM;
@@ -109,8 +103,8 @@ let (default_io_helpers, get_progress) =
                  return ()
       end;
     run_pp = begin
-      fun opts doc -> run_pp opts doc;
-                      return ()
+      fun fout_opt doc -> run_pp fout_opt doc;
+                          return ()
       end;
     print_endline = begin
       fun str -> print_endline str;
@@ -173,8 +167,6 @@ let cpp (conf, io) ~filename =
 
 let c_frontend ?(cnnames=[]) (conf, io) (core_stdlib, core_impl) ~filename =
   Cerb_fresh.set_digest filename;
-  let wrap_fout z = if List.mem FOut conf.ppflags then z else None in
-  (* -- *)
   let parse filename file_content =
     C_parser_driver.parse_from_string ~filename file_content >>= fun cabs_tunit ->
     io.set_progress "CPARS" >>= fun () ->
@@ -186,6 +178,13 @@ let c_frontend ?(cnnames=[]) (conf, io) (core_stdlib, core_impl) ~filename =
       fun () -> io.warn (fun () -> "TODO: Cabs pprint to yet supported")
     end >>= fun () -> return cabs_tunit in
   (* -- *)
+  let mk_pp_program pp fout_opt file =
+    let fout_opt = List.assoc_opt Ail conf.ppouts in
+    let saved = !Cerb_colour.do_colour in
+    Cerb_colour.do_colour := Unix.isatty Unix.stdout && Option.is_none fout_opt;
+    let ret = pp file in
+    Cerb_colour.do_colour := saved;
+    ret in
   let desugar cabs_tunit =
     let (ailnames, core_stdlib_fun_map) = core_stdlib in
     Cabs_to_ail.desugar (ailnames, core_stdlib_fun_map, core_impl) cnnames
@@ -197,7 +196,9 @@ let c_frontend ?(cnnames=[]) (conf, io) (core_stdlib, core_impl) ~filename =
             fun () -> io.run_pp None (Pp_ail_ast.pp_program true false ail_prog)
           end
       >|> whenM (conf.debug_level > 4 && List.mem Ail conf.pprints) begin
-            fun () -> io.run_pp (wrap_fout (Some (filename, "ail"))) (Pp_ail.pp_program true false ail_prog)
+            fun () ->
+            let fout_opt = List.assoc_opt Ail conf.ppouts in
+            io.run_pp fout_opt (mk_pp_program (Pp_ail.pp_program ~show_include:false) fout_opt ail_prog)
           end
       >>= fun () -> return (markers_env, ail_prog) in
   (* -- *)
@@ -216,12 +217,13 @@ let c_frontend ?(cnnames=[]) (conf, io) (core_stdlib, core_impl) ~filename =
     end >>= fun () ->
     whenM (conf.debug_level <= 4 && List.mem Ail conf.pprints) begin
       fun () ->
+        let fout_opt = List.assoc_opt Ail conf.ppouts in
         let doc = if conf.debug_level = 4 then
           (* (for debug 4) pretty-printing Ail with type annotations *)
-          Pp_ail.pp_program_with_annot ailtau_prog
+          mk_pp_program Pp_ail.pp_program_with_annot fout_opt ailtau_prog
         else
-          Pp_ail.pp_program true false ailtau_prog in
-        io.run_pp (wrap_fout (Some (filename, "ail"))) doc
+          mk_pp_program (Pp_ail.pp_program ~show_include:false) fout_opt ailtau_prog in
+        io.run_pp fout_opt doc
     end >>= fun () -> return ailtau_prog in
   (* -- *)
   io.print_debug 2 (fun () -> "Using the C frontend") >>= fun () ->
@@ -505,15 +507,20 @@ let typed_core_passes (conf, io) core_file =
   return (untype_file typed_core_file'', typed_core_file'')
 
 let print_core (conf, io) ~filename core_file =
-  let wrap_fout z = if List.mem FOut conf.ppflags then z else None in
   whenM (List.mem Core conf.astprints) begin
     fun () ->
-      io.run_pp (wrap_fout (Some (filename, "core"))) (Pp_core_ast.pp_file core_file)
+      io.run_pp None (Pp_core_ast.pp_file core_file)
   end >>= fun () ->
   whenM (List.mem Core conf.pprints) begin
       fun () ->
-      let pp_file = if List.mem Annot conf.ppflags then Pp_core.WithStd.pp_file else Pp_core.Basic.pp_file in
-      io.run_pp (wrap_fout (Some (filename, "core"))) (pp_file core_file)
+      let fout_opt = List.assoc_opt Core conf.ppouts in
+      let pp_file file =
+        let saved = !Cerb_colour.do_colour in
+        Cerb_colour.do_colour := Unix.isatty Unix.stdout && Option.is_none fout_opt;
+        let ret = (if List.mem Annot conf.ppflags then Pp_core.WithStd.pp_file else Pp_core.Basic.pp_file) file in
+        Cerb_colour.do_colour := saved;
+        ret in
+      io.run_pp fout_opt (pp_file core_file)
   end >>= fun () ->
   return core_file
 

backend/common/pipeline.mli

@@ -4,13 +4,14 @@ type language =
   | Cabs | Ail | Core | Types
 
 type pp_flag =
-  | Annot | FOut
+  | Annot
 
 type configuration = {
   debug_level: int;
   pprints: language list;
   astprints: language list;
   ppflags: pp_flag list;
+  ppouts: (language * string) list;
   typecheck_core: bool;
   rewrite_core: bool;
   sequentialise_core: bool;
@@ -21,15 +22,15 @@ type configuration = {
 type io_helpers = {
   pass_message: string -> (unit, Errors.error) Exception.exceptM;
   set_progress: string -> (unit, Errors.error) Exception.exceptM;
-  run_pp: (string * string) option -> PPrint.document -> (unit, Errors.error) Exception.exceptM;
+  run_pp: string option -> PPrint.document -> (unit, Errors.error) Exception.exceptM;
   print_endline: string -> (unit, Errors.error) Exception.exceptM;
   print_debug: int -> (unit -> string) -> (unit, Errors.error) Exception.exceptM;
   warn: ?always:bool -> (unit -> string) -> (unit, Errors.error) Exception.exceptM;
 }
 val default_io_helpers: io_helpers
 val get_progress: unit -> int
 
-val run_pp: ?remove_path:bool -> (string * string) option -> PPrint.document -> unit
+val run_pp: string option -> PPrint.document -> unit
 
 val core_stdlib_path: unit -> string
 

backend/driver/main.ml

@@ -97,7 +97,7 @@ let cerberus debug_level progress core_obj
              link_lib_path link_core_obj
              impl_name
              exec exec_mode iso_switches switches batch concurrency
-             astprints pprints ppflags
+             astprints pprints ppflags pp_ail_out pp_core_out
              sequentialise_core rewrite_core typecheck_core defacto permissive ignore_bitfields
              fs_dump fs trace
              output_name
@@ -114,9 +114,17 @@ let cerberus debug_level progress core_obj
     | None -> []
     | Some args -> Str.split (Str.regexp "[ \t]+") args
   in
+  let ppouts =
+    match pp_ail_out with
+      | Some file -> [Ail, file]
+      | None -> [] in
+  let ppouts =
+    match pp_core_out with
+      | Some file -> (Core, file) :: ppouts
+      | None -> ppouts in
   (* set global configuration *)
   set_cerb_conf "Driver" exec exec_mode concurrency QuoteStd defacto permissive agnostic ignore_bitfields false;
-  let conf = { astprints; pprints; ppflags; debug_level; typecheck_core;
+  let conf = { astprints; pprints; ppflags; ppouts; debug_level; typecheck_core;
                rewrite_core; sequentialise_core; cpp_cmd; cpp_stderr = true } in
   let prelude =
     (* Looking for and parsing the core standard library *)
@@ -418,11 +426,18 @@ let fs =
 
 let ppflags =
   let open Pipeline in
-  let doc = "Pretty print flags [annot: include location and ISO annotations, \
-             fout: output in a file]." in
-  Arg.(value & opt (list (enum ["annot", Annot; "fout", FOut])) [] &
+  let doc = "Pretty print flags [annot: include location and ISO annotations]." in
+  Arg.(value & opt (list (enum ["annot", Annot ])) [] &
        info ["pp_flags"] ~doc)
 
+let pp_ail_out =
+  let doc = "Write Ail pprint to a file." in
+  Arg.(value & opt (some string) None & info ["pp_ail_out"] ~doc)
+
+let pp_core_out =
+  let doc = "Write Core pprint to a file." in
+  Arg.(value & opt (some string) None & info ["pp_core_out"] ~doc)
+
 let files =
   let doc = "source C or Core file" in
   Arg.(value & pos_all file [] & info [] ~docv:"FILE" ~doc)
@@ -494,7 +509,7 @@ let () =
                          impl $
                          exec $ exec_mode $ iso $ switches $ batch $
                          concurrency $
-                         astprints $ pprints $ ppflags $
+                         astprints $ pprints $ ppflags $ pp_ail_out $ pp_core_out $
                          sequentialise $ rewrite $ typecheck_core $ defacto $ permissive $ ignore_bitfields $
                          fs_dump $ fs $ trace $
                          output_file $

backend/web/instance.ml

@@ -36,6 +36,7 @@ let setup conf =
       pprints=            [];
       astprints=          [];
       ppflags=            [];
+      ppouts=             [];
       typecheck_core=     false;
       rewrite_core=       conf.rewrite_core;
       sequentialise_core= conf.sequentialise_core;
@@ -140,7 +141,7 @@ let result_of_elaboration (_, _, cabs, ail, core) =
   Elaboration
     { pp= {
         cabs= None;
-        ail=  mk_elab @@ Pp_ail.pp_program false false ail;
+        ail=  mk_elab @@ Cerb_colour.without_colour (Pp_ail.pp_program ~show_include:false) ail;
         core= Some (elim_paragraph_sym core)
       };
       ast= {

ocaml_frontend/pprinters/pp_ail.ml

@@ -892,8 +892,7 @@ let filter_external_decl (id, sigma) =
   let pred (_, (loc, _, _)) = Cerb_location.from_main_file loc in
   (id, { sigma with declarations = List.filter pred sigma.declarations} )
 
-let pp_program do_colour show_include ail_prog =
-  Cerb_colour.do_colour := do_colour && Unix.isatty Unix.stdout;
+let pp_program ~show_include ail_prog =
   let filtered_ail_prog = if show_include then ail_prog else filter_external_decl ail_prog in
   pp_program_aux (fun _ doc -> doc) filtered_ail_prog
 

ocaml_frontend/pprinters/pp_ail.mli

@@ -73,7 +73,7 @@ let pp_static_assertion (e, lit) =
   pp_keyword "_Static_assert" ^^ P.parens (pp_expression e ^^ P.comma ^^^ pp_stringLiteral lit)
 *)
 
-val pp_program: bool -> bool -> 'a ail_program -> PPrint.document
+val pp_program: show_include:bool -> 'a ail_program -> PPrint.document
 val pp_program_with_annot: GenTypes.genTypeCategory ail_program -> PPrint.document
 
 (* DEBUG *)