amelioration de la generation des unsafeCoerce

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

9 files changed, 37 insertions, 17 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 7507296600..d03cd00fd8 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -352,7 +352,7 @@ let preamble prm = match lang () with
   | Ocaml -> Ocaml.preamble prm   
   | Haskell -> Haskell.preamble prm
   | Scheme -> Scheme.preamble prm
-  | Toplevel -> (fun _ _ -> mt ())
+  | Toplevel -> (fun _ _ _ -> mt ())
 
 let preamble_sig prm = match lang () with 
   | Ocaml -> Ocaml.preamble_sig prm   
@@ -385,9 +385,13 @@ let print_structure_to_file f prm struc =
     else (create_mono_renamings struc; [])
   in 
   let print_dummys =
-    (struct_ast_search MLdummy struc, 
+    (struct_ast_search ((=) MLdummy) struc, 
      struct_type_search Tdummy struc, 
      struct_type_search Tunknown struc)
+  in 
+  let print_magic = 
+    if lang () <> Haskell then false 
+    else struct_ast_search (function MLmagic _ -> true | _ -> false) struc
   in
   (* print the implementation *)
   let cout = option_app (fun (f,_) -> open_out f) f in 
@@ -395,7 +399,7 @@ let print_structure_to_file f prm struc =
     | None -> !Pp_control.std_ft
     | Some cout -> Pp_control.with_output_to cout in 
   begin try 
-    msg_with ft (preamble prm used_modules print_dummys);
+    msg_with ft (preamble prm used_modules print_dummys print_magic);
     msg_with ft (pp_struct struc);
     option_iter close_out cout; 
   with e -> 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 8859ebc7a9..b761d13610 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -30,22 +30,38 @@ let keywords =
     "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
   Idset.empty
 
-let preamble prm used_modules (mldummy,tdummy,tunknown) =
+let preamble prm used_modules (mldummy,tdummy,tunknown) magic =
   let pp_mp = function 
     | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
     | _ -> assert false 
   in  
+  (if not magic then mt () 
+   else
+     str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++
+     str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n")
+  ++
   str "module " ++ pr_upper_id prm.mod_name ++ str " where" ++ fnl () 
   ++ fnl() ++ 
   str "import qualified Prelude" ++ fnl() ++
-  str "import qualified GHC.Base" ++ fnl() ++
   prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules
   ++ fnl () ++
-  str "unsafeCoerce = GHC.Base.unsafeCoerce#" ++ fnl() ++ fnl() ++
-  (if mldummy then 
+  (if not magic then mt () 
+   else str "\
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+import qualified IOExts
+unsafeCoerce = IOExts.unsafeCoerce
+#endif")
+  ++
+  fnl() ++ fnl() 
+  ++
+  (if not mldummy then mt () 
+   else
      str "__ = Prelude.error \"Logical or arity value used\"" 
-     ++ fnl () ++ fnl()
-   else mt())
+     ++ fnl () ++ fnl())
 
 let preamble_sig prm used_modules (mldummy,tdummy,tunknown) = failwith "TODO" 
 
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 16cb5554bf..430ec1fce5 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -15,6 +15,6 @@ open Miniml
 val keywords : Idset.t
 
 val preamble : 
-  extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+  extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 6dcfaf2a1f..d015663bc9 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -253,7 +253,7 @@ let struct_get_references_list struc =
 exception Found
 
 let rec ast_search t a = 
-  if t = a then raise Found else ast_iter (ast_search t) a
+  if t a then raise Found else ast_iter (ast_search t) a
 
 let decl_ast_search t = function 
   | Dterm (_,a,_) -> ast_search t a
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index 07425c30af..cea988de80 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -43,7 +43,7 @@ val add_labels_mp : module_path -> label list -> module_path
 
 (*s Functions upon ML modules. *)
 
-val struct_ast_search : ml_ast -> ml_structure -> bool
+val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
 val struct_type_search : ml_type -> ml_structure -> bool
 
 type do_ref = global_reference -> unit 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 575f199eb6..088e666221 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -130,7 +130,7 @@ let keywords =
     "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] 
   Idset.empty
 
-let preamble _ used_modules (mldummy,tdummy,tunknown) = 
+let preamble _ used_modules (mldummy,tdummy,tunknown) _ = 
   let pp_mp = function 
     | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
     | _ -> assert false 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index e08489b239..7a13590e21 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -37,10 +37,10 @@ val get_db_name : int -> env -> identifier
 val keywords : Idset.t
 
 val preamble : 
-  extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+  extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
 
 val preamble_sig : 
-  extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+  extraction_params -> module_path list -> bool*bool*bool -> std_ppcmds
 
 (*s Production of Ocaml syntax. We export both a functor to be used for 
     extraction in the Coq toplevel and a function to extract some 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index f83be535d6..068e60a9b7 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -29,7 +29,7 @@ let keywords =
       "error"; "delay"; "force"; "_"; "__"] 
     Idset.empty
 
-let preamble _ _ (mldummy,_,_) = 
+let preamble _ _ (mldummy,_,_) _ = 
   (if mldummy then 
      str "(define __ (lambda (_) __))" 
      ++ fnl () ++ fnl()
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index b66bb6b8a1..bded1a8a8b 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -17,7 +17,7 @@ open Names
 val keywords : Idset.t
 
 val preamble : 
-  extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+  extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp