From ed04b8eb07ca3925af852c30a75c553c134f7d72 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 29 Oct 2018 17:56:10 +0100
Subject: Local universes for opaque polymorphic constants.

---
 printing/prettyp.ml  |  7 ++++---
 printing/printer.ml  | 15 ++++++++++-----
 printing/printer.mli |  6 +++---
 printing/printmod.ml |  2 +-
 4 files changed, 18 insertions(+), 12 deletions(-)

(limited to 'printing')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 712eb21ee6..f9f4d7f7f8 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -96,8 +96,9 @@ let print_ref reduce ref udecl =
     then Printer.pr_universe_instance sigma inst
     else mt ()
   in
+  let priv = None in (* We deliberately don't print private univs in About. *)
   hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ 
-           Printer.pr_abstract_universe_ctx sigma ?variance univs)
+           Printer.pr_abstract_universe_ctx sigma ?variance univs ~priv)
 
 (********************************)
 (** Printing implicit arguments *)
@@ -580,11 +581,11 @@ let print_constant with_values sep sp udecl =
 	str"*** [ " ++
 	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-        Printer.pr_constant_universes sigma univs
+        Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs
     | Some (c, ctx) ->
 	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
 	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
-        Printer.pr_constant_universes sigma univs)
+        Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs)
 
 let gallina_print_constant_with_infos sp udecl =
   print_constant true " = " sp udecl ++
diff --git a/printing/printer.ml b/printing/printer.ml
index 4840577cbf..ebe8e3eebb 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -211,16 +211,21 @@ let pr_universe_ctx sigma ?variance c =
   else
     mt()
 
-let pr_abstract_universe_ctx sigma ?variance c =
-  if !Detyping.print_universes && not (Univ.AUContext.is_empty c) then
+let pr_abstract_universe_ctx sigma ?variance c ~priv =
+  let open Univ in
+  let priv = Option.default Univ.ContextSet.empty priv in
+  if !Detyping.print_universes && not (Univ.AUContext.is_empty c && Univ.ContextSet.is_empty priv) then
+    let local = if ContextSet.is_empty priv then mt() else
+        str "local: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) priv
+    in
     fnl()++pr_in_comment (fun c -> v 0
-      (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
+      (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c) ++ v 0 local) c
   else
     mt()
 
-let pr_constant_universes sigma = function
+let pr_constant_universes sigma ~priv = function
   | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx
-  | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx
+  | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx ~priv
 
 let pr_cumulativity_info sigma cumi =
   if !Detyping.print_universes 
diff --git a/printing/printer.mli b/printing/printer.mli
index cefc005c74..b0232ec4ac 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -87,10 +87,10 @@ val pr_universe_instance   : evar_map -> Univ.Instance.t -> Pp.t
 val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t
 val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
   Univ.UContext.t -> Pp.t
-val pr_abstract_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
-  Univ.AUContext.t -> Pp.t
+val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array ->
+  Univ.AUContext.t -> priv:Univ.ContextSet.t option -> Pp.t
 val pr_universe_ctx_set    : evar_map -> Univ.ContextSet.t -> Pp.t
-val pr_constant_universes  : evar_map -> Declarations.constant_universes -> Pp.t
+val pr_constant_universes  : evar_map -> priv:Univ.ContextSet.t option -> Declarations.constant_universes -> Pp.t
 val pr_cumulativity_info   : evar_map -> Univ.CumulativityInfo.t -> Pp.t
 val pr_abstract_cumulativity_info   : evar_map -> Univ.ACumulativityInfo.t -> Pp.t
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 2c3ab46670..1360ad4af4 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -310,7 +310,7 @@ let print_body is_impl extent env mp (l,body) =
 		hov 2 (str ":= " ++
                        Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l))
 	      | _ -> mt ()) ++ str "." ++
-            Printer.pr_abstract_universe_ctx sigma ctx)
+            Printer.pr_abstract_universe_ctx sigma ctx ~priv:cb.const_private_poly_univs)
     | SFBmind mib ->
       match extent with
       | WithContents ->
-- 
cgit v1.2.3


From 828d9447073b06a85421857d7f8b872af6cdfe6b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 9 Nov 2018 16:23:57 +0100
Subject: Fix printing of private universes.

Set Printing Universes.
Set Universe Polymorphism.
Lemma foo : Type.
Proof. exact (forall _ : Type, Type).
Qed.

Print foo.

Before:
(*
foo@{Top.1} =
Type@{Top.2} -> Type@{Top.3}
     : Type@{Top.1}
(* Top.1 |= Prop < Set
            Set < Top.1
            local: {Top.3 Top.2} |= Top.2 < Top.1
                                    Top.3 < Top.1
                                     *)

foo is universe polymorphic
*)

Now:
(* Public universes:
Top.1 |= Set < Top.1
Private universes:
{Top.3 Top.2} |= Top.2 < Top.1
                 Top.3 < Top.1 *)
---
 printing/printer.ml | 26 +++++++++++---------------
 1 file changed, 11 insertions(+), 15 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index ebe8e3eebb..94b514239a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -143,7 +143,7 @@ let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
 let _ = Termops.Internal.set_print_constr
   (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t))
 
-let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
+let pr_in_comment x = str "(* " ++ x ++ str " *)"
 
 (** Term printers resilient to [Nametab] errors *)
 
@@ -199,27 +199,25 @@ let safe_pr_constr_env = safe_gen pr_constr_env
 
 let pr_universe_ctx_set sigma c =
   if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
-    fnl()++pr_in_comment (fun c -> v 0
-      (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c
+    fnl()++pr_in_comment (v 0 (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c))
   else
     mt()
 
 let pr_universe_ctx sigma ?variance c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
-    fnl()++pr_in_comment (fun c -> v 0 
-      (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
+    fnl()++pr_in_comment (v 0 (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c))
   else
     mt()
 
 let pr_abstract_universe_ctx sigma ?variance c ~priv =
   let open Univ in
   let priv = Option.default Univ.ContextSet.empty priv in
-  if !Detyping.print_universes && not (Univ.AUContext.is_empty c && Univ.ContextSet.is_empty priv) then
-    let local = if ContextSet.is_empty priv then mt() else
-        str "local: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) priv
-    in
-    fnl()++pr_in_comment (fun c -> v 0
-      (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c) ++ v 0 local) c
+  let has_priv = not (ContextSet.is_empty priv) in
+  if !Detyping.print_universes && (not (Univ.AUContext.is_empty c) || has_priv) then
+    let prlev u = Termops.pr_evd_level sigma u in
+    let pub = (if has_priv then str "Public universes:" ++ fnl() else mt()) ++ v 0 (Univ.pr_abstract_universe_context prlev ?variance c) in
+    let priv = if has_priv then fnl() ++ str "Private universes:" ++ fnl() ++ v 0 (Univ.pr_universe_context_set prlev priv) else mt() in
+    fnl()++pr_in_comment (pub ++ priv)
   else
     mt()
 
@@ -230,16 +228,14 @@ let pr_constant_universes sigma ~priv = function
 let pr_cumulativity_info sigma cumi =
   if !Detyping.print_universes 
   && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
-    fnl()++pr_in_comment (fun uii -> v 0 
-      (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
+    fnl()++pr_in_comment (v 0 (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) cumi))
   else
     mt()
 
 let pr_abstract_cumulativity_info sigma cumi =
   if !Detyping.print_universes
   && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then
-    fnl()++pr_in_comment (fun uii -> v 0
-      (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
+    fnl()++pr_in_comment (v 0 (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) cumi))
   else
     mt()
 
-- 
cgit v1.2.3