Merge PR #13144: Closes #13142: more standardized pretty-printing of Coq records

Reviewed-by: ejgallego
Ack-by: SkySkimmer

2 files changed, 41 insertions, 17 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 4200268acc..8da1d636f0 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -234,6 +234,42 @@ let tag_var = tag Tag.variable
             let f (id,c) = pr_lident id ++ str ":=" ++ pr ltop c in
             str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}"))
 
+  (* Assuming "{" and "}" brackets, prints
+     - if there is enough room
+       { a; b; c }
+     - otherwise
+       {
+        a;
+        b;
+        c
+       }
+    Alternatively, replace outer hv with h to get instead:
+       { a;
+         b;
+         c }
+    Replace the inner hv with hov to respectively get instead (if enough room):
+       {
+        a; b;
+        c
+       }
+    or
+       { a; b;
+         c }
+  *)
+  let pr_record left right pr = function
+    | [] -> str left ++ str " " ++ str right
+    | l ->
+      hv 0 (
+        str left ++
+        brk (1,String.length left) ++
+        hv 0 (prlist_with_sep pr_semicolon pr l) ++
+        brk (1,0) ++
+        str right)
+
+  let pr_record_body left right pr l =
+    let pr_defined_field (id, c) = hov 2 (pr_reference id ++ str" :=" ++ pr c) in
+    pr_record left right pr_defined_field l
+
   let las = lapp
   let lpator = 0
   let lpatrec = 0
@@ -242,11 +278,7 @@ let tag_var = tag Tag.variable
   let rec pr_patt sep inh p =
     let (strm,prec) = match CAst.(p.v) with
       | CPatRecord l ->
-        let pp (c, p) =
-          pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc lpattop p
-        in
-        (if l = [] then str "{| |}"
-         else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec
+        pr_record_body "{|" "|}" (pr_patt spc lpattop) l, lpatrec
 
       | CPatAlias (p, na) ->
         pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las
@@ -287,6 +319,7 @@ let tag_var = tag Tag.variable
 
       | CPatDelimiters (k,p) ->
         pr_delimiters k (pr_patt mt lsimplepatt p), 1
+
       | CPatCast _ ->
         assert false
     in
@@ -464,11 +497,6 @@ let tag_var = tag Tag.variable
       pr (LevelLt lapp) a  ++
         prlist (fun a -> spc () ++ pr_expl_args pr a) l)
 
-  let pr_record_body_gen pr l =
-    spc () ++
-    prlist_with_sep pr_semicolon
-      (fun (id, c) -> pr_reference id ++ str" :=" ++ pr ltop c) l
-
   let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc ()
 
   let pr_fun n = keyword "fun" ++ pr_com_at n ++ spc ()
@@ -568,10 +596,7 @@ let tag_var = tag Tag.variable
       | CApp ((None,a),l) ->
         return (pr_app (pr mt) a l, lapp)
       | CRecord l ->
-        return (
-          hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
-          latom
-        )
+        return (pr_record_body "{|" "|}" (pr spc ltop) l, latom)
       | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) ->
         return (
           hv 0 (
@@ -717,7 +742,5 @@ let tag_var = tag Tag.variable
 
   let pr_cases_pattern_expr = pr_patt ltop
 
-  let pr_record_body = pr_record_body_gen pr
-
   let pr_binders env sigma = pr_undelimited_binders spc (pr_expr env sigma ltop)
 
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 2850e4bfa0..02e04573f8 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -41,7 +41,8 @@ val pr_guard_annot
   -> recursion_order_expr option
   -> Pp.t
 
-val pr_record_body : (qualid * constr_expr) list -> Pp.t
+val pr_record : string -> string -> ('a -> Pp.t) -> 'a list -> Pp.t
+val pr_record_body : string -> string -> ('a -> Pp.t) -> (Libnames.qualid * 'a) list -> Pp.t
 val pr_binders : Environ.env -> Evd.evar_map -> local_binder_expr list -> Pp.t
 val pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t
 val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t