Splitting kernel universe code in two modules.

1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.

1 files changed, 868 insertions, 0 deletions

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
new file mode 100644
index 000000000..356cf4da6
--- /dev/null
+++ b/kernel/uGraph.ml
@@ -0,0 +1,868 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+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] *)
+
+(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau, 
+   Pierre-Marie Pédrot *)
+
+let error_inconsistency o u v (p:explanation option) =
+  raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
+
+type status = Unset | SetLe | SetLt
+
+(* Comparison on this type is pointer equality *)
+type canonical_arc =
+    { univ: Level.t;
+      lt: Level.t list;
+      le: Level.t list;
+      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. *)
+    }
+
+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)
+
+(* 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
+  | Equiv of Level.t
+
+type universes = univ_entry UMap.t
+
+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
+  | Equiv _ -> ()
+  | Canonical arc -> arc.status <- Unset
+  in
+  UMap.iter iter g
+
+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
+
+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 *)
+(* canonical representative : we follow the Equiv links *)
+
+let rec repr g u =
+  let a =
+    try UMap.find u g
+    with Not_found -> 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_prop_arc g = repr g Level.prop
+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
+            
+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
+  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) *)
+    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 *)
+  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 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
+        in
+        find [] arc.lt
+  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 get_explanation strict g arcu arcv =
+  if !Flags.univ_print then Some (get_explanation strict g arcu arcv)
+  else None
+
+type fast_order = FastEQ | FastLT | FastLE | FastNLE
+
+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
+
+  in
+  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 ->
+    (** 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 fast_compare g arcu arcv =
+  if arcu == arcv then FastEQ else fast_compare_neq true g arcu arcv
+
+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
+  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 *)
+
+(** 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
+    is_lt g arcu arcv
+  else
+    is_prop_arc arcu 
+    || (is_set_arc arcu && not (is_prop_arc arcv))
+    || is_leq g arcu arcv
+
+(** Then, checks on universes *)
+
+type 'a check_function = universes -> 'a -> 'a -> bool
+
+let check_equal_expr g x y =
+  x == y || (let (u, n) = x and (v, m) = y in 
+               Int.equal n m && check_equal g u v)
+
+let check_eq_univs g l1 l2 =
+  let f x1 x2 = check_equal_expr g x1 x2 in
+  let exists x1 l = Universe.exists (fun x2 -> f x1 x2) l in
+    Universe.for_all (fun x1 -> exists x1 l2) l1
+    && Universe.for_all (fun x2 -> exists x2 l1) l2
+
+let check_eq g u v =
+  Universe.equal u v || check_eq_univs g u v
+
+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
+    | _ -> false
+
+let exists_bigger g ul l =
+  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 ||
+    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
+
+(* enforce_univ_eq : Level.t -> Level.t -> unit *)
+(* enforce_univ_eq u v will force u=v if possible, will fail otherwise *)
+
+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 *)
+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")
+
+(* 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
+
+(* Prop = Set is forbidden here. *)
+let initial_universes = empty_universes
+
+let is_initial_universes g = UMap.equal (==) g initial_universes
+      
+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) =
+  match d with
+  | Eq -> check_equal g l r
+  | Le -> check_smaller g false l r
+  | Lt -> check_smaller g true l r
+
+let check_constraints c g =
+  Constraint.for_all (check_constraint g) c
+
+(* Normalization *)
+
+let lookup_level u g =
+  try Some (UMap.find u g) with Not_found -> None
+
+(** [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
+    (see the assertion)... I (Stéphane Glondu) am not sure if this
+    plays a role in the rest of the module. *)
+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
+  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
+
+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
+    | Equiv v -> Constraint.add (u,Eq,v) acc
+  in
+  UMap.fold constraints_of g 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
+  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
+  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
+  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 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
+  in
+  Array.fold_left_i fold sorted types
+
+(** Instances *)
+
+let check_eq_instances g t1 t2 =
+  let t1 = Instance.to_array t1 in
+  let t2 = Instance.to_array t2 in
+  t1 == t2 ||
+    (Int.equal (Array.length t1) (Array.length t2) &&
+        let rec aux i =
+          (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1))
+        in aux 0)
+
+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
+      prl u ++ str " " ++
+      v 0
+        (pr_sequence (fun v -> str "< " ++ prl v) lt ++
+         opt_sep ++
+         pr_sequence (fun v -> str "<= " ++ prl v) le) ++
+      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
+  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} ->
+        let u_str = Level.to_string u in
+        List.iter (fun v -> output Lt (Level.to_string v) u_str) lt;
+        List.iter (fun v -> output Le (Level.to_string v) u_str) le
+    | Equiv v ->
+      output Eq (Level.to_string u) (Level.to_string v)
+  in
+  UMap.iter dump_arc g
+
+(** Profiling *)
+
+let merge_constraints = 
+  if Flags.profile then 
+    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
+      Profile.profile2 key check_constraints
+  else check_constraints
+
+let check_eq = 
+  if Flags.profile then
+    let check_eq_key = Profile.declare_profile "check_eq" in
+      Profile.profile3 check_eq_key check_eq
+  else check_eq
+
+let check_leq = 
+  if Flags.profile then 
+    let check_leq_key = Profile.declare_profile "check_leq" in
+      Profile.profile3 check_leq_key check_leq
+  else check_leq