aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-08-24 17:36:36 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-08-24 17:36:36 +0000
commit7993d50d0d1dd029b34745e1ee089d9cf7c5ffbd (patch)
treec63659baaa5fbb525c6fc1cb4ad882e8e6b55e1c /plugins
parent6a2f9c59ea44d754050b4a2ccb624adcc846924d (diff)
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
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extract_env.ml8
-rw-r--r--plugins/extraction/haskell.ml16
-rw-r--r--plugins/extraction/miniml.mli6
-rw-r--r--plugins/extraction/ocaml.ml9
-rw-r--r--plugins/extraction/scheme.ml7
-rw-r--r--plugins/extraction/table.ml12
-rw-r--r--plugins/extraction/table.mli4
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