un paquet de corrections de bugs

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

5 files changed, 47 insertions, 23 deletions

diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 69f3c4e387..a3e0aa12fb 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -244,7 +244,7 @@ let rec pp_ind first kn i ind =
 
 (*s Pretty-printing of a declaration. *)
 
-
+let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
 
 let pp_decl mpl = 
   local_mpl := mpl;
@@ -256,16 +256,16 @@ let pp_decl mpl =
       if is_inline_custom r then mt () 
       else 
 	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
+	let st = 
+	  try 
+	    let ids,s = find_type_custom r in 
+	    prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
+	  with not_found -> 
+	    prlist (fun id -> pr_id id ++ str " ") 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 ()
+	hov 2 (str "type " ++ pp_global r ++ spc () ++ st) ++ fnl () ++ fnl ()
   | Dfix (rv, defs,_) ->
       let ppv = Array.map pp_global rv in 
       prlist_with_sep (fun () -> fnl () ++ fnl ())
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 5b15527215..3d4ab11a67 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -117,9 +117,9 @@ let rec mgu = function
 
 let needs_magic p = try mgu p; false with Impossible -> true
 
-let put_magic_if b a = if b then MLmagic a else a
+let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
 
-let put_magic p a = if needs_magic p then MLmagic a else a
+let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
 
 
 (*S ML type env. *)
@@ -744,10 +744,15 @@ let rec simpl o = function
   | MLcase (i,e,br) ->
       let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in 
       simpl_case o i br (simpl o e) 
-  | MLletin(id,c,e) when 
-      (id = dummy_name) || (is_atomic c) || (is_atomic e) ||
-      (let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let)) -> 
+  | MLletin(id,c,e) -> 
+      let e = (simpl o e) in 
+      if 
+	(id = dummy_name) || (is_atomic c) || (is_atomic e) ||
+	(let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let))
+      then 
 	simpl o (ast_subst c e)
+      else 
+	MLletin(id, simpl o c, e)
   | MLfix(i,ids,c) -> 
       let n = Array.length ids in 
       if ast_occurs_itvl 1 n c.(i) then 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 3797e5d97c..dfc0d27653 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -178,13 +178,21 @@ let find_projections = function Record l -> l | _ -> raise NoRecord
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
+let kn_sig = 
+  let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in 
+  make_kn specif empty_dirpath (mk_label "sig")
+
 let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ | Taxiom -> assert false
     | Tvar i -> (try pp_tvar (List.nth vl (pred i)) 
 		 with _ -> (str "'a" ++ int i))
     | Tglob (r,[]) -> pp_global r
-    | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global r
+    | Tglob (r,l) -> 
+	if r = IndRef (kn_sig,0) then 
+	  pp_tuple_light pp_rec l
+	else 
+	  pp_tuple_light pp_rec l ++ spc () ++ pp_global r
     | Tarr (t1,t2) ->
 	pp_par par 
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index cf8f987b58..e08489b239 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -19,7 +19,6 @@ 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
 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 679ee9e226..f83be535d6 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -43,6 +43,12 @@ let pp_abst st = function
   | l -> paren 
 	(str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
 
+let pp_apply st _ = function 
+  | [] -> st 
+  | [a] -> hov 2 (paren (st ++ spc () ++ a))
+  | args -> hov 2 (paren (str "@ " ++ st ++ 
+			  (prlist (fun x -> spc () ++ x) args))) 
+
 (*s The pretty-printing functor. *)
 
 module Make = functor(P : Mlpp_param) -> struct
@@ -63,7 +69,7 @@ let rec pp_expr env args =
     | MLlam _ as a -> 
       	let fl,a' = collect_lams a in
 	let fl,env' = push_vars fl env in
-	pp_abst (pp_expr env' [] a') (List.rev fl)
+	apply (pp_abst (pp_expr env' [] a') (List.rev fl))
     | MLletin (id,a1,a2) ->
 	let i,env' = push_vars [id] env in
 	apply 
@@ -82,10 +88,8 @@ let rec pp_expr env args =
 	let st = 
 	  str "`" ++ 
 	  paren (pp_global r ++ 
-		 (if args' = [] then mt () else (spc () ++ str ",")) ++
-		 prlist_with_sep 
-		   (fun () -> spc () ++ str ",") 
-		   (pp_expr env []) args')
+		 (if args' = [] then mt () else spc ()) ++
+		 prlist_with_sep spc (pp_cons_args env) args')
 	in 
 	if i = Coinductive then paren (str "delay " ++ st) else st 
     | MLcase (i,t, pv) ->
@@ -105,6 +109,13 @@ let rec pp_expr env args =
     | MLmagic a ->
 	pp_expr env args a
     | MLaxiom -> paren (str "absurd ;;AXIOM TO BE REALIZED\n")
+
+and pp_cons_args env = function 
+  | MLcons (i,r,args) when i<>Coinductive -> 
+      paren (pp_global r ++ 
+	     (if args = [] then mt () else spc ()) ++
+	     prlist_with_sep spc (pp_cons_args env) args)
+  | e -> str "," ++ pp_expr env [] e
 	
 
 and pp_one_pat env (r,ids,t) = 
@@ -129,7 +140,8 @@ and pp_fix env j (ids,bl) args =
       (str "letrec " ++
        (v 0 (paren 
 	       (prvect_with_sep fnl
-		  (fun (fi,ti) -> paren ((pr_id fi) ++ (pp_expr env [] ti)))
+		  (fun (fi,ti) -> 
+		     paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
 		  (array_map2 (fun id b -> (id,b)) ids bl)) ++
 	     fnl () ++
       	     hov 2 (pp_apply (pr_id (ids.(j))) true args))))