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.

1 files changed, 33 insertions, 2 deletions

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