Merge PR #11563: Mini improvement of the formatting rule for printing fix and cofix

Reviewed-by: SkySkimmer

2 files changed, 23 insertions, 25 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 2416819a6a..f9f46e1ceb 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -224,7 +224,7 @@ let tag_var = tag Tag.variable
 
   let pr_opt_type_spc pr = function
     | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt ()
-    | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
+    | t ->  str " :" ++ pr_sep_com (fun()->brk(1,4)) (pr ltop) t
 
   let pr_prim_token = function
     | Numeral (SPlus,n) -> str (NumTok.to_string n)
@@ -387,12 +387,12 @@ let tag_var = tag Tag.variable
     if is_open then pr_delimited_binders pr_com_at sep pr_c
     else pr_undelimited_binders sep pr_c
 
-  let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
+  let pr_recursive_decl pr pr_dangling kw dangling_with_for id bl annot t c =
     let pr_body =
       if dangling_with_for then pr_dangling else pr in
-    pr_id id ++ (if bl = [] then mt () else str" ") ++
+    hov 0 (str kw ++ brk(1,2) ++ pr_id id ++ (if bl = [] then mt () else brk(1,2)) ++
       hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++
-      pr_opt_type_spc pr t ++ str " :=" ++
+      pr_opt_type_spc pr t ++ str " :=") ++
       pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
 
   let pr_guard_annot pr_aux bl ro =
@@ -407,28 +407,28 @@ let tag_var = tag Tag.variable
               | CLocalPattern _ -> assert false
             in let ids = List.flatten (List.map names_of_binder bl) in
                if List.length ids > 1 then
-                 spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}"
+                 spc() ++ str "{" ++ keyword "struct" ++ brk (1,1) ++ pr_id id ++ str"}"
                else mt()
           | CWfRec (id,c) ->
-            spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_lident id ++ str"}"
+            spc() ++ str "{" ++ keyword "wf" ++ brk (1,1) ++ pr_aux c ++ brk (1,1) ++ pr_lident id ++ str"}"
           | CMeasureRec (id,m,r) ->
-            spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++
-            match id with None -> mt() | Some id -> spc () ++ pr_lident id ++
+            spc() ++ str "{" ++ keyword "measure" ++ brk (1,1) ++ pr_aux m ++
+            match id with None -> mt() | Some id -> brk (1,1) ++ pr_lident id ++
               (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}"
 
-  let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) =
+  let pr_fixdecl pr prd kw dangling_with_for ({v=id},ro,bl,t,c) =
     let annot = pr_guard_annot (pr lsimpleconstr) bl ro in
-    pr_recursive_decl pr prd dangling_with_for id bl annot t c
+    pr_recursive_decl pr prd kw dangling_with_for id bl annot t c
 
-  let pr_cofixdecl pr prd dangling_with_for ({v=id},bl,t,c) =
-    pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
+  let pr_cofixdecl pr prd kw dangling_with_for ({v=id},bl,t,c) =
+    pr_recursive_decl pr prd kw dangling_with_for id bl (mt()) t c
 
-  let pr_recursive pr_decl id = function
+  let pr_recursive kw pr_decl id = function
     | [] -> anomaly (Pp.str "(co)fixpoint with no definition.")
-    | [d1] -> pr_decl false d1
+    | [d1] -> pr_decl kw false d1
     | dl ->
-      prlist_with_sep (fun () -> fnl() ++ keyword "with" ++ spc ())
-        (pr_decl true) dl ++
+      prlist_with_sep (fun () -> fnl())
+        (pr_decl "with" true) dl ++
         fnl() ++ keyword "for" ++ spc () ++ pr_id id
 
   let pr_asin pr na indnalopt =
@@ -494,15 +494,13 @@ let tag_var = tag Tag.variable
         return (pr_cref r us, latom)
       | CFix (id,fix) ->
         return (
-          hov 0 (keyword "fix" ++ spc () ++
-                   pr_recursive
+          hv 0 (pr_recursive "fix"
                    (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v fix),
           lfix
         )
       | CCoFix (id,cofix) ->
         return (
-          hov 0 (keyword "cofix" ++ spc () ++
-                   pr_recursive
+          hv 0 (pr_recursive "cofix"
                    (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v cofix),
           lfix
         )
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index 6879cbc3c2..60bc9cbf55 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -1,8 +1,8 @@
-fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : 
-list B := match l with
-          | nil => nil
-          | a :: l0 => f a :: F A B f l0
-          end
+fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : list B :=
+  match l with
+  | nil => nil
+  | a :: l0 => f a :: F A B f l0
+  end
      : forall A B : Set, (A -> B) -> list A -> list B
 let fix f (m : nat) : nat := match m with
                              | 0 => 0