ajout des unsafeCoerce + 2 bugs haskell

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

2 files changed, 18 insertions, 9 deletions

diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 12f7fbb1a..219ebc011 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -27,7 +27,7 @@ let keywords =
   [ "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" ]
+    "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
   Idset.empty
 
 let preamble prm used_modules (mldummy,tdummy,tunknown) =
@@ -38,8 +38,10 @@ let preamble prm used_modules (mldummy,tdummy,tunknown) =
   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() ++
   (if mldummy then 
      str "__ = Prelude.error \"Logical or arity value used\"" 
      ++ fnl () ++ fnl()
@@ -146,7 +148,8 @@ let rec pp_expr par env args =
 	pp_par par (str "Prelude.error" ++ spc () ++ qs s)
     | MLdummy ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
-    | MLmagic a ->  pp_expr par env args a
+    | MLmagic a ->  
+	pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
     | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
 
 and pp_pat env pv = 
@@ -210,7 +213,7 @@ let pp_one_ind ip pl cv =
        | [] -> (mt ()) 
        | _  -> (str " " ++
       	       	prlist_with_sep 
-		  (fun () -> (str " ")) (pp_type true (List.rev pl)) l))
+		  (fun () -> (str " ")) (pp_type true pl) l))
   in
   str (if cv = [||] then "type " else "data ") ++ 
   pp_global (IndRef ip) ++ str " " ++
@@ -249,10 +252,9 @@ let pp_decl mpl =
       if is_inline_custom r then mt () 
       else 
 	let l = rename_tvars keywords l in
-	let l' = List.rev l in 
 	hov 2 (str "type " ++ pp_global r ++ spc () ++ 
 	       prlist (fun id -> pr_id id ++ str " ") l ++
-	       str "=" ++ spc () ++ pp_type false l' t) ++ fnl () ++ fnl ()
+	       str "=" ++ spc () ++ pp_type false l t) ++ fnl () ++ fnl ()
   | Dfix (rv, defs,_) ->
       let ppv = Array.map pp_global rv in 
       prlist_with_sep (fun () -> fnl () ++ fnl ())
@@ -262,7 +264,12 @@ let pp_decl mpl =
   | Dterm (r, a, _) ->
       if is_inline_custom r then mt () 
       else 
-	hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl () ++ fnl ())
+	if is_custom r then 	
+	  hov 0 (pp_global r ++ str " = " ++ str (find_custom r) 
+		 ++ fnl() ++ fnl ())
+	else 
+	  hov 0 (pp_function (empty_env ()) (pp_global r) a 
+		 ++ fnl () ++ fnl ())
 
 let pp_structure_elem mpl = function 
   | (l,SEdecl d) -> pp_decl mpl d
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index f4b84361a..83e1f0f89 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -173,9 +173,11 @@ let ast_iter_references do_term do_cons do_type a =
     ast_iter iter a;
     match a with 
       | MLglob r -> do_term r
-      | MLcons (i,r,_) -> record_iter_references do_term i; do_cons r 
+      | MLcons (i,r,_) -> 
+	  if lang () = Ocaml then record_iter_references do_term i; 
+	  do_cons r 
       | MLcase (i,_,v) as a -> 
-	  record_iter_references do_term i; 
+	  if lang () = Ocaml then record_iter_references do_term i; 
 	  Array.iter (fun (r,_,_) -> do_cons r) v
       | _ -> ()
   in iter a
@@ -186,7 +188,7 @@ let ind_iter_references do_term do_cons do_type kn ind =
   let packet_iter ip p = 
     do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types 
   in
-  record_iter_references do_term ind.ind_info; 
+  if lang () = Ocaml then record_iter_references do_term ind.ind_info; 
   Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
   
 let decl_iter_references do_term do_cons do_type =