Merge PR #8451: Print Universes Subgraph

10 files changed, 80 insertions, 26 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 253f14e9b0..ca63d60a52 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -95,6 +95,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 3ddfc9aec1..391afcb1f7 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/kernel/uGraph.ml b/kernel/uGraph.ml
index 9ff51fca55..9083156745 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -942,34 +942,36 @@ let check_eq_instances g t1 t2 =
 
 (** Pretty-printing *)
 
+let pr_umap sep pr map =
+  let cmp (u,_) (v,_) = Level.compare u v in
+  Pp.prlist_with_sep sep pr (List.sort cmp (UMap.bindings map))
+
 let pr_arc prl = function
   | _, Canonical {univ=u; ltle; _} ->
     if UMap.is_empty ltle then mt ()
     else
       prl u ++ str " " ++
       v 0
-        (pr_sequence (fun (v, strict) ->
+        (pr_umap Pp.spc (fun (v, strict) ->
           (if strict then str "< " else str "<= ") ++ prl v)
-           (UMap.bindings ltle)) ++
+           ltle) ++
       fnl ()
   | u, Equiv v ->
       prl u  ++ str " = " ++ prl v ++ fnl ()
 
 let pr_universes prl g =
-  let graph = UMap.fold (fun u a l -> (u,a)::l) g.entries [] in
-  prlist (pr_arc prl) graph
+  pr_umap mt (pr_arc prl) g.entries
 
 (* Dumping constraints to a file *)
 
 let dump_universes output g =
   let dump_arc u = function
     | Canonical {univ=u; ltle; _} ->
-        let u_str = Level.to_string u in
         UMap.iter (fun v strict ->
           let typ = if strict then Lt else Le in
-          output typ u_str (Level.to_string v)) ltle;
+          output typ u v) ltle;
     | Equiv v ->
-      output Eq (Level.to_string u) (Level.to_string v)
+      output Eq u v
   in
   UMap.iter dump_arc g.entries
 
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 4336a22b8c..a2cc5b3116 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -86,7 +86,7 @@ val check_subtype : AUContext.t check_function
 (** {6 Dumping to a file } *)
 
 val dump_universes :
-  (constraint_type -> string -> string -> unit) -> t -> unit
+  (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit
 
 (** {6 Debugging} *)
 val check_universes_invariants : t -> unit
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..7a76fb9560 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -319,7 +319,7 @@ let print_registered () =
   hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ())
 
 
-let dump_universes_gen g s =
+let dump_universes_gen prl g s =
   let output = open_out s in
   let output_constraint, close =
     if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin
@@ -344,10 +344,12 @@ let dump_universes_gen g s =
           | Univ.Lt -> "<"
           | Univ.Le -> "<="
           | Univ.Eq -> "="
-        in Printf.fprintf output "%s %s %s ;\n" left kind right
+        in
+        Printf.fprintf output "%s %s %s ;\n" left kind right
       end, (fun () -> close_out output)
     end
   in
+  let output_constraint k l r = output_constraint k (prl l) (prl r) in
   try
     UGraph.dump_universes output_constraint g;
     close ();
@@ -357,6 +359,36 @@ 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
+  let prl = UnivNames.pr_with_global_universes in
+  begin match dst with
+    | None -> UGraph.pr_universes prl univ ++ pr_remaining
+    | Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s
+  end
+
 (*********************)
 (* "Locate" commands *)
 
@@ -1826,17 +1858,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