Make ugraph implementation abstract wrt universe specifics

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

1 files changed, 78 insertions, 898 deletions

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 5fc8d0297f..8187dea41b 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -8,749 +8,80 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Pp
-open Util
 open Univ
 
-(* 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] *)
+module G = AcyclicGraph.Make(struct
+    type t = Level.t
+    module Set = LSet
+    module Map = LMap
+    module Constraint = Constraint
 
-(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu
-   Sozeau, Pierre-Marie Pédrot, Jacques-Henri Jourdan *)
+    let equal = Level.equal
+    let compare = Level.compare
 
-let error_inconsistency o u v p =
-  raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
+    type explanation = Univ.explanation
+    let error_inconsistency d u v p =
+      raise (UniverseInconsistency (d,Universe.make u, Universe.make v, p))
 
-(* 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$.
+    let pr = Level.pr
+  end) [@@inlined] (* without inline, +1% ish on HoTT, compcert. See jenkins 594 vs 596 *)
+(* Do not include G to make it easier to control universe specific
+   code (eg add_universe with a constraint vs G.add with no
+   constraint) *)
 
-   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_node =
-    { univ: Level.t;
-      ltle: bool UMap.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 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 _ n = match n with
-  | Equiv _ -> ()
-  | Canonical n -> n.status <- NoMark
-  in
-  UMap.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 =
-      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.entries
-    with Not_found -> CErrors.anomaly ~label:"Univ.repr"
-        (str"Universe " ++ Level.pr u ++ str" undefined.")
-  in
-  match a with
-    | Equiv v -> repr g v
-    | Canonical arc -> arc
-
-let get_set_arc g = repr g Level.set
-let is_set_arc u = Level.is_set u.univ
-let is_prop_arc u = Level.is_prop u.univ
-
-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 UMap.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 = 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.
-
-   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 =
-      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
-      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 =
-    let fold _ n acc =
-      let fold u strict acc =
-        if strict then UMap.add u strict acc
-        else if UMap.mem u acc then acc
-        else UMap.add u false acc
-      in
-      UMap.fold fold n.ltle acc
-    in
-    UMap.fold fold to_merge_lvl UMap.empty
-  in
-  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 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+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
-
-      (* 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 = 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 add_universe_gen vlev 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
-    { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }, v
-
-let add_universe vlev strict g =
-  let g, v = add_universe_gen vlev g in
-  insert_edge strict (get_set_arc g) v g
-
-let add_universe_unconstrained vlev g =
-  fst (add_universe_gen vlev g)
-
-exception UndeclaredLevel of Univ.Level.t
-let check_declared_universes g us =
-  let check l = if not (UMap.mem l g.entries) then raise (UndeclaredLevel l) in
-  Univ.LSet.iter check us
-
-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 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 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
-    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 *)
-
-let check_equal g u v =
-  let arcu = repr g u and arcv = repr g v in
-    arcu == arcv
-
-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
-    search_path true arcu arcv g
-  else
-    is_prop_arc arcu 
-    || (is_set_arc arcu && not (is_prop_arc arcv))
-    || search_path false arcu arcv g
-
-(** Then, checks on universes *)
-
-type 'a check_function = universes -> 'a -> 'a -> bool
+type t = G.t
+type 'a check_function = 'a G.check_function
 
 let check_smaller_expr g (u,n) (v,m) =
   let diff = n - m in
     match diff with
-    | 0 -> check_smaller g false u v
-    | 1 -> check_smaller g true u v
-    | x when x < 0 -> check_smaller g false u v
+    | 0 -> G.check_leq g u v
+    | 1 -> G.check_lt g u v
+    | x when x < 0 -> G.check_leq g u v
     | _ -> false
 
 let exists_bigger g ul l =
-  Universe.exists (fun ul' -> 
+  Universe.exists (fun ul' ->
     check_smaller_expr g ul ul') l
 
 let real_check_leq g u v =
   Universe.for_all (fun ul -> exists_bigger g ul v) u
-    
+
 let check_leq g u v =
   Universe.equal u v ||
     is_type0m_univ u ||
     real_check_leq g u v
 
-let check_eq_univs g l1 l2 =
-  real_check_leq g l1 l2 && real_check_leq g l2 l1
-
 let check_eq g u v =
-  Universe.equal u v || check_eq_univs g u v
-
-(* enforce_univ_eq g 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)
-
-(* enforce_univ_leq g u v will force u<=v if possible, will fail otherwise *)
-let enforce_univ_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 ->
-    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 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 =
-  { entries = UMap.empty; index = 0; n_nodes = 0; n_edges = 0 }
+  Universe.equal u v ||
+  (real_check_leq g u v && real_check_leq g v u)
+
+let check_eq_level = G.check_eq
+
+let empty_universes = G.empty
 
 let initial_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
-
-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
-
-let check_constraint g (l,d,r) =
+  let big_rank = 1000000 in
+  let g = G.empty in
+  let g = G.add ~rank:big_rank Level.prop g in
+  let g = G.add ~rank:big_rank Level.set g in
+  G.enforce_lt Level.prop Level.set g
+
+let enforce_constraint (u,d,v) g =
+  match d with
+  | Le -> G.enforce_leq u v g
+  | Lt -> G.enforce_lt u v g
+  | Eq -> G.enforce_eq u v g
+
+let merge_constraints csts g = Constraint.fold enforce_constraint csts g
+
+let check_constraint g (u,d,v) =
   match d with
-  | Eq -> check_equal g l r
-  | Le -> check_smaller g false l r
-  | Lt -> check_smaller g true l r
+  | Le -> G.check_leq g u v
+  | Lt -> G.check_lt g u v
+  | Eq -> G.check_eq g u v
 
-let check_constraints c g =
-  Constraint.for_all (check_constraint g) c
+let check_constraints csts g = Constraint.for_all (check_constraint g) csts
 
 let leq_expr (u,m) (v,n) =
   let d = match m - n with
@@ -760,6 +91,7 @@ let leq_expr (u,m) (v,n) =
   (u,d,v)
 
 let enforce_leq_alg u v g =
+  let open Util in
   let enforce_one (u,v) = function
     | Inr _ as orig -> orig
     | Inl (cstrs,g) as orig ->
@@ -791,148 +123,19 @@ let enforce_leq_alg u v g =
   assert (check_leq g u v);
   cg
 
-(* 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 = UMap.map (fun entry ->
-        match entry with
-        | Equiv u -> Equiv ((repr g u).univ)
-        | Canonical ucan -> Canonical { ucan with rank = 1 })
-        g.entries }
-  in
-  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 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; _} ->
-      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 -> UF.union u v uf; acc
-  in
-  let csts = UMap.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, enforce_eq_level u arcu.univ csts
-      else
-        match LMap.find arcu.univ rmap with
-        | v -> rmap, enforce_eq_level u 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_universes g =
-  let cans =
-    UMap.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 =
-    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
-  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 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_lvl + 1) (function
-    | 0 -> Level.prop
-    | 1 -> Level.set
-    | n -> Level.make (Level.UGlobal.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
-  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
+exception AlreadyDeclared = G.AlreadyDeclared
+let add_universe u strict g =
+  let g = G.add u g in
+  let d = if strict then Lt else Le in
+  enforce_constraint (Level.set,d,u) g
+
+let add_universe_unconstrained u g = G.add u g
+
+exception UndeclaredLevel = G.Undeclared
+let check_declared_universes = G.check_declared
+
+let constraints_of_universes = G.constraints_of
+let constraints_for = G.constraints_for
 
 (** Subtyping of polymorphic contexts *)
 
@@ -957,45 +160,23 @@ 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_umap sep pr map =
-  let cmp (u,_) (v,_) = Level.compare u v in
-  Pp.prlist_with_sep sep pr (List.sort cmp (UMap.bindings map))
-
-let pr_arc prl = function
-  | _, Canonical {univ=u; ltle; _} ->
-    if UMap.is_empty ltle then mt ()
-    else
-      prl u ++ str " " ++
-      v 0
-        (pr_umap Pp.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_universes prl g =
-  pr_umap mt (pr_arc prl) g.entries
-
-(* Dumping constraints to a file *)
-
-let dump_universes output g =
-  let dump_arc u = function
-    | Canonical {univ=u; ltle; _} ->
-        UMap.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
-  UMap.iter dump_arc g.entries
+let domain = G.domain
+let choose = G.choose
+
+let dump_universes = G.dump
+
+let check_universes_invariants g = G.check_invariants ~required_canonical:Level.is_small g
+
+let pr_universes = G.pr
+
+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.sort make_dummy [Level.prop;Level.set] g
 
 (** Profiling *)
 
-let merge_constraints = 
-  if Flags.profile then 
+let merge_constraints =
+  if Flags.profile then
     let key = CProfile.declare_profile "merge_constraints" in
       CProfile.profile2 key merge_constraints
   else merge_constraints
@@ -1005,15 +186,14 @@ let check_constraints =
       CProfile.profile2 key check_constraints
   else check_constraints
 
-let check_eq = 
+let check_eq =
   if Flags.profile then
     let check_eq_key = CProfile.declare_profile "check_eq" in
       CProfile.profile3 check_eq_key check_eq
   else check_eq
 
-let check_leq = 
-  if Flags.profile then 
+let check_leq =
+  if Flags.profile then
     let check_leq_key = CProfile.declare_profile "check_leq" in
       CProfile.profile3 check_leq_key check_leq
   else check_leq
-