Extraction Blacklist : a new command for avoiding conflicts with existing files

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

6 files changed, 114 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index df1b82a98..fbb3b5541 100644
--- a/CHANGES
+++ b/CHANGES
@@ -436,6 +436,9 @@ Extraction
   possible if several branches are identical. For instance, functions
   corresponding to decidability of equalities are now linear instead of 
   quadratic.
+- A new instruction Extraction Blacklist id1 .. idn allows to prevent filename
+  conflits with existing code, for instance when extracting module List
+  to Ocaml. 
 
 CoqIDE
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index aac44a6ff..e59c5811f 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -348,8 +348,13 @@ let mono_filename f =
 
 let module_filename m =
   let d = descr () in
-  let f = if d.capital_file then String.capitalize else String.uncapitalize in
-  let fn = f (string_of_id m) in
+  let fc = String.capitalize (string_of_id m) in
+  let fn =
+    if is_blacklisted fc then
+      if d.capital_file then "Coq_"^fc else "coq_"^fc
+    else
+      if d.capital_file then fc else String.uncapitalize fc
+  in
   Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, m
 
 (*s Extraction of one decl to stdout. *)
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index d89d855b3..2b561616b 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -89,6 +89,23 @@ VERNAC COMMAND EXTEND ResetExtractionInline
   -> [ reset_extraction_inline () ]
 END
 
+VERNAC COMMAND EXTEND ExtractionBlacklist
+(* Force Extraction to not use some filenames *)
+| [ "Extraction" "Blacklist" ne_ident_list(l) ]
+  -> [ extraction_blacklist l ]
+END
+
+VERNAC COMMAND EXTEND PrintExtractionBlacklist
+| [ "Print" "Extraction" "Blacklist" ]
+  -> [ print_extraction_blacklist () ]
+END
+
+VERNAC COMMAND EXTEND ResetExtractionBlacklist
+| [ "Reset" "Extraction" "Blacklist" ]
+  -> [ reset_extraction_blacklist () ]
+END
+
+
 (* Overriding of a Coq object by an ML one *)
 VERNAC COMMAND EXTEND ExtractionConstant
 | [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ]
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 1612c8dd8..f653b3a48 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -507,6 +507,62 @@ let (reset_inline,_) =
 
 let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
+(*s Extraction Blacklist of filenames not to use while extracting *)
+
+let blacklist_table = ref Stringset.empty
+
+let is_blacklisted s =
+ (Stringset.mem (String.capitalize s) !blacklist_table) ||
+ (Stringset.mem (String.uncapitalize s) !blacklist_table)
+
+let string_of_modfile mp =
+  let s = string_of_modfile mp in
+  if is_blacklisted s then "Coq_"^s else s
+
+let add_blacklist_entries l =
+  blacklist_table := List.fold_right Stringset.add l !blacklist_table
+
+(* Registration of operations for rollback. *)
+
+let (blacklist_extraction,_) =
+  declare_object
+    {(default_object "Extraction Blacklist") with
+       cache_function = (fun (_,l) -> add_blacklist_entries l);
+       load_function = (fun _ (_,l) -> add_blacklist_entries l);
+       export_function = (fun x -> Some x);
+       classify_function = (fun (_,o) -> Libobject.Keep o);
+       subst_function = (fun (_,_,x) -> x)
+    }
+
+let _ = declare_summary "Extraction Blacklist"
+	  { freeze_function = (fun () -> !blacklist_table);
+	    unfreeze_function = ((:=) blacklist_table);
+	    init_function = (fun () -> blacklist_table := Stringset.empty);
+	    survive_module = true;
+	    survive_section = true }
+
+(* Grammar entries. *)
+
+let extraction_blacklist l =
+  let l = List.rev_map string_of_id l in
+  Lib.add_anonymous_leaf (blacklist_extraction l)
+
+(* Printing part *)
+
+let print_extraction_blacklist () =
+  msgnl
+    (prlist_with_sep fnl str (Stringset.elements !blacklist_table))
+
+(* Reset part *)
+
+let (reset_blacklist,_) =
+  declare_object
+    {(default_object "Reset Extraction Blacklist") with
+       cache_function = (fun (_,_)-> blacklist_table := Stringset.empty);
+       load_function = (fun _ (_,_)-> blacklist_table := Stringset.empty);
+       export_function = (fun x -> Some x)}
+
+let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 
 (*s Extract Constant/Inductive. *)
 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index fc29e871c..608eb6771 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -141,6 +141,13 @@ val extract_constant_inline :
   bool -> reference -> string list -> string -> unit
 val extract_inductive : reference -> string * string list -> unit
 
+(*s Table of blacklisted filenames *)
+
+val is_blacklisted : string -> bool
+
+val extraction_blacklist : identifier list -> unit
+val reset_extraction_blacklist : unit -> unit
+val print_extraction_blacklist : unit -> unit
 
 
 
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index da9b3e717..ba07182a6 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -282,6 +282,30 @@ Extract Inductive list => "list" [ "[]" "(::)" ].
 Extract Inductive prod => "(*)"  [ "(,)" ].
 \end{coq_example}
 
+\asubsection{Avoiding conflicts with existing filenames}
+
+\comindex{Extraction Blaclist}
+
+When using {\tt Extraction Library}, the names of the extracted files
+directly depends from the names of the \Coq\ files. It may happen that
+these filenames are in conflict with already existing files, 
+either in the standard library of the target language or in other
+code that is meant to be linked with the extracted code. 
+For instance the module {\tt List} exists both in \Coq\ and in Ocaml.
+It is possible to instruct the extraction not to use particular filenames.
+
+\begin{description}
+\item{\tt Extraction Blacklist \ident \ldots \ident.} ~\par
+  Instruct the extraction to avoid using these names as filenames
+  for extracted code. 
+\item{\tt Print Extraction Blacklist.} ~\par
+  Show the current list of filenames the extraction should avoid.
+\item{\tt Reset Extraction Blacklist.} ~\par
+  Allow the extraction to use any filename.
+\end{description}
+
+For Ocaml, a typical use of these commands is
+{\tt Extraction Blacklist String List}.
 
 \asection{Differences between \Coq\ and ML type systems}