Further pushing up the printing and sorting of universes.

We expose the representation function in UGraph and change the printer
signature to work over the representation instead of the abstract type.
Similarly, the topological sorting algorithm is moved to Vernacentries.
It is now even simpler.

2 files changed, 16 insertions, 26 deletions

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 5d7cc92181..b988ec40a7 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -222,19 +222,6 @@ let choose p g u = if Level.is_sprop u
   then if p u then Some u else None
   else G.choose p g.graph u
 
-(* Dumping constraints to a file *)
-
-let dump_universes output g =
-  let dump_arc u = function
-    | G.Node ltle ->
-      LMap.iter (fun v strict ->
-          let typ = if strict then Lt else Le in
-          output typ u v) ltle;
-    | G.Alias v ->
-      output Eq u v
-  in
-  LMap.iter dump_arc (G.repr g.graph)
-
 let check_universes_invariants g = G.check_invariants ~required_canonical:Level.is_small g.graph
 
 (** Pretty-printing *)
@@ -257,11 +244,13 @@ let pr_arc prl = let open Pp in
   | u, G.Alias v ->
     prl u  ++ str " = " ++ prl v ++ fnl ()
 
-let pr_universes prl g = pr_pmap Pp.mt (pr_arc prl) (G.repr g.graph)
+type node = G.node =
+| Alias of Level.t
+| Node of bool LMap.t
+
+let repr g = G.repr g.graph
 
-let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"]
-let make_dummy i = Level.(make (UGlobal.make dummy_mp i))
-let sort_universes g = g_map (G.sort make_dummy [Level.prop;Level.set]) g
+let pr_universes prl g = pr_pmap Pp.mt (pr_arc prl) g
 
 (** Profiling *)
 
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 87b3634e28..9ac29f5139 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -77,15 +77,9 @@ exception UndeclaredLevel of Univ.Level.t
 
 val check_declared_universes : t -> Univ.LSet.t -> unit
 
-(** {6 Pretty-printing of universes. } *)
-
-val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t
-
 (** The empty graph of universes *)
 val empty_universes : t
 
-val sort_universes : t -> t
-
 (** [constraints_of_universes g] returns [csts] and [partition] where
    [csts] are the non-Eq constraints and [partition] is the partition
    of the universes into equivalence classes. *)
@@ -108,10 +102,17 @@ val check_subtype : lbound:Bound.t -> AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)
 
-(** {6 Dumping to a file } *)
+(** {6 Dumping} *)
+
+type node =
+| Alias of Level.t
+| Node of bool LMap.t (** Nodes v s.t. u < v (true) or u <= v (false) *)
+
+val repr : t -> node LMap.t
+
+(** {6 Pretty-printing of universes. } *)
 
-val dump_universes :
-  (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit
+val pr_universes : (Level.t -> Pp.t) -> node LMap.t -> Pp.t
 
 (** {6 Debugging} *)
 val check_universes_invariants : t -> unit