Merge branch 'v8.5'

5 files changed, 14 insertions, 6 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 90ee6d0ef1..5ea4fb763e 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -440,7 +440,8 @@ let mono_filename f =
 let module_filename mp =
   let f = file_of_modfile mp in
   let d = descr () in
-  Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, Id.of_string f
+  let p = d.file_naming mp ^ d.file_suffix in
+  Some p, Option.map ((^) f) d.sig_suffix, Id.of_string f
 
 (*s Extraction of one decl to stdout. *)
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 5e08fef5fe..52459f78eb 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -26,7 +26,7 @@ let pr_upper_id id = str (String.capitalize (Id.to_string id))
 
 let keywords =
   List.fold_right (fun s -> Id.Set.add (Id.of_string s))
-  [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
+  [ "Any"; "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
     "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance";
     "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
     "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
@@ -56,11 +56,14 @@ let preamble mod_name comment used_modules usf =
    else str "\
 \n#ifdef __GLASGOW_HASKELL__\
 \nimport qualified GHC.Base\
+\nimport qualified GHC.Prim\
+\ntype Any = GHC.Prim.Any\
 \nunsafeCoerce :: a -> b\
 \nunsafeCoerce = GHC.Base.unsafeCoerce#\
 \n#else\
 \n-- HUGS\
 \nimport qualified IOExts\
+\ntype Any = ()\
 \nunsafeCoerce :: a -> b\
 \nunsafeCoerce = IOExts.unsafeCoerce\
 \n#endif" ++ fnl2 ())
@@ -102,7 +105,7 @@ let rec pp_type par vl t =
 	pp_par par
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy _ -> str "()"
-    | Tunknown -> str "()"
+    | Tunknown -> str "Any"
     | Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
  in
   hov 0 (pp_rec par t)
@@ -243,12 +246,12 @@ let pp_logical_ind packet =
 	      prvect_with_sep spc pr_id packet.ip_consnames)
 
 let pp_singleton kn packet =
+  let name = pp_global Type (IndRef (kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
-  let l' = List.rev l in
-  hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++
+  hov 2 (str "type " ++ name ++ spc () ++
 	 prlist_with_sep spc pr_id l ++
 	 (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++
-	 pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
+	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
 	 pp_comment (str "singleton inductive, whose constructor was " ++
 		     pr_id packet.ip_consnames.(0)))
 
@@ -360,6 +363,7 @@ let pp_struct =
 let haskell_descr = {
   keywords = keywords;
   file_suffix = ".hs";
+  file_naming = string_of_modfile;
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 1e491d36f7..b7dee6cb14 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -197,6 +197,7 @@ type language_descr = {
 
   (* Concerning the source file *)
   file_suffix : string;
+  file_naming : module_path -> string;
   (* the second argument is a comment to add to the preamble *)
   preamble :
     Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 85f18a0933..8c482b4b1d 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -746,6 +746,7 @@ let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt ()
 let ocaml_descr = {
   keywords = keywords;
   file_suffix = ".ml";
+  file_naming = file_of_modfile;
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = Some ".mli";
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 69dea25aac..99b4fd448d 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -225,6 +225,7 @@ let pp_struct =
 let scheme_descr = {
   keywords = keywords;
   file_suffix = ".scm";
+  file_naming = file_of_modfile;
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;