New algorithm for universe cycle detections.

1 files changed, 651 insertions, 613 deletions

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index ee4231b1f..9e8ffbc7f 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -18,67 +18,73 @@ open Univ
 (* Support for universe polymorphism by MS [2014] *)
 
 (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau, 
-   Pierre-Marie Pédrot *)
+   Pierre-Marie Pédrot, Jacques-Henri Jourdan *)
 
 let error_inconsistency o u v (p:explanation option) =
   raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
 
-type status = Unset | SetLe | SetLt
+(* Universes 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.
+
+  *)
+
+open Universe
+
+module UMap = LMap
+
+type status = NoMark | Visited | WeakVisited | ToMerge
 
 (* Comparison on this type is pointer equality *)
-type canonical_arc =
+type canonical_node =
     { univ: Level.t;
-      lt: Level.t list;
-      le: Level.t list;
+      ltle: bool UMap.t;  (* true: strict (lt) constraint.
+                             false: weak  (le) constraint. *)
+      gtge: LSet.t;
       rank : int;
-      mutable status : status;
-      (** Guaranteed to be unset out of the [compare_neq] functions. It is used
-          to do an imperative traversal of the graph, ensuring a O(1) check that
-          a node has already been visited. Quite performance critical indeed. *)
+      klvl: int;
+      ilvl: int;
+      mutable status: status
     }
 
-let arc_is_le arc = match arc.status with
-| Unset -> false
-| SetLe | SetLt -> true
-
-let arc_is_lt arc = match arc.status with
-| Unset | SetLe -> false
-| SetLt -> true
-
-let terminal u = {univ=u; lt=[]; le=[]; rank=0; status = Unset}
-
-module UMap :
-sig
-  type key = Level.t
-  type +'a t
-  val empty : 'a t
-  val add : key -> 'a -> 'a t -> 'a t
-  val find : key -> 'a t -> 'a
-  val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
-  val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-  val iter : (key -> 'a -> unit) -> 'a t -> unit
-  val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
-end = HMap.Make(Level)
+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_arc
+    Canonical of canonical_node
   | Equiv of Level.t
 
-type universes = univ_entry UMap.t
+type universes =
+  { entries : univ_entry UMap.t;
+    index : int;
+    n_nodes : int; n_edges : int }
 
 type t = universes
 
 (** 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 _ arc = match arc with
+  let iter _ n = match n with
   | Equiv _ -> ()
-  | Canonical arc -> arc.status <- Unset
+  | Canonical n -> n.status <- NoMark
   in
-  UMap.iter iter g
+  UMap.iter iter g.entries
 
 let rec cleanup_universes g =
   try unsafe_cleanup_universes g
@@ -89,30 +95,43 @@ let rec cleanup_universes g =
         succeed. *)
     cleanup_universes g; raise e
 
-let enter_equiv_arc u v g =
-  UMap.add u (Equiv v) g
-
-let enter_arc ca g =
-  UMap.add ca.univ (Canonical ca) g
-
 (* Every Level.t has a unique canonical arc representative *)
 
-(** The graph always contains nodes for Prop and Set. *)
-
-let terminal_lt u v =
-  {(terminal u) with lt=[v]}
-    
-let empty_universes =
-  let g = enter_arc (terminal Level.set) UMap.empty in
-  let g = enter_arc (terminal_lt Level.prop Level.set) g in
-    g
-
-(* repr : universes -> Level.t -> canonical_arc *)
+(* 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 =
+      UMap.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 =
+      UMap.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 UMap.find u g
+    try UMap.find u g.entries
     with Not_found -> anomaly ~label:"Univ.repr"
         (str"Universe " ++ Level.pr u ++ str" undefined")
   in
@@ -127,272 +146,474 @@ let is_prop_arc u = Level.is_prop u.univ
 
 exception AlreadyDeclared
             
-let add_universe vlev strict g =
-  try
-    let _arcv = UMap.find vlev g in
-      raise AlreadyDeclared
-  with Not_found -> 
-    let v = terminal vlev in
-    let arc =
-      let arc = get_set_arc g in
-        if strict then
-          { arc with lt=vlev::arc.lt}
-        else 
-          { arc with le=vlev::arc.le}
-    in
-    let g = enter_arc arc g in
-      enter_arc v g
-
-(* reprleq : canonical_arc -> canonical_arc list *)
-(* All canonical arcv such that arcu<=arcv with arcv#arcu *)
-let reprleq g arcu =
-  let rec searchrec w = function
-    | [] -> w
-    | v :: vl ->
-        let arcv = repr g v in
-        if List.memq arcv w || arcu==arcv then
-          searchrec w vl
-        else
-          searchrec (arcv :: w) vl
+(* 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 rec safe_repr g u =
+  let rec safe_repr_rec entries u =
+    match UMap.find u entries with
+    | Equiv v -> safe_repr_rec entries v
+    | Canonical arc -> arc
   in
-  searchrec [] arcu.le
-
-
-(* between : Level.t -> canonical_arc -> canonical_arc list *)
-(* between u v = { w | u<=w<=v, w canonical }          *)
-(* between is the most costly operation *)
-
-let between g arcu arcv =
-  (* good are all w | u <= w <= v  *)
-  (* bad are all w | u <= w ~<= v *)
-    (* find good and bad nodes in {w | u <= w} *)
-    (* explore b u = (b or "u is good") *)
-  let rec explore ((good, bad, b) as input) arcu =
-    if List.memq arcu good then
-      (good, bad, true) (* b or true *)
-    else if List.memq arcu bad then
-      input    (* (good, bad, b or false) *)
+  try g, safe_repr_rec g.entries u
+  with Not_found ->
+    let can =
+      { univ = u;
+        ltle = UMap.empty; gtge = LSet.empty;
+        rank = if Level.is_small u then big_rank else 0;
+        klvl = 0; ilvl = 0;
+        status = NoMark }
+    in
+    let g = { g with
+      entries = UMap.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_universes_invariants g =
+  let n_edges = ref 0 in
+  let n_nodes = ref 0 in
+  UMap.iter (fun l u ->
+    match u with
+    | Canonical u ->
+      UMap.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 &&
+            (UMap.mem u.univ v.ltle ||
+             UMap.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 (UMap.mem u.univ u.ltle));
+      incr n_nodes
+    | Equiv _ -> assert (not (Level.is_small l)))
+    g.entries;
+  assert (!n_edges = g.n_edges);
+  assert (!n_nodes = g.n_nodes)
+
+let clean_ltle g ltle =
+  UMap.fold (fun u strict acc ->
+      let uu = (repr g u).univ in
+      if Level.equal uu u then acc
+      else (
+        let acc = UMap.remove u (fst acc) in
+        if not strict && UMap.mem uu acc then (acc, true)
+        else (UMap.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 = UMap.cardinal u.ltle in
+    let sz2 = UMap.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 UMap.find t g.entries with
+    | Equiv _ -> ()
+    | Canonical t ->
+      t.status <- NoMark) to_revert
+
+exception AbortBackward of universes
+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. *)
+
+(* [delta] is the timeout for backward search. It might be
+    usefull 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 =
+      UMap.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
-      let leq = reprleq g arcu in
-        (* is some universe >= u good ? *)
-      let good, bad, b_leq =
-        List.fold_left explore (good, bad, false) leq
-      in
-        if b_leq then
-          arcu::good, bad, true (* b or true *)
-        else
-          good, arcu::bad, b    (* b or false *)
+      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 -> UMap.add u.univ u acc)
+      UMap.empty to_merge
+  in
+  let ltle =
+    UMap.fold (fun _ n acc ->
+      UMap.merge (fun _ strict1 strict2 ->
+        match strict1, strict2 with
+        | Some true, _ | _, Some true -> Some true
+        | _, _ -> Some false)
+        acc n.ltle)
+      to_merge_lvl UMap.empty
   in
-  let good,_,_ = explore ([arcv],[],false) arcu in
-    good
-(* We assume  compare(u,v) = LE with v canonical (see compare below).
-   In this case List.hd(between g u v) = repr u
-   Otherwise, between g u v = []
- *)
-
-(** [fast_compare_neq] : is [arcv] in the transitive upward closure of [arcu] ?
-
-  In [strict] mode, we fully distinguish between LE and LT, while in
-  non-strict mode, we simply answer LE for both situations.
-
-  If [arcv] is encountered in a LT part, we could directly answer
-  without visiting unneeded parts of this transitive closure.
-  In [strict] mode, if [arcv] is encountered in a LE part, we could only
-  change the default answer (1st arg [c]) from NLE to LE, since a strict
-  constraint may appear later. During the recursive traversal,
-  [lt_done] and [le_done] are universes we have already visited,
-  they do not contain [arcv]. The 4rd arg is [(lt_todo,le_todo)],
-  two lists of universes not yet considered, known to be above [arcu],
-  strictly or not.
-
-  We use depth-first search, but the presence of [arcv] in [new_lt]
-  is checked as soon as possible : this seems to be slightly faster
-  on a test.
-
-  We do the traversal imperatively, setting the [status] flag on visited nodes.
-  This ensures O(1) check, but it also requires unsetting the flag when leaving
-  the function. Some special care has to be taken in order to ensure we do not
-  recover a messed up graph at the end. This occurs in particular when the
-  traversal raises an exception. Even though the code below is exception-free,
-  OCaml may still raise random exceptions, essentially fatal exceptions or
-  signal handlers. Therefore we ensure the cleanup by a catch-all clause. Note
-  also that the use of an imperative solution does make this function
-  thread-unsafe. For now we do not check universes in different threads, but if
-  ever this is to be done, we would need some lock somewhere.
+  let ltle, _ = clean_ltle g ltle in
+  let ltle =
+    UMap.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 =
+    UMap.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 (UMap.domain to_merge_lvl) in
+  (ltle, gtge)
 
-*)
 
-let get_explanation strict g arcu arcv =
-  (* [c] characterizes whether (and how) arcv has already been related
-     to arcu among the lt_done,le_done universe *)
-  let rec cmp c to_revert lt_todo le_todo = match lt_todo, le_todo with
-  | [],[] -> (to_revert, c)
-  | (arc,p)::lt_todo, le_todo ->
-    if arc_is_lt arc then
-      cmp c to_revert lt_todo le_todo
-    else
-      let rec find lt_todo lt le = match le with
-      | [] ->
-        begin match lt with
-        | [] ->
-          let () = arc.status <- SetLt in
-          cmp c (arc :: to_revert) lt_todo le_todo
-        | u :: lt ->
-          let arc = repr g u in
-          let p = (Lt, Universe.make u) :: p in
-          if arc == arcv then
-            if strict then (to_revert, p) else (to_revert, p)
-          else find ((arc, p) :: lt_todo) lt le
-        end
-      | u :: le ->
-        let arc = repr g u in
-        let p = (Le, Universe.make u) :: p in
-        if arc == arcv then
-          if strict then (to_revert, p) else (to_revert, p)
-        else find ((arc, p) :: lt_todo) lt le
-      in
-      find lt_todo arc.lt arc.le
-  | [], (arc,p)::le_todo ->
-    if arc == arcv then
-      (* No need to continue inspecting universes above arc:
-         if arcv is strictly above arc, then we would have a cycle.
-         But we cannot answer LE yet, a stronger constraint may
-         come later from [le_todo]. *)
-      if strict then cmp p to_revert [] le_todo else (to_revert, p)
-    else
-      if arc_is_le arc then
-        cmp c to_revert [] le_todo
-      else
-        let rec find lt_todo lt = match lt with
-        | [] ->
-          let fold accu u =
-            let p = (Le, Universe.make u) :: p in
-            let node = (repr g u, p) in
-            node :: accu
-          in
-          let le_new = List.fold_left fold le_todo arc.le in
-          let () = arc.status <- SetLe in
-          cmp c (arc :: to_revert) lt_todo le_new
-        | u :: lt ->
-          let arc = repr g u in
-          let p = (Lt, Universe.make u) :: p in
-          if arc == arcv then
-            if strict then (to_revert, p) else (to_revert, p)
-          else find ((arc, p) :: lt_todo) lt
+let reorder g u v =
+  (* STEP 1: 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 2: 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 3: 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
-        find [] arc.lt
+        List.iter (fun u -> u.status <- NoMark) to_revert;
+        r
+      end
+    else [], b_traversed, f_traversed
   in
-  let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in
-  try
-    let (to_revert, c) = cmp start [] [] [(arcu, [])] in
-    (** Reset all the touched arcs. *)
-    let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
-    List.rev c
-  with e ->
-    (** Unlikely event: fatal error or signal *)
-    let () = cleanup_universes g in
-    raise e
+  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
 
-let get_explanation strict g arcu arcv =
-  if !Flags.univ_print then Some (get_explanation strict g arcu arcv)
-  else None
+      (* 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
 
-type fast_order = FastEQ | FastLT | FastLE | FastNLE
+      (* Updating g.n_edges *)
+      let oldsz =
+        List.fold_left (fun sz u -> sz+UMap.cardinal u.ltle)
+          0 to_merge
+      in
+      let sz = UMap.cardinal ltle in
+      let g = { g with n_edges = g.n_edges + sz - oldsz } in
 
-let fast_compare_neq strict g arcu arcv =
-  (* [c] characterizes whether arcv has already been related
-     to arcu among the lt_done,le_done universe *)
-  let rec cmp c to_revert lt_todo le_todo = match lt_todo, le_todo with
-  | [],[] -> (to_revert, c)
-  | arc::lt_todo, le_todo ->
-    if arc_is_lt arc then
-      cmp c to_revert lt_todo le_todo
-    else
-      let () = arc.status <- SetLt in
-      process_lt c (arc :: to_revert) lt_todo le_todo arc.lt arc.le
-  | [], arc::le_todo ->
-    if arc == arcv then
-      (* No need to continue inspecting universes above arc:
-         if arcv is strictly above arc, then we would have a cycle.
-         But we cannot answer LE yet, a stronger constraint may
-         come later from [le_todo]. *)
-      if strict then cmp FastLE to_revert [] le_todo else (to_revert, FastLE)
-    else
-      if arc_is_le arc then
-        cmp c to_revert [] le_todo
-      else
-        let () = arc.status <- SetLe in
-        process_le c (arc :: to_revert) [] le_todo arc.lt arc.le
-
-  and process_lt c to_revert lt_todo le_todo lt le = match le with
-  | [] ->
-    begin match lt with
-    | [] -> cmp c to_revert lt_todo le_todo
-    | u :: lt ->
-      let arc = repr g u in
-      if arc == arcv then
-        if strict then (to_revert, FastLT) else (to_revert, FastLE)
-      else process_lt c to_revert (arc :: lt_todo) le_todo lt le
-    end
-  | u :: le ->
-    let arc = repr g u in
-    if arc == arcv then
-      if strict then (to_revert, FastLT) else (to_revert, FastLE)
-    else process_lt c to_revert (arc :: lt_todo) le_todo lt le
-
-  and process_le c to_revert lt_todo le_todo lt le = match lt with
-  | [] ->
-    let fold accu u =
-      let node = repr g u in
-      node :: accu
-    in
-    let le_new = List.fold_left fold le_todo le in
-    cmp c to_revert lt_todo le_new
-  | u :: lt ->
-    let arc = repr g u in
-    if arc == arcv then
-      if strict then (to_revert, FastLT) else (to_revert, FastLE)
-    else process_le c to_revert (arc :: lt_todo) le_todo lt le
+      (* 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 4: 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 (to_revert, c) = cmp FastNLE [] [] [arcu] in
-    (** Reset all the touched arcs. *)
-    let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
-    c
-  with e ->
+    let u = ucan.univ and v = vcan.univ in
+    (* do we need to reorder nodes ? *)
+    let g = if topo_compare ucan vcan <= 0 then g else reorder g u v in
+
+    (* 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 = UMap.find v.univ u.ltle in
+            if strict && not oldstrict then
+              change_node g { u with ltle = UMap.add v.univ true u.ltle }
+            else g
+        with Not_found ->
+          { (change_node g { u with ltle = UMap.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 get_explanation_strict g arcu arcv = get_explanation true g arcu arcv
+let add_universe vlev strict g =
+  try
+    let _arcv = UMap.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 = 0;
+      klvl = 0;
+      ilvl = g.index;
+      status = NoMark;
+    }
+    in
+    let entries = UMap.add vlev (Canonical v) g.entries in
+    let g = { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges } in
+    insert_edge strict (get_set_arc g) v g
+
+exception Found_explanation of explanation
+
+let get_explanation strict u v g =
+  let v = repr g v in
+  let visited_strict = ref UMap.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 (UMap.find u.univ !visited_strict) || strict
+        with Not_found -> false
+      in
+      if visited then None
+      else begin
+        visited_strict := UMap.add u.univ strict !visited_strict;
+        try
+          UMap.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, make u') :: exp)))
+            u.ltle;
+          None
+        with Found_explanation exp -> Some exp
+      end
+  in
+  let u = repr g u in
+  if u == v then [(Eq, make v.univ)]
+  else match traverse strict u with Some exp -> exp | None -> assert false
 
-let fast_compare g arcu arcv =
-  if arcu == arcv then FastEQ else fast_compare_neq true g arcu arcv
+let get_explanation strict u v g =
+  if !Flags.univ_print then Some (get_explanation strict u v g)
+  else None
 
-let is_leq g arcu arcv =
-  arcu == arcv ||
-    (match fast_compare_neq false g arcu arcv with
-    | FastNLE -> false
-    | (FastEQ|FastLE|FastLT) -> true)
-    
-let is_lt g arcu arcv =
-  if arcu == arcv then false
+(* 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 UMap.find v.univ u.ltle || not strict
+           with Not_found -> false
+        then raise (Found to_revert)
+        else
+          begin
+            let next_todo =
+              UMap.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
-    match fast_compare_neq true g arcu arcv with
-    | FastLT -> true
-    | (FastEQ|FastLE|FastNLE) -> false
-
-(* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ
-                compare(u,v) = LT or LE => compare(v,u) = NLE
-                compare(u,v) = NLE => compare(v,u) = NLE or LE or LT
-
-   Adding u>=v is consistent iff compare(v,u) # LT
-    and then it is redundant iff compare(u,v) # NLE
-   Adding u>v is consistent iff compare(v,u) = NLE
-    and then it is redundant iff compare(u,v) = LT *)
-
-(** * Universe checks [check_eq] and [check_leq], used in coqchk *)
+    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 =
+  check_universes_invariants g;
+  let g = insert_edge strict ucan vcan g in
+  check_universes_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 *)
 
@@ -405,11 +626,11 @@ let check_eq_level g u v = u == v || check_equal g u v
 let check_smaller g strict u v =
   let arcu = repr g u and arcv = repr g v in
   if strict then
-    is_lt g arcu arcv
+    search_path true arcu arcv g
   else
     is_prop_arc arcu 
     || (is_set_arc arcu && not (is_prop_arc arcv))
-    || is_leq g arcu arcv
+    || search_path false arcu arcv g
 
 (** Then, checks on universes *)
 
@@ -448,145 +669,68 @@ let check_leq g u v =
     is_type0m_univ u ||
     check_eq_univs g u v || real_check_leq g u v
 
-(** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
-
-(* setlt : Level.t -> Level.t -> reason -> unit *)
-(* forces u > v *)
-(* this is normally an update of u in g rather than a creation. *)
-let setlt g arcu arcv =
-  let arcu' = {arcu with lt=arcv.univ::arcu.lt} in
-    enter_arc arcu' g, arcu'
-
-(* checks that non-redundant *)
-let setlt_if (g,arcu) v =
-  let arcv = repr g v in
-  if is_lt g arcu arcv then g, arcu
-  else setlt g arcu arcv
-
-(* setleq : Level.t -> Level.t -> unit *)
-(* forces u >= v *)
-(* this is normally an update of u in g rather than a creation. *)
-let setleq g arcu arcv =
-  let arcu' = {arcu with le=arcv.univ::arcu.le} in
-    enter_arc arcu' g, arcu'
-
-(* checks that non-redundant *)
-let setleq_if (g,arcu) v =
-  let arcv = repr g v in
-  if is_leq g arcu arcv then g, arcu
-  else setleq g arcu arcv
-
-(* merge : Level.t -> Level.t -> unit *)
-(* we assume  compare(u,v) = LE *)
-(* merge u v  forces u ~ v with repr u as canonical repr *)
-let merge g arcu arcv =
-  (* we find the arc with the biggest rank, and we redirect all others to it *)
-  let arcu, g, v =
-    let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
-      if Level.is_small arc.univ ||
-           (arc.rank >= max_rank && not (Level.is_small best_arc.univ))
-      then (arc.rank, max_rank, arc, best_arc::rest)
-      else (max_rank, old_max_rank, best_arc, arc::rest)
-    in
-      match between g arcu arcv with
-      | [] -> anomaly (str "Univ.between")
-      | arc::rest ->
-        let (max_rank, old_max_rank, best_arc, rest) =
-          List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in
-          if max_rank > old_max_rank then best_arc, g, rest
-          else begin
-              (* one redirected node also has max_rank *)
-            let arcu = {best_arc with rank = max_rank + 1} in
-              arcu, enter_arc arcu g, rest
-          end 
-  in
-  let redirect (g,w,w') arcv =
-    let g' = enter_equiv_arc arcv.univ arcu.univ g in
-    (g',List.unionq arcv.lt w,arcv.le@w')
-  in
-  let (g',w,w') = List.fold_left redirect (g,[],[]) v in
-  let g_arcu = (g',arcu) in
-  let g_arcu = List.fold_left setlt_if g_arcu w in
-  let g_arcu = List.fold_left setleq_if g_arcu w' in
-  fst g_arcu
-
-(* merge_disc : Level.t -> Level.t -> unit *)
-(* we assume  compare(u,v) = compare(v,u) = NLE *)
-(* merge_disc u v  forces u ~ v with repr u as canonical repr *)
-let merge_disc g arc1 arc2 =
-  let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
-  let arcu, g = 
-    if not (Int.equal arc1.rank arc2.rank) then arcu, g
-    else
-      let arcu = {arcu with rank = succ arcu.rank} in 
-      arcu, enter_arc arcu g
-  in
-  let g' = enter_equiv_arc arcv.univ arcu.univ g in
-  let g_arcu = (g',arcu) in
-  let g_arcu = List.fold_left setlt_if g_arcu arcv.lt in
-  let g_arcu = List.fold_left setleq_if g_arcu arcv.le in
-  fst g_arcu
+(* enforc_univ_eq g u v will force u=v if possible, will fail otherwise *)
 
-(* enforce_univ_eq : Level.t -> Level.t -> unit *)
-(* enforce_univ_eq u v will force u=v if possible, will fail otherwise *)
+let rec enforce_univ_eq u v g =
+  let ucan = repr g u in
+  let vcan = repr g v in
+  if topo_compare ucan vcan = 1 then enforce_univ_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 ->
+      error_inconsistency Eq v u (get_explanation true u v g)
 
-let enforce_univ_eq u v g =
-  let arcu = repr g u and arcv = repr g v in
-    match fast_compare g arcu arcv with
-    | FastEQ -> g
-    | FastLT ->
-      let p = get_explanation_strict g arcu arcv in
-      error_inconsistency Eq v u p
-    | FastLE -> merge g arcu arcv
-    | FastNLE ->
-      (match fast_compare g arcv arcu with
-      | FastLT ->
-        let p = get_explanation_strict g arcv arcu in
-        error_inconsistency Eq u v p
-      | FastLE -> merge g arcv arcu
-      | FastNLE -> merge_disc g arcu arcv
-      | FastEQ -> anomaly (Pp.str "Univ.compare"))
-
-(* enforce_univ_leq : Level.t -> Level.t -> unit *)
-(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
+(* enforce_univ_leq g u v will force u<=v if possible, will fail otherwise *)
 let enforce_univ_leq u v g =
-  let arcu = repr g u and arcv = repr g v in
-  if is_leq g arcu arcv then g
-  else
-    match fast_compare g arcv arcu with
-    | FastLT ->
-      let p = get_explanation_strict g arcv arcu in
-      error_inconsistency Le u v p
-    | FastLE  -> merge g arcv arcu
-    | FastNLE -> fst (setleq g arcu arcv)
-    | FastEQ -> anomaly (Pp.str "Univ.compare")
+  let ucan = repr g u in
+  let vcan = repr g v in
+  try insert_edge false ucan vcan g
+  with CycleDetected ->
+    error_inconsistency Le u v (get_explanation true v u g)
 
 (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
 let enforce_univ_lt u v g =
-  let arcu = repr g u and arcv = repr g v in
-    match fast_compare g arcu arcv with
-    | FastLT -> g
-    | FastLE -> fst (setlt g arcu arcv)
-    | FastEQ -> error_inconsistency Lt u v (Some [(Eq,Universe.make v)])
-    | FastNLE ->
-      match fast_compare_neq false g arcv arcu with
-        FastNLE -> fst (setlt g arcu arcv)
-      | FastEQ -> anomaly (Pp.str "Univ.compare")
-      | (FastLE|FastLT) ->
-        let p = get_explanation false g arcv arcu  in
-        error_inconsistency Lt u v p
+  let ucan = repr g u in
+  let vcan = repr g v in
+  try insert_edge true ucan vcan g
+  with CycleDetected ->
+    error_inconsistency Lt u v (get_explanation false v u g)
+
+let empty_universes =
+  let set_arc = Canonical {
+    univ = Level.set;
+    ltle = LMap.empty;
+    gtge = LSet.empty;
+    rank = big_rank;
+    klvl = 0;
+    ilvl = (-1);
+    status = NoMark;
+  } in
+  let prop_arc = Canonical {
+    univ = Level.prop;
+    ltle = LMap.empty;
+    gtge = LSet.empty;
+    rank = big_rank;
+    klvl = 0;
+    ilvl = 0;
+    status = NoMark;
+  } in
+  let entries = UMap.add Level.set set_arc (UMap.singleton Level.prop prop_arc) in
+  let empty = { entries; index = (-2); n_nodes = 2; n_edges = 0 } in
+  enforce_univ_lt Level.prop Level.set empty
 
 (* Prop = Set is forbidden here. *)
 let initial_universes = empty_universes
 
-let is_initial_universes g = UMap.equal (==) g initial_universes
-      
+let is_initial_universes g = UMap.equal (==) g.entries initial_universes.entries
+
 let enforce_constraint cst g =
   match cst with
     | (u,Lt,v) -> enforce_univ_lt u v g
     | (u,Le,v) -> enforce_univ_leq u v g
     | (u,Eq,v) -> enforce_univ_eq u v g
-      
+
 let merge_constraints c g =
   Constraint.fold enforce_constraint c g
 
@@ -608,193 +752,89 @@ let lookup_level u g =
     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
-    (see the assertion)... I (Stéphane Glondu) am not sure if this
-    plays a role in the rest of the module. *)
+    a [Canonical] element is its own name, by keeping [Equiv] edges. *)
 let normalize_universes g =
-  let rec visit u arc cache = match lookup_level u cache with
-    | Some x -> x, cache
-    | None -> match Lazy.force arc with
-    | None ->
-      u, UMap.add u u cache
-    | Some (Canonical {univ=v; lt=_; le=_}) ->
-      v, UMap.add u v cache
-    | Some (Equiv v) ->
-      let v, cache = visit v (lazy (lookup_level v g)) cache in
-      v, UMap.add u v cache
-  in
-  let cache = UMap.fold
-    (fun u arc cache -> snd (visit u (Lazy.lazy_from_val (Some arc)) cache))
-    g UMap.empty
-  in
-  let repr x = UMap.find x cache in
-  let lrepr us = List.fold_left
-    (fun e x -> LSet.add (repr x) e) LSet.empty us
+  let g =
+    { g with
+      entries = UMap.map (fun entry ->
+        match entry with
+        | Equiv u -> Equiv ((repr g u).univ)
+        | Canonical ucan -> Canonical { ucan with rank = 1 })
+        g.entries }
   in
-  let canonicalize u = function
-    | Equiv _ -> Equiv (repr u)
-    | Canonical {univ=v; lt=lt; le=le; rank=rank} ->
-      assert (u == v);
-      (* avoid duplicates and self-loops *)
-      let lt = lrepr lt and le = lrepr le in
-      let le = LSet.filter
-        (fun x -> x != u && not (LSet.mem x lt)) le
-      in
-      LSet.iter (fun x -> assert (x != u)) lt;
-      Canonical {
-        univ = v;
-        lt = LSet.elements lt;
-        le = LSet.elements le;
-        rank = rank;
-        status = Unset;
-      }
-  in
-  UMap.mapi canonicalize g
+  UMap.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_universes g =
   let constraints_of u v acc =
     match v with
-    | Canonical {univ=u; lt=lt; le=le} ->
-      let acc = List.fold_left (fun acc v -> Constraint.add (u,Lt,v) acc) acc lt in
-      let acc = List.fold_left (fun acc v -> Constraint.add (u,Le,v) acc) acc le in
-        acc
+    | Canonical {univ=u; ltle} ->
+      UMap.fold (fun v strict acc->
+        let typ = if strict then Lt else Le in
+        Constraint.add (u,typ,v) acc) ltle acc
     | Equiv v -> Constraint.add (u,Eq,v) acc
   in
-  UMap.fold constraints_of g Constraint.empty
+  UMap.fold constraints_of g.entries Constraint.empty
 
 let constraints_of_universes g =
   constraints_of_universes (normalize_universes g)
 
-(** Longest path algorithm. This is used to compute the minimal number of
-    universes required if the only strict edge would be the Lt one. This
-    algorithm assumes that the given universes constraints are a almost DAG, in
-    the sense that there may be {Eq, Le}-cycles. This is OK for consistent
-    universes, which is the only case where we use this algorithm. *)
-
-(** Adjacency graph *)
-type graph = constraint_type LMap.t LMap.t
-
-exception Connected
-
-(** Check connectedness *)
-let connected x y (g : graph) =
-  let rec connected x target seen g =
-    if Level.equal x target then raise Connected
-    else if not (LSet.mem x seen) then
-      let seen = LSet.add x seen in
-      let fold z _ seen = connected z target seen g in
-      let neighbours = try LMap.find x g with Not_found -> LMap.empty in
-      LMap.fold fold neighbours seen
-    else seen
+(** [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_universes g =
+  let cans =
+    UMap.fold (fun _ u l ->
+      match u with
+      | Equiv _ -> l
+      | Canonical can -> can :: l
+    ) g.entries []
   in
-  try ignore(connected x y LSet.empty g); false with Connected -> true
-
-let add_edge x y v (g : graph) =
-  try
-    let neighbours = LMap.find x g in
-    let neighbours = LMap.add y v neighbours in
-    LMap.add x neighbours g
-  with Not_found ->
-    LMap.add x (LMap.singleton y v) g
-
-(** We want to keep the graph DAG. If adding an edge would cause a cycle, that
-    would necessarily be an {Eq, Le}-cycle, otherwise there would have been a
-    universe inconsistency. Therefore we may omit adding such a cycling edge
-    without changing the compacted graph. *)
-let add_eq_edge x y v g = if connected y x g then g else add_edge x y v g
-
-(** Construct the DAG and its inverse at the same time. *)
-let make_graph g : (graph * graph) =
-  let fold u arc accu = match arc with
-  | Equiv v ->
-    let (dir, rev) = accu in
-    (add_eq_edge u v Eq dir, add_eq_edge v u Eq rev)
-  | Canonical { univ; lt; le; } ->
-    let () = assert (u == univ) in
-    let fold_lt (dir, rev) v = (add_edge u v Lt dir, add_edge v u Lt rev) in
-    let fold_le (dir, rev) v = (add_eq_edge u v Le dir, add_eq_edge v u Le rev) in
-    (** Order is important : lt after le, because of the possible redundancy
-        between [le] and [lt] in a canonical arc. This way, the [lt] constraint
-        is the last one set, which is correct because it implies [le]. *)
-    let accu = List.fold_left fold_le accu le in
-    let accu = List.fold_left fold_lt accu lt in
-    accu
-  in
-  UMap.fold fold g (LMap.empty, LMap.empty)
-
-(** Construct a topological order out of a DAG. *)
-let rec topological_fold u g rem seen accu =
-  let is_seen =
-    try
-      let status = LMap.find u seen in
-      assert status; (** If false, not a DAG! *)
-      true
-    with Not_found -> false
+  let cans = List.sort topo_compare cans in
+  let lowest_levels =
+    UMap.mapi (fun u _ -> if Level.is_small u then 0 else 2)
+      (UMap.filter
+         (fun _ u -> match u with Equiv _ -> false | Canonical _ -> true)
+         g.entries)
   in
-  if not is_seen then
-    let rem = LMap.remove u rem in
-    let seen = LMap.add u false seen in
-    let neighbours = try LMap.find u g with Not_found -> LMap.empty in
-    let fold v _ (rem, seen, accu) = topological_fold v g rem seen accu in
-    let (rem, seen, accu) = LMap.fold fold neighbours (rem, seen, accu) in
-    (rem, LMap.add u true seen, u :: accu)
-  else (rem, seen, accu)
-
-let rec topological g rem seen accu =
-  let node = try Some (LMap.choose rem) with Not_found -> None in
-  match node with
-  | None -> accu
-  | Some (u, _) ->
-    let rem, seen, accu = topological_fold u g rem seen accu in
-    topological g rem seen accu
-
-(** Compute the longest path from any vertex. *)
-let constraint_cost = function
-| Eq | Le -> 0
-| Lt -> 1
-
-(** This algorithm browses the graph in topological order, computing for each
-    encountered node the length of the longest path leading to it. Should be
-    O(|V|) or so (modulo map representation). *)
-let rec flatten_graph rem (rev : graph) map mx = match rem with
-| [] -> map, mx
-| u :: rem ->
-  let prev = try LMap.find u rev with Not_found -> LMap.empty in
-  let fold v cstr accu =
-    let v_cost = LMap.find v map in
-    max (v_cost + constraint_cost cstr) accu
+  let lowest_levels =
+    List.fold_left (fun lowest_levels can ->
+      let lvl = UMap.find can.univ lowest_levels in
+      UMap.fold (fun u' strict lowest_levels ->
+        let cost = if strict then 1 else 0 in
+        let u' = (repr g u').univ in
+        UMap.modify u' (fun _ lvl0 -> max lvl0 (lvl+cost)) lowest_levels)
+       can.ltle lowest_levels)
+     lowest_levels cans
   in
-  let u_cost = LMap.fold fold prev 0 in
-  let map = LMap.add u u_cost map in
-  flatten_graph rem rev map (max mx u_cost)
-
-(** [sort_universes g] builds a map from universes in [g] to natural
-    numbers. It outputs a graph containing equivalence edges from each
-    level appearing in [g] to [Type.n], and [lt] edges between the
-    [Type.n]s. The output graph should imply the input graph (and the
-    [Type.n]s. The output graph should imply the input graph (and the
-    implication will be strict most of the time), but is not
-    necessarily minimal. 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_universes orig =
-  let (dir, rev) = make_graph orig in
-  let order = topological dir dir LMap.empty [] in
-  let compact, max = flatten_graph order rev LMap.empty 0 in
+  let max_lvl = UMap.fold (fun _ a b -> max a b) lowest_levels 0 in
   let mp = Names.DirPath.make [Names.Id.of_string "Type"] in
-  let types = Array.init (max + 1) (fun n -> Level.make mp n) in
-  (** Old universes are made equal to [Type.n] *)
-  let fold u level accu = UMap.add u (Equiv types.(level)) accu in
-  let sorted = LMap.fold fold compact UMap.empty in
-  (** Add all [Type.n] nodes *)
-  let fold i accu u =
-    if i < max then
-      let pred = types.(i + 1) in
-      let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in
-      UMap.add u (Canonical arc) accu
-    else accu
+  let types = Array.init (max_lvl + 1) (function
+    | 0 -> Level.prop
+    | 1 -> Level.set
+    | n -> Level.make mp (n-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
-  Array.fold_left_i fold sorted types
+  let g = if max_lvl >= 2 then enforce_univ_lt Level.set types.(2) g else g in
+  let g =
+    UMap.fold (fun u lvl g -> enforce_univ_eq u (types.(lvl)) g)
+      lowest_levels g
+  in
+  normalize_universes g
 
 (** Instances *)
 
@@ -807,39 +847,38 @@ let check_eq_instances g t1 t2 =
           (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1))
         in aux 0)
 
+(** Pretty-printing *)
+
 let pr_arc prl = function
-  | _, Canonical {univ=u; lt=[]; le=[]} ->
-      mt ()
-  | _, Canonical {univ=u; lt=lt; le=le} ->
-      let opt_sep = match lt, le with
-      | [], _ | _, [] -> mt ()
-      | _ -> spc ()
-      in
+  | _, Canonical {univ=u; ltle} ->
+    if UMap.is_empty ltle then mt ()
+    else
       prl u ++ str " " ++
       v 0
-        (pr_sequence (fun v -> str "< " ++ prl v) lt ++
-         opt_sep ++
-         pr_sequence (fun v -> str "<= " ++ prl v) le) ++
+        (pr_sequence (fun (v, strict) ->
+          (if strict then str "< " else str "<= ") ++ prl v)
+           (UMap.bindings ltle)) ++
       fnl ()
   | u, Equiv v ->
       prl u  ++ str " = " ++ prl v ++ fnl ()
 
 let pr_universes prl g =
-  let graph = UMap.fold (fun u a l -> (u,a)::l) g [] in
+  let graph = UMap.fold (fun u a l -> (u,a)::l) g.entries [] in
   prlist (pr_arc prl) graph
 
 (* Dumping constraints to a file *)
 
 let dump_universes output g =
   let dump_arc u = function
-    | Canonical {univ=u; lt=lt; le=le} ->
+    | Canonical {univ=u; ltle} ->
         let u_str = Level.to_string u in
-        List.iter (fun v -> output Lt u_str (Level.to_string v)) lt;
-        List.iter (fun v -> output Le u_str (Level.to_string v)) le
+        UMap.iter (fun v strict ->
+          let typ = if strict then Lt else Le in
+          output typ u_str (Level.to_string v)) ltle;
     | Equiv v ->
       output Eq (Level.to_string u) (Level.to_string v)
   in
-  UMap.iter dump_arc g
+  UMap.iter dump_arc g.entries
 
 (** Profiling *)
 
@@ -848,7 +887,6 @@ let merge_constraints =
     let key = Profile.declare_profile "merge_constraints" in
       Profile.profile2 key merge_constraints
   else merge_constraints
-
 let check_constraints =
   if Flags.profile then
     let key = Profile.declare_profile "check_constraints" in