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).

4 files changed, 40 insertions, 16 deletions

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