Imported Upstream version 8.5~beta1+dfsg

1 files changed, 1706 insertions, 551 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 822f6ca6..08e9fee0 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <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        *)
@@ -10,10 +10,13 @@
 (* 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 *)
+(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau, 
+   Pierre-Marie Pédrot *)
 
 open Pp
+open Errors
 open Util
 
 (* Universes are stratified by a partial ordering $\le$.
@@ -28,40 +31,337 @@ open Util
    union-find algorithm. The assertions $<$ and $\le$ are represented by
    adjacency lists *)
 
-module UniverseLevel = struct
+module type Hashconsed =
+sig
+  type t
+  val hash : t -> int
+  val equal : t -> t -> bool
+  val hcons : t -> t
+end
 
-  type t =
-    | Set
-    | Level of Names.dir_path * int
+module HashedList (M : Hashconsed) :
+sig
+  type t = private Nil | Cons of M.t * int * t
+  val nil : t
+  val cons : M.t -> t -> t
+end =
+struct
+  type t = Nil | Cons of M.t * int * t
+  module Self =
+  struct
+    type _t = t
+    type t = _t
+    type u = (M.t -> M.t)
+    let hash = function Nil -> 0 | Cons (_, h, _) -> h
+    let equal l1 l2 = match l1, l2 with
+    | Nil, Nil -> true
+    | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2
+    | _ -> false
+    let hashcons hc = function
+    | Nil -> Nil
+    | Cons (x, h, l) -> Cons (hc x, h, l)
+  end
+  module Hcons = Hashcons.Make(Self)
+  let hcons = Hashcons.simple_hcons Hcons.generate Hcons.hcons M.hcons
+  (** No recursive call: the interface guarantees that all HLists from this
+      program are already hashconsed. If we get some external HList, we can
+      still reconstruct it by traversing it entirely. *)
+  let nil = Nil
+  let cons x l =
+    let h = M.hash x in
+    let hl = match l with Nil -> 0 | Cons (_, h, _) -> h in
+    let h = Hashset.Combine.combine h hl in
+    hcons (Cons (x, h, l))
+end
+
+module HList = struct
+
+  module type S = sig
+    type elt
+    type t = private Nil | Cons of elt * int * t
+    val hash : t -> int
+    val nil : t
+    val cons : elt -> t -> t
+    val tip : elt -> t
+    val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+    val map : (elt -> elt) -> t -> t
+    val smartmap : (elt -> elt) -> t -> t
+    val exists : (elt -> bool) -> t -> bool
+    val for_all : (elt -> bool) -> t -> bool
+    val for_all2 : (elt -> elt -> bool) -> t -> t -> bool
+    val mem : elt -> t -> bool
+    val remove : elt -> t -> t
+    val to_list : t -> elt list
+    val compare : (elt -> elt -> int) -> t -> t -> int
+  end
+
+  module Make (H : Hashconsed) : S with type elt = H.t =
+  struct
+  type elt = H.t
+  include HashedList(H)
+
+  let hash = function Nil -> 0 | Cons (_, h, _) -> h
+
+  let tip e = cons e nil
 
-  (* A specialized comparison function: we compare the [int] part
-     first (this property is used by the [check_sorted] function
-     below). This way, most of the time, the [dir_path] part is not
-     considered. *)
+  let rec fold f l accu = match l with
+  | Nil -> accu
+  | Cons (x, _, l) -> fold f l (f x accu)
+
+  let rec map f = function
+  | Nil -> nil
+  | Cons (x, _, l) -> cons (f x) (map f l)
+
+  let smartmap = map
+  (** Apriori hashconsing ensures that the map is equal to its argument *)
+
+  let rec exists f = function
+  | Nil -> false
+  | Cons (x, _, l) -> f x || exists f l
+
+  let rec for_all f = function
+  | Nil -> true
+  | Cons (x, _, l) -> f x && for_all f l
+
+  let rec for_all2 f l1 l2 = match l1, l2 with
+  | Nil, Nil -> true
+  | Cons (x1, _, l1), Cons (x2, _, l2) -> f x1 x2 && for_all2 f l1 l2
+  | _ -> false
+
+  let rec to_list = function
+  | Nil -> []
+  | Cons (x, _, l) -> x :: to_list l
+
+  let rec remove x = function
+  | Nil -> nil
+  | Cons (y, _, l) ->
+    if H.equal x y then l
+    else cons y (remove x l)
+
+  let rec mem x = function
+  | Nil -> false
+  | Cons (y, _, l) -> H.equal x y || mem x l
+
+  let rec compare cmp l1 l2 = match l1, l2 with
+  | Nil, Nil -> 0
+  | Cons (x1, h1, l1), Cons (x2, h2, l2) ->
+    let c = Int.compare h1 h2 in
+    if c == 0 then
+      let c = cmp x1 x2 in
+      if c == 0 then
+        compare cmp l1 l2
+      else c
+    else c
+  | Cons _, Nil -> 1
+  | Nil, Cons _ -> -1
+
+  end
+end
 
-  let compare u v = match u,v with
+module RawLevel =
+struct
+  open Names
+  type t =
+    | Prop
+    | Set
+    | Level of int * DirPath.t
+    | Var of int
+
+  (* Hash-consing *)
+
+  let equal x y =
+    x == y ||
+      match x, y with
+      | Prop, Prop -> true
+      | Set, Set -> true
+      | Level (n,d), Level (n',d') ->
+        Int.equal n n' && DirPath.equal d d'
+      | Var n, Var n' -> Int.equal n n'
+      | _ -> false
+
+  let compare u v =
+    match u, v with
+    | Prop,Prop -> 0
+    | Prop, _ -> -1
+    | _, Prop -> 1
     | Set, Set -> 0
     | Set, _ -> -1
     | _, Set -> 1
-    | Level (dp1, i1), Level (dp2, i2) ->
+    | Level (i1, dp1), Level (i2, dp2) ->
       if i1 < i2 then -1
       else if i1 > i2 then 1
-      else compare dp1 dp2
+      else DirPath.compare dp1 dp2
+    | Level _, _ -> -1
+    | _, Level _ -> 1
+    | Var n, Var m -> Int.compare n m
+      
+  let hcons = function
+    | Prop as x -> x
+    | Set as x -> x
+    | Level (n,d) as x -> 
+      let d' = Names.DirPath.hcons d in
+        if d' == d then x else Level (n,d')
+    | Var n as x -> x
+
+  open Hashset.Combine
+
+  let hash = function
+    | Prop -> combinesmall 1 0
+    | Set -> combinesmall 1 1
+    | Var n -> combinesmall 2 n
+    | Level (n, d) -> combinesmall 3 (combine n (Names.DirPath.hash d))
+
+end
+
+module Level = struct
+
+  open Names
+
+  type raw_level = RawLevel.t =
+  | Prop
+  | Set
+  | Level of int * DirPath.t
+  | Var of int
+
+  (** Embed levels with their hash value *)
+  type t = { 
+    hash : int;
+    data : RawLevel.t }
+
+  let equal x y = 
+    x == y || Int.equal x.hash y.hash && RawLevel.equal x.data y.data
+
+  let hash x = x.hash
+
+  let hcons x = 
+    let data' = RawLevel.hcons x.data in
+      if data' == x.data then x
+      else { x with data = data' }
+
+  let data x = x.data
+
+  (** Hashcons on levels + their hash *)
+
+  let make =
+    let module Self = struct
+      type _t = t
+      type t = _t
+      let equal = equal
+      let hash = hash
+    end in
+    let module WH = Weak.Make(Self) in
+    let pool = WH.create 4910 in fun x ->
+    let x = { hash = RawLevel.hash x; data = x } in
+    try WH.find pool x
+    with Not_found -> WH.add pool x; x
+
+  let set = make Set
+  let prop = make Prop
+
+  let is_small x = 
+    match data x with
+    | Level _ -> false
+    | _ -> true
 
-  let to_string = function
+  let is_prop x =
+    match data x with
+    | Prop -> true
+    | _ -> false
+
+  let is_set x =
+    match data x with
+    | Set -> true
+    | _ -> false
+
+  let compare u v =
+    if u == v then 0
+    else
+      let c = Int.compare (hash u) (hash v) in
+	if c == 0 then RawLevel.compare (data u) (data v)
+	else c
+
+  let natural_compare u v =
+    if u == v then 0
+    else RawLevel.compare (data u) (data v)
+	    
+  let to_string x = 
+    match data x with
+    | Prop -> "Prop"
     | Set -> "Set"
-    | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
+    | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n
+    | Var n -> "Var(" ^ string_of_int n ^ ")"
+
+  let pr u = str (to_string u)
+
+  let apart u v =
+    match data u, data v with
+    | Prop, Set | Set, Prop -> true
+    | _ -> false
+
+  let vars = Array.init 20 (fun i -> make (Var i))
+
+  let var n = 
+    if n < 20 then vars.(n) else make (Var n)
+
+  let var_index u =
+    match data u with
+    | Var n -> Some n | _ -> None
+
+  let make m n = make (Level (n, Names.DirPath.hcons m))
+
+end
+
+(** Level maps *)
+module LMap = struct 
+  module M = HMap.Make (Level)
+  include M
+
+  let union l r = 
+    merge (fun k l r -> 
+      match l, r with
+      | Some _, _ -> l
+      | _, _ -> r) l r
+
+  let subst_union l r = 
+    merge (fun k l r -> 
+      match l, r with
+      | Some (Some _), _ -> l
+      | Some None, None -> l
+      | _, _ -> r) l r
+
+  let diff ext orig =
+    fold (fun u v acc -> 
+      if mem u orig then acc 
+      else add u v acc)
+      ext empty
+
+  let pr f m =
+    h 0 (prlist_with_sep fnl (fun (u, v) ->
+      Level.pr u ++ f v) (bindings m))
+end
+
+module LSet = struct
+  include LMap.Set
+
+  let pr prl s =
+    str"{" ++ prlist_with_sep spc prl (elements s) ++ str"}"
+
+  let of_array l =
+    Array.fold_left (fun acc x -> add x acc) empty l
+
 end
 
-module UniverseLMap = Map.Make (UniverseLevel)
-module UniverseLSet = Set.Make (UniverseLevel)
 
-type universe_level = UniverseLevel.t
+type 'a universe_map = 'a LMap.t
+
+type universe_level = Level.t
 
-let compare_levels = UniverseLevel.compare
+type universe_level_subst_fn = universe_level -> universe_level
+
+type universe_set = LSet.t
 
 (* An algebraic universe [universe] is either a universe variable
-   [UniverseLevel.t] or a formal universe known to be greater than some
+   [Level.t] or a formal universe known to be greater than some
    universe variables and strictly greater than some (other) universe
    variables
 
@@ -72,121 +372,354 @@ let compare_levels = UniverseLevel.compare
    maximum of two algebraic universes
 *)
 
-type universe =
-  | Atom of UniverseLevel.t
-  | Max of UniverseLevel.t list * UniverseLevel.t list
-
-let make_universe_level (m,n) = UniverseLevel.Level (m,n)
-let make_universe l = Atom l
-let make_univ c = Atom (make_universe_level c)
+module Universe =
+struct
+  (* Invariants: non empty, sorted and without duplicates *)
 
-let universe_level = function
-  | Atom l -> Some l
-  | Max _ -> None
-
-let pr_uni_level u = str (UniverseLevel.to_string u)
+  module Expr = 
+  struct
+    type t = Level.t * int
+    type _t = t
+	
+    (* Hashing of expressions *)
+    module ExprHash = 
+    struct
+      type t = _t
+      type u = Level.t -> Level.t
+      let hashcons hdir (b,n as x) = 
+	let b' = hdir b in 
+	  if b' == b then x else (b',n)
+      let equal l1 l2 =
+        l1 == l2 || 
+        match l1,l2 with
+	| (b,n), (b',n') -> b == b' && n == n'
+
+      let hash (x, n) = n + Level.hash x
+
+    end
+
+    module HExpr = 
+    struct 
+
+      module H = Hashcons.Make(ExprHash)
+
+      type t = ExprHash.t
+
+      let hcons =
+	Hashcons.simple_hcons H.generate H.hcons Level.hcons
+      let hash = ExprHash.hash
+      let equal x y = x == y ||
+	(let (u,n) = x and (v,n') = y in
+	   Int.equal n n' && Level.equal u v)
+
+    end
+
+    let hcons = HExpr.hcons
+
+    let make l = hcons (l, 0)
+
+    let compare u v =
+      if u == v then 0
+      else 
+	let (x, n) = u and (x', n') = v in
+	  if Int.equal n n' then Level.compare x x'
+	  else n - n'
+
+    let prop = make Level.prop
+    let set = make Level.set
+    let type1 = hcons (Level.set, 1)
+
+    let is_prop = function
+      | (l,0) -> Level.is_prop l
+      | _ -> false
+	
+    let is_small = function
+      | (l,0) -> Level.is_small l
+      | _ -> false
+
+    let equal x y = x == y ||
+      (let (u,n) = x and (v,n') = y in
+	 Int.equal n n' && Level.equal u v)
+
+    let leq (u,n) (v,n') =
+      let cmp = Level.compare u v in
+	if Int.equal cmp 0 then n <= n'
+	else if n <= n' then 
+	  (Level.is_prop u && Level.is_small v)
+	else false
+
+    let successor (u,n) =
+      if Level.is_prop u then type1
+      else hcons (u, n + 1)
+
+    let addn k (u,n as x) = 
+      if k = 0 then x 
+      else if Level.is_prop u then
+	hcons (Level.set,n+k)
+      else hcons (u,n+k)
+	
+    let super (u,n as x) (v,n' as y) =
+      let cmp = Level.compare u v in
+	if Int.equal cmp 0 then 
+	  if n < n' then Inl true
+	  else Inl false
+	else if is_prop x then Inl true
+	else if is_prop y then Inl false
+	else Inr cmp
+
+    let to_string (v, n) =
+      if Int.equal n 0 then Level.to_string v
+      else Level.to_string v ^ "+" ^ string_of_int n
+
+    let pr x = str(to_string x)
+
+    let pr_with f (v, n) = 
+      if Int.equal n 0 then f v
+      else f v ++ str"+" ++ int n
+
+    let is_level = function
+      | (v, 0) -> true
+      | _ -> false
+
+    let level = function
+      | (v,0) -> Some v
+      | _ -> None
+	
+    let get_level (v,n) = v
+
+    let map f (v, n as x) = 
+      let v' = f v in 
+	if v' == v then x
+	else if Level.is_prop v' && n != 0 then
+	  hcons (Level.set, n)
+	else hcons (v', n)
+
+  end
+    
+  let compare_expr = Expr.compare
+
+  module Huniv = HList.Make(Expr.HExpr)
+  type t = Huniv.t
+  open Huniv
+    
+  let equal x y = x == y || 
+    (Huniv.hash x == Huniv.hash y && 
+       Huniv.for_all2 Expr.equal x y)
+
+  let hash = Huniv.hash
+
+  let compare x y =
+    if x == y then 0
+    else 
+      let hx = Huniv.hash x and hy = Huniv.hash y in
+      let c = Int.compare hx hy in 
+	if c == 0 then
+	  Huniv.compare (fun e1 e2 -> compare_expr e1 e2) x y
+	else c
+
+  let rec hcons = function
+  | Nil -> Huniv.nil
+  | Cons (x, _, l) -> Huniv.cons x (hcons l)
+
+  let make l = Huniv.tip (Expr.make l)
+  let tip x = Huniv.tip x
+
+  let pr l = match l with
+    | Cons (u, _, Nil) -> Expr.pr u
+    | _ -> 
+      str "max(" ++ hov 0
+	(prlist_with_sep pr_comma Expr.pr (to_list l)) ++
+        str ")"
 
-let pr_uni = function
-  | Atom u ->
-      pr_uni_level u
-  | Max ([],[u]) ->
-      str "(" ++ pr_uni_level u ++ str ")+1"
-  | Max (gel,gtl) ->
+  let pr_with f l = match l with
+    | Cons (u, _, Nil) -> Expr.pr_with f u
+    | _ -> 
       str "max(" ++ hov 0
-       (prlist_with_sep pr_comma pr_uni_level gel ++
-	  (if gel <> [] & gtl <> [] then pr_comma () else mt ()) ++
-	prlist_with_sep pr_comma
-	  (fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl) ++
-      str ")"
-
-(* Returns the formal universe that lies juste above the universe variable u.
-   Used to type the sort u. *)
-let super = function
-  | Atom u ->
-      Max ([],[u])
-  | Max _ ->
-      anomaly ("Cannot take the successor of a non variable universe:\n"^
-               "(maybe a bugged tactic)")
-
-(* Returns the formal universe that is greater than the universes u and v.
-   Used to type the products. *)
-let sup u v =
-  match u,v with
-    | Atom u, Atom v ->
-	if UniverseLevel.compare u v = 0 then Atom u else Max ([u;v],[])
-    | u, Max ([],[]) -> u
-    | Max ([],[]), v -> v
-    | Atom u, Max (gel,gtl) -> Max (list_add_set u gel,gtl)
-    | Max (gel,gtl), Atom v -> Max (list_add_set v gel,gtl)
-    | Max (gel,gtl), Max (gel',gtl') ->
-	let gel'' = list_union gel gel' in
-	let gtl'' = list_union gtl gtl' in
-	Max (list_subtract gel'' gtl'',gtl'')
+	(prlist_with_sep pr_comma (Expr.pr_with f) (to_list l)) ++
+        str ")"
 
-(* Comparison on this type is pointer equality *)
-type canonical_arc =
-    { univ: UniverseLevel.t;
-      lt: UniverseLevel.t list;
-      le: UniverseLevel.t list;
-      rank: int }
+  let is_level l = match l with
+    | Cons (l, _, Nil) -> Expr.is_level l
+    | _ -> false
 
-let terminal u = {univ=u; lt=[]; le=[]; rank=0}
+  let level l = match l with
+    | Cons (l, _, Nil) -> Expr.level l
+    | _ -> None
 
-(* A UniverseLevel.t is either an alias for another one, or a canonical one,
-   for which we know the universes that are above *)
+  let levels l = 
+    fold (fun x acc -> LSet.add (Expr.get_level x) acc) l LSet.empty
 
-type univ_entry =
-    Canonical of canonical_arc
-  | Equiv of UniverseLevel.t
+  let is_small u = 
+    match u with
+    | Cons (l, _, Nil) -> Expr.is_small l
+    | _ -> false
 
+  (* The lower predicative level of the hierarchy that contains (impredicative)
+     Prop and singleton inductive types *)
+  let type0m = tip Expr.prop
 
-type universes = univ_entry UniverseLMap.t
+  (* The level of sets *)
+  let type0 = tip Expr.set
 
-let enter_equiv_arc u v g =
-  UniverseLMap.add u (Equiv v) g
+  (* When typing [Prop] and [Set], there is no constraint on the level,
+     hence the definition of [type1_univ], the type of [Prop] *)    
+  let type1 = tip (Expr.successor Expr.set)
 
-let enter_arc ca g =
-  UniverseLMap.add ca.univ (Canonical ca) g
+  let is_type0m x = equal type0m x
+  let is_type0 x = equal type0 x
+
+  (* Returns the formal universe that lies juste above the universe variable u.
+     Used to type the sort u. *)
+  let super l = 
+    if is_small l then type1
+    else
+      Huniv.map (fun x -> Expr.successor x) l
+
+  let addn n l =
+    Huniv.map (fun x -> Expr.addn n x) l
+
+  let rec merge_univs l1 l2 =
+    match l1, l2 with
+    | Nil, _ -> l2
+    | _, Nil -> l1
+    | Cons (h1, _, t1), Cons (h2, _, t2) ->
+      (match Expr.super h1 h2 with
+      | Inl true (* h1 < h2 *) -> merge_univs t1 l2
+      | Inl false -> merge_univs l1 t2
+      | Inr c -> 
+        if c <= 0 (* h1 < h2 is name order *)
+	then cons h1 (merge_univs t1 l2)
+	else cons h2 (merge_univs l1 t2))
+
+  let sort u =
+    let rec aux a l = 
+      match l with
+      | Cons (b, _, l') ->
+        (match Expr.super a b with
+	| Inl false -> aux a l'
+	| Inl true -> l
+	| Inr c ->
+	  if c <= 0 then cons a l
+	  else cons b (aux a l'))
+      | Nil -> cons a l
+    in 
+      fold (fun a acc -> aux a acc) u nil
+	
+  (* Returns the formal universe that is greater than the universes u and v.
+     Used to type the products. *)
+  let sup x y = merge_univs x y
+
+  let empty = nil
+
+  let exists = Huniv.exists
+
+  let for_all = Huniv.for_all
+
+  let smartmap = Huniv.smartmap
 
-(* The lower predicative level of the hierarchy that contains (impredicative)
-   Prop and singleton inductive types *)
-let type0m_univ = Max ([],[])
+end
 
-let is_type0m_univ = function
-  | Max ([],[]) -> true
-  | _ -> false
+type universe = Universe.t
 
 (* The level of predicative Set *)
-let type0_univ = Atom UniverseLevel.Set
+let type0m_univ = Universe.type0m
+let type0_univ = Universe.type0
+let type1_univ = Universe.type1
+let is_type0m_univ = Universe.is_type0m
+let is_type0_univ = Universe.is_type0
+let is_univ_variable l = Universe.level l != None
+let is_small_univ = Universe.is_small
+let pr_uni = Universe.pr
 
-let is_type0_univ = function
-  | Atom UniverseLevel.Set -> true
-  | Max ([UniverseLevel.Set], []) -> msg_warn "Non canonical Set"; true
-  | u -> false
+let sup = Universe.sup
+let super = Universe.super
 
-let is_univ_variable = function
-  | Atom a when a<>UniverseLevel.Set -> true
-  | _ -> false
+open Universe
 
-(* When typing [Prop] and [Set], there is no constraint on the level,
-   hence the definition of [type1_univ], the type of [Prop] *)
+let universe_level = Universe.level
 
-let type1_univ = Max ([], [UniverseLevel.Set])
+type status = Unset | SetLe | SetLt
 
-let initial_universes = UniverseLMap.empty
-let is_initial_universes = UniverseLMap.is_empty
+(* Comparison on this type is pointer equality *)
+type canonical_arc =
+    { univ: Level.t;
+      lt: Level.t list;
+      le: Level.t list;
+      rank : int;
+      predicative : bool;
+      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; predicative=false; 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 *)
 
-(* Every UniverseLevel.t has a unique canonical arc representative *)
+type univ_entry =
+    Canonical of canonical_arc
+  | Equiv of Level.t
+
+type universes = univ_entry UMap.t
+
+(** 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
 
-(* repr : universes -> UniverseLevel.t -> canonical_arc *)
+(* Every Level.t has a unique canonical arc representative *)
+
+(* repr : universes -> Level.t -> canonical_arc *)
 (* canonical representative : we follow the Equiv links *)
 
 let repr g u =
   let rec repr_rec u =
     let a =
-      try UniverseLMap.find u g
-      with Not_found -> anomalylabstrm "Univ.repr"
-	  (str"Universe " ++ pr_uni_level u ++ str" undefined")
+      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_rec v
@@ -194,14 +727,12 @@ let repr g u =
   in
   repr_rec u
 
-let can g = List.map (repr g)
-
 (* [safe_repr] also search for the canonical representative, but
    if the graph doesn't contain the searched universe, we add it. *)
 
 let safe_repr g u =
   let rec safe_repr_rec u =
-    match UniverseLMap.find u g with
+    match UMap.find u g with
       | Equiv v -> safe_repr_rec v
       | Canonical arc -> arc
   in
@@ -225,8 +756,8 @@ let reprleq g arcu =
   searchrec [] arcu.le
 
 
-(* between : UniverseLevel.t -> canonical_arc -> canonical_arc list *)
-(* between u v = {w|u<=w<=v, w canonical}          *)
+(* 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 =
@@ -258,10 +789,20 @@ let between g arcu arcv =
    Otherwise, between g u v = []
  *)
 
+type constraint_type = Lt | Le | Eq
+
+type explanation = (constraint_type * universe) list
 
-type order = EQ | LT | LE | NLE
+let constraint_type_ord c1 c2 = match c1, c2 with
+| Lt, Lt -> 0
+| Lt, _ -> -1
+| Le, Lt -> 1
+| Le, Le -> 0
+| Le, Eq -> -1
+| Eq, Eq -> 0
+| Eq, _ -> 1
 
-(** [compare_neq] : is [arcv] in the transitive upward closure of [arcu] ?
+(** [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.
@@ -279,46 +820,179 @@ type order = EQ | LT | LE | NLE
   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 compare_neq strict g arcu arcv =
-  let rec cmp c lt_done le_done = function
-  | [],[] -> c
+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, 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, 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, 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, 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
+  try
+    let (to_revert, c) = cmp [] [] [] [(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 List.memq arc lt_done then
-      cmp c lt_done le_done (lt_todo,le_todo)
+    if arc_is_lt arc then
+      cmp c to_revert lt_todo le_todo
     else
-      let lt_new = can g (arc.lt@arc.le) in
-      if List.memq arcv lt_new then
-	if strict then LT else LE
-      else cmp c (arc::lt_done) le_done (lt_new@lt_todo,le_todo)
+      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
+          if arc == arcv then
+            if strict then (to_revert, FastLT) else (to_revert, FastLE)
+          else find (arc :: lt_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 find (arc :: lt_todo) lt le
+      in
+      find lt_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 LE lt_done le_done ([],le_todo) else LE
+      if strict then cmp FastLE to_revert [] le_todo else (to_revert, FastLE)
     else
-      if (List.memq arc lt_done) || (List.memq arc le_done) then
-	cmp c lt_done le_done ([],le_todo)
+      if arc_is_le arc then
+        cmp c to_revert [] le_todo
       else
-	let lt_new = can g arc.lt in
-	if List.memq arcv lt_new then
-	  if strict then LT else LE
-	else
-	  let le_new = can g arc.le in
-	  cmp c lt_done (arc::le_done) (lt_new, le_new@le_todo)
+        let rec find lt_todo lt = 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 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
+          if arc == arcv then
+            if strict then (to_revert, FastLT) else (to_revert, FastLE)
+          else find (arc :: lt_todo) lt
+        in
+        find [] arc.lt
   in
-  cmp NLE [] [] ([],[arcu])
+  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 compare g arcu arcv =
-  if arcu == arcv then EQ else compare_neq true g arcu arcv
+let get_explanation_strict g arcu arcv = get_explanation true g arcu arcv
 
-let is_leq g arcu arcv =
-  arcu == arcv || (compare_neq false g arcu arcv = LE)
+let fast_compare g arcu arcv =
+  if arcu == arcv then FastEQ else fast_compare_neq true g arcu arcv
 
-let is_lt g arcu arcv = (compare g arcu arcv = LT)
+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
@@ -329,60 +1003,84 @@ let is_lt g arcu arcv = (compare g arcu arcv = LT)
    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_geq], used in coqchk *)
+(** * Universe checks [check_eq] and [check_leq], used in coqchk *)
+
+(** First, checks on universe levels *)
 
-let compare_eq g u v =
+let check_equal g u v =
   let g, arcu = safe_repr g u in
   let _, arcv = safe_repr g v in
   arcu == arcv
 
-type check_function = universes -> universe -> universe -> bool
+let check_eq_level g u v = u == v || check_equal g u v
 
-let incl_list cmp l1 l2 =
-  List.for_all (fun x1 -> List.exists (fun x2 -> cmp x1 x2) l2) l1
+let is_set_arc u = Level.is_set u.univ
+let is_prop_arc u = Level.is_prop u.univ
+let get_prop_arc g = snd (safe_repr g Level.prop)
 
-let compare_list cmp l1 l2 =
-  incl_list cmp l1 l2 && incl_list cmp l2 l1
-
-let rec check_eq g u v =
-  match (u,v) with
-    | Atom ul, Atom vl -> compare_eq g ul vl
-    | Max(ule,ult), Max(vle,vlt) ->
-        (* TODO: remove elements of lt in le! *)
-        compare_list (compare_eq g) ule vle &&
-        compare_list (compare_eq g) ult vlt
-    | _ -> anomaly "check_eq" (* not complete! (Atom(u) = Max([u],[]) *)
-
-let compare_greater g strict u v =
+let check_smaller g strict u v =
   let g, arcu = safe_repr g u in
   let g, arcv = safe_repr g v in
   if strict then
-    is_lt g arcv arcu
+    is_lt g arcu arcv
   else
-    arcv == snd (safe_repr g UniverseLevel.Set) || is_leq g arcv arcu
-
-(*
-let compare_greater g strict u v =
-  let b = compare_greater g strict u v in
-  ppnl(str (if b then if strict then ">" else ">=" else "NOT >="));
-  b
-*)
-let check_geq g u v =
-  match u, v with
-    | Atom ul, Atom vl -> compare_greater g false ul vl
-    | Atom ul, Max(le,lt) ->
-        List.for_all (fun vl -> compare_greater g false ul vl) le &&
-        List.for_all (fun vl -> compare_greater g true ul vl) lt
-    | _ -> anomaly "check_greater"
+    is_prop_arc arcu 
+    || (is_set_arc arcu && arcv.predicative) 
+    || 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 = Huniv.exists (fun x2 -> f x1 x2) l in
+    Huniv.for_all (fun x1 -> exists x1 l2) l1
+    && Huniv.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 =
+  Huniv.exists (fun ul' -> 
+    check_smaller_expr g ul ul') l
+
+let real_check_leq g u v =
+  Huniv.for_all (fun ul -> exists_bigger g ul v) u
+    
+let check_leq g u v =
+  Universe.equal u v ||
+    Universe.is_type0m u ||
+    check_eq_univs g u v || real_check_leq g u v
 
 (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
 
-(* setlt : UniverseLevel.t -> UniverseLevel.t -> unit *)
+(** To speed up tests of Set </<= i *)
+let set_predicative g arcv = 
+  enter_arc {arcv with predicative = true} g
+
+(* 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'
+  let g = 
+    if is_set_arc arcu then set_predicative g arcv
+    else g
+  in
+    enter_arc arcu' g, arcu'
 
 (* checks that non-redundant *)
 let setlt_if (g,arcu) v =
@@ -390,13 +1088,17 @@ let setlt_if (g,arcu) v =
   if is_lt g arcu arcv then g, arcu
   else setlt g arcu arcv
 
-(* setleq : UniverseLevel.t -> UniverseLevel.t -> unit *)
+(* 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'
-
+  let g = 
+    if is_set_arc arcu' then
+      set_predicative g arcv
+    else g
+  in
+    enter_arc arcu' g, arcu'
 
 (* checks that non-redundant *)
 let setleq_if (g,arcu) v =
@@ -404,32 +1106,32 @@ let setleq_if (g,arcu) v =
   if is_leq g arcu arcv then g, arcu
   else setleq g arcu arcv
 
-(* merge : UniverseLevel.t -> UniverseLevel.t -> unit *)
+(* 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 arc.rank >= max_rank
+      if Level.is_small arc.univ || arc.rank >= max_rank
       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 "Univ.between"
+      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
+          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')
+    (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
@@ -437,13 +1139,13 @@ let merge g arcu arcv =
   let g_arcu = List.fold_left setleq_if g_arcu w' in
   fst g_arcu
 
-(* merge_disc : UniverseLevel.t -> UniverseLevel.t -> unit *)
+(* 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 arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
   let arcu, g = 
-    if arc1.rank <> arc2.rank then 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
@@ -457,107 +1159,241 @@ let merge_disc g arc1 arc2 =
 (* Universe inconsistency: error raised when trying to enforce a relation
    that would create a cycle in the graph of universes. *)
 
-type constraint_type = Lt | Le | Eq
+type univ_inconsistency = constraint_type * universe * universe * explanation option
 
-exception UniverseInconsistency of constraint_type * universe * universe
+exception UniverseInconsistency of univ_inconsistency
 
-let error_inconsistency o u v = raise (UniverseInconsistency (o,Atom u,Atom v))
+let error_inconsistency o u v (p:explanation option) =
+  raise (UniverseInconsistency (o,make u,make v,p))
+
+(* enforc_univ_eq : Level.t -> Level.t -> unit *)
+(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
 
-(* enforce_univ_leq : UniverseLevel.t -> UniverseLevel.t -> unit *)
+let enforce_univ_eq u v g =
+  let g,arcu = safe_repr g u in
+  let g,arcv = safe_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 g,arcu = safe_repr g u in
   let g,arcv = safe_repr g v in
   if is_leq g arcu arcv then g
-  else match compare g arcv arcu with
-    | LT -> error_inconsistency Le u v
-    | LE -> merge g arcv arcu
-    | NLE -> fst (setleq g arcu arcv)
-    | EQ -> anomaly "Univ.compare"
-
-(* enforc_univ_eq : UniverseLevel.t -> UniverseLevel.t -> unit *)
-(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
-let enforce_univ_eq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
-  match compare g arcu arcv with
-    | EQ -> g
-    | LT -> error_inconsistency Eq u v
-    | LE -> merge g arcu arcv
-    | NLE ->
-	(match compare g arcv arcu with
-           | LT -> error_inconsistency Eq u v
-           | LE -> merge g arcv arcu
-           | NLE -> merge_disc g arcu arcv
-           | EQ -> anomaly "Univ.compare")
+  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 g,arcu = safe_repr g u in
   let g,arcv = safe_repr g v in
-  match compare g arcu arcv with
-    | LT -> g
-    | LE -> fst (setlt g arcu arcv)
-    | EQ -> error_inconsistency Lt u v
-    | NLE ->
-      if is_leq g arcv arcu then error_inconsistency Lt u v
-      else fst (setlt g arcu arcv)
-
-(* Constraints and sets of consrtaints. *)
-
-type univ_constraint = UniverseLevel.t * constraint_type * UniverseLevel.t
+    match fast_compare g arcu arcv with
+    | FastLT -> g
+    | FastLE -> fst (setlt g arcu arcv)
+    | FastEQ -> error_inconsistency Lt u v (Some [(Eq,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 empty_universes = UMap.empty
+
+(* Prop = Set is forbidden here. *)
+let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty
+
+let is_initial_universes g = UMap.equal (==) g initial_universes
+
+let add_universe vlev g = 
+  let v = terminal vlev in
+  let proparc = get_prop_arc g in
+    enter_arc {proparc with le=vlev::proparc.le}
+      (enter_arc v g)
+      
+(* Constraints and sets of constraints. *)    
+
+type univ_constraint = Level.t * constraint_type * Level.t
 
 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 pr_constraint_type op = 
+  let op_str = match op with
+    | Lt -> " < "
+    | Le -> " <= "
+    | Eq -> " = "
+  in str op_str
+
+module UConstraintOrd =
+struct
+  type t = univ_constraint
+  let compare (u,c,v) (u',c',v') =
+    let i = constraint_type_ord c c' in
+    if not (Int.equal i 0) then i
+    else
+      let i' = Level.compare u u' in
+      if not (Int.equal i' 0) then i'
+      else Level.compare v v'
+end
 
-module Constraint = Set.Make(
-  struct
-    type t = univ_constraint
-    let compare (u,c,v) (u',c',v') =
-      let i = Pervasives.compare c c' in
-      if i <> 0 then i
-      else
-	let i' = UniverseLevel.compare u u' in
-	if i' <> 0 then i'
-	else UniverseLevel.compare v v'
-  end)
+module Constraint = 
+struct 
+  module S = Set.Make(UConstraintOrd)
+  include S
 
-type constraints = Constraint.t
+  let pr prl c =
+    fold (fun (u1,op,u2) pp_std ->
+      pp_std ++ prl u1 ++ pr_constraint_type op ++
+	prl u2 ++ fnl () )  c (str "")
+
+end
 
 let empty_constraint = Constraint.empty
-let is_empty_constraint = Constraint.is_empty
+let union_constraint = Constraint.union
+let eq_constraint = Constraint.equal
+let merge_constraints c g =
+  Constraint.fold enforce_constraint c g
 
-let union_constraints = Constraint.union
+type constraints = Constraint.t
 
-type constraint_function =
-    universe -> universe -> constraints -> constraints
+module Hconstraint =
+  Hashcons.Make(
+    struct
+      type t = univ_constraint
+      type u = universe_level -> universe_level
+      let hashcons hul (l1,k,l2) = (hul l1, k, hul l2)
+      let equal (l1,k,l2) (l1',k',l2') =
+	l1 == l1' && k == k' && l2 == l2'
+      let hash = Hashtbl.hash
+    end)
 
-let constraint_add_leq v u c =
-  if v = UniverseLevel.Set then c else Constraint.add (v,Le,u) c
+module Hconstraints =
+  Hashcons.Make(
+    struct
+      type t = constraints
+      type u = univ_constraint -> univ_constraint
+      let hashcons huc s =
+	Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
+      let equal s s' =
+	List.for_all2eq (==)
+	  (Constraint.elements s)
+	  (Constraint.elements s')
+      let hash = Hashtbl.hash
+    end)
+
+let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate Hconstraint.hcons Level.hcons
+let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate Hconstraints.hcons hcons_constraint
+
+
+(** A value with universe constraints. *)
+type 'a constrained = 'a * constraints
+
+let constraints_of (_, cst) = cst
 
-let enforce_geq u v c =
-  match u, v with
-  | Atom u, Atom v -> constraint_add_leq v u c
-  | Atom u, Max (gel,gtl) ->
-      let d = List.fold_right (fun v -> constraint_add_leq v u) gel c in
-      List.fold_right (fun v -> Constraint.add (v,Lt,u)) gtl d
-  | _ -> anomaly "A universe bound can only be a variable"
+(** Constraint functions. *)
+
+type 'a constraint_function = 'a -> 'a -> constraints -> constraints
+
+let enforce_eq_level u v c =
+  (* We discard trivial constraints like u=u *)
+  if Level.equal u v then c 
+  else if Level.apart u v then
+    error_inconsistency Eq u v None
+  else Constraint.add (u,Eq,v) c
 
 let enforce_eq u v c =
-  match (u,v) with
-    | Atom u, Atom v -> Constraint.add (u,Eq,v) c
-    | _ -> anomaly "A universe comparison can only happen between variables"
+  match Universe.level u, Universe.level v with
+    | Some u, Some v -> enforce_eq_level u v c
+    | _ -> anomaly (Pp.str "A universe comparison can only happen between variables")
 
-let merge_constraints c g =
-  Constraint.fold enforce_constraint c g
+let check_univ_eq u v = Universe.equal u v
+
+let enforce_eq u v c =
+  if check_univ_eq u v then c
+  else enforce_eq u v c
+
+let constraint_add_leq v u c =
+  (* We just discard trivial constraints like u<=u *)
+  if Expr.equal v u then c
+  else 
+    match v, u with
+    | (x,n), (y,m) -> 
+    let j = m - n in
+      if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
+	Constraint.add (x,Lt,y) c
+      else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
+	if Level.equal x y then (* u+(k+1) <= u *)
+	  raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, None))
+	else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints")
+      else if j = 0 then
+	Constraint.add (x,Le,y) c
+      else (* j >= 1 *) (* m = n + k, u <= v+k *)
+	if Level.equal x y then c (* u <= u+k, trivial *)
+	else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
+	else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints")
+	  
+let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
+
+let check_univ_leq u v = 
+  Universe.for_all (fun u -> check_univ_leq_one u v) u
+
+let enforce_leq u v c =
+  let open Universe.Huniv in
+  match v with
+  | Cons (v, _, Nil) ->
+    fold (fun u -> constraint_add_leq u v) u c
+  | _ -> anomaly (Pp.str"A universe bound can only be a variable")
+
+let enforce_leq u v c =
+  if check_univ_leq u v then c
+  else enforce_leq u v c
+
+let enforce_leq_level u v c =
+  if Level.equal u v then c else Constraint.add (u,Le,v) c
+
+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
+
+let enforce_univ_constraint (u,d,v) =
+  match d with
+  | Eq -> enforce_eq u v
+  | Le -> enforce_leq u v
+  | Lt -> enforce_leq (super u) v
 
 (* Normalization *)
 
 let lookup_level u g =
-  try Some (UniverseLMap.find u g) with Not_found -> None
+  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
@@ -571,20 +1407,20 @@ let normalize_universes g =
     | Some x -> x, cache
     | None -> match Lazy.force arc with
     | None ->
-      u, UniverseLMap.add u u cache
+      u, UMap.add u u cache
     | Some (Canonical {univ=v; lt=_; le=_}) ->
-      v, UniverseLMap.add u v cache
+      v, UMap.add u v cache
     | Some (Equiv v) ->
       let v, cache = visit v (lazy (lookup_level v g)) cache in
-      v, UniverseLMap.add u v cache
+      v, UMap.add u v cache
   in
-  let cache = UniverseLMap.fold
+  let cache = UMap.fold
     (fun u arc cache -> snd (visit u (Lazy.lazy_from_val (Some arc)) cache))
-    g UniverseLMap.empty
+    g UMap.empty
   in
-  let repr x = UniverseLMap.find x cache in
+  let repr x = UMap.find x cache in
   let lrepr us = List.fold_left
-    (fun e x -> UniverseLSet.add (repr x) e) UniverseLSet.empty us
+    (fun e x -> LSet.add (repr x) e) LSet.empty us
   in
   let canonicalize u = function
     | Equiv _ -> Equiv (repr u)
@@ -592,355 +1428,674 @@ let normalize_universes g =
       assert (u == v);
       (* avoid duplicates and self-loops *)
       let lt = lrepr lt and le = lrepr le in
-      let le = UniverseLSet.filter
-        (fun x -> x != u && not (UniverseLSet.mem x lt)) le
+      let le = LSet.filter
+        (fun x -> x != u && not (LSet.mem x lt)) le
       in
-      UniverseLSet.iter (fun x -> assert (x != u)) lt;
+      LSet.iter (fun x -> assert (x != u)) lt;
       Canonical {
         univ = v;
-        lt = UniverseLSet.elements lt;
-        le = UniverseLSet.elements le;
-	rank = rank
+        lt = LSet.elements lt;
+        le = LSet.elements le;
+	rank = rank;
+	predicative = false;
+	status = Unset;
       }
   in
-  UniverseLMap.mapi canonicalize g
-
-(** [check_sorted g sorted]: [g] being a universe graph, [sorted]
-    being a map to levels, checks that all constraints in [g] are
-    satisfied in [sorted]. *)
-let check_sorted g sorted =
-  let get u = try UniverseLMap.find u sorted with
-    | Not_found -> assert false
-  in UniverseLMap.iter (fun u arc -> let lu = get u in match arc with
-    | Equiv v -> assert (lu = get v)
-    | Canonical {univ=u'; lt=lt; le=le} ->
-      assert (u == u');
-      List.iter (fun v -> assert (lu <= get v)) le;
-      List.iter (fun v -> assert (lu < get v)) lt) g
-
-(**
-  Bellman-Ford algorithm with a few customizations:
-    - [weight(eq|le) = 0], [weight(lt) = -1]
-    - a [le] edge is initially added from [bottom] to all other
-      vertices, and [bottom] is used as the source vertex
-*)
-let bellman_ford bottom g =
-  assert (lookup_level bottom g = None);
-  let ( << ) a b = match a, b with
-    | _, None -> true
-    | None, _ -> false
-    | Some x, Some y -> x < y
-  and ( ++ ) a y = match a with
-    | None -> None
-    | Some x -> Some (x-y)
-  and push u x m = match x with
-    | None -> m
-    | Some y -> UniverseLMap.add u y m
+  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
-  let relax u v uv distances =
-    let x = lookup_level u distances ++ uv in
-    if x << lookup_level v distances then push v x distances
-    else distances
+  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
-  let init = UniverseLMap.add bottom 0 UniverseLMap.empty in
-  let vertices = UniverseLMap.fold (fun u arc res ->
-    let res = UniverseLSet.add u res in
-    match arc with
-      | Equiv e -> UniverseLSet.add e res
-      | Canonical {univ=univ; lt=lt; le=le} ->
-        assert (u == univ);
-        let add res v = UniverseLSet.add v res in
-        let res = List.fold_left add res le in
-        let res = List.fold_left add res lt in
-        res) g UniverseLSet.empty
+  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
-  let g =
-    let node = Canonical {
-      univ = bottom;
-      lt = [];
-      le = UniverseLSet.elements vertices;
-      rank = 0
-    } in UniverseLMap.add bottom node g
+  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
-  let rec iter count accu =
-    if count <= 0 then
-      accu
-    else
-      let accu = UniverseLMap.fold (fun u arc res -> match arc with
-        | Equiv e -> relax e u 0 (relax u e 0 res)
-        | Canonical {univ=univ; lt=lt; le=le} ->
-          assert (u == univ);
-          let res = List.fold_left (fun res v -> relax u v 0 res) res le in
-          let res = List.fold_left (fun res v -> relax u v 1 res) res lt in
-          res) g accu
-      in iter (count-1) accu
+  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 distances = iter (UniverseLSet.cardinal vertices) init in
-  let () = UniverseLMap.iter (fun u arc ->
-    let lu = lookup_level u distances in match arc with
-      | Equiv v ->
-        let lv = lookup_level v distances in
-        assert (not (lu << lv) && not (lv << lu))
-      | Canonical {univ=univ; lt=lt; le=le} ->
-        assert (u == univ);
-        List.iter (fun v -> assert (not (lu ++ 0 << lookup_level v distances))) le;
-        List.iter (fun v -> assert (not (lu ++ 1 << lookup_level v distances))) lt) g
-  in distances
+  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 mp = Names.make_dirpath [Names.id_of_string "Type"] in
-  let rec make_level accu g i =
-    let type0 = UniverseLevel.Level (mp, i) in
-    let distances = bellman_ford type0 g in
-    let accu, continue = UniverseLMap.fold (fun u x (accu, continue) ->
-      let continue = continue || x < 0 in
-      let accu =
-        if x = 0 && u != type0 then UniverseLMap.add u i accu
-        else accu
-      in accu, continue) distances (accu, false)
-    in
-    let filter x = not (UniverseLMap.mem x accu) in
-    let push g u =
-      if UniverseLMap.mem u g then g else UniverseLMap.add u (Equiv u) g
-    in
-    let g = UniverseLMap.fold (fun u arc res -> match arc with
-      | Equiv v as x ->
-        begin match filter u, filter v with
-          | true, true -> UniverseLMap.add u x res
-          | true, false -> push res u
-          | false, true -> push res v
-          | false, false -> res
-        end
-      | Canonical {univ=v; lt=lt; le=le; rank=r} ->
-        assert (u == v);
-        if filter u then
-          let lt = List.filter filter lt in
-          let le = List.filter filter le in
-          UniverseLMap.add u (Canonical {univ=u; lt=lt; le=le; rank=r}) res
-        else
-          let res = List.fold_left (fun g u -> if filter u then push g u else g) res lt in
-          let res = List.fold_left (fun g u -> if filter u then push g u else g) res le in
-          res) g UniverseLMap.empty
-    in
-    if continue then make_level accu g (i+1) else i, accu
+  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 0 < i then
+      let pred = types.(i - 1) in
+      let arc = {univ = u; lt = [pred]; le = []; rank = 0; predicative = false; status = Unset; } in
+      UMap.add u (Canonical arc) accu
+    else accu
   in
-  let max, levels = make_level UniverseLMap.empty orig 0 in
-  (* defensively check that the result makes sense *)
-  check_sorted orig levels;
-  let types = Array.init (max+1) (fun x -> UniverseLevel.Level (mp, x)) in
-  let g = UniverseLMap.map (fun x -> Equiv types.(x)) levels in
-  let g =
-    let rec aux i g =
-      if i < max then
-        let u = types.(i) in
-        let g = UniverseLMap.add u (Canonical {
-          univ = u;
-          le = [];
-          lt = [types.(i+1)];
-	  rank = 1
-        }) g in aux (i+1) g
-      else g
-    in aux 0 g
-  in g
+  Array.fold_left_i fold sorted types
+
+(* Miscellaneous functions to remove or test local univ assumed to
+   occur in a universe *)
+
+let univ_level_mem u v = Huniv.mem (Expr.make u) v
+
+let univ_level_rem u v min = 
+  match Universe.level v with
+  | Some u' -> if Level.equal u u' then min else v
+  | None -> Huniv.remove (Universe.Expr.make u) v
 
+(* Is u mentionned in v (or equals to v) ? *)
+
+
+(**********************************************************************)
+(** Universe polymorphism                                             *)
 (**********************************************************************)
-(* Tools for sort-polymorphic inductive types                         *)
 
-(* Temporary inductive type levels *)
+(** A universe level substitution, note that no algebraic universes are
+    involved *)
 
-let fresh_level =
-  let n = ref 0 in fun () -> incr n; UniverseLevel.Level (Names.make_dirpath [],!n)
+type universe_level_subst = universe_level universe_map
 
-let fresh_local_univ () = Atom (fresh_level ())
+(** A full substitution might involve algebraic universes *)
+type universe_subst = universe universe_map
 
-(* Miscellaneous functions to remove or test local univ assumed to
-   occur only in the le constraints *)
+let level_subst_of f = 
+  fun l -> 
+    try let u = f l in 
+	  match Universe.level u with
+	  | None -> l
+	  | Some l -> l
+    with Not_found -> l
+     
+module Instance : sig 
+    type t = Level.t array
+
+    val empty : t
+    val is_empty : t -> bool
+      
+    val of_array : Level.t array -> t
+    val to_array : t -> Level.t array
 
-let make_max = function
-  | ([u],[]) -> Atom u
-  | (le,lt) -> Max (le,lt)
+    val append : t -> t -> t
+    val equal : t -> t -> bool
+    val length : t -> int
 
-let remove_large_constraint u = function
-  | Atom u' as x -> if u = u' then Max ([],[]) else x
-  | Max (le,lt) -> make_max (list_remove u le,lt)
+    val hcons : t -> t
+    val hash : t -> int
 
-let is_direct_constraint u = function
-  | Atom u' -> u = u'
-  | Max (le,lt) -> List.mem u le
+    val share : t -> t * int
 
-(*
-   Solve a system of universe constraint of the form
+    val subst_fn : universe_level_subst_fn -> t -> t
+    
+    val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+    val levels : t -> LSet.t
+    val check_eq : t check_function 
+end = 
+struct
+  type t = Level.t array
 
-   u_s11, ..., u_s1p1, w1 <= u1
-   ...
-   u_sn1, ..., u_snpn, wn <= un
+  let empty : t = [||]
 
-where
+  module HInstancestruct =
+  struct
+    type _t = t
+    type t = _t
+    type u = Level.t -> Level.t
+
+    let hashcons huniv a = 
+      let len = Array.length a in
+	if Int.equal len 0 then empty
+	else begin
+	  for i = 0 to len - 1 do
+	    let x = Array.unsafe_get a i in
+	    let x' = huniv x in
+	      if x == x' then ()
+	      else Array.unsafe_set a i x'
+	  done;
+	  a
+	end
+
+    let equal t1 t2 =
+      t1 == t2 ||
+	(Int.equal (Array.length t1) (Array.length t2) &&
+	   let rec aux i =
+	     (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
+	   in aux 0)
+	
+    let hash a = 
+      let accu = ref 0 in
+	for i = 0 to Array.length a - 1 do
+	  let l = Array.unsafe_get a i in
+	  let h = Level.hash l in
+	    accu := Hashset.Combine.combine !accu h;
+	done;
+	(* [h] must be positive. *)
+	let h = !accu land 0x3FFFFFFF in
+	  h
+  end
+
+  module HInstance = Hashcons.Make(HInstancestruct)
+
+  let hcons = Hashcons.simple_hcons HInstance.generate HInstance.hcons Level.hcons
+    
+  let hash = HInstancestruct.hash
+    
+  let share a = (hcons a, hash a)
+	      
+  let empty = hcons [||]
+
+  let is_empty x = Int.equal (Array.length x) 0
+
+  let append x y =
+    if Array.length x = 0 then y
+    else if Array.length y = 0 then x 
+    else Array.append x y
+
+  let of_array a = a
+
+  let to_array a = a
+
+  let length a = Array.length a
+
+  let subst_fn fn t = 
+    let t' = CArray.smartmap fn t in
+      if t' == t then t else t'
+
+  let levels x = LSet.of_array x
+
+  let pr =
+    prvect_with_sep spc
+
+  let equal t u = 
+    t == u ||
+      (Array.is_empty t && Array.is_empty u) ||
+      (CArray.for_all2 Level.equal t u 
+	 (* Necessary as universe instances might come from different modules and 
+	    unmarshalling doesn't preserve sharing *))
+
+  let check_eq g t1 t2 =
+    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)
 
-  - the ui (1 <= i <= n) are universe variables,
-  - the sjk select subsets of the ui for each equations,
-  - the wi are arbitrary complex universes that do not mention the ui.
+end
+
+let enforce_eq_instances x y = 
+  let ax = Instance.to_array x and ay = Instance.to_array y in
+    if Array.length ax != Array.length ay then
+      anomaly (Pp.(++) (Pp.str "Invalid argument: enforce_eq_instances called with")
+		 (Pp.str " instances of different lengths"));
+    CArray.fold_right2 enforce_eq_level ax ay
+
+type universe_instance = Instance.t
+
+type 'a puniverses = 'a * Instance.t
+let out_punivs (x, y) = x
+let in_punivs x = (x, Instance.empty)
+let eq_puniverses f (x, u) (y, u') =
+  f x y && Instance.equal u u'
+
+(** A context of universe levels with universe constraints,
+    representiong local universe variables and constraints *)
+
+module UContext =
+struct
+  type t = Instance.t constrained
+
+  let make x = x
+
+  (** Universe contexts (variables as a list) *)
+  let empty = (Instance.empty, Constraint.empty)
+  let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
+
+  let pr prl (univs, cst as ctx) =
+    if is_empty ctx then mt() else
+      Instance.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst)
+
+  let hcons (univs, cst) =
+    (Instance.hcons univs, hcons_constraints cst)
+
+  let instance (univs, cst) = univs
+  let constraints (univs, cst) = cst
+
+  let union (univs, cst) (univs', cst') =
+    Instance.append univs univs', Constraint.union cst cst'
+      
+  let dest x = x
+end
+
+type universe_context = UContext.t
+let hcons_universe_context = UContext.hcons
+
+(** A set of universes with universe constraints.
+    We linearize the set to a list after typechecking. 
+    Beware, representation could change.
 *)
 
-let is_direct_sort_constraint s v = match s with
-  | Some u -> is_direct_constraint u v
-  | None -> false
-
-let solve_constraints_system levels level_bounds =
-  let levels =
-    Array.map (Option.map (function Atom u -> u | _ -> anomaly "expects Atom"))
-      levels in
-  let v = Array.copy level_bounds in
-  let nind = Array.length v in
-  for i=0 to nind-1 do
-    for j=0 to nind-1 do
-      if i<>j & is_direct_sort_constraint levels.(j) v.(i) then
-	v.(i) <- sup v.(i) level_bounds.(j)
-    done;
-    for j=0 to nind-1 do
-      match levels.(j) with
-      | Some u -> v.(i) <- remove_large_constraint u v.(i)
-      | None -> ()
-    done
-  done;
-  v
-
-let subst_large_constraint u u' v =
-  match u with
-  | Atom u ->
-      if is_direct_constraint u v then sup u' (remove_large_constraint u v)
-      else v
-  | _ ->
-      anomaly "expect a universe level"
-
-let subst_large_constraints =
-  List.fold_right (fun (u,u') -> subst_large_constraint u u')
-
-let no_upper_constraints u cst =
-  match u with
-  | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst
-  | Max _ -> anomaly "no_upper_constraints"
+module ContextSet =
+struct
+  type t = universe_set constrained
 
-(* Is u mentionned in v (or equals to v) ? *)
+  let empty = (LSet.empty, Constraint.empty)
+  let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst
+
+  let of_set s = (s, Constraint.empty)
+  let singleton l = of_set (LSet.singleton l)
+  let of_instance i = of_set (Instance.levels i)
 
-let univ_depends u v =
-  match u, v with
-    | Atom u, Atom v -> u = v
-    | Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl
-    | _ -> anomaly "univ_depends given a non-atomic 1st arg"
+  let union (univs, cst as x) (univs', cst' as y) =
+    if x == y then x
+    else LSet.union univs univs', Constraint.union cst cst'
 
-(* Pretty-printing *)
+  let append (univs, cst) (univs', cst') =
+    let univs = LSet.fold LSet.add univs univs' in
+    let cst = Constraint.fold Constraint.add cst cst' in
+    (univs, cst)
 
-let pr_arc = function
+  let diff (univs, cst) (univs', cst') =
+    LSet.diff univs univs', Constraint.diff cst cst'
+
+  let add_universe u (univs, cst) =
+    LSet.add u univs, cst
+
+  let add_constraints cst' (univs, cst) =
+    univs, Constraint.union cst cst'
+
+  let add_instance inst (univs, cst) =
+    let v = Instance.to_array inst in
+    let fold accu u = LSet.add u accu in
+    let univs = Array.fold_left fold univs v in
+    (univs, cst)
+
+  let sort_levels a = 
+    Array.sort Level.natural_compare a; a
+
+  let to_context (ctx, cst) =
+    (Instance.of_array (sort_levels (Array.of_list (LSet.elements ctx))), cst)
+
+  let of_context (ctx, cst) =
+    (Instance.levels ctx, cst)
+
+  let pr prl (univs, cst as ctx) =
+    if is_empty ctx then mt() else
+      LSet.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst)
+
+  let constraints (univs, cst) = cst
+  let levels (univs, cst) = univs
+
+end
+
+type universe_context_set = ContextSet.t
+
+(** A value in a universe context (resp. context set). *)
+type 'a in_universe_context = 'a * universe_context
+type 'a in_universe_context_set = 'a * universe_context_set
+
+(** Substitutions. *)
+
+let empty_subst = LMap.empty
+let is_empty_subst = LMap.is_empty
+
+let empty_level_subst = LMap.empty
+let is_empty_level_subst = LMap.is_empty
+
+(** Substitution functions *)
+
+(** With level to level substitutions. *)
+let subst_univs_level_level subst l =
+  try LMap.find l subst
+  with Not_found -> l
+
+let subst_univs_level_universe subst u =
+  let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in
+  let u' = Universe.smartmap f u in
+    if u == u' then u
+    else Universe.sort u'
+
+let subst_univs_level_instance subst i =
+  let i' = Instance.subst_fn (subst_univs_level_level subst) i in
+    if i == i' then i
+    else i'
+	
+let subst_univs_level_constraint subst (u,d,v) =
+  let u' = subst_univs_level_level subst u 
+  and v' = subst_univs_level_level subst v in
+    if d != Lt && Level.equal u' v' then None
+    else Some (u',d,v')
+
+let subst_univs_level_constraints subst csts =
+  Constraint.fold 
+    (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
+    csts Constraint.empty 
+
+(** With level to universe substitutions. *)
+type universe_subst_fn = universe_level -> universe
+
+let make_subst subst = fun l -> LMap.find l subst
+
+let subst_univs_expr_opt fn (l,n) =
+  Universe.addn n (fn l)
+
+let subst_univs_universe fn ul =
+  let subst, nosubst = 
+    Universe.Huniv.fold (fun u (subst,nosubst) -> 
+      try let a' = subst_univs_expr_opt fn u in
+	    (a' :: subst, nosubst)
+      with Not_found -> (subst, u :: nosubst))
+      ul ([], [])
+  in 
+    if CList.is_empty subst then ul
+    else 
+      let substs = 
+	List.fold_left Universe.merge_univs Universe.empty subst
+      in
+	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u))
+	  substs nosubst
+
+let subst_univs_level fn l = 
+  try Some (fn l)
+  with Not_found -> None
+
+let subst_univs_constraint fn (u,d,v as c) cstrs =
+  let u' = subst_univs_level fn u in
+  let v' = subst_univs_level fn v in
+  match u', v' with
+  | None, None -> Constraint.add c cstrs
+  | Some u, None -> enforce_univ_constraint (u,d,make v) cstrs
+  | None, Some v -> enforce_univ_constraint (make u,d,v) cstrs
+  | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs
+
+let subst_univs_constraints subst csts =
+  Constraint.fold 
+    (fun c cstrs -> subst_univs_constraint subst c cstrs)
+    csts Constraint.empty 
+
+let subst_instance_level s l =
+  match l.Level.data with
+  | Level.Var n -> s.(n) 
+  | _ -> l
+
+let subst_instance_instance s i = 
+  Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+  let u' = Universe.smartmap f u in
+    if u == u' then u
+    else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+  let u' = subst_instance_level s u in
+  let v' = subst_instance_level s v in
+    if u' == u && v' == v then c
+    else (u',d,v')
+
+let subst_instance_constraints s csts =
+  Constraint.fold 
+    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+    csts Constraint.empty 
+
+(** Substitute instance inst for ctx in csts *)
+let instantiate_univ_context (ctx, csts) = 
+  (ctx, subst_instance_constraints ctx csts)
+
+let instantiate_univ_constraints u (_, csts) = 
+  subst_instance_constraints u csts
+
+let make_instance_subst i = 
+  let arr = Instance.to_array i in
+    Array.fold_left_i (fun i acc l ->
+      LMap.add l (Level.var i) acc)
+      LMap.empty arr
+
+let make_inverse_instance_subst i = 
+  let arr = Instance.to_array i in
+    Array.fold_left_i (fun i acc l ->
+      LMap.add (Level.var i) l acc)
+      LMap.empty arr
+
+let abstract_universes poly ctx =
+  let instance = UContext.instance ctx in
+    if poly then
+      let subst = make_instance_subst instance in
+      let cstrs = subst_univs_level_constraints subst 
+	(UContext.constraints ctx)
+      in
+      let ctx = UContext.make (instance, cstrs) in
+	subst, ctx
+    else empty_level_subst, ctx
+
+(** Pretty-printing *)
+
+let pr_arc prl = function
   | _, Canonical {univ=u; lt=[]; le=[]} ->
       mt ()
   | _, Canonical {univ=u; lt=lt; le=le} ->
-      pr_uni_level u ++ str " " ++
+      let opt_sep = match lt, le with
+      | [], _ | _, [] -> mt ()
+      | _ -> spc ()
+      in
+      prl u ++ str " " ++
       v 0
-        (prlist_with_sep pr_spc (fun v -> str "< " ++ pr_uni_level v) lt ++
-	 (if lt <> [] & le <> [] then spc () else mt()) ++
-         prlist_with_sep pr_spc (fun v -> str "<= " ++ pr_uni_level v) le) ++
+        (pr_sequence (fun v -> str "< " ++ prl v) lt ++
+	 opt_sep ++
+         pr_sequence (fun v -> str "<= " ++ prl v) le) ++
       fnl ()
   | u, Equiv v ->
-      pr_uni_level u  ++ str " = " ++ pr_uni_level v ++ fnl ()
+      prl u  ++ str " = " ++ prl v ++ fnl ()
 
-let pr_universes g =
-  let graph = UniverseLMap.fold (fun u a l -> (u,a)::l) g [] in
-  prlist pr_arc graph
+let pr_universes prl g =
+  let graph = UMap.fold (fun u a l -> (u,a)::l) g [] in
+  prlist (pr_arc prl) graph
 
-let pr_constraints c =
-  Constraint.fold (fun (u1,op,u2) pp_std ->
-		     let op_str = match op with
-		       | Lt -> " < "
-		       | Le -> " <= "
-		       | Eq -> " = "
-		     in pp_std ++  pr_uni_level u1 ++ str op_str ++
-			  pr_uni_level u2 ++ fnl () )  c (str "")
+let pr_constraints prl = Constraint.pr prl
+
+let pr_universe_context = UContext.pr
+
+let pr_universe_context_set = ContextSet.pr
+
+let pr_universe_subst = 
+  LMap.pr (fun u -> str" := " ++ Universe.pr u ++ spc ())
+
+let pr_universe_level_subst = 
+  LMap.pr (fun u -> str" := " ++ Level.pr u ++ spc ())
 
 (* 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 = UniverseLevel.to_string u in
-	List.iter (fun v -> output Lt u_str (UniverseLevel.to_string v)) lt;
-	List.iter (fun v -> output Le u_str (UniverseLevel.to_string v)) 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 (UniverseLevel.to_string u) (UniverseLevel.to_string v)
+      output Eq (Level.to_string u) (Level.to_string v)
   in
-    UniverseLMap.iter dump_arc g
-
-(* Hash-consing *)
-
-module Hunivlevel =
-  Hashcons.Make(
-    struct
-      type t = universe_level
-      type u = Names.dir_path -> Names.dir_path
-      let hash_sub hdir = function
-	| UniverseLevel.Set -> UniverseLevel.Set
-	| UniverseLevel.Level (d,n) -> UniverseLevel.Level (hdir d,n)
-      let equal l1 l2 = match l1,l2 with
-	| UniverseLevel.Set, UniverseLevel.Set -> true
-	| UniverseLevel.Level (d,n), UniverseLevel.Level (d',n') ->
-	  n == n' && d == d'
-	| _ -> false
-      let hash = Hashtbl.hash
-    end)
+  UMap.iter dump_arc g
 
-module Huniv =
+module Huniverse_set = 
   Hashcons.Make(
     struct
-      type t = universe
+      type t = universe_set
       type u = universe_level -> universe_level
-      let hash_sub hdir = function
-	| Atom u -> Atom (hdir u)
-	| Max (gel,gtl) -> Max (List.map hdir gel, List.map hdir gtl)
-      let equal u v =
-	match u, v with
-	  | Atom u, Atom v -> u == v
-	  | Max (gel,gtl), Max (gel',gtl') ->
-	      (list_for_all2eq (==) gel gel') &&
-              (list_for_all2eq (==) gtl gtl')
-	  | _ -> false
+      let hashcons huc s =
+	LSet.fold (fun x -> LSet.add (huc x)) s LSet.empty
+      let equal s s' =
+	LSet.equal s s'
       let hash = Hashtbl.hash
     end)
 
-let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.f Names.hcons_dirpath
-let hcons_univ = Hashcons.simple_hcons Huniv.f hcons_univlevel
+let hcons_universe_set = 
+  Hashcons.simple_hcons Huniverse_set.generate Huniverse_set.hcons Level.hcons
 
-module Hconstraint =
-  Hashcons.Make(
-    struct
-      type t = univ_constraint
-      type u = universe_level -> universe_level
-      let hash_sub hul (l1,k,l2) = (hul l1, k, hul l2)
-      let equal (l1,k,l2) (l1',k',l2') =
-	l1 == l1' && k = k' && l2 == l2'
-      let hash = Hashtbl.hash
-    end)
+let hcons_universe_context_set (v, c) = 
+  (hcons_universe_set v, hcons_constraints c)
 
-module Hconstraints =
-  Hashcons.Make(
-    struct
-      type t = constraints
-      type u = univ_constraint -> univ_constraint
-      let hash_sub huc s =
-	Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
-      let equal s s' =
-	list_for_all2eq (==)
-	  (Constraint.elements s)
-	  (Constraint.elements s')
-      let hash = Hashtbl.hash
-    end)
+let hcons_univ x = Universe.hcons x
 
-let hcons_constraint = Hashcons.simple_hcons Hconstraint.f hcons_univlevel
-let hcons_constraints = Hashcons.simple_hcons Hconstraints.f hcons_constraint
+let explain_universe_inconsistency prl (o,u,v,p) =
+  let pr_uni = Universe.pr_with prl in
+  let pr_rel = function
+    | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" 
+  in
+  let reason = match p with
+    | None | Some [] -> mt()
+    | Some p ->
+      str " because" ++ spc() ++ pr_uni v ++
+	prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v)
+	p ++
+	(if Universe.equal (snd (List.last p)) u then mt() else
+	    (spc() ++ str "= " ++ pr_uni u)) 
+  in
+    str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
+      pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")"
+
+let compare_levels = Level.compare
+let eq_levels = Level.equal
+let equal_universes = Universe.equal
+
+
+let subst_instance_constraints = 
+  if Flags.profile then 
+    let key = Profile.declare_profile "subst_instance_constraints" in
+      Profile.profile2 key subst_instance_constraints
+  else subst_instance_constraints
+
+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