Setting a system to register printers for Ltac values.

The model provides three kinds of printers depending on whether the
printer needs a context, and, if yes if it supports levels. In the
latter case, it takes defaults levels for printing when in a
surrounded context (lconstr style) and for printing when not in a
surrounded context (constr style).

This model preserves the 8.7 focussing semantics of "idtac"
(i.e. focussing only when an env is needed) but it also shows that the
semantics of "idtac", which focusses the goal depending on the type of
its arguments, is a bit ad hoc to understand.

See discussion at PR#6047
"https://github.com/coq/coq/pull/6047#discussion_r148278454".

7 files changed, 221 insertions, 41 deletions

diff --git a/API/API.mli b/API/API.mli
index 608bd43cd..589745b61 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4973,12 +4973,23 @@ end
 
 module Genprint :
 sig
+  type printer_with_level =
+    { default_already_surrounded : Notation_term.tolerability;
+      default_ensure_surrounded : Notation_term.tolerability;
+      printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t }
+  type printer_result =
+    | PrinterBasic of (unit -> Pp.t)
+    | PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+    | PrinterNeedsContextAndLevel of printer_with_level
   type 'a printer = 'a -> Pp.t
-  val generic_top_print : Genarg.tlevel Genarg.generic_argument printer
+  type 'a top_printer = 'a -> printer_result
   val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
-                        'raw printer -> 'glb printer -> 'top printer -> unit
+                        'raw printer -> 'glb printer -> 'top top_printer -> unit
   val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
                         'raw printer -> unit
+  val register_val_print0 : 'top Geninterp.Val.typ -> 'top top_printer -> unit
+  val generic_top_print : Genarg.tlevel Genarg.generic_argument top_printer
+  val generic_val_print : Geninterp.Val.t top_printer
 end
 
 module Pputils :
@@ -4999,6 +5010,8 @@ sig
   val pr_name : Names.Name.t -> Pp.t
   [@@ocaml.deprecated "alias of API.Names.Name.print"]
 
+  val lsimpleconstr : Notation_term.tolerability
+  val ltop : Notation_term.tolerability
   val pr_id : Names.Id.t -> Pp.t
   val pr_or_var : ('a -> Pp.t) -> 'a Misctypes.or_var -> Pp.t
   val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
@@ -5031,6 +5044,7 @@ sig
   val pr_constr_pattern : Pattern.constr_pattern -> Pp.t
   val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t
   val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t
+  val pr_econstr_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> EConstr.constr -> Pp.t
   val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
   val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
   val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
@@ -5043,6 +5057,7 @@ sig
   val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
 
   val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
+  val pr_closed_glob_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Ltac_pretype.closed_glob_constr -> Pp.t
   val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t
   val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t
   val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 00ce94f6c..37c610e44 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -116,7 +116,13 @@ type 'a extra_genarg_printer =
         | Val.Base t ->
           begin match Val.eq t tag with
           | None -> default
-          | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+          | Some Refl ->
+             let open Genprint in
+             match generic_top_print (in_gen (Topwit wit) x) with
+             | PrinterBasic pr -> pr ()
+             | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty
+             | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+                printer (Global.env()) Evd.empty default_ensure_surrounded
           end
         | _ -> default
 
@@ -1175,8 +1181,8 @@ let declare_extra_genarg_pprule wit
     g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x
   in
   let h x =
-    let env = Global.env () in
-    h (pr_econstr_env env Evd.empty) (pr_leconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x
+    Genprint.PrinterNeedsContext (fun env sigma ->
+        h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x)
   in
   Genprint.register_print0 wit f g h
 
@@ -1186,76 +1192,111 @@ let declare_extra_vernac_genarg_pprule wit f =
 
 (** Registering *)
 
-let run_delayed c = c (Global.env ()) Evd.empty
+let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma ->
+  let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in
+  Miscprint.pr_intro_pattern print_constr p)
+
+let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma ->
+  pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma,
+               pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r)
+
+let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma ->
+  let sigma, bl = bl env sigma in
+  Miscprint.pr_bindings
+    (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl)
+
+let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma ->
+  let sigma, bl = bl env sigma in
+  pr_with_bindings
+    (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl)
 
-let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *)
-  | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (snd (run_delayed g))
-  | clear_flag,ElimOnAnonHyp n as x -> x
-  | clear_flag,ElimOnIdent id as x -> x
+let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma ->
+  let sigma, c = match c with
+  | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c)
+  | clear_flag,ElimOnAnonHyp n as x -> sigma, x
+  | clear_flag,ElimOnIdent id as x -> sigma, x in
+  pr_destruction_arg
+    (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c)
+
+let make_constr_printer f c =
+  Genprint.PrinterNeedsContextAndLevel {
+      Genprint.default_already_surrounded = Ppconstr.lsimpleconstr;
+      Genprint.default_ensure_surrounded = Ppconstr.ltop;
+      Genprint.printer = (fun env sigma n -> f env sigma n c)}
+
+let lift f a = Genprint.PrinterBasic (fun () -> f a)
 
 let () =
   let pr_bool b = if b then str "true" else str "false" in
   let pr_unit _ = str "()" in
-  let pr_string s = str "\"" ++ str s ++ str "\"" in
   Genprint.register_print0 wit_int_or_var
-    (pr_or_var int) (pr_or_var int) int;
+    (pr_or_var int) (pr_or_var int) (lift int);
   Genprint.register_print0 wit_ref
-    pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+    pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global);
   Genprint.register_print0 wit_ident
-    pr_id pr_id pr_id;
+    pr_id pr_id (lift pr_id);
   Genprint.register_print0 wit_var
-    (pr_located pr_id) (pr_located pr_id) pr_id;
+    (pr_located pr_id) (pr_located pr_id) (lift pr_id);
   Genprint.register_print0
     wit_intro_pattern
     (Miscprint.pr_intro_pattern pr_constr_expr)
     (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
-    (Miscprint.pr_intro_pattern (fun c -> pr_econstr (snd (run_delayed c))));
+    pr_intro_pattern_env;
   Genprint.register_print0
     wit_clause_dft_concl
     (pr_clauses (Some true) pr_lident)
     (pr_clauses (Some true) pr_lident)
-    (pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)))
+    (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c))
   ;
   Genprint.register_print0
     wit_constr
     Ppconstr.pr_constr_expr
     (fun (c, _) -> Printer.pr_glob_constr c)
-    Printer.pr_econstr
+    (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0
     wit_uconstr
     Ppconstr.pr_constr_expr
     (fun (c,_) -> Printer.pr_glob_constr c)
-    Printer.pr_closed_glob
+    (make_constr_printer Printer.pr_closed_glob_n_env)
   ;
   Genprint.register_print0
     wit_open_constr
     Ppconstr.pr_constr_expr
     (fun (c, _) -> Printer.pr_glob_constr c)
-    Printer.pr_econstr
+    (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0 wit_red_expr
     (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
     (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
-    (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern));
-  Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
+    pr_red_expr_env
+  ;
+  Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis);
   Genprint.register_print0 wit_bindings
     (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
     (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (snd (run_delayed it)));
+    pr_bindings_env
+  ;
   Genprint.register_print0 wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_with_bindings pr_econstr pr_leconstr (snd (run_delayed it)));
+    pr_with_bindings_env
+  ;
+  Genprint.register_print0 wit_open_constr_with_bindings
+    (pr_with_bindings pr_constr_expr pr_lconstr_expr)
+    (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+    pr_with_bindings_env
+  ;
   Genprint.register_print0 Tacarg.wit_destruction_arg
     (pr_destruction_arg pr_constr_expr pr_lconstr_expr)
     (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_destruction_arg pr_econstr pr_leconstr (run_delayed_destruction_arg it));
-  Genprint.register_print0 Stdarg.wit_int int int int;
-  Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
-  Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
-  Genprint.register_print0 Stdarg.wit_pre_ident str str str;
-  Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string
+    pr_destruction_arg_env
+  ;
+  Genprint.register_print0 Stdarg.wit_int int int (lift int);
+  Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool);
+  Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit);
+  Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str);
+  Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring)
 
 let () =
   let printer _ _ prtac = prtac (0, E) in
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index b47f07a45..5ecfaf590 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -125,3 +125,6 @@ val pr_value : tolerability -> Val.t -> Pp.t
 
 
 val ltop : tolerability
+
+val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) ->
+  'a Genprint.top_printer
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index a79a92a66..4d171ecbc 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -17,15 +17,23 @@ open Geninterp
 
 exception CannotCoerceTo of string
 
+let base_val_typ wit =
+  match val_tag (topwit wit) with Val.Base t -> t | _ -> CErrors.anomaly (Pp.str "Not a base val.")
+
 let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) =
   let wit = Genarg.create_arg "constr_context" in
   let () = register_val0 wit None in
+  let () = Genprint.register_val_print0 (base_val_typ wit)
+    (Pptactic.make_constr_printer Printer.pr_econstr_n_env) in
   wit
 
 (* includes idents known to be bound and references *)
 let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type) =
   let wit = Genarg.create_arg "constr_under_binders" in
   let () = register_val0 wit None in
+  let () = Genprint.register_val_print0 (base_val_typ wit)
+             (fun c ->
+               Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in
   wit
 
 (** All the types considered here are base types *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 66f124d2d..ec8777a45 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -76,6 +76,9 @@ let out_gen wit v =
 
 let val_tag wit = val_tag (topwit wit)
 
+let base_val_typ wit =
+  match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.")
+
 let pr_argument_type arg =
   let Val.Dyn (tag, _) = arg in
   Val.pr tag
@@ -124,6 +127,8 @@ type tacvalue =
 let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
   let wit = Genarg.create_arg "tacvalue" in
   let () = register_val0 wit None in
+  let () = Genprint.register_val_print0 (base_val_typ wit)
+             (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in
   wit
 
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
diff --git a/printing/genprint.ml b/printing/genprint.ml
index b20ea0b62..776a212b5 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -8,13 +8,100 @@
 
 open Pp
 open Genarg
+open Geninterp
+
+(* We register printers at two levels:
+   - generic arguments for general printers
+   - generic values for printing ltac values *)
+
+(* Printing generic values *)
+
+type printer_with_level =
+  { default_already_surrounded : Notation_term.tolerability;
+    default_ensure_surrounded : Notation_term.tolerability;
+    printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t }
+
+type printer_result =
+| PrinterBasic of (unit -> Pp.t)
+| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+| PrinterNeedsContextAndLevel of printer_with_level
 
 type 'a printer = 'a -> Pp.t
 
+type 'a top_printer = 'a -> printer_result
+
+module ValMap = ValTMap (struct type 'a t = 'a -> printer_result end)
+
+let print0_val_map = ref ValMap.empty
+
+let find_print_val_fun tag =
+  try ValMap.find tag !print0_val_map
+  with Not_found ->
+    let msg s = Pp.(str "print function not found for a value interpreted as " ++ str s ++ str ".") in
+    CErrors.anomaly (msg (Val.repr tag))
+
+let generic_val_print v =
+  let Val.Dyn (tag,v) = v in
+  find_print_val_fun tag v
+
+let register_val_print0 s pr =
+  print0_val_map := ValMap.add s pr !print0_val_map
+
+let combine_dont_needs pr_pair pr1 = function
+  | PrinterBasic pr2 ->
+     PrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ()))
+  | PrinterNeedsContext pr2 ->
+     PrinterNeedsContext (fun env sigma ->
+         pr_pair (pr1 ()) (pr2 env sigma))
+  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+     PrinterNeedsContext (fun env sigma ->
+         pr_pair (pr1 ()) (printer env sigma default_ensure_surrounded))
+
+let combine_needs pr_pair pr1 = function
+  | PrinterBasic pr2 ->
+     PrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ()))
+  | PrinterNeedsContext pr2 ->
+     PrinterNeedsContext (fun env sigma ->
+         pr_pair (pr1 env sigma) (pr2 env sigma))
+  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+     PrinterNeedsContext (fun env sigma ->
+         pr_pair (pr1 env sigma) (printer env sigma default_ensure_surrounded))
+
+let combine pr_pair pr1 v2 =
+  match pr1 with
+  | PrinterBasic pr1 ->
+     combine_dont_needs pr_pair pr1 (generic_val_print v2)
+  | PrinterNeedsContext pr1 ->
+     combine_needs pr_pair pr1 (generic_val_print v2)
+  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+     combine_needs pr_pair (fun env sigma -> printer env sigma default_ensure_surrounded)
+       (generic_val_print v2)
+
+let _ =
+  let pr_cons a b = Pp.(a ++ spc () ++ b) in
+  register_val_print0 Val.typ_list
+    (function
+     | [] -> PrinterBasic mt
+     | a::l ->
+        List.fold_left (combine pr_cons) (generic_val_print a) l)
+
+let _ =
+  register_val_print0 Val.typ_opt
+    (function
+     | None -> PrinterBasic Pp.mt
+     | Some v -> generic_val_print v)
+
+let _ =
+  let pr_pair a b = Pp.(a ++ spc () ++ b) in
+  register_val_print0 Val.typ_pair
+    (fun (v1,v2) -> combine pr_pair (generic_val_print v1) v2)
+
+(* Printing generic arguments *)
+
 type ('raw, 'glb, 'top) genprinter = {
   raw : 'raw printer;
   glb : 'glb printer;
-  top : 'top printer;
+  top : 'top -> printer_result;
 }
 
 module PrintObj =
@@ -27,7 +114,7 @@ struct
     let printer = {
       raw = (fun _ -> str "<genarg:" ++ str name ++ str ">");
       glb = (fun _ -> str "<genarg:" ++ str name ++ str ">");
-      top = (fun _ -> str "<genarg:" ++ str name ++ str ">");
+      top = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
     } in
     Some printer
   | _ -> assert false
@@ -37,7 +124,13 @@ module Print = Register (PrintObj)
 
 let register_print0 wit raw glb top =
   let printer = { raw; glb; top; } in
-  Print.register0 wit printer
+  Print.register0 wit printer;
+  match val_tag (Topwit wit), wit with
+  | Val.Base t, ExtraArg t' when Geninterp.Val.repr t = ArgT.repr t' ->
+     register_val_print0 t top
+  | _ ->
+     (* An alias, thus no primitive printer attached *)
+     ()
 
 let register_vernac_print0 wit raw =
   let glb _ = CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.") in
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 76d80f3b5..2da9bbc36 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -10,22 +10,37 @@
 
 open Genarg
 
+type printer_with_level =
+  { default_already_surrounded : Notation_term.tolerability;
+    default_ensure_surrounded : Notation_term.tolerability;
+    printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t }
+
+type printer_result =
+| PrinterBasic of (unit -> Pp.t)
+| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+| PrinterNeedsContextAndLevel of printer_with_level
+
 type 'a printer = 'a -> Pp.t
 
-val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> Pp.t
+type 'a top_printer = 'a -> printer_result
+
+val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw printer
 (** Printer for raw level generic arguments. *)
 
-val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> Pp.t
+val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb printer
 (** Printer for glob level generic arguments. *)
 
-val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> Pp.t
+val top_print : ('raw, 'glb, 'top) genarg_type -> 'top top_printer
 (** Printer for top level generic arguments. *)
 
-val generic_raw_print : rlevel generic_argument printer
-val generic_glb_print : glevel generic_argument printer
-val generic_top_print : tlevel generic_argument printer
-
 val register_print0 : ('raw, 'glb, 'top) genarg_type ->
-  'raw printer -> 'glb printer -> 'top printer -> unit
+  'raw printer -> 'glb printer -> ('top -> printer_result) -> unit
+val register_val_print0 : 'top Geninterp.Val.typ ->
+  'top top_printer -> unit
 val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type ->
   'raw printer -> unit
+
+val generic_raw_print : rlevel generic_argument printer
+val generic_glb_print : glevel generic_argument printer
+val generic_top_print : tlevel generic_argument top_printer
+val generic_val_print : Geninterp.Val.t top_printer