Binding ltac printing functions to the system of generic printing.

This concerns pr_value and message_of_value.

This has a few consequences. For instance, no more ad hoc message "a
term" or "a tactic", when not enough information is available for
printing, one gets a generic message "a value of type foobar".

But we also have more printers, satisfying e.g. request #5786.

5 files changed, 105 insertions, 63 deletions

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 37c610e44b..e467d3e2ca 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1220,8 +1220,8 @@ let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma ->
 
 let make_constr_printer f c =
   Genprint.PrinterNeedsContextAndLevel {
-      Genprint.default_already_surrounded = Ppconstr.lsimpleconstr;
-      Genprint.default_ensure_surrounded = Ppconstr.ltop;
+      Genprint.default_already_surrounded = Ppconstr.ltop;
+      Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr;
       Genprint.printer = (fun env sigma n -> f env sigma n c)}
 
 let lift f a = Genprint.PrinterBasic (fun () -> f a)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ec8777a45c..8b90a0188c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -236,24 +236,16 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with
 (* Displays a value *)
 let pr_value env v =
   let v = Value.normalize v in
-  if has_type v (topwit wit_tacvalue) then str "a tactic"
-  else if has_type v (topwit wit_constr_context) then
-    let c = out_gen (topwit wit_constr_context) v in
+  let pr_with_env pr =
     match env with
-    | Some (env,sigma) -> pr_leconstr_env env sigma c
-    | _ -> str "a term"
-  else if has_type v (topwit wit_constr) then
-    let c = out_gen (topwit wit_constr) v in
-    match env with
-    | Some (env,sigma) -> pr_leconstr_env env sigma c
-    | _ -> str "a term"
-  else if has_type v (topwit wit_constr_under_binders) then
-    let c = out_gen (topwit wit_constr_under_binders) v in
-    match env with
-    | Some (env,sigma) -> pr_lconstr_under_binders_env env sigma c
-    | _ -> str "a term"
-  else
-    str "a value of type" ++ spc () ++ pr_argument_type v
+    | Some (env,sigma) -> pr env sigma
+    | None -> str "a value of type" ++ spc () ++ pr_argument_type v in
+  let open Genprint in
+  match generic_val_print v with
+  | PrinterBasic pr -> pr ()
+  | PrinterNeedsContext pr -> pr_with_env pr
+  | PrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
+     pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
 
 let pr_closure env ist body =
   let pp_body = Pptactic.pr_glob_tactic env body in
@@ -823,51 +815,16 @@ let interp_constr_may_eval ist env sigma c =
   end
 
 (** TODO: should use dedicated printers *)
-let rec message_of_value v =
+let message_of_value v =
   let v = Value.normalize v in
-  let open Ftactic in
-  if has_type v (topwit wit_tacvalue) then
-    Ftactic.return (str "<tactic>")
-  else if has_type v (topwit wit_constr) then
-    let v = out_gen (topwit wit_constr) v in
-    Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end
-  else if has_type v (topwit wit_constr_under_binders) then
-    let c = out_gen (topwit wit_constr_under_binders) v in
-    Ftactic.enter begin fun gl ->
-      Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c)
-    end
-  else if has_type v (topwit wit_unit) then
-    Ftactic.return (str "()")
-  else if has_type v (topwit wit_int) then
-    Ftactic.return (int (out_gen (topwit wit_int) v))
-  else if has_type v (topwit wit_intro_pattern) then
-    let p = out_gen (topwit wit_intro_pattern) v in
-    let print env sigma c =
-      let (sigma, c) = c env sigma in
-      pr_econstr_env env sigma c
-    in
-    Ftactic.enter begin fun gl ->
-      Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p)
-    end
-  else if has_type v (topwit wit_constr_context) then
-    let c = out_gen (topwit wit_constr_context) v in
-    Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end
-  else if has_type v (topwit wit_uconstr) then
-    let c = out_gen (topwit wit_uconstr) v in
-    Ftactic.enter begin fun gl ->
-      Ftactic.return (pr_closed_glob_env (pf_env gl)
-                        (project gl) c)
-    end
-  else if has_type v (topwit wit_var) then
-    let id = out_gen (topwit wit_var) v in
-    Ftactic.enter begin fun gl -> Ftactic.return (Id.print id) end
-  else match Value.to_list v with
-  | Some l ->
-    Ftactic.List.map message_of_value l >>= fun l ->
-    Ftactic.return (prlist_with_sep spc (fun x -> x) l)
-  | None ->
-    let tag = pr_argument_type v in
-    Ftactic.return (str "<" ++ tag ++ str ">") (** TODO *)
+  let pr_with_env pr =
+    Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in
+  let open Genprint in
+  match generic_val_print v with
+  | PrinterBasic pr -> Ftactic.return (pr ())
+  | PrinterNeedsContext pr -> pr_with_env pr
+  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+     pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded)
 
 let interp_message_token ist = function
   | MsgString s -> Ftactic.return (str s)
diff --git a/test-suite/bugs/closed/5786.v b/test-suite/bugs/closed/5786.v
new file mode 100644
index 0000000000..20301ec4f5
--- /dev/null
+++ b/test-suite/bugs/closed/5786.v
@@ -0,0 +1,29 @@
+(* Printing all kinds of Ltac generic arguments *)
+
+Tactic Notation "myidtac" string(v) := idtac v.
+Goal True.
+myidtac "foo".
+Abort.
+
+Tactic Notation "myidtac2" ref(c) := idtac c.
+Goal True.
+myidtac2 True.
+Abort.
+
+Tactic Notation "myidtac3" preident(s) := idtac s.
+Goal True.
+myidtac3 foo.
+Abort.
+
+Tactic Notation "myidtac4" int_or_var(n) := idtac n.
+Goal True.
+myidtac4 3.
+Abort.
+
+Tactic Notation "myidtac5" ident(id) := idtac id.
+Goal True.
+myidtac5 foo.
+Abort.
+
+
+
diff --git a/test-suite/output/idtac.out b/test-suite/output/idtac.out
new file mode 100644
index 0000000000..3855f88a72
--- /dev/null
+++ b/test-suite/output/idtac.out
@@ -0,0 +1,11 @@
+"foo"
+True
+foo
+3
+foo
+2
+< True False Prop >
+< True False Prop >
+<  >
+<  >
+<< 1 2 3 >>
diff --git a/test-suite/output/idtac.v b/test-suite/output/idtac.v
new file mode 100644
index 0000000000..ac60ea9175
--- /dev/null
+++ b/test-suite/output/idtac.v
@@ -0,0 +1,45 @@
+(* Printing all kinds of Ltac generic arguments *)
+
+Tactic Notation "myidtac" string(v) := idtac v.
+Goal True.
+myidtac "foo".
+Abort.
+
+Tactic Notation "myidtac2" ref(c) := idtac c.
+Goal True.
+myidtac2 True.
+Abort.
+
+Tactic Notation "myidtac3" preident(s) := idtac s.
+Goal True.
+myidtac3 foo.
+Abort.
+
+Tactic Notation "myidtac4" int_or_var(n) := idtac n.
+Goal True.
+myidtac4 3.
+Abort.
+
+Tactic Notation "myidtac5" ident(id) := idtac id.
+Goal True.
+myidtac5 foo.
+Abort.
+
+(* Checking non focussing of idtac for integers *)
+Goal True/\True. split.
+all:let c:=numgoals in idtac c.
+Abort.
+
+(* Checking printing of lists and its focussing *)
+Tactic Notation "myidtac6" constr_list(l) := idtac "<" l ">".
+Goal True/\True. split.
+all:myidtac6 True False Prop.
+(* An empty list is focussing because of interp_genarg of a constr *)
+(* even if it is not focussing on printing *)
+all:myidtac6.
+Abort.
+
+Tactic Notation "myidtac7" int_list(l) := idtac "<<" l ">>".
+Goal True/\True. split.
+all:myidtac7 1 2 3.
+Abort.