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 +++++++++++++++++++++++++++++++++--
 lib/acyclicGraph.ml  | 40 +++++++---------------------------------
 lib/acyclicGraph.mli | 11 ++++++++---
 3 files changed, 48 insertions(+), 38 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))
diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml
index 8da09dc98a..856d059a6e 100644
--- a/lib/acyclicGraph.ml
+++ b/lib/acyclicGraph.ml
@@ -814,40 +814,14 @@ module Make (Point:Point) = struct
     in
     normalize g
 
-  (** Pretty-printing *)
+  type node = Alias of Point.t | Node of bool Point.Map.t
+  type repr = node Point.Map.t
 
-  let pr_pmap sep pr map =
-    let cmp (u,_) (v,_) = Point.compare u v in
-    Pp.prlist_with_sep sep pr (List.sort cmp (PMap.bindings map))
-
-  let pr_arc prl = let open Pp in
-    function
-    | _, Canonical {canon=u; ltle; _} ->
-      if PMap.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, Equiv v ->
-      prl u  ++ str " = " ++ prl v ++ fnl ()
-
-  let pr prl g =
-    pr_pmap Pp.mt (pr_arc prl) g.entries
-
-  (* Dumping constraints to a file *)
-
-  let dump output g =
-    let dump_arc u = function
-      | Canonical {canon=u; ltle; _} ->
-        PMap.iter (fun v strict ->
-            let typ = if strict then Lt else Le in
-            output typ u v) ltle;
-      | Equiv v ->
-        output Eq u v
+  let repr g =
+    let map n = match n with
+    | Canonical n -> Node n.ltle
+    | Equiv u -> Alias u
     in
-    PMap.iter dump_arc g.entries
+    Point.Map.map map g.entries
 
 end
diff --git a/lib/acyclicGraph.mli b/lib/acyclicGraph.mli
index e9f05ed74d..fece242ec2 100644
--- a/lib/acyclicGraph.mli
+++ b/lib/acyclicGraph.mli
@@ -65,6 +65,14 @@ module Make (Point:Point) : sig
 
   val choose : (Point.t -> bool) -> t -> Point.t -> Point.t option
 
+  (** {5 High-level representation} *)
+
+  type node =
+  | Alias of Point.t
+  | Node of bool Point.Map.t (** Nodes v s.t. u < v (true) or u <= v (false) *)
+  type repr = node Point.Map.t
+  val repr : t -> repr
+
   val sort : (int -> Point.t) -> Point.t list -> t -> t
   (** [sort mk first g] builds a totally ordered graph. The output
      graph should imply the input graph (and the implication will be
@@ -76,7 +84,4 @@ module Make (Point:Point) : sig
      Note: the result is unspecified if the input graph already
      contains [mk n] nodes. *)
 
-  val pr : (Point.t -> Pp.t) -> t -> Pp.t
-
-  val dump : (constraint_type -> Point.t -> Point.t -> unit) -> t -> unit
 end
-- 
cgit v1.2.3