Merge PR #6047: A generic printer for ltac values

6 files changed, 155 insertions, 22 deletions

diff --git a/printing/genprint.ml b/printing/genprint.ml
index 543b05024d..776a212b5c 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,6 +124,18 @@ module Print = Register (PrintObj)
 
 let register_print0 wit raw glb top =
   let printer = { raw; glb; top; } in
+  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
+  let top _ = CErrors.anomaly (Pp.str "vernac argument needs not wit printer.") in
+  let printer = { raw; glb; top; } in
   Print.register0 wit printer
 
 let raw_print wit v = (Print.obj wit).raw v
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 130a89c929..2da9bbc36b 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -10,20 +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 register_print0 : ('raw, 'glb, 'top) genarg_type ->
+  '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 printer
-
-val register_print0 : ('raw, 'glb, 'top) genarg_type ->
-  'raw printer -> 'glb printer -> 'top printer -> unit
+val generic_top_print : tlevel generic_argument top_printer
+val generic_val_print : Geninterp.Val.t top_printer
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 102c6ef6de..109a40a037 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -738,34 +738,40 @@ let tag_var = tag Tag.variable
     pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
   }
 
-  type precedence =  Notation_term.precedence * Notation_term.parenRelation
   let modular_constr_pr = pr
   let rec fix rf x = rf (fix rf) x
   let pr = fix modular_constr_pr mt
 
+  let pr prec = function
+    (* A toplevel printer hack mimicking parsing, incidentally meaning
+       that we cannot use [pr] correctly anymore in a recursive loop
+       if the current expr is followed by other exprs which would be
+       interpreted as arguments *)
+    | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us
+    | c -> pr prec c
+
   let transf env c =
     if !Flags.beautify_file then
       let r = Constrintern.for_grammar (Constrintern.intern_constr env) c in
       Constrextern.extern_glob_constr (Termops.vars_of_env env) r
     else c
 
-  let pr prec c = pr prec (transf (Global.env()) c)
+  let pr_expr prec c = pr prec (transf (Global.env()) c)
 
-  let pr_simpleconstr = function
-    | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us
-    | c -> pr lsimpleconstr c
+  let pr_simpleconstr = pr_expr lsimpleconstr
 
   let default_term_pr = {
     pr_constr_expr   = pr_simpleconstr;
-    pr_lconstr_expr  = pr ltop;
+    pr_lconstr_expr  = pr_expr ltop;
     pr_constr_pattern_expr  = pr_simpleconstr;
-    pr_lconstr_pattern_expr = pr ltop
+    pr_lconstr_pattern_expr = pr_expr ltop
   }
 
   let term_pr = ref default_term_pr
 
   let set_term_pr = (:=) term_pr
 
+  let pr_constr_expr_n n c = pr_expr n c
   let pr_constr_expr c   = !term_pr.pr_constr_expr   c
   let pr_lconstr_expr c  = !term_pr.pr_lconstr_expr  c
   let pr_constr_pattern_expr c  = !term_pr.pr_constr_pattern_expr  c
@@ -775,5 +781,5 @@ let tag_var = tag Tag.variable
 
   let pr_record_body = pr_record_body_gen pr
 
-  let pr_binders = pr_undelimited_binders spc (pr ltop)
+  let pr_binders = pr_undelimited_binders spc (pr_expr ltop)
 
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 7546c748d8..be96cfce50 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -60,6 +60,7 @@ val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
 val pr_constr_expr : constr_expr -> Pp.t
 val pr_lconstr_expr : constr_expr -> Pp.t
 val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t
+val pr_constr_expr_n : tolerability -> constr_expr -> Pp.t
 
 type term_pr = {
   pr_constr_expr   : constr_expr -> Pp.t;
@@ -86,9 +87,8 @@ val default_term_pr : term_pr
   Which has the same type. We can turn a modular printer into a printer by
   taking its fixpoint. *)
 
-type precedence
-val lsimpleconstr : precedence
-val ltop : precedence
+val lsimpleconstr : tolerability
+val ltop : tolerability
 val modular_constr_pr :
-  ((unit->Pp.t) -> precedence -> constr_expr -> Pp.t) ->
-  (unit->Pp.t) -> precedence  -> constr_expr -> Pp.t
+  ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) ->
+  (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t
diff --git a/printing/printer.ml b/printing/printer.ml
index 28b10c7812..c6650ea3b8 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -79,11 +79,14 @@ let _ =
    and only names of goal/section variables and rel names that do
    _not_ occur in the scope of the binder to be printed are avoided. *)
 
+let pr_econstr_n_core goal_concl_style env sigma n t =
+  pr_constr_expr_n n (extern_constr goal_concl_style env sigma t)
 let pr_econstr_core goal_concl_style env sigma t =
   pr_constr_expr (extern_constr goal_concl_style env sigma t)
 let pr_leconstr_core goal_concl_style env sigma t =
   pr_lconstr_expr (extern_constr goal_concl_style env sigma t)
 
+let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c)
 let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c)
 let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c)
 let _ = Hook.set Refine.pr_constr pr_constr_env
@@ -94,6 +97,7 @@ let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (ECons
 let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c
 let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c
 
+let pr_econstr_n_env env sigma c = pr_econstr_n_core false env sigma c
 let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c
 let pr_econstr_env env sigma c = pr_econstr_core false env sigma c
 
@@ -166,6 +170,8 @@ let pr_glob_constr c =
   let (sigma, env) = get_current_context () in
   pr_glob_constr_env env c
 
+let pr_closed_glob_n_env env sigma n c =
+  pr_constr_expr_n n (extern_closed_glob false env sigma c)
 let pr_closed_glob_env env sigma c =
   pr_constr_expr (extern_closed_glob false env sigma c)
 let pr_closed_glob c =
diff --git a/printing/printer.mli b/printing/printer.mli
index ba849bee6a..658ea6060b 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -33,6 +33,8 @@ val pr_constr_env          : env -> evar_map -> constr -> Pp.t
 val pr_constr              : constr -> Pp.t
 val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
+val pr_constr_n_env        : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t
+
 (** Same, but resilient to [Nametab] errors. Prints fully-qualified
     names when [shortest_qualid_of_global] has failed. Prints "??"
     in case of remaining issues (such as reference not in env). *)
@@ -48,6 +50,8 @@ val pr_econstr         : EConstr.t -> Pp.t
 val pr_leconstr_env     : env -> evar_map -> EConstr.t -> Pp.t
 val pr_leconstr         : EConstr.t -> Pp.t
 
+val pr_econstr_n_env    : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t
+
 val pr_etype_env           : env -> evar_map -> EConstr.types -> Pp.t
 val pr_letype_env           : env -> evar_map -> EConstr.types -> Pp.t
 
@@ -70,6 +74,7 @@ val pr_ltype               : types -> Pp.t
 val pr_type_env            : env -> evar_map -> types -> Pp.t
 val pr_type                : types -> Pp.t
 
+val pr_closed_glob_n_env   : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t
 val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> Pp.t
 val pr_closed_glob         : closed_glob_constr -> Pp.t