Print Universes Subgraph

This adds an optional [Subgraph] part to the Print Universes command,
eg [Print Universes Subgraph(i j)] to print only constraints related
to i and j (and Prop/Set).

8 files changed, 65 insertions, 16 deletions

diff --git a/CHANGES.md b/CHANGES.md
index e280cc2fb5..7081593805 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -93,6 +93,11 @@ Standard Library
 
 - Added `ByteVector` type that can convert to and from [string].
 
+Universes
+
+- Added `Print Universes Subgraph` variant of `Print Universes`.
+  Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).`
+
 Changes from 8.8.2 to 8.9+beta1
 ===============================
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 9dae7fd102..53ee14f708 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2155,6 +2155,12 @@ If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
 language, and can be processed by Graphviz tools. The format is
 unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
 
+.. cmdv:: Print Universes Subgraph(@names)
+
+Prints the graph restricted to the requested names (adjusting
+constraints to preserve the implied transitive constraints between
+kept universes).
+
 .. _existential-variables:
 
 Existential variables
diff --git a/test-suite/output/PrintUnivsSubgraph.out b/test-suite/output/PrintUnivsSubgraph.out
new file mode 100644
index 0000000000..c42e15e4e8
--- /dev/null
+++ b/test-suite/output/PrintUnivsSubgraph.out
@@ -0,0 +1,5 @@
+Prop < Set
+Set < i
+    < j
+i < j
+
diff --git a/test-suite/output/PrintUnivsSubgraph.v b/test-suite/output/PrintUnivsSubgraph.v
new file mode 100644
index 0000000000..ec9cf44d4f
--- /dev/null
+++ b/test-suite/output/PrintUnivsSubgraph.v
@@ -0,0 +1,9 @@
+
+Universes i j k l.
+
+Definition foo : Type@{j} := Type@{i}.
+
+Definition baz : Type@{k} := Type@{l}.
+
+Print Universes Subgraph(i j).
+(* should print [i < j], not [l < k] (and not prelude universes) *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1d0a5ab0a3..960e74827a 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -989,8 +989,9 @@ GRAMMAR EXTEND Gram
       | IDENT "Scope"; s = IDENT -> { PrintScope s }
       | IDENT "Visibility"; s = OPT IDENT -> { PrintVisibility s }
       | IDENT "Implicit"; qid = smart_global -> { PrintImplicit qid }
-      | IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (false, fopt) }
-      | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (true, fopt) }
+      | b = [ IDENT "Sorted" -> { true } | -> { false } ]; IDENT "Universes";
+        g = OPT printunivs_subgraph; fopt = OPT ne_string ->
+        { PrintUniverses (b, g, fopt) }
       | IDENT "Assumptions"; qid = smart_global -> { PrintAssumptions (false, false, qid) }
       | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, false, qid) }
       | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (false, true, qid) }
@@ -1000,6 +1001,9 @@ GRAMMAR EXTEND Gram
       | IDENT "Registered" -> { PrintRegistered }
     ] ]
   ;
+  printunivs_subgraph:
+    [ [ IDENT "Subgraph"; "("; l = LIST0 reference; ")" -> { l } ] ]
+  ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> { FunClass }
       | IDENT "Sortclass" -> { SortClass }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 1c1faca599..f65fae60ee 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -492,12 +492,13 @@ open Pputils
       keyword "Print Hint *"
     | PrintHintDbName s ->
       keyword "Print HintDb" ++ spc () ++ str s
-    | PrintUniverses (b, fopt) ->
+    | PrintUniverses (b, g, fopt) ->
       let cmd =
         if b then "Print Sorted Universes"
         else "Print Universes"
       in
-      keyword cmd ++ pr_opt str fopt
+      let pr_subgraph = prlist_with_sep spc pr_qualid in
+      keyword cmd ++ pr_opt pr_subgraph g ++ pr_opt str fopt
     | PrintName (qid,udecl) ->
       keyword "Print" ++ spc()  ++ pr_smart_global qid ++ pr_univ_name_list udecl
     | PrintModuleType qid ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1fab35b650..bc554fb4bf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -357,6 +357,35 @@ let dump_universes_gen g s =
     close ();
     iraise reraise
 
+let universe_subgraph ?loc g univ =
+  let open Univ in
+  let sigma = Evd.from_env (Global.env()) in
+  let univs_of q =
+    let q =  Glob_term.(GType (UNamed q)) in
+    (* this function has a nice error message for not found univs *)
+    LSet.singleton (Pretyping.interp_known_glob_level ?loc sigma q)
+  in
+  let univs = List.fold_left (fun univs q -> LSet.union univs (univs_of q)) LSet.empty g in
+  let csts = UGraph.constraints_for ~kept:(LSet.add Level.prop (LSet.add Level.set univs)) univ in
+  let univ = LSet.fold UGraph.add_universe_unconstrained univs UGraph.initial_universes in
+  UGraph.merge_constraints csts univ
+
+let print_universes ?loc ~sort ~subgraph dst =
+  let univ = Global.universes () in
+  let univ = match subgraph with
+    | None -> univ
+    | Some g -> universe_subgraph ?loc g univ
+  in
+  let univ = if sort then UGraph.sort_universes univ else univ in
+  let pr_remaining =
+    if Global.is_joined_environment () then mt ()
+    else str"There may remain asynchronous universe constraints"
+  in
+  begin match dst with
+    | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining
+    | Some s -> dump_universes_gen univ s
+  end
+
 (*********************)
 (* "Locate" commands *)
 
@@ -1826,17 +1855,7 @@ let vernac_print ~atts env sigma =
   | PrintCoercionPaths (cls,clt) ->
     Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)
   | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma
-  | PrintUniverses (b, dst) ->
-     let univ = Global.universes () in
-     let univ = if b then UGraph.sort_universes univ else univ in
-     let pr_remaining =
-       if Global.is_joined_environment () then mt ()
-       else str"There may remain asynchronous universe constraints"
-     in
-     begin match dst with
-     | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining
-     | Some s -> dump_universes_gen univ s
-     end
+  | PrintUniverses (sort, subgraph, dst) -> print_universes ~sort ~subgraph dst
   | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r)
   | PrintHintGoal -> Hints.pr_applicable_hint ()
   | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 594e9eca48..180d763946 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -45,7 +45,7 @@ type printable =
   | PrintCoercions
   | PrintCoercionPaths of class_rawexpr * class_rawexpr
   | PrintCanonicalConversions
-  | PrintUniverses of bool * string option
+  | PrintUniverses of bool * qualid list option * string option
   | PrintHint of qualid or_by_notation
   | PrintHintGoal
   | PrintHintDbName of string