Experimental support for a comment in the files' preamble in extraction.

Scheme comments are output on a single line because Ocaml's Format
module which serves as a backend to Pp has an integer, rather than a string
as identation value, so we cannot make it so that each new line in the
comment starts with ";; ".

I've tried something with Pp.ifb but it was hackish at best and had somewhat
strange results.

Known bug: as Pp.std_ppcmds is non-persistent, the comment is actually printed
only once per Extraction command, even if it outputs several files.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15763 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 47 insertions, 15 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 292ae7955..588fe0cf2 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -470,10 +470,14 @@ let print_structure_to_file (fn,si,mo) dry struc =
   (* Print the implementation *)
   let cout = if dry then None else Option.map open_out fn in
   let ft = formatter dry cout in
+  let file_comment =
+    let split_comment = Str.split (Str.regexp "[ \t\n]+") (file_comment ()) in
+    prlist_with_sep spc str split_comment
+  in
   begin try
     (* The real printing of the implementation *)
     set_phase Impl;
-    pp_with ft (d.preamble mo opened unsafe_needs);
+    pp_with ft (d.preamble mo file_comment opened unsafe_needs);
     pp_with ft (d.pp_struct struc);
     Option.iter close_out cout;
   with e ->
@@ -487,7 +491,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
        let ft = formatter false (Some cout) in
        begin try
 	 set_phase Intf;
-	 pp_with ft (d.sig_preamble mo opened unsafe_needs);
+	 pp_with ft (d.sig_preamble mo file_comment opened unsafe_needs);
 	 pp_with ft (d.pp_sig (signature_of_structure struc));
 	 close_out cout;
        with e ->
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 1a9f27552..2bc2306f1 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -33,13 +33,19 @@ let keywords =
     "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
   Idset.empty
 
-let preamble mod_name used_modules usf =
+let pp_comment s = str "-- " ++ s ++ fnl ()
+let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}"
+
+let preamble mod_name comment used_modules usf =
   let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n")
   in
   (if not usf.magic then mt ()
    else
-     str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++
-     str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n")
+     str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}" ++ fnl () ++
+     str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}")
+  ++ fnl () ++ fnl ()
+  ++
+  pp_bracket_comment comment ++ fnl () ++ fnl ()
   ++
   str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++
   str "import qualified Prelude" ++ fnl () ++
@@ -231,8 +237,6 @@ and pp_function env f t =
 
 (*s Pretty-printing of inductive types declaration. *)
 
-let pp_comment s = str "-- " ++ s ++ fnl ()
-
 let pp_logical_ind packet =
   pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
   pp_comment (str "with constructors : " ++
@@ -359,7 +363,7 @@ let haskell_descr = {
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
-  sig_preamble = (fun _ _ _ -> mt ());
+  sig_preamble = (fun _ s _ _ -> (pp_bracket_comment s)++fnl());
   pp_sig = (fun _ -> mt ());
   pp_decl = pp_decl;
 }
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 76ceb797a..261a2c6ee 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -195,12 +195,14 @@ type language_descr = {
 
   (* Concerning the source file *)
   file_suffix : string;
-  preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
+  (* the second argument is a comment to add to the preamble *)
+  preamble : identifier -> std_ppcmds -> module_path list -> unsafe_needs -> std_ppcmds;
   pp_struct : ml_structure -> std_ppcmds;
 
   (* Concerning a possible interface file *)
   sig_suffix : string option;
-  sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
+  (* the second argument is a comment to add to the preamble *)
+  sig_preamble : identifier -> std_ppcmds -> module_path list -> unsafe_needs -> std_ppcmds;
   pp_sig : ml_signature -> std_ppcmds;
 
   (* for an isolated declaration print *)
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index be2ad57bf..3d21fc2d8 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -62,7 +62,10 @@ let keywords =
 
 let pp_open mp = str ("open "^ string_of_modfile mp ^"\n")
 
-let preamble _ used_modules usf =
+let pp_comment s = str "(* " ++ hov 0 s ++ str " *)"
+
+let preamble _ comment used_modules usf =
+  pp_comment comment ++ fnl () ++ fnl () ++
   prlist pp_open used_modules ++
   (if used_modules = [] then mt () else fnl ()) ++
   (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++
@@ -71,7 +74,8 @@ let preamble _ used_modules usf =
    else mt ()) ++
   (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ())
 
-let sig_preamble _ used_modules usf =
+let sig_preamble _ comment used_modules usf =
+  pp_comment comment ++ fnl () ++ fnl () ++
   prlist pp_open used_modules ++
   (if used_modules = [] then mt () else fnl ()) ++
   (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt())
@@ -413,7 +417,6 @@ let pp_equiv param_list name = function
   | RenEquiv ren, _  ->
       str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
 
-let pp_comment s = str "(* " ++ s ++ str " *)"
 
 let pp_one_ind prefix ip_equiv pl name cnames ctyps =
   let pl = rename_tvars keywords pl in
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 03a7c2006..27529258b 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -28,7 +28,10 @@ let keywords =
       "error"; "delay"; "force"; "_"; "__"]
     Idset.empty
 
-let preamble _ _ usf =
+let pp_comment s = str";; "++h 0 s++fnl ()
+
+let preamble _ comment _ usf =
+  pp_comment comment ++ fnl () ++
   str ";; This extracted scheme code relies on some additional macros\n" ++
   str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme\n" ++
   str "(load \"macros_extr.scm\")\n\n" ++
@@ -223,7 +226,7 @@ let scheme_descr = {
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
-  sig_preamble = (fun _ _ _ -> mt ());
+  sig_preamble = (fun _ s _ _ -> pp_comment s ++ fnl () ++ fnl ());
   pp_sig = (fun _ -> mt ());
   pp_decl = pp_decl;
 }
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 3fb183995..1fd4840fe 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -547,6 +547,18 @@ let _ = declare_bool_option
    optwrite = (fun b -> conservative_types_ref := b) }
 
 
+(* Allows to print a comment at the beginning of the output files *)
+let file_comment_ref = ref ""
+let file_comment () = !file_comment_ref
+
+let _ = declare_string_option
+  {optsync = true;
+   optdepr = false;
+   optname = "Extraction File Comment";
+   optkey = ["Extraction"; "File"; "Comment"];
+   optread = (fun () -> !file_comment_ref);
+   optwrite = (fun s -> file_comment_ref := s) }
+
 (*s Extraction Lang *)
 
 type lang = Ocaml | Haskell | Scheme
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index b17f83715..16c2275f1 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -136,6 +136,10 @@ val optims :  unit -> opt_flag
 
 val conservative_types : unit -> bool
 
+(*s A comment to print at the beginning of the files *)
+
+val file_comment : unit -> string
+
 (*s Target language. *)
 
 type lang = Ocaml | Haskell | Scheme