Extraction: improved indentation of extracted code (fix #2497)

 For Haskell, we still try to provide readable indentation,
 but we now avoid relying on this indentation for correctness.
 Instead, we use layout-independant syntax with { } when
 necessary (after "case of" and "let"). It is much safer this
 way, even if the syntax gets a bit more cumbersome.

 For people allergic to {;}, they can most of the time do a
 tr -d "{;}" without changing the meaning of the program.
 Be careful nonetheless: since "case of" is now delimited,
 some parenthesis that used to be mandatory are now removed.

 Note also that the initial "module ... where" is still without
 { }: even when Format goes crazy it doesn't tamper with column 0.

 Other modifications:

 - Using "Set Printing Width" now affects uniformly the extraction
 pretty-printers. You can set a greater value than the default 78
 before extracting a program that you know to be "really deep".

 - In ocaml (and also a bit in Haskell), we now try to avoid abusing
 of 2-char-right-indentation. For instance | is now aligned with
 the "m" of match. This way, max_indent will be reached less frequently.

 - As soon as a pretty-print box contains an explicit newline,
 we set its virtual size to a big number, in order to prevent this
 box to be part of some horizontal arrangement.

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

5 files changed, 65 insertions, 46 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 61e2f8c28..ad2f40063 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -41,6 +41,13 @@ let pr_binding = function
   | [] -> mt ()
   | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
 
+(** By default, in module Format, you can do horizontal placing of blocks
+    even if they include newlines, as long as the number of chars in the
+    blocks are less that a line length. To avoid this awkward situation,
+    we attach a big virtual size to [fnl] newlines. *)
+
+let fnl () = stras (1000000,"") ++ fnl ()
+
 let fnl2 () = fnl () ++ fnl ()
 
 let space_if = function true -> str " " | false -> mt ()
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 0abb47c22..7fc3279af 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -12,6 +12,12 @@ open Miniml
 open Mlutil
 open Pp
 
+(** By default, in module Format, you can do horizontal placing of blocks
+    even if they include newlines, as long as the number of chars in the
+    blocks are less that a line length. To avoid this awkward situation,
+    we attach a big virtual size to [fnl] newlines. *)
+
+val fnl : unit -> std_ppcmds
 val fnl2 : unit -> std_ppcmds
 val space_if : bool -> std_ppcmds
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 1218dd80c..8a812664f 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -395,13 +395,20 @@ let print_one_decl struc mp decl =
 (*s Extraction of a ml struct to a file. *)
 
 let formatter dry file =
-  if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
-  else match file with
-    | None -> !Pp_control.std_ft
-    | Some cout ->
-	let ft = Pp_control.with_output_to cout in
-	Option.iter (Format.pp_set_margin ft) (Pp_control.get_margin ());
-	ft
+  let ft =
+    if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
+    else Pp_control.with_output_to (Option.default stdout file)
+  in
+  (* We never want to see ellipsis ... in extracted code *)
+  Format.pp_set_max_boxes ft max_int;
+  (* We reuse the width information given via "Set Printing Width" *)
+  (match Pp_control.get_margin () with
+    | None -> ()
+    | Some i ->
+      Format.pp_set_margin ft i;
+      Format.pp_set_max_indent ft (i-10));
+      (* note: max_indent should be < margin above, otherwise it's ignored *)
+  ft
 
 let print_structure_to_file (fn,si,mo) dry struc =
   let d = descr () in
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 32362d32c..6cad5d294 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -104,7 +104,7 @@ let rec pp_type par vl t =
 
 let expr_needs_par = function
   | MLlam _  -> true
-  | MLcase _ -> true
+  | MLcase _ -> false (* now that we use the case ... of { ... } syntax *)
   | _        -> false
 
 
@@ -127,14 +127,14 @@ let rec pp_expr par env args =
 	let pp_id = pr_id (List.hd i)
 	and pp_a1 = pp_expr false env [] a1
 	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
-	hv 0
-	  (apply
-	     (pp_par par'
-		(hv 0
-		   (hov 5
-		      (str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++
-		    spc () ++ str "in") ++
-		 spc () ++ hov 0 pp_a2)))
+	let pp_def =
+	  str "let {" ++ cut () ++
+	  hov 1 (pp_id ++ str " = " ++ pp_a1 ++ str "}")
+	in
+	apply
+	  (pp_par par'
+	     (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++
+		    spc () ++ hov 0 pp_a2)))
     | MLglob r ->
 	apply (pp_global Term r)
     | MLcons (_,r,[]) ->
@@ -159,8 +159,8 @@ let rec pp_expr par env args =
 		 ++ pp_expr true env [] t)))
     | MLcase (info,t, pv) ->
       	apply (pp_par par'
-		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
-		       fnl () ++ str "  " ++ pp_pat env info pv)))
+		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++
+		       fnl () ++ pp_pat env info pv)))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -177,12 +177,11 @@ and pp_pat env info pv =
   let pp_one_pat (name,ids,t) =
     let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
     let par = expr_needs_par t in
-    hov 2 (pp_global Cons name ++
+    hov 2 (str " " ++ pp_global Cons name ++
 	   (match ids with
 	      | [] -> mt ()
 	      | _  -> (str " " ++
-		       prlist_with_sep
-			 (fun () -> (spc ())) pr_id (List.rev ids))) ++
+		       prlist_with_sep spc pr_id (List.rev ids))) ++
 	   str " ->" ++ spc () ++ pp_expr par env' [] t)
   in
   let factor_br, factor_set = try match info.m_same with
@@ -199,18 +198,18 @@ and pp_pat env info pv =
   prvecti
     (fun i x -> if Intset.mem i factor_set then mt () else
        (pp_one_pat pv.(i) ++
-       if i = last && Intset.is_empty factor_set then mt () else
-       fnl () ++ str "  ")) pv
+       if i = last && Intset.is_empty factor_set then str "}" else
+	 (str ";" ++ fnl ()))) pv
   ++
   if Intset.is_empty factor_set then mt () else
   let par = expr_needs_par factor_br in
   match info.m_same with
     | BranchFun _ ->
         let ids, env' = push_vars [anonymous_name] env in
-        hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++
-	       pp_expr par env' [] factor_br)
+        hov 2 (str " " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
+	       pp_expr par env' [] factor_br ++ str "}")
     | BranchCst _ ->
-        hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br)
+        hov 2 (str " _ ->" ++ spc () ++ pp_expr par env [] factor_br ++ str "}")
     | BranchNone -> mt ()
 
 (*s names of the functions ([ids]) are already pushed in [env],
@@ -219,12 +218,12 @@ and pp_pat env info pv =
 and pp_fix par env i (ids,bl) args =
   pp_par par
     (v 0
-       (v 2 (str "let" ++ fnl () ++
-	     prvect_with_sep fnl
+       (v 1 (str "let {" ++ fnl () ++
+	     prvect_with_sep (fun () -> str ";" ++ fnl ())
 	       (fun (fi,ti) -> pp_function env (pr_id fi) ti)
-	       (array_map2 (fun a b -> a,b) ids bl)) ++
-	fnl () ++
-	hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
+	       (array_map2 (fun a b -> a,b) ids bl) ++
+	     str "}") ++
+        fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args))
 
 and pp_function env f t =
   let bl,t' = collect_lams t in
@@ -263,12 +262,12 @@ let pp_one_ind ip pl cv =
 		  (fun () -> (str " ")) (pp_type true pl) l))
   in
   str (if Array.length cv = 0 then "type " else "data ") ++
-  pp_global Type (IndRef ip) ++ str " " ++
-  prlist_with_sep (fun () -> str " ") pr_lower_id pl ++
-  (if pl = [] then mt () else str " ") ++
-  if Array.length cv = 0 then str "= () -- empty inductive"
+  pp_global Type (IndRef ip) ++
+  prlist_strict (fun id -> str " " ++ pr_lower_id id) pl ++ str " =" ++
+  if Array.length cv = 0 then str " () -- empty inductive"
   else
-    (v 0 (str "= " ++
+    (fnl () ++ str " " ++
+     v 0 (str "  " ++
 	  prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor
 	    (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv)))
 
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index e4a145586..543cec6e5 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -292,7 +292,7 @@ let rec pp_expr par env args =
 		  (try pp_ifthenelse par' env expr pv
 		   with Not_found ->
 		     v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++
-			  str "  | " ++ pp_pat env info pv))))
+			  pp_pat env info pv))))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -356,19 +356,19 @@ and pp_pat env info pv =
   prvecti
     (fun i x -> if Intset.mem i factor_set then mt () else
        let s1,s2 = pp_one_pat env info x in
-       hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++
-       if i = last && Intset.is_empty factor_set then mt () else
-       fnl () ++ str "  | ") pv
+       hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++
+       if i = last && Intset.is_empty factor_set then mt () else fnl ())
+    pv
   ++
   if Intset.is_empty factor_set then mt () else
   let par = expr_needs_par factor_br in
   match info.m_same with
     | BranchFun _ ->
         let ids, env' = push_vars [anonymous_name] env in
-        hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++
-		 pp_expr par env' [] factor_br)
+        hv 2 (str "| " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
+		 hov 2 (pp_expr par env' [] factor_br))
     | BranchCst _ ->
-        hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br)
+        hv 2 (str "| _ ->" ++ spc () ++ hov 2 (pp_expr par env [] factor_br))
     | BranchNone -> mt ()
 
 and pp_function env t =
@@ -380,11 +380,11 @@ and pp_function env t =
 	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
 	  pr_binding (List.rev (List.tl bl)) ++
        	  str " = function" ++ fnl () ++
-	  v 0 (str "  | " ++ pp_pat env' i pv)
+	  v 0 (pp_pat env' i pv)
 	else
           pr_binding (List.rev bl) ++
           str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
-	  v 0 (str "  | " ++ pp_pat env' i pv)
+	  v 0 (pp_pat env' i pv)
     | _ ->
           pr_binding (List.rev bl) ++
 	  str " =" ++ fnl () ++ str "  " ++
@@ -440,7 +440,7 @@ let pp_one_ind prefix ip_equiv pl name cnames ctyps =
   let pl = rename_tvars keywords pl in
   let pp_constructor i typs =
     (if i=0 then mt () else fnl ()) ++
-    hov 5 (str "  | " ++ cnames.(i) ++
+    hov 3 (str "| " ++ cnames.(i) ++
 	   (if typs = [] then mt () else str " of ") ++
 	   prlist_with_sep
 	    (fun () -> spc () ++ str "* ") (pp_type true pl) typs)