Make ugraph implementation abstract wrt universe specifics

This should give better visibility of universe specific operations vs
generic graph operations.

3 files changed, 937 insertions, 0 deletions

diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml
new file mode 100644
index 0000000000..9afee6f0fd
--- /dev/null
+++ b/lib/acyclicGraph.ml
@@ -0,0 +1,863 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type constraint_type = Lt | Le | Eq
+
+module type Point = sig
+  type t
+
+  module Set : CSig.SetS with type elt = t
+  module Map : CMap.ExtS with type key = t and module Set := Set
+
+  module Constraint : CSet.S with type elt = (t * constraint_type * t)
+
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+
+  type explanation = (constraint_type * t) list
+  val error_inconsistency : constraint_type -> t -> t -> explanation lazy_t option -> 'a
+
+  val pr : t -> Pp.t
+end
+
+module Make (Level:Point) = struct
+
+  (* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *)
+  (* Functional code by Jean-Christophe Filliâtre for Coq V7.0 [1999] *)
+  (* Extension with algebraic universes by HH for Coq V7.0 [Sep 2001] *)
+  (* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *)
+  (* Support for universe polymorphism by MS [2014] *)
+
+  (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu
+     Sozeau, Pierre-Marie Pédrot, Jacques-Henri Jourdan *)
+
+  (* Points are stratified by a partial ordering $\le$.
+     Let $\~{}$ be the associated equivalence. We also have a strict ordering
+     $<$ between equivalence classes, and we maintain that $<$ is acyclic,
+     and contained in $\le$ in the sense that $[U]<[V]$ implies $U\le V$.
+
+     At every moment, we have a finite number of universes, and we
+     maintain the ordering in the presence of assertions $U<V$ and $U\le V$.
+
+     The equivalence $\~{}$ is represented by a tree structure, as in the
+     union-find algorithm. The assertions $<$ and $\le$ are represented by
+     adjacency lists.
+
+     We use the algorithm described in the paper:
+
+     Bender, M. A., Fineman, J. T., Gilbert, S., & Tarjan, R. E. (2011). A
+     new approach to incremental cycle detection and related
+     problems. arXiv preprint arXiv:1112.0784.
+
+  *)
+
+  module LMap = Level.Map
+  module LSet = Level.Set
+  module Constraint = Level.Constraint
+
+  type status = NoMark | Visited | WeakVisited | ToMerge
+
+  (* Comparison on this type is pointer equality *)
+  type canonical_node =
+    { univ: Level.t;
+      ltle: bool LMap.t;  (* true: strict (lt) constraint.
+                             false: weak  (le) constraint. *)
+      gtge: LSet.t;
+      rank : int;
+      klvl: int;
+      ilvl: int;
+      mutable status: status
+    }
+
+  let big_rank = 1000000
+
+  (* A Level.t is either an alias for another one, or a canonical one,
+     for which we know the universes that are above *)
+
+  type univ_entry =
+      Canonical of canonical_node
+    | Equiv of Level.t
+
+  type t =
+    { entries : univ_entry LMap.t;
+      index : int;
+      n_nodes : int; n_edges : int }
+
+  (** Used to cleanup universes if a traversal function is interrupted before it
+      has the opportunity to do it itself. *)
+  let unsafe_cleanup_universes g =
+    let iter _ n = match n with
+      | Equiv _ -> ()
+      | Canonical n -> n.status <- NoMark
+    in
+    LMap.iter iter g.entries
+
+  let rec cleanup_universes g =
+    try unsafe_cleanup_universes g
+    with e ->
+      (* The only way unsafe_cleanup_universes may raise an exception is when
+         a serious error (stack overflow, out of memory) occurs, or a signal is
+         sent. In this unlikely event, we relaunch the cleanup until we finally
+         succeed. *)
+      cleanup_universes g; raise e
+
+  (* Every Level.t has a unique canonical arc representative *)
+
+  (* Low-level function : makes u an alias for v.
+     Does not removes edges from n_edges, but decrements n_nodes.
+     u should be entered as canonical before.  *)
+  let enter_equiv g u v =
+    { entries =
+        LMap.modify u (fun _ a ->
+            match a with
+            | Canonical n ->
+              n.status <- NoMark;
+              Equiv v
+            | _ -> assert false) g.entries;
+      index = g.index;
+      n_nodes = g.n_nodes - 1;
+      n_edges = g.n_edges }
+
+  (* Low-level function : changes data associated with a canonical node.
+     Resets the mutable fields in the old record, in order to avoid breaking
+     invariants for other users of this record.
+     n.univ should already been inserted as a canonical node. *)
+  let change_node g n =
+    { g with entries =
+               LMap.modify n.univ
+                 (fun _ a ->
+                    match a with
+                    | Canonical n' ->
+                      n'.status <- NoMark;
+                      Canonical n
+                    | _ -> assert false)
+                 g.entries }
+
+  (* repr : universes -> Level.t -> canonical_node *)
+  (* canonical representative : we follow the Equiv links *)
+  let rec repr g u =
+    let a =
+      try LMap.find u g.entries
+      with Not_found -> CErrors.anomaly ~label:"Univ.repr"
+                          Pp.(str"Universe " ++ Level.pr u ++ str" undefined.")
+    in
+    match a with
+    | Equiv v -> repr g v
+    | Canonical arc -> arc
+
+  exception AlreadyDeclared
+
+  (* Reindexes the given universe, using the next available index. *)
+  let use_index g u =
+    let u = repr g u in
+    let g = change_node g { u with ilvl = g.index } in
+    assert (g.index > min_int);
+    { g with index = g.index - 1 }
+
+  (* [safe_repr] is like [repr] but if the graph doesn't contain the
+     searched universe, we add it. *)
+  let safe_repr g u =
+    let rec safe_repr_rec entries u =
+      match LMap.find u entries with
+      | Equiv v -> safe_repr_rec entries v
+      | Canonical arc -> arc
+    in
+    try g, safe_repr_rec g.entries u
+    with Not_found ->
+      let can =
+        { univ = u;
+          ltle = LMap.empty; gtge = LSet.empty;
+          rank = 0;
+          klvl = 0; ilvl = 0;
+          status = NoMark }
+      in
+      let g = { g with
+                entries = LMap.add u (Canonical can) g.entries;
+                n_nodes = g.n_nodes + 1 }
+      in
+      let g = use_index g u in
+      g, repr g u
+
+  (* Returns 1 if u is higher than v in topological order.
+             -1        lower
+             0 if u = v *)
+  let topo_compare u v =
+    if u.klvl > v.klvl then 1
+    else if u.klvl < v.klvl then -1
+    else if u.ilvl > v.ilvl then 1
+    else if u.ilvl < v.ilvl then -1
+    else (assert (u==v); 0)
+
+  (* Checks most of the invariants of the graph. For debugging purposes. *)
+  let check_invariants ~required_canonical g =
+    let n_edges = ref 0 in
+    let n_nodes = ref 0 in
+    LMap.iter (fun l u ->
+        match u with
+        | Canonical u ->
+          LMap.iter (fun v _strict ->
+              incr n_edges;
+              let v = repr g v in
+              assert (topo_compare u v = -1);
+              if u.klvl = v.klvl then
+                assert (LSet.mem u.univ v.gtge ||
+                        LSet.exists (fun l -> u == repr g l) v.gtge))
+            u.ltle;
+          LSet.iter (fun v ->
+              let v = repr g v in
+              assert (v.klvl = u.klvl &&
+                      (LMap.mem u.univ v.ltle ||
+                       LMap.exists (fun l _ -> u == repr g l) v.ltle))
+            ) u.gtge;
+          assert (u.status = NoMark);
+          assert (Level.equal l u.univ);
+          assert (u.ilvl > g.index);
+          assert (not (LMap.mem u.univ u.ltle));
+          incr n_nodes
+        | Equiv _ -> assert (not (required_canonical l)))
+      g.entries;
+    assert (!n_edges = g.n_edges);
+    assert (!n_nodes = g.n_nodes)
+
+  let clean_ltle g ltle =
+    LMap.fold (fun u strict acc ->
+        let uu = (repr g u).univ in
+        if Level.equal uu u then acc
+        else (
+          let acc = LMap.remove u (fst acc) in
+          if not strict && LMap.mem uu acc then (acc, true)
+          else (LMap.add uu strict acc, true)))
+      ltle (ltle, false)
+
+  let clean_gtge g gtge =
+    LSet.fold (fun u acc ->
+        let uu = (repr g u).univ in
+        if Level.equal uu u then acc
+        else LSet.add uu (LSet.remove u (fst acc)), true)
+      gtge (gtge, false)
+
+  (* [get_ltle] and [get_gtge] return ltle and gtge arcs.
+     Moreover, if one of these lists is dirty (e.g. points to a
+     non-canonical node), these functions clean this node in the
+     graph by removing some duplicate edges *)
+  let get_ltle g u =
+    let ltle, chgt_ltle = clean_ltle g u.ltle in
+    if not chgt_ltle then u.ltle, u, g
+    else
+      let sz = LMap.cardinal u.ltle in
+      let sz2 = LMap.cardinal ltle in
+      let u = { u with ltle } in
+      let g = change_node g u in
+      let g = { g with n_edges = g.n_edges + sz2 - sz } in
+      u.ltle, u, g
+
+  let get_gtge g u =
+    let gtge, chgt_gtge = clean_gtge g u.gtge in
+    if not chgt_gtge then u.gtge, u, g
+    else
+      let u = { u with gtge } in
+      let g = change_node g u in
+      u.gtge, u, g
+
+  (* [revert_graph] rollbacks the changes made to mutable fields in
+     nodes in the graph.
+     [to_revert] contains the touched nodes. *)
+  let revert_graph to_revert g =
+    List.iter (fun t ->
+        match LMap.find t g.entries with
+        | Equiv _ -> ()
+        | Canonical t ->
+          t.status <- NoMark) to_revert
+
+  exception AbortBackward of t
+  exception CycleDetected
+
+  (* Implementation of the algorithm described in § 5.1 of the following paper:
+
+     Bender, M. A., Fineman, J. T., Gilbert, S., & Tarjan, R. E. (2011). A
+     new approach to incremental cycle detection and related
+     problems. arXiv preprint arXiv:1112.0784.
+
+     The "STEP X" comments contained in this file refers to the
+     corresponding step numbers of the algorithm described in Section
+     5.1 of this paper.  *)
+
+  (* [delta] is the timeout for backward search. It might be
+      useful to tune a multiplicative constant. *)
+  let get_delta g =
+    int_of_float
+      (min (float_of_int g.n_edges ** 0.5)
+         (float_of_int g.n_nodes ** (2./.3.)))
+
+  let rec backward_traverse to_revert b_traversed count g x =
+    let x = repr g x in
+    let count = count - 1 in
+    if count < 0 then begin
+      revert_graph to_revert g;
+      raise (AbortBackward g)
+    end;
+    if x.status = NoMark then begin
+      x.status <- Visited;
+      let to_revert = x.univ::to_revert in
+      let gtge, x, g = get_gtge g x in
+      let to_revert, b_traversed, count, g =
+        LSet.fold (fun y (to_revert, b_traversed, count, g) ->
+            backward_traverse to_revert b_traversed count g y)
+          gtge (to_revert, b_traversed, count, g)
+      in
+      to_revert, x.univ::b_traversed, count, g
+    end
+    else to_revert, b_traversed, count, g
+
+  let rec forward_traverse f_traversed g v_klvl x y =
+    let y = repr g y in
+    if y.klvl < v_klvl then begin
+      let y = { y with klvl = v_klvl;
+                       gtge = if x == y then LSet.empty
+                         else LSet.singleton x.univ }
+      in
+      let g = change_node g y in
+      let ltle, y, g = get_ltle g y in
+      let f_traversed, g =
+        LMap.fold (fun z _ (f_traversed, g) ->
+            forward_traverse f_traversed g v_klvl y z)
+          ltle (f_traversed, g)
+      in
+      y.univ::f_traversed, g
+    end else if y.klvl = v_klvl && x != y then
+      let g = change_node g
+          { y with gtge = LSet.add x.univ y.gtge } in
+      f_traversed, g
+    else f_traversed, g
+
+  let rec find_to_merge to_revert g x v =
+    let x = repr g x in
+    match x.status with
+    | Visited -> false, to_revert   | ToMerge -> true, to_revert
+    | NoMark ->
+      let to_revert = x::to_revert in
+      if Level.equal x.univ v then
+        begin x.status <- ToMerge; true, to_revert end
+      else
+        begin
+          let merge, to_revert = LSet.fold
+              (fun y (merge, to_revert) ->
+                 let merge', to_revert = find_to_merge to_revert g y v in
+                 merge' || merge, to_revert) x.gtge (false, to_revert)
+          in
+          x.status <- if merge then ToMerge else Visited;
+          merge, to_revert
+        end
+    | _ -> assert false
+
+  let get_new_edges g to_merge =
+    (* Computing edge sets. *)
+    let to_merge_lvl =
+      List.fold_left (fun acc u -> LMap.add u.univ u acc)
+        LMap.empty to_merge
+    in
+    let ltle =
+      let fold _ n acc =
+        let fold u strict acc =
+          if strict then LMap.add u strict acc
+          else if LMap.mem u acc then acc
+          else LMap.add u false acc
+        in
+        LMap.fold fold n.ltle acc
+      in
+      LMap.fold fold to_merge_lvl LMap.empty
+    in
+    let ltle, _ = clean_ltle g ltle in
+    let ltle =
+      LMap.merge (fun _ a strict ->
+          match a, strict with
+          | Some _, Some true ->
+            (* There is a lt edge inside the new component. This is a
+                "bad cycle". *)
+            raise CycleDetected
+          | Some _, Some false -> None
+          | _, _ -> strict
+        ) to_merge_lvl ltle
+    in
+    let gtge =
+      LMap.fold (fun _ n acc -> LSet.union acc n.gtge)
+        to_merge_lvl LSet.empty
+    in
+    let gtge, _ = clean_gtge g gtge in
+    let gtge = LSet.diff gtge (LMap.domain to_merge_lvl) in
+    (ltle, gtge)
+
+
+  let reorder g u v =
+    (* STEP 2: backward search in the k-level of u. *)
+    let delta = get_delta g in
+
+    (* [v_klvl] is the chosen future level for u, v and all
+        traversed nodes. *)
+    let b_traversed, v_klvl, g =
+      try
+        let to_revert, b_traversed, _, g = backward_traverse [] [] delta g u in
+        revert_graph to_revert g;
+        let v_klvl = (repr g u).klvl in
+        b_traversed, v_klvl, g
+      with AbortBackward g ->
+        (* Backward search was too long, use the next k-level. *)
+        let v_klvl = (repr g u).klvl + 1 in
+        [], v_klvl, g
+    in
+    let f_traversed, g =
+      (* STEP 3: forward search. Contrary to what is described in
+          the paper, we do not test whether v_klvl = u.klvl nor we assign
+          v_klvl to v.klvl. Indeed, the first call to forward_traverse
+          will do all that. *)
+      forward_traverse [] g v_klvl (repr g v) v
+    in
+
+    (* STEP 4: merge nodes if needed. *)
+    let to_merge, b_reindex, f_reindex =
+      if (repr g u).klvl = v_klvl then
+        begin
+          let merge, to_revert = find_to_merge [] g u v in
+          let r =
+            if merge then
+              List.filter (fun u -> u.status = ToMerge) to_revert,
+              List.filter (fun u -> (repr g u).status <> ToMerge) b_traversed,
+              List.filter (fun u -> (repr g u).status <> ToMerge) f_traversed
+            else [], b_traversed, f_traversed
+          in
+          List.iter (fun u -> u.status <- NoMark) to_revert;
+          r
+        end
+      else [], b_traversed, f_traversed
+    in
+    let to_reindex, g =
+      match to_merge with
+      | [] -> List.rev_append f_reindex b_reindex, g
+      | n0::q0 ->
+        (* Computing new root. *)
+        let root, rank_rest =
+          List.fold_left (fun ((best, _rank_rest) as acc) n ->
+              if n.rank >= best.rank then n, best.rank else acc)
+            (n0, min_int) q0
+        in
+        let ltle, gtge = get_new_edges g to_merge in
+        (* Inserting the new root. *)
+        let g = change_node g
+            { root with ltle; gtge;
+                        rank = max root.rank (rank_rest + 1); }
+        in
+
+        (* Inserting shortcuts for old nodes. *)
+        let g = List.fold_left (fun g n ->
+            if Level.equal n.univ root.univ then g else enter_equiv g n.univ root.univ)
+            g to_merge
+        in
+
+        (* Updating g.n_edges *)
+        let oldsz =
+          List.fold_left (fun sz u -> sz+LMap.cardinal u.ltle)
+            0 to_merge
+        in
+        let sz = LMap.cardinal ltle in
+        let g = { g with n_edges = g.n_edges + sz - oldsz } in
+
+        (* Not clear in the paper: we have to put the newly
+            created component just between B and F. *)
+        List.rev_append f_reindex (root.univ::b_reindex), g
+
+    in
+
+    (* STEP 5: reindex traversed nodes. *)
+    List.fold_left use_index g to_reindex
+
+  (* Assumes [u] and [v] are already in the graph. *)
+  (* Does NOT assume that ucan != vcan. *)
+  let insert_edge strict ucan vcan g =
+    try
+      let u = ucan.univ and v = vcan.univ in
+      (* STEP 1: do we need to reorder nodes ? *)
+      let g = if topo_compare ucan vcan <= 0 then g else reorder g u v in
+
+      (* STEP 6: insert the new edge in the graph. *)
+      let u = repr g u in
+      let v = repr g v in
+      if u == v then
+        if strict then raise CycleDetected else g
+      else
+        let g =
+          try let oldstrict = LMap.find v.univ u.ltle in
+            if strict && not oldstrict then
+              change_node g { u with ltle = LMap.add v.univ true u.ltle }
+            else g
+          with Not_found ->
+            { (change_node g { u with ltle = LMap.add v.univ strict u.ltle })
+              with n_edges = g.n_edges + 1 }
+        in
+        if u.klvl <> v.klvl || LSet.mem u.univ v.gtge then g
+        else
+          let v = { v with gtge = LSet.add u.univ v.gtge } in
+          change_node g v
+    with
+    | CycleDetected as e -> raise e
+    | e ->
+      (* Unlikely event: fatal error or signal *)
+      let () = cleanup_universes g in
+      raise e
+
+  let add ?(rank=0) vlev g =
+    try
+      let _arcv = LMap.find vlev g.entries in
+      raise AlreadyDeclared
+    with Not_found ->
+      assert (g.index > min_int);
+      let v = {
+        univ = vlev;
+        ltle = LMap.empty;
+        gtge = LSet.empty;
+        rank;
+        klvl = 0;
+        ilvl = g.index;
+        status = NoMark;
+      }
+      in
+      let entries = LMap.add vlev (Canonical v) g.entries in
+      { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }
+
+  exception Undeclared of Level.t
+  let check_declared g us =
+    let check l = if not (LMap.mem l g.entries) then raise (Undeclared l) in
+    LSet.iter check us
+
+  exception Found_explanation of (constraint_type * Level.t) list
+
+  let get_explanation strict u v g =
+    let v = repr g v in
+    let visited_strict = ref LMap.empty in
+    let rec traverse strict u =
+      if u == v then
+        if strict then None else Some []
+      else if topo_compare u v = 1 then None
+      else
+        let visited =
+          try not (LMap.find u.univ !visited_strict) || strict
+          with Not_found -> false
+        in
+        if visited then None
+        else begin
+          visited_strict := LMap.add u.univ strict !visited_strict;
+          try
+            LMap.iter (fun u' strictu' ->
+                match traverse (strict && not strictu') (repr g u') with
+                | None -> ()
+                | Some exp ->
+                  let typ = if strictu' then Lt else Le in
+                  raise (Found_explanation ((typ, u') :: exp)))
+              u.ltle;
+            None
+          with Found_explanation exp -> Some exp
+        end
+    in
+    let u = repr g u in
+    if u == v then [(Eq, v.univ)]
+    else match traverse strict u with Some exp -> exp | None -> assert false
+
+  let get_explanation strict u v g =
+    Some (lazy (get_explanation strict u v g))
+
+  (* To compare two nodes, we simply do a forward search.
+     We implement two improvements:
+     - we ignore nodes that are higher than the destination;
+     - we do a BFS rather than a DFS because we expect to have a short
+         path (typically, the shortest path has length 1)
+  *)
+  exception Found of canonical_node list
+  let search_path strict u v g =
+    let rec loop to_revert todo next_todo =
+      match todo, next_todo with
+      | [], [] -> to_revert (* No path found *)
+      | [], _ -> loop to_revert next_todo []
+      | (u, strict)::todo, _ ->
+        if u.status = Visited || (u.status = WeakVisited && strict)
+        then loop to_revert todo next_todo
+        else
+          let to_revert =
+            if u.status = NoMark then u::to_revert else to_revert
+          in
+          u.status <- if strict then WeakVisited else Visited;
+          if try LMap.find v.univ u.ltle || not strict
+            with Not_found -> false
+          then raise (Found to_revert)
+          else
+            begin
+              let next_todo =
+                LMap.fold (fun u strictu next_todo ->
+                    let strict = not strictu && strict in
+                    let u = repr g u in
+                    if u == v && not strict then raise (Found to_revert)
+                    else if topo_compare u v = 1 then next_todo
+                    else (u, strict)::next_todo)
+                  u.ltle next_todo
+              in
+              loop to_revert todo next_todo
+            end
+    in
+    if u == v then not strict
+    else
+      try
+        let res, to_revert =
+          try false, loop [] [u, strict] []
+          with Found to_revert -> true, to_revert
+        in
+        List.iter (fun u -> u.status <- NoMark) to_revert;
+        res
+      with e ->
+        (* Unlikely event: fatal error or signal *)
+        let () = cleanup_universes g in
+        raise e
+
+  (** Uncomment to debug the cycle detection algorithm. *)
+  (*let insert_edge strict ucan vcan g =
+    let check_invariants = check_invariants ~required_canonical:(fun _ -> false) in
+    check_invariants g;
+    let g = insert_edge strict ucan vcan g in
+    check_invariants g;
+    let ucan = repr g ucan.univ in
+    let vcan = repr g vcan.univ in
+    assert (search_path strict ucan vcan g);
+    g*)
+
+  (** First, checks on universe levels *)
+
+  type 'a check_function = t -> 'a -> 'a -> bool
+
+  let check_eq g u v =
+    u == v ||
+    let arcu = repr g u and arcv = repr g v in
+    arcu == arcv
+
+  let check_smaller g strict u v =
+    search_path strict (repr g u) (repr g v) g
+
+  let check_leq g u v = check_smaller g false u v
+  let check_lt g u v = check_smaller g true u v
+
+  (* enforce_eq g u v will force u=v if possible, will fail otherwise *)
+
+  let rec enforce_eq u v g =
+    let ucan = repr g u in
+    let vcan = repr g v in
+    if topo_compare ucan vcan = 1 then enforce_eq v u g
+    else
+      let g = insert_edge false ucan vcan g in  (* Cannot fail *)
+      try insert_edge false vcan ucan g
+      with CycleDetected ->
+        Level.error_inconsistency Eq v u (get_explanation true u v g)
+
+  (* enforce_leq g u v will force u<=v if possible, will fail otherwise *)
+  let enforce_leq u v g =
+    let ucan = repr g u in
+    let vcan = repr g v in
+    try insert_edge false ucan vcan g
+    with CycleDetected ->
+      Level.error_inconsistency Le u v (get_explanation true v u g)
+
+  (* enforce_lt u v will force u<v if possible, will fail otherwise *)
+  let enforce_lt u v g =
+    let ucan = repr g u in
+    let vcan = repr g v in
+    try insert_edge true ucan vcan g
+    with CycleDetected ->
+      Level.error_inconsistency Lt u v (get_explanation false v u g)
+
+  let empty =
+    { entries = LMap.empty; index = 0; n_nodes = 0; n_edges = 0 }
+
+  (* Normalization *)
+
+  (** [normalize_universes g] returns a graph where all edges point
+      directly to the canonical representent of their target. The output
+      graph should be equivalent to the input graph from a logical point
+      of view, but optimized. We maintain the invariant that the key of
+      a [Canonical] element is its own name, by keeping [Equiv] edges. *)
+  let normalize_universes g =
+    let g =
+      { g with
+        entries = LMap.map (fun entry ->
+            match entry with
+            | Equiv u -> Equiv ((repr g u).univ)
+            | Canonical ucan -> Canonical { ucan with rank = 1 })
+            g.entries }
+    in
+    LMap.fold (fun _ u g ->
+        match u with
+        | Equiv _u -> g
+        | Canonical u ->
+          let _, u, g = get_ltle g u in
+          let _, _, g = get_gtge g u in
+          g)
+      g.entries g
+
+  let constraints_of g =
+    let module UF = Unionfind.Make (LSet) (LMap) in
+    let uf = UF.create () in
+    let constraints_of u v acc =
+      match v with
+      | Canonical {univ=u; ltle; _} ->
+        LMap.fold (fun v strict acc->
+            let typ = if strict then Lt else Le in
+            Constraint.add (u,typ,v) acc) ltle acc
+      | Equiv v -> UF.union u v uf; acc
+    in
+    let csts = LMap.fold constraints_of g.entries Constraint.empty in
+    csts, UF.partition uf
+
+  (* domain g.entries = kept + removed *)
+  let constraints_for ~kept g =
+    (* rmap: partial map from canonical universes to kept universes *)
+    let rmap, csts = LSet.fold (fun u (rmap,csts) ->
+        let arcu = repr g u in
+        if LSet.mem arcu.univ kept then
+          LMap.add arcu.univ arcu.univ rmap, Constraint.add (u,Eq,arcu.univ) csts
+        else
+          match LMap.find arcu.univ rmap with
+          | v -> rmap, Constraint.add (u,Eq,v) csts
+          | exception Not_found -> LMap.add arcu.univ u rmap, csts)
+        kept (LMap.empty,Constraint.empty)
+    in
+    let rec add_from u csts todo = match todo with
+      | [] -> csts
+      | (v,strict)::todo ->
+        let v = repr g v in
+        (match LMap.find v.univ rmap with
+         | v ->
+           let d = if strict then Lt else Le in
+           let csts = Constraint.add (u,d,v) csts in
+           add_from u csts todo
+         | exception Not_found ->
+           (* v is not equal to any kept universe *)
+           let todo = LMap.fold (fun v' strict' todo ->
+               (v',strict || strict') :: todo)
+               v.ltle todo
+           in
+           add_from u csts todo)
+    in
+    LSet.fold (fun u csts ->
+        let arc = repr g u in
+        LMap.fold (fun v strict csts -> add_from u csts [v,strict])
+          arc.ltle csts)
+      kept csts
+
+  let domain g = LMap.domain g.entries
+
+  let choose p g u =
+    let exception Found of Level.t in
+    let ru = (repr g u).univ in
+    if p ru then Some ru
+    else
+      try LMap.iter (fun v -> function
+          | Canonical _ -> () (* we already tried [p ru] *)
+          | Equiv v' ->
+            let rv = (repr g v').univ in
+            if rv == ru && p v then raise (Found v)
+            (* NB: we could also try [p v'] but it will come up in the
+               rest of the iteration regardless. *)
+        ) g.entries; None
+      with Found v -> Some v
+
+  (** [sort_universes g] builds a totally ordered universe graph.  The
+      output graph should imply the input graph (and the implication
+      will be strict most of the time), but is not necessarily minimal.
+      Moreover, it adds levels [Type.n] to identify universes at level
+      n. An artificial constraint Set < Type.2 is added to ensure that
+      Type.n and small universes are not merged. Note: the result is
+      unspecified if the input graph already contains [Type.n] nodes
+      (calling a module Type is probably a bad idea anyway). *)
+  let sort make_dummy univs g =
+    let cans =
+      LMap.fold (fun _ u l ->
+          match u with
+          | Equiv _ -> l
+          | Canonical can -> can :: l
+        ) g.entries []
+    in
+    let cans = List.sort topo_compare cans in
+    let lowest_levels =
+      LMap.mapi (fun u _ -> if CList.mem_f Level.equal u univs then 0 else 2)
+        (LMap.filter
+           (fun _ u -> match u with Equiv _ -> false | Canonical _ -> true)
+           g.entries)
+    in
+    let lowest_levels =
+      List.fold_left (fun lowest_levels can ->
+          let lvl = LMap.find can.univ lowest_levels in
+          LMap.fold (fun u' strict lowest_levels ->
+              let cost = if strict then 1 else 0 in
+              let u' = (repr g u').univ in
+              LMap.modify u' (fun _ lvl0 -> max lvl0 (lvl+cost)) lowest_levels)
+            can.ltle lowest_levels)
+        lowest_levels cans
+    in
+    let max_lvl = LMap.fold (fun _ a b -> max a b) lowest_levels 0 in
+    let types = Array.init (max_lvl + 1) (fun i ->
+        match List.nth_opt univs i with
+        | Some u -> u
+        | None -> make_dummy (i-2))
+    in
+    let g = Array.fold_left (fun g u ->
+        let g, u = safe_repr g u in
+        change_node g { u with rank = big_rank }) g types
+    in
+    let g = if max_lvl > List.length univs && not (CList.is_empty univs) then
+        enforce_lt (CList.last univs) types.(List.length univs) g
+      else g
+    in
+    let g =
+      LMap.fold (fun u lvl g -> enforce_eq u (types.(lvl)) g)
+        lowest_levels g
+    in
+    normalize_universes g
+
+  (** 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 (LMap.bindings map))
+
+  let pr_arc prl = let open Pp in
+    function
+    | _, Canonical {univ=u; ltle; _} ->
+      if LMap.is_empty ltle then mt ()
+      else
+        prl u ++ str " " ++
+        v 0
+          (pr_umap 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_umap Pp.mt (pr_arc prl) g.entries
+
+  (* Dumping constraints to a file *)
+
+  let dump output g =
+    let dump_arc u = function
+      | Canonical {univ=u; ltle; _} ->
+        LMap.iter (fun v strict ->
+            let typ = if strict then Lt else Le in
+            output typ u v) ltle;
+      | Equiv v ->
+        output Eq u v
+    in
+    LMap.iter dump_arc g.entries
+
+end
diff --git a/lib/acyclicGraph.mli b/lib/acyclicGraph.mli
new file mode 100644
index 0000000000..8a2eb7098f
--- /dev/null
+++ b/lib/acyclicGraph.mli
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Graphs representing strict orders *)
+
+type constraint_type = Lt | Le | Eq
+
+module type Point = sig
+  type t
+
+  module Set : CSig.SetS with type elt = t
+  module Map : CMap.ExtS with type key = t and module Set := Set
+
+  module Constraint : CSet.S with type elt = (t * constraint_type * t)
+
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+
+  type explanation = (constraint_type * t) list
+  val error_inconsistency : constraint_type -> t -> t -> explanation lazy_t option -> 'a
+
+  val pr : t -> Pp.t
+end
+
+module Make (Level:Point) : sig
+
+  type t
+
+  val empty : t
+
+  val check_invariants : required_canonical:(Level.t -> bool) -> t -> unit
+
+  exception AlreadyDeclared
+  val add : ?rank:int -> Level.t -> t -> t
+  (** Use a large [rank] to keep the node canonical *)
+
+  exception Undeclared of Level.t
+  val check_declared : t -> Level.Set.t -> unit
+
+  type 'a check_function = t -> 'a -> 'a -> bool
+
+  val check_eq : Level.t check_function
+  val check_leq : Level.t check_function
+  val check_lt : Level.t check_function
+
+  val enforce_eq : Level.t -> Level.t -> t -> t
+  val enforce_leq : Level.t -> Level.t -> t -> t
+  val enforce_lt : Level.t -> Level.t -> t -> t
+
+  val constraints_of : t -> Level.Constraint.t * Level.Set.t list
+
+  val constraints_for : kept:Level.Set.t -> t -> Level.Constraint.t
+
+  val domain : t -> Level.Set.t
+
+  val choose : (Level.t -> bool) -> t -> Level.t -> Level.t option
+
+  val sort : (int -> Level.t) -> Level.t list -> t -> t
+  (** [sort make_dummy points g] sorts [g]. The [points] are the first
+     in the result graph. If the graph is bigger than the list, the
+     rest is named according to [make_dummy]. *)
+
+  val pr : (Level.t -> Pp.t) -> t -> Pp.t
+
+  val dump : (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit
+end
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 206b2504db..2db59712b9 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -11,6 +11,7 @@ Feedback
 CErrors
 CWarnings
 
+AcyclicGraph
 Rtree
 System
 Explore