amelioration du pretty-print des modules

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

1 files changed, 95 insertions, 66 deletions

diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index f7a07f581..cf13cc7b6 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -65,6 +65,8 @@ let space_if = function true -> str " " | false -> mt ()
 
 let sec_space_if = function true -> spc () | false -> mt ()
 
+let fnl2 () = fnl () ++ fnl () 
+
 (*s Generic renaming issues. *)
 
 let rec rename_id id avoid = 
@@ -344,7 +346,7 @@ and pp_fix par env i (ids,bl) args =
 
 let pp_val e typ = 
   str "(** val " ++ e ++ str " : " ++ pp_type false [] typ ++ 
-  str " **)"  ++ fnl () ++ fnl ()
+  str " **)"  ++ fnl2 ()
 
 (*s Pretty-printing of [Dfix] *)
 
@@ -355,12 +357,11 @@ let rec pp_Dfix init i ((rv,c,t) as fix) =
     if is_inline_custom r then pp_Dfix init (i+1) fix
     else 
       let e = pp_global r in
-      (if init then mt () else fnl ()) ++
+      (if init then mt () else fnl2 ()) ++
       pp_val e t.(i) ++
       str (if init then "let rec " else "and ") ++
       (if is_custom r then e ++ str " = " ++ str (find_custom r)
        else pp_function (empty_env ()) e c.(i)) ++
-      fnl () ++ 
       pp_Dfix false (i+1) fix 
 	
 (*s Pretty-printing of inductive types declaration. *)
@@ -408,7 +409,7 @@ let pp_record kn packet =
   str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++
   hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) 
 	   (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l) 
-  ++ str " }" ++ fnl () 
+  ++ str " }"
 
 let pp_coind ip pl = 
   let r = IndRef ip in 
@@ -416,72 +417,85 @@ let pp_coind ip pl =
   pp_parameters pl ++ pp_global r ++ str " = " ++ 
   pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t"
 
-let rec pp_ind co first kn i ind =
-  if i >= Array.length ind.ind_packets then 
-    if first then mt () else fnl ()
-  else 
-    let ip = (kn,i) in 
-    let p = ind.ind_packets.(i) in 
-    if is_custom (IndRef (kn,i)) then pp_ind co first kn (i+1) ind
+exception Empty
+
+let pp_ind co kn ind =
+  let some = ref false in 
+  let init= ref (str "type ") in 
+  let rec pp i =  
+    if i >= Array.length ind.ind_packets then mt () 
     else 
-      if p.ip_logical then  
-	pp_logical_ind ip p ++ pp_ind co first kn (i+1) ind
-      else 
-	str (if first then "type " else "and ") ++
-	(if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ()) ++ 
-	pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++
-	fnl () ++ pp_ind co false kn (i+1) ind
+      let ip = (kn,i) in 
+      let p = ind.ind_packets.(i) in 
+      if is_custom (IndRef (kn,i)) then pp (i+1)
+      else begin 
+	some := true; 
+	if p.ip_logical then pp_logical_ind ip p ++ pp (i+1)
+	else 
+	  let s = !init in 
+	  begin 
+	    init := (fnl () ++ str "and "); 
+	    s ++
+	    (if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ())
+	    ++ pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++
+	    pp (i+1)
+	  end
+      end
+  in 
+  let st = pp 0 in if !some then st else raise Empty
+	     
 
 (*s Pretty-printing of a declaration. *)
 
 let pp_mind kn i = 
   let kn = long_kn kn in 
   (match i.ind_info with 
-     | Singleton -> pp_singleton kn i.ind_packets.(0) ++ fnl ()
+     | Singleton -> pp_singleton kn i.ind_packets.(0)
      | Coinductive -> 
 	 let nop _ = () 
 	 and add r = cons_cofix := Refset.add (long_r r) !cons_cofix in 
 	 decl_iter_references nop add nop (Dind (kn,i)); 
-	 hov 0 (pp_ind true true kn 0 i) ++ fnl () 
-     | Record -> pp_record kn i.ind_packets.(0) ++ fnl () 
-     | _ -> hov 0 (pp_ind false true kn 0 i))
-  
+	 pp_ind true kn i
+     | Record -> pp_record kn i.ind_packets.(0)
+     | _ -> pp_ind false kn i)
+
 let pp_decl mp = 
   local_mp := mp; 
   function
     | Dind (kn,i) as d -> pp_mind kn i
     | Dtype (r, l, t) ->
-	if is_inline_custom r then mt () 
+	if is_inline_custom r then raise Empty
 	else 
 	  let l = rename_tvars keywords l in 
 	  let def = try str (find_custom r) with not_found -> pp_type false l t 
 	  in 
-	  hov 0 (str "type" ++ spc () ++ pp_parameters l ++ pp_global r ++ 
-		 spc () ++ str "=" ++ spc () ++ def ++ fnl () ++ fnl ())
+	  hov 2 (str "type" ++ spc () ++ pp_parameters l ++ pp_global r ++ 
+		 spc () ++ str "=" ++ spc () ++ def)
     | Dterm (r, a, t) -> 
-	if is_inline_custom r then mt () 
+	if is_inline_custom r then raise Empty
 	else 
 	  let e = pp_global r in 
 	  pp_val e t ++
 	  hov 0 
 	    (str "let " ++ 
-	     if is_custom r then e ++ str " = " ++ str (find_custom r) ++ fnl () 
+	     if is_custom r then 
+	       e ++ str " = " ++ str (find_custom r) ++ fnl () 
 	     else if is_projection r then e ++ str " x = x." ++ e ++ fnl () 
-	     else pp_function (empty_env ()) e a ++ fnl ()) ++ fnl ()
+	     else pp_function (empty_env ()) e a)
     | Dfix (rv,defs,typs) ->
-	hov 0 (pp_Dfix true 0 (rv,defs,typs)) ++ fnl ()
+	pp_Dfix true 0 (rv,defs,typs)
 
 let pp_spec mp = 
   local_mp := mp; 
   function 
     | Sind (kn,i) -> pp_mind kn i
     | Sval (r,t) -> 
-	if is_inline_custom r then mt () 
+	if is_inline_custom r then raise Empty
 	else 
-	  hov 0 (str "val" ++ spc () ++ pp_global r ++ str " :" ++ spc () ++
-		 pp_type false [] t ++ fnl () ++ fnl ())
+	  hov 2 (str "val" ++ spc () ++ pp_global r ++ str " :" ++ spc () ++
+		 pp_type false [] t)
     | Stype (r,vl,ot) -> 
-	if is_inline_custom r then mt () 
+	if is_inline_custom r then raise Empty
 	else 
 	  let l = rename_tvars keywords vl in 
 	  let def = 
@@ -491,24 +505,28 @@ let pp_spec mp =
 		| None -> mt () 
 		| Some t -> str "=" ++ spc () ++ pp_type false l t 
 	  in 
-	  hov 0 (str "type" ++ spc () ++ pp_parameters l ++ 
-		 pp_global r ++ spc () ++ def ++ fnl () ++ fnl ())
+	  hov 2 (str "type" ++ spc () ++ pp_parameters l ++ 
+		 pp_global r ++ spc () ++ def)
 
 let rec pp_structure_elem mp = function 
   | (_,SEdecl d) -> pp_decl mp d
   | (l,SEmodule m) ->
-      str "module " ++ P.pp_short_module (id_of_label l) ++ 
-      (match m.ml_mod_equiv with 
-	 | None -> 
-	     str ":" ++ fnl () ++ pp_module_type m.ml_mod_type ++ fnl () ++ 
-	     str " = " ++ fnl () ++ 
-	     (match m.ml_mod_expr with 
-		| None -> failwith "TODO: if this happens, see Jacek"
-		| Some me -> pp_module_expr me ++ fnl ())
-	 | Some mp -> str " = " ++ P.pp_long_module mp ++ fnl ()) ++ fnl ()
+      hov 1 
+	(str "module " ++ P.pp_short_module (id_of_label l) ++ 
+	 (match m.ml_mod_equiv with 
+	    | None -> 
+		str ":" ++ fnl () ++ 
+		pp_module_type m.ml_mod_type ++ fnl () ++
+		str "= " ++ fnl () ++ 
+		(match m.ml_mod_expr with 
+		   | None -> assert false (* see Jacek *)
+		   | Some me -> pp_module_expr me)
+	    | Some mp -> 
+		str " = " ++ P.pp_long_module mp))
   | (l,SEmodtype m) -> 
-      str "module type " ++ P.pp_short_module (id_of_label l) ++
-      str " = " ++ pp_module_type m ++ fnl () ++ fnl ()
+      hov 1 
+	(str "module type " ++ P.pp_short_module (id_of_label l) ++
+	 str " = " ++ fnl () ++ pp_module_type m)
 
 and pp_module_expr = function 
   | MEident mp -> P.pp_long_module mp 
@@ -517,14 +535,15 @@ and pp_module_expr = function
       P.pp_short_module (id_of_mbid mbid) ++
       str ":" ++
       pp_module_type mt ++
-      str ") ->" ++
+      str ") ->" ++ fnl () ++
       pp_module_expr me
   | MEapply (me, me') -> 
-      str "(" ++ pp_module_expr me ++ str " (" ++ pp_module_expr me' ++ str ")"
+      str "(" ++ pp_module_expr me ++ spc () ++ pp_module_expr me' ++ str ")"
   | MEstruct (msid, sel) -> 
+      let l = map_succeed (pp_structure_elem (MPself msid)) sel in 
       str "struct " ++ fnl () ++
-      prlist_with_sep fnl (pp_structure_elem (MPself msid)) sel ++ fnl () ++
-      str "end" 
+      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ 
+      fnl () ++ str "end" 
 
 and pp_module_type = function 
   | MTident kn -> 
@@ -534,29 +553,39 @@ and pp_module_type = function
       P.pp_short_module (id_of_mbid mbid) ++
       str ":" ++
       pp_module_type mt ++
-      str ") ->" ++ 
+      str ") ->" ++ fnl () ++
       pp_module_type mt'
   | MTsig (msid, sign) -> 
+      let l = map_succeed (pp_specif (MPself msid)) sign in 
       str "sig " ++ fnl () ++ 
-      prlist_with_sep fnl (pp_specif (MPself msid)) sign ++ fnl () ++
-      str "end"
+      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
+      fnl () ++ str "end"
 
 and pp_specif mp = function 
   | (_,Spec s) -> pp_spec mp s 
   | (l,Smodule mt) -> 
-      str "module " ++ 
-      P.pp_short_module (id_of_label l) ++
-      str " : " ++ pp_module_type mt ++ fnl () ++ fnl ()
+      hov 1 
+	(str "module " ++ 
+	 P.pp_short_module (id_of_label l) ++
+	 str " : " ++ fnl () ++ pp_module_type mt)
   | (l,Smodtype mt) -> 
-      str "module type " ++
-      P.pp_short_module (id_of_label l) ++
-      str " : " ++ pp_module_type mt ++ fnl () ++ fnl ()
-
-let pp_struct =
-  prlist (fun (mp,sel) -> prlist (pp_structure_elem mp) sel)
-
-let pp_signature = 
-  prlist (fun (mp,sign) -> prlist (pp_specif mp) sign)
+      hov 1
+	(str "module type " ++
+	 P.pp_short_module (id_of_label l) ++
+	 str " : " ++ fnl () ++ pp_module_type mt)
+
+let pp_struct s =
+  let l mp sel = map_succeed (pp_structure_elem mp) sel in 
+  prlist (fun (mp,sel) -> prlist_with_sep fnl2 identity (l mp sel)) s ++ 
+  fnl2 ()
+
+let pp_signature s = 
+  let l mp sign = map_succeed (pp_specif mp) sign in 
+  prlist (fun (mp,sign) -> prlist_with_sep fnl2 identity (l mp sign)) s ++ 
+  fnl2 ()
+
+let pp_decl mp d = 
+  try pp_decl mp d with Empty -> mt () 
 
 end