Extraction Library Foo creates Foo.ml, not foo.ml

 And similarly for Haskell: we do not force capitalized/uncapitalized
 filenames anymore, but we rather follow the name of the .v file (with
 new extensions of course). Ok, this is an incompatible change, but
 it is really convenient, some people where actually already doing
 some hacks to have this behavior (cf. Compcert).

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

8 files changed, 16 insertions, 10 deletions

diff --git a/CHANGES b/CHANGES
index ac5b4a7917..1d90d85ba7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -134,6 +134,9 @@ Module system
 
 Extraction
 
+- When using (Recursive) Extraction Library, the filenames are directly the
+  Coq ones with new appropriate extensions : we do not force anymore
+  uncapital first letters for Ocaml and capital ones for Haskell.
 - The extraction now tries harder to avoid code transformations that can be
   dangerous for the complexity. In particular many eta-expansions at the top
   of functions body are now avoided, clever partial applications will likely
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index b1195b4be5..db7504e3eb 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -370,11 +370,10 @@ let mono_filename f =
 
 (* Builds a suitable filename from a module id *)
 
-let module_filename fc =
+let module_filename mp =
+  let f = file_of_modfile mp in
   let d = descr () in
-  let fn = if d.capital_file then fc else String.uncapitalize fc
-  in
-  Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, id_of_string fc
+  Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f
 
 (*s Extraction of one decl to stdout. *)
 
@@ -531,8 +530,7 @@ let extraction_library is_rec m =
   let print = function
     | (MPfile dir as mp, sel) as e ->
 	let dry = not is_rec && dir <> dir_m in
-	let s = string_of_modfile mp in
-	print_structure_to_file (module_filename s) dry [e]
+	print_structure_to_file (module_filename mp) dry [e]
     | _ -> assert false
   in
   List.iter print struc;
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index e03c7313af..d428406131 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -336,7 +336,6 @@ let pp_struct =
 let haskell_descr = {
   keywords = keywords;
   file_suffix = ".hs";
-  capital_file = true;
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index a1e59e2a09..a27a9cf031 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -178,7 +178,6 @@ type language_descr = {
 
   (* Concerning the source file *)
   file_suffix : string;
-  capital_file : bool; (* should we capitalize filenames ? *)
   preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
   pp_struct : ml_structure -> std_ppcmds;
 
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index baec2eae4d..1ec08b3ece 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -736,7 +736,6 @@ let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt ()
 let ocaml_descr = {
   keywords = keywords;
   file_suffix = ".ml";
-  capital_file = false;
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = Some ".mli";
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 64b86e6e26..9bace75c99 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -204,7 +204,6 @@ let pp_struct =
 let scheme_descr = {
   keywords = keywords;
   file_suffix = ".scm";
-  capital_file = false;
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 439bb2a56f..301b6ed501 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -600,6 +600,14 @@ let string_of_modfile mp =
     modfile_mps := MPmap.add mp s' !modfile_mps;
     s'
 
+(* same as [string_of_modfile], but preserves the capital/uncapital 1st char *)
+
+let file_of_modfile mp =
+  let s0 = raw_string_of_modfile mp in
+  let s = string_of_modfile mp in
+  if s.[0] <> s0.[0] then s.[0] <- s0.[0];
+  s
+
 let add_blacklist_entries l =
   blacklist_table :=
     List.fold_right (fun s -> Idset.add (id_of_string (String.capitalize s)))
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index f3da84933f..18904a8b4b 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -46,6 +46,7 @@ val current_toplevel : unit -> module_path
 val base_mp : module_path -> module_path
 val is_modfile : module_path -> bool
 val string_of_modfile : module_path -> string
+val file_of_modfile : module_path -> string
 val is_toplevel : module_path -> bool
 val at_toplevel : module_path -> bool
 val visible_kn : kernel_name -> bool