reparation des Extract Constant avec Haskell

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

4 files changed, 25 insertions, 15 deletions

diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 6ca2689b0..69f3c4e38 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -41,7 +41,7 @@ let preamble prm used_modules (mldummy,tdummy,tunknown) =
   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() ++
+  str "unsafeCoerce = GHC.Base.unsafeCoerce#" ++ fnl() ++ fnl() ++
   (if mldummy then 
      str "__ = Prelude.error \"Logical or arity value used\"" 
      ++ fnl () ++ fnl()
@@ -63,7 +63,10 @@ module Make = functor(P : Mlpp_param) -> struct
 
 let local_mpl = ref ([] : module_path list)
 
-let pp_global r = P.pp_global !local_mpl r
+let pp_global r = 
+  if is_inline_custom r then str (find_custom r) 
+  else P.pp_global !local_mpl r
+
 let empty_env () = [], P.globals()
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
@@ -83,7 +86,6 @@ let rec pp_type par vl t =
     | Tdummy -> str "()"
     | Tunknown -> str "()"
     | Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
-    | Tcustom s -> str s
  in 
   hov 0 (pp_rec par t)
 
@@ -242,6 +244,8 @@ let rec pp_ind first kn i ind =
 
 (*s Pretty-printing of a declaration. *)
 
+
+
 let pp_decl mpl = 
   local_mpl := mpl;
   function
@@ -251,10 +255,17 @@ let pp_decl mpl =
   | Dtype (r, l, t) ->
       if is_inline_custom r then mt () 
       else 
-	let l = rename_tvars keywords 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 ()
+	let l = rename_tvars keywords l in 
+	let ids, def = try 
+	  let ids,s = find_type_custom r in 
+	  pp_string_parameters ids, str "=" ++ spc () ++ str s
+	with not_found -> 
+	  pp_string_parameters (List.map string_of_id l), 
+	  if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
+	  else str "=" ++ spc () ++ pp_type false l t
+	in 
+	hov 2 (str "type " ++ pp_global r ++ spc () ++ ids ++ def)
+	++ fnl () ++ fnl ()
   | Dfix (rv, defs,_) ->
       let ppv = Array.map pp_global rv in 
       prlist_with_sep (fun () -> fnl () ++ fnl ())
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 03d0c37d9..b2cfc905b 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -35,7 +35,6 @@ type ml_type =
   | Tdummy
   | Tunknown
   | Taxiom
-  | Tcustom of string
 
 and ml_meta = { id : int; mutable contents : ml_type option }
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index d00e36f60..3797e5d97 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -66,6 +66,12 @@ let sec_space_if = function true -> spc () | false -> mt ()
 
 let fnl2 () = fnl () ++ fnl () 
 
+let pp_parameters l = 
+  (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
+
+let pp_string_parameters l = 
+  (pp_boxed_tuple str l ++ space_if (l<>[])) 
+
 (*s Generic renaming issues. *)
 
 let rec rename_id id avoid = 
@@ -184,7 +190,6 @@ let rec pp_type par vl t =
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy -> str "__"
     | Tunknown -> str "__"
-    | Tcustom s -> str s
   in 
   hov 0 (pp_rec par t)
 
@@ -385,12 +390,6 @@ let rec pp_Dfix init i ((rv,c,t) as fix) =
 	
 (*s Pretty-printing of inductive types declaration. *)
 
-let pp_parameters l = 
-  (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
-
-let pp_string_parameters l = 
-  (pp_boxed_tuple str l ++ space_if (l<>[])) 
-
 let pp_one_ind prefix ip pl cv =
   let pl = rename_tvars keywords pl in
   let pp_constructor (r,l) =
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index e08489b23..cf8f987b5 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -19,6 +19,7 @@ val pp_par : bool -> std_ppcmds -> std_ppcmds
 val pp_abst : identifier list -> std_ppcmds
 val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds 
 val pr_binding : identifier list -> std_ppcmds
+val pp_string_parameters : string list -> std_ppcmds
 
 val rename_id : identifier -> Idset.t -> identifier