From bdd186a7d6fc6e413e1b575085402f3c88fa5c23 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Jan 2021 16:15:12 +0100
Subject: Move universe printing out of AcyclicGraph.

Instead we export a representation function that gives a high-level view
of the data structure in terms of constraints.
---
 kernel/uGraph.ml | 35 +++++++++++++++++++++++++++++++++--
 1 file changed, 33 insertions(+), 2 deletions(-)

(limited to 'kernel/uGraph.ml')

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 096e458ec4..5d7cc92181 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -222,11 +222,42 @@ 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
 
-let dump_universes f g = G.dump f g.graph
+(* 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
 
-let pr_universes prl g = G.pr prl g.graph
+(** Pretty-printing *)
+
+let pr_pmap sep pr map =
+  let cmp (u,_) (v,_) = Level.compare u v in
+  Pp.prlist_with_sep sep pr (List.sort cmp (LMap.bindings map))
+
+let pr_arc prl = let open Pp in
+  function
+  | u, G.Node ltle ->
+    if LMap.is_empty ltle then mt ()
+    else
+      prl u ++ str " " ++
+      v 0
+        (pr_pmap spc (fun (v, strict) ->
+              (if strict then str "< " else str "<= ") ++ prl v)
+            ltle) ++
+      fnl ()
+  | 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)
 
 let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"]
 let make_dummy i = Level.(make (UGlobal.make dummy_mp i))
-- 
cgit v1.2.3


From f821438c9759c4788d597688b25cb78f2a2c01c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Jan 2021 21:54:12 +0100
Subject: 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.
---
 kernel/uGraph.ml | 23 ++++++-----------------
 1 file changed, 6 insertions(+), 17 deletions(-)

(limited to 'kernel/uGraph.ml')

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 *)
 
-- 
cgit v1.2.3