Merge PR #6158: Allows a level in the raw and glob printers

3 files changed, 57 insertions, 39 deletions

diff --git a/printing/genprint.ml b/printing/genprint.ml
index 776a212b5..37a94fe21 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -16,21 +16,27 @@ open Geninterp
 
 (* Printing generic values *)
 
-type printer_with_level =
+type 'a 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 }
+    printer : 'a }
 
 type printer_result =
 | PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
-| PrinterNeedsContextAndLevel of printer_with_level
+| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
 
-type 'a printer = 'a -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
 
-type 'a top_printer = 'a -> printer_result
+type top_printer_result =
+| TopPrinterBasic of (unit -> Pp.t)
+| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
 
-module ValMap = ValTMap (struct type 'a t = 'a -> printer_result end)
+type 'a printer = 'a -> printer_result
+
+type 'a top_printer = 'a -> top_printer_result
+
+module ValMap = ValTMap (struct type 'a t = 'a -> top_printer_result end)
 
 let print0_val_map = ref ValMap.empty
 
@@ -48,32 +54,32 @@ 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 ->
+  | TopPrinterBasic pr2 ->
+     TopPrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ()))
+  | TopPrinterNeedsContext pr2 ->
+     TopPrinterNeedsContext (fun env sigma ->
          pr_pair (pr1 ()) (pr2 env sigma))
-  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
-     PrinterNeedsContext (fun env sigma ->
+  | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+     TopPrinterNeedsContext (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 ->
+  | TopPrinterBasic pr2 ->
+     TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ()))
+  | TopPrinterNeedsContext pr2 ->
+     TopPrinterNeedsContext (fun env sigma ->
          pr_pair (pr1 env sigma) (pr2 env sigma))
-  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
-     PrinterNeedsContext (fun env sigma ->
+  | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+     TopPrinterNeedsContext (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 ->
+  | TopPrinterBasic pr1 ->
      combine_dont_needs pr_pair pr1 (generic_val_print v2)
-  | PrinterNeedsContext pr1 ->
+  | TopPrinterNeedsContext pr1 ->
      combine_needs pr_pair pr1 (generic_val_print v2)
-  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+  | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
      combine_needs pr_pair (fun env sigma -> printer env sigma default_ensure_surrounded)
        (generic_val_print v2)
 
@@ -81,14 +87,14 @@ let _ =
   let pr_cons a b = Pp.(a ++ spc () ++ b) in
   register_val_print0 Val.typ_list
     (function
-     | [] -> PrinterBasic mt
+     | [] -> TopPrinterBasic 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
+     | None -> TopPrinterBasic Pp.mt
      | Some v -> generic_val_print v)
 
 let _ =
@@ -99,9 +105,9 @@ let _ =
 (* Printing generic arguments *)
 
 type ('raw, 'glb, 'top) genprinter = {
-  raw : 'raw printer;
-  glb : 'glb printer;
-  top : 'top -> printer_result;
+  raw : 'raw -> printer_result;
+  glb : 'glb -> printer_result;
+  top : 'top -> top_printer_result;
 }
 
 module PrintObj =
@@ -112,9 +118,9 @@ struct
   | ExtraArg tag ->
     let name = ArgT.repr tag in
     let printer = {
-      raw = (fun _ -> str "<genarg:" ++ str name ++ str ">");
-      glb = (fun _ -> str "<genarg:" ++ str name ++ str ">");
-      top = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
+      raw = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
+      glb = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
+      top = (fun _ -> TopPrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
     } in
     Some printer
   | _ -> assert false
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 2da9bbc36..baa60fcb2 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -10,19 +10,25 @@
 
 open Genarg
 
-type printer_with_level =
+type 'a 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 }
+    printer : 'a }
 
 type printer_result =
 | PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
-| PrinterNeedsContextAndLevel of printer_with_level
+| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
 
-type 'a printer = 'a -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
 
-type 'a top_printer = 'a -> printer_result
+type top_printer_result =
+| TopPrinterBasic of (unit -> Pp.t)
+| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
+
+type 'a printer = 'a -> printer_result
+
+type 'a top_printer = 'a -> top_printer_result
 
 val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw printer
 (** Printer for raw level generic arguments. *)
@@ -34,7 +40,7 @@ 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
+  'raw printer -> 'glb printer -> 'top top_printer -> unit
 val register_val_print0 : 'top Geninterp.Val.typ ->
   'top top_printer -> unit
 val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type ->
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 12d5338ad..a544b4762 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -130,7 +130,10 @@ let rec pr_raw_generic env (GenArg (Rawwit wit, x)) =
       let q = in_gen (rawwit wit2) q in
       hov_if_not_empty 0 (pr_sequence (pr_raw_generic env) [p; q])
     | ExtraArg s ->
-      Genprint.generic_raw_print (in_gen (rawwit wit) x)
+       let open Genprint in
+       match generic_raw_print (in_gen (rawwit wit) x) with
+       | PrinterBasic pp -> pp ()
+       | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded
 
 
 let rec pr_glb_generic env (GenArg (Glbwit wit, x)) =
@@ -152,4 +155,7 @@ let rec pr_glb_generic env (GenArg (Glbwit wit, x)) =
       let ans = pr_sequence (pr_glb_generic env) [p; q] in
       hov_if_not_empty 0 ans
     | ExtraArg s ->
-      Genprint.generic_glb_print (in_gen (glbwit wit) x)
+       let open Genprint in
+       match generic_glb_print (in_gen (glbwit wit) x) with
+       | PrinterBasic pp -> pp ()
+       | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded