Ltac2: fix printing of constructor values with arguments

Fix coq#18556

plugins/ltac2/tac2print.ml

@@ -737,12 +737,14 @@ let register_val_printer kn pr =
 
 open Tac2ffi
 
-let rec pr_valexpr env sigma v t = match kind t with
+let rec pr_valexpr_gen env sigma lvl v t = match kind t with
 | GTypVar _ -> str "<poly>"
 | GTypRef (Other kn, params) ->
   let pr = try Some (KNmap.find kn !printers) with Not_found -> None in
   begin match pr with
-  | Some pr -> pr.val_printer env sigma v params
+  | Some pr ->
+    (* for now assume all printers produce atomic expressions so no need to pass [lvl] *)
+    pr.val_printer env sigma v params
   | None ->
     let n, repr = Tac2env.interp_type kn in
     if KerName.equal kn t_list then
@@ -756,29 +758,37 @@ let rec pr_valexpr env sigma v t = match kind t with
       if Valexpr.is_int v then
         pr_internal_constructor kn (Tac2ffi.to_int v) true
       else
+        let paren = match lvl with
+          | E0 -> paren
+          | E1 | E2 | E3 | E4 | E5 -> fun x -> x
+        in
         let (n, args) = Tac2ffi.to_block v in
         let (id, tpe) = find_constructor n false alg.galg_constructors in
         let knc = change_kn_label kn id in
         let args = pr_constrargs env sigma params args tpe in
-        hv 2 (pr_constructor knc ++ spc () ++ str "(" ++ args ++ str ")")
+        paren (pr_constructor knc ++ spc () ++ args)
     | GTydRec rcd ->
       let (_, args) = Tac2ffi.to_block v in
       pr_record env sigma params args rcd
     | GTydOpn ->
       begin match Tac2ffi.to_open v with
       | (knc, [||]) -> pr_constructor knc
       | (knc, args) ->
+        let paren = match lvl with
+          | E0 -> paren
+          | E1 | E2 | E3 | E4 | E5 -> fun x -> x
+        in
         let data = Tac2env.interp_constructor knc in
         let args = pr_constrargs env sigma params args data.Tac2env.cdata_args in
-        hv 2 (pr_constructor knc ++ spc () ++ str "(" ++ args ++ str ")")
+        paren (pr_constructor knc ++ spc () ++ args)
       end
   end
 | GTypArrow _ -> str "<fun>"
 | GTypRef (Tuple 0, []) -> str "()"
 | GTypRef (Tuple _, tl) ->
   let blk = Array.to_list (snd (to_block v)) in
   if List.length blk == List.length tl then
-    let prs = List.map2 (fun v t -> pr_valexpr env sigma v t) blk tl in
+    let prs = List.map2 (fun v t -> pr_valexpr_gen env sigma E1 v t) blk tl in
     hv 2 (str "(" ++ prlist_with_sep pr_comma (fun p -> p) prs ++ str ")")
   else
     str "<unknown>"
@@ -788,7 +798,7 @@ and pr_constrargs env sigma params args tpe =
   let tpe = List.map (fun t -> subst_type subst t) tpe in
   let args = Array.to_list args in
   let args = List.combine args tpe in
-  prlist_with_sep pr_comma (fun (v, t) -> pr_valexpr env sigma v t) args
+  pr_sequence (fun (v, t) -> pr_valexpr_gen env sigma E0 v t) args
 
 and pr_record env sigma params args rcd =
   let subst = Array.of_list params in
@@ -797,13 +807,15 @@ and pr_record env sigma params args rcd =
   let args = Array.to_list args in
   let fields = List.combine rcd args in
   let pr_field ((id, t), arg) =
-    Id.print id ++ spc () ++ str ":=" ++ spc () ++ pr_valexpr env sigma arg t
+    Id.print id ++ spc () ++ str ":=" ++ spc () ++ pr_valexpr_gen env sigma E1 arg t
   in
   str "{" ++ spc () ++ prlist_with_sep pr_semicolon pr_field fields ++ spc () ++ str "}"
 
 and pr_val_list env sigma args tpe =
-  let pr v = pr_valexpr env sigma v tpe in
-  str "[" ++ prlist_with_sep pr_semicolon pr args ++ str "]"
+  let pr v = pr_valexpr_gen env sigma E4 v tpe in
+  hov 1 (str "[" ++ prlist_with_sep pr_semicolon pr args ++ str "]")
+
+let pr_valexpr env sigma v t = pr_valexpr_gen env sigma E5 v t
 
 let register_init n f =
   let kn = KerName.make Tac2env.coq_prefix (Label.make n) in
@@ -827,29 +839,29 @@ end
 let () = register_init "constr" begin fun env sigma c ->
   let c = to_constr c in
   let c = try Printer.pr_leconstr_env env sigma c with _ -> str "..." in
-  str "constr:(" ++ c ++ str ")"
+  hov 2 (str "constr:(" ++ c ++ str ")")
 end
 
 let () = register_init "preterm" begin fun env sigma c ->
   let c = to_preterm c in
   (* XXX should we get the ltac2 env out of the closure and print it too? Maybe with a debug flag? *)
   let c = try Printer.pr_closed_glob_env env sigma c with _ -> str "..." in
-  str "preterm:(" ++ c ++ str ")"
+  hov 2 (str "preterm:(" ++ c ++ str ")")
 end
 
 let () = register_init "pattern" begin fun env sigma c ->
   let c = to_pattern c in
   let c = try Printer.pr_lconstr_pattern_env env sigma c with _ -> str "..." in
-  str "pat:(" ++ c ++ str ")"
+  hov 2 (str "pat:(" ++ c ++ str ")")
 end
 
 let () = register_init "message" begin fun _ _ pp ->
-  str "message:(" ++ to_pp pp ++ str ")"
+  hov 2 (str "message:(" ++ to_pp pp ++ str ")")
 end
 
 let () = register_init "err" begin fun _ _ e ->
   let e = to_ext val_exn e in
-  str "err:(" ++ CErrors.iprint_no_report e ++ str ")"
+  hov 2 (str "err:(" ++ CErrors.iprint_no_report e ++ str ")")
 end
 
 let () =

test-suite/output/bug_16716.out

@@ -1,3 +1,3 @@
 File "./output/bug_16716.v", line 11, characters 0-55:
 The command has indeed failed with message:
-Uncaught Ltac2 exception: E (constr:(?X4.(r _)))
+Uncaught Ltac2 exception: E constr:(?X4.(r _))

test-suite/output/bug_17155.out

@@ -1,12 +1,12 @@
 File "./output/bug_17155.v", line 6, characters 0-23:
 The command has indeed failed with message:
-Uncaught Ltac2 exception: Invalid_argument (None)
+Uncaught Ltac2 exception: Invalid_argument None
 File "./output/bug_17155.v", line 8, characters 0-23:
 The command has indeed failed with message:
 Backtrace:
 Call M.g
 Call bug_17155.M.f (* local *)
 Prim <coq-core.plugins.ltac2:throw>
-Uncaught Ltac2 exception: Invalid_argument (None)
+Uncaught Ltac2 exception: Invalid_argument None
 Ltac2 M.g : unit -> 'a
       M.g := fun _ => bug_17155.M.f (* local *) ()

test-suite/output/ltac2_bt.out

@@ -6,14 +6,14 @@ Call {Control.zero e}
 Prim <coq-core.plugins.ltac2:zero>
 Backtrace:
 
-Uncaught Ltac2 exception: Invalid_argument (None)
+Uncaught Ltac2 exception: Invalid_argument None
 File "./output/ltac2_bt.v", line 9, characters 2-49:
 The command has indeed failed with message:
 Backtrace:
 Prim <coq-core.plugins.ltac2:plus>
 Call {Control.throw e}
 Prim <coq-core.plugins.ltac2:throw>
-Uncaught Ltac2 exception: Invalid_argument (None)
+Uncaught Ltac2 exception: Invalid_argument None
 File "./output/ltac2_bt.v", line 10, characters 2-60:
 The command has indeed failed with message:
 Backtrace:
@@ -22,11 +22,11 @@ Call f
 Prim <coq-core.plugins.ltac2:zero>
 Backtrace:
 
-Uncaught Ltac2 exception: Invalid_argument (None)
+Uncaught Ltac2 exception: Invalid_argument None
 File "./output/ltac2_bt.v", line 11, characters 2-61:
 The command has indeed failed with message:
 Backtrace:
 Prim <coq-core.plugins.ltac2:plus_bt>
 Call f
 Prim <coq-core.plugins.ltac2:zero>
-Uncaught Ltac2 exception: Invalid_argument (None)
+Uncaught Ltac2 exception: Invalid_argument None

test-suite/output/ltac2_notations_eval_in.out

@@ -16,6 +16,6 @@ constr:((fix add (n m : nat) {struct n} : nat :=
 - : constr = constr:(6)
 - : constr = constr:(1 + 2 + 3)
 - : constr = constr:(1 + 2 + 3)
-- : constr list = [constr:(0 <> 0); constr:(0 = 0 -> False);
-constr:((fun P : Prop => P -> False) (0 = 0)); constr:(
-0 <> 0)]
+- : constr list =
+[constr:(0 <> 0); constr:(0 = 0 -> False);
+ constr:((fun P : Prop => P -> False) (0 = 0)); constr:(0 <> 0)]

test-suite/output/ltac2_pr_ctor.out

@@ -0,0 +1,3 @@
+- : pair = C 0 0
+- : pair' = C' (0, 0)
+- : ppair = D (C 0 0)

test-suite/output/ltac2_pr_ctor.v

@@ -0,0 +1,17 @@
+Require Import Ltac2.Ltac2.
+
+(* cf bug #18556 *)
+
+Ltac2 Type pair := [ C (int, int) ].
+
+Ltac2 Eval C 0 0.
+(* prints "C (0, 0)", should be "C 0 0" *)
+
+Ltac2 Type pair' := [ C' (int * int) ].
+
+Ltac2 Eval C' (0, 0).
+(* prints "C' ((0, 0))", sound but over-parenthesized *)
+
+Ltac2 Type ppair := [ D (pair) ].
+
+Ltac2 Eval D (C 0 0).