From 4c8808bcdadc7c6f6645d4f01bc564480be20c7b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 10 Jun 2014 14:40:24 +0200
Subject: More cleanup/reorganizing of univ.ml to separate constraint/universe
 handling from the instance/contexts and substitution code.

---
 kernel/univ.ml  | 1154 ++++++++++++++++++++++++++++---------------------------
 kernel/univ.mli |  248 ++++++------
 2 files changed, 705 insertions(+), 697 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 18064d2469..a330fed327 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -400,21 +400,20 @@ module Level = struct
 
 end
 
-let pr_universe_level_list l = 
-  prlist_with_sep spc Level.pr l
-
 module LSet = struct
   module M = Set.Make (Level)
   include M
 
   let pr s = 
-    str"{" ++ pr_universe_level_list (elements s) ++ str"}"
+    str"{" ++ prlist_with_sep spc Level.pr (elements s) ++ str"}"
 
   let of_array l =
     Array.fold_left (fun acc x -> add x acc) empty l
 
 end
 
+
+(** Level maps *)
 module LMap = struct 
   module M = Map.Make (Level)
   include M
@@ -458,12 +457,13 @@ module LMap = struct
     with Not_found -> None
 end
 
+type 'a universe_map = 'a LMap.t
+
 type universe_level = Level.t
 
 type universe_level_subst_fn = universe_level -> universe_level
 
 type universe_set = LSet.t
-type 'a universe_map = 'a LMap.t
 
 (* An algebraic universe [universe] is either a universe variable
    [Level.t] or a formal universe known to be greater than some
@@ -1270,6 +1270,9 @@ let enforce_constraint cst g =
     | (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 pr_constraint_type op = 
   let op_str = match op with
@@ -1340,379 +1343,508 @@ let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate hcons_constr
 (** A value with universe constraints. *)
 type 'a constrained = 'a * constraints
 
-(** A universe level substitution, note that no algebraic universes are
-    involved *)
-type universe_level_subst = universe_level universe_map
+let constraints_of (_, cst) = cst
 
-(** A full substitution might involve algebraic universes *)
-type universe_subst = universe universe_map
+(** Constraint functions. *)
 
-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
+type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
-    val empty : t
-    val is_empty : t -> bool
-      
-    val of_array : Level.t array -> t
-    val to_array : t -> Level.t array
+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 []
+  else Constraint.add (u,Eq,v) c
 
-    val of_list : Level.t list -> t
-    val to_list : t -> Level.t list
+let enforce_eq u v c =
+  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")
 
-    val append : t -> t -> t
-    val equal : t -> t -> bool
-    val hcons : t -> t
-    val hash : t -> int
+let check_univ_eq u v = Universe.equal u v
 
-    val share : t -> t * int
+let enforce_eq u v c =
+  if check_univ_eq u v then c
+  else enforce_eq u v c
 
-    val eqeq : t -> t -> bool
-    val subst_fn : universe_level_subst_fn -> t -> t
-    val subst : universe_level_subst -> t -> t
-    
-    val pr : t -> Pp.std_ppcmds
-    val levels : t -> LSet.t
-    val check_eq : t check_function 
-end = 
-struct
-  type t = Level.t array
+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, []))
+	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 empty : t = [||]
+let check_univ_leq u v = 
+  Universe.for_all (fun u -> check_univ_leq_one u v) u
 
-  module HInstancestruct =
-  struct
-    type _t = t
-    type t = _t
-    type u = Level.t -> Level.t
+let enforce_leq u v c =
+  match Huniv.node v with
+  | Universe.Huniv.Cons (v, n) when Universe.is_empty n -> 
+    Universe.Huniv.fold (fun u -> constraint_add_leq u v) u c
+  | _ -> anomaly (Pp.str"A universe bound can only be a variable")
 
-    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 enforce_leq u v c =
+  if check_univ_leq u v then c
+  else enforce_leq u v c
 
-    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
+let enforce_leq_level u v c =
+  if Level.equal u v then c else Constraint.add (u,Le,v) c
 
-  module HInstance = Hashcons.Make(HInstancestruct)
+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 hcons = Hashcons.simple_hcons HInstance.generate Level.hcons
-    
-  let hash = HInstancestruct.hash
-    
-  let share a = (a, hash a)
-	      
-  let empty = hcons [||]
+let check_constraints c g =
+  Constraint.for_all (check_constraint g) c
 
-  let is_empty x = Int.equal (Array.length x) 0
+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
 
-  let append x y =
-    if Array.length x = 0 then y
-    else if Array.length y = 0 then x 
-    else hcons (Array.append x y)
+(* Normalization *)
 
-  let of_array a = hcons a
+let lookup_level u g =
+  try Some (UMap.find u g) with Not_found -> None
 
-  let to_array a = a
+(** [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;
+	predicative = false;
+      }
+  in
+  UMap.mapi canonicalize g
 
-  let of_list a = of_array (Array.of_list a)
-  let to_list = Array.to_list
+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 eqeq = HInstancestruct.equal
+let constraints_of_universes g =
+  constraints_of_universes (normalize_universes g)
 
-  let subst_fn fn t = 
-    let t' = CArray.smartmap fn t in
-      if t' == t then t else hcons t'
+(** 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. *)
 
-  let subst s t =
-    let t' = 
-      CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t
-    in if t' == t then t else hcons t'
+(** Adjacency graph *)
+type graph = constraint_type LMap.t LMap.t
 
-  let levels x = LSet.of_array x
+exception Connected
 
-  let pr =
-    prvect_with_sep spc Level.pr
+(** 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 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)
-
-end
-
-type universe_instance = Instance.t
-
-type 'a puniverses = 'a * Instance.t
-let out_punivs (x, y) = x
-let in_punivs x = (x, Instance.empty)
-
-(** A context of universe levels with universe constraints,
-    representiong local universe variables and constraints *)
+let add_edge x y v (g : graph) =
+  try
+    let neighbours = LMap.find x g in
+    let () = assert (not (LMap.mem y neighbours)) 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
 
-module UContext =
-struct
-  type t = Instance.t constrained
+(** 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
 
-  let make x = x
+(** 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
+    let accu = List.fold_left fold_lt accu lt in
+    let accu = List.fold_left fold_le accu le in
+    accu
+  in
+  UMap.fold fold g (LMap.empty, LMap.empty)
 
-  (** 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
+(** 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 pr (univs, cst as ctx) =
-    if is_empty ctx then mt() else
-      Instance.pr univs ++ str " |= " ++ v 1 (Constraint.pr cst)
+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
 
-  let hcons (univs, cst) =
-    (Instance.hcons univs, hcons_constraints cst)
+(** Compute the longest path from any vertex. *)
+let constraint_cost = function
+| Eq | Le -> 0
+| Lt -> 1
 
-  let instance (univs, cst) = univs
-  let constraints (univs, cst) = cst
+(** 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)
 
-  let union (univs, cst) (univs', cst') =
-    Instance.append univs univs', Constraint.union cst cst'
-end
+(** [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 0 < i then
+      let pred = types.(i - 1) in
+      let arc = {univ = u; lt = [pred]; le = []; rank = 0; predicative = false} in
+      UMap.add u (Canonical arc) accu
+    else accu
+  in
+  Array.fold_left_i fold sorted types
 
-type universe_context = UContext.t
-let hcons_universe_context = UContext.hcons
+(**********************************************************************)
+(* Tools for sort-polymorphic inductive types                         *)
 
-(** A set of universes with universe constraints.
-    We linearize the set to a list after typechecking. 
-    Beware, representation could change.
-*)
+(* Miscellaneous functions to remove or test local univ assumed to
+   occur only in the le constraints *)
 
-module ContextSet =
-struct
-  type t = universe_set constrained
+let remove_large_constraint 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
 
-  let empty = (LSet.empty, Constraint.empty)
-  let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst
+(* [is_direct_constraint u v] if level [u] is a member of universe [v] *)
+let is_direct_constraint u v =
+  match Universe.level v with
+  | Some u' -> Level.equal u u'
+  | None -> 
+    let expr = Universe.Expr.make u in
+      Universe.exists (Universe.Expr.equal expr) v
 
-  let of_set s = (s, Constraint.empty)
-  let singleton l = of_set (LSet.singleton l)
-  let of_instance i = of_set (Instance.levels i)
+(*
+   Solve a system of universe constraint of the form
 
-  let union (univs, cst) (univs', cst') =
-    LSet.union univs univs', Constraint.union cst cst'
+   u_s11, ..., u_s1p1, w1 <= u1
+   ...
+   u_sn1, ..., u_snpn, wn <= un
 
-  let diff (univs, cst) (univs', cst') =
-    LSet.diff univs univs', Constraint.diff cst cst'
+where
 
-  let add_constraints (univs, cst) cst' =
-    univs, Constraint.union cst cst'
+  - 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.
+*)
 
-  let add_universes univs ctx =
-    union (of_instance univs) ctx
+let is_direct_sort_constraint s v = match s with
+  | Some u -> is_direct_constraint u v
+  | None -> false
 
-  let to_context (ctx, cst) =
-    (Instance.of_array (Array.of_list (LSet.elements ctx)), cst)
+let solve_constraints_system levels level_bounds level_min =
+  let levels =
+    Array.map (Option.map (fun u -> match level u with Some u -> u | _ -> anomaly (Pp.str"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 not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
+	(v.(i) <- Universe.sup v.(i) level_bounds.(j);
+	 level_min.(i) <- Universe.sup level_min.(i) level_min.(j))
+    done;
+    for j=0 to nind-1 do
+      match levels.(j) with
+      | Some u -> v.(i) <- remove_large_constraint u v.(i) level_min.(i)
+      | None -> ()
+    done
+  done;
+  v
 
-  let of_context (ctx, cst) =
-    (Instance.levels ctx, cst)
+let subst_large_constraint u u' v =
+  match level u with
+  | Some u ->
+      (* if is_direct_constraint u v then  *)
+	Universe.sup u' (remove_large_constraint u v type0m_univ)
+      (* else v *)
+  | _ ->
+      anomaly (Pp.str "expect a universe level")
 
-  let pr (univs, cst as ctx) =
-    if is_empty ctx then mt() else
-      LSet.pr univs ++ str " |= " ++ v 1 (Constraint.pr cst)
+let subst_large_constraints =
+  List.fold_right (fun (u,u') -> subst_large_constraint u u')
 
-  let constraints (univs, cst) = cst
-  let levels (univs, cst) = univs
+let no_upper_constraints u cst =
+  match level u with
+  | Some u ->
+    let test (u1, _, _) =
+      not (Int.equal (Level.compare u1 u) 0) in
+    Constraint.for_all test cst
+  | _ -> anomaly (Pp.str "no_upper_constraints")
 
-end
+(* Is u mentionned in v (or equals to v) ? *)
 
-type universe_context_set = ContextSet.t
+let univ_depends u v =
+  match atom u with
+    | Some u -> Huniv.mem u v
+    | _ -> anomaly (Pp.str"univ_depends given a non-atomic 1st arg")
 
-(** 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
+(**********************************************************************)
+(** Universe polymorphism                                             *)
+(**********************************************************************)
 
-(** Pretty-printing *)
-let pr_constraints = Constraint.pr
+(** A universe level substitution, note that no algebraic universes are
+    involved *)
 
-let pr_universe_context = UContext.pr
+type universe_level_subst = universe_level universe_map
 
-let pr_universe_context_set = ContextSet.pr
+(** A full substitution might involve algebraic universes *)
+type universe_subst = universe universe_map
 
-let pr_universe_subst = 
-  LMap.pr (fun u -> str" := " ++ Universe.pr u ++ spc ())
+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
 
-let pr_universe_level_subst = 
-  LMap.pr (fun u -> str" := " ++ Level.pr u ++ spc ())
+    val empty : t
+    val is_empty : t -> bool
+      
+    val of_array : Level.t array -> t
+    val to_array : t -> Level.t array
 
-let constraints_of (_, cst) = cst
+    val of_list : Level.t list -> t
+    val to_list : t -> Level.t list
 
-(** Substitutions. *)
+    val append : t -> t -> t
+    val equal : t -> t -> bool
+    val hcons : t -> t
+    val hash : t -> int
 
-let make_universe_subst inst (ctx, csts) = 
-  try Array.fold_left2 (fun acc c i -> LMap.add c i acc)
-        LMap.empty (Instance.to_array ctx) (Instance.to_array inst)
-  with Invalid_argument _ -> 
-    anomaly (Pp.str "Mismatched instance and context when building universe substitution")
+    val share : t -> t * int
 
-let empty_subst = LMap.empty
-let is_empty_subst = LMap.is_empty
+    val eqeq : t -> t -> bool
+    val subst_fn : universe_level_subst_fn -> t -> t
+    val subst : universe_level_subst -> t -> t
+    
+    val pr : t -> Pp.std_ppcmds
+    val levels : t -> LSet.t
+    val check_eq : t check_function 
+end = 
+struct
+  type t = Level.t array
 
-let empty_level_subst = LMap.empty
-let is_empty_level_subst = LMap.is_empty
+  let empty : t = [||]
 
-(** Substitution functions *)
+  module HInstancestruct =
+  struct
+    type _t = t
+    type t = _t
+    type u = Level.t -> Level.t
 
-(** With level to level substitutions. *)
-let subst_univs_level_level subst l =
-  try LMap.find l subst
-  with Not_found -> l
+    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 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 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 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_level fn l = 
-  try fn l
-  with Not_found -> make l
-
-let subst_univs_expr_opt fn (l,n) =
-  try Some (Universe.addn n (fn l))
-  with Not_found -> None
-
-let subst_univs_universe fn ul =
-  let subst, nosubst = 
-    Universe.Huniv.fold (fun u (subst,nosubst) -> 
-      match subst_univs_expr_opt fn u with
-      | Some a' -> (a' :: subst, nosubst)
-      | None -> (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 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
 
-let subst_univs_constraint fn (u,d,v) =
-  let u' = subst_univs_level fn u and v' = subst_univs_level fn v in
-    if d != Lt && Universe.equal u' v' then None
-    else Some (u',d,v')
+  module HInstance = Hashcons.Make(HInstancestruct)
 
-(** Constraint functions. *)
+  let hcons = Hashcons.simple_hcons HInstance.generate Level.hcons
+    
+  let hash = HInstancestruct.hash
+    
+  let share a = (a, hash a)
+	      
+  let empty = hcons [||]
 
-type 'a constraint_function = 'a -> 'a -> constraints -> constraints
+  let is_empty x = Int.equal (Array.length x) 0
 
-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, []))
-	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_eq u v = Universe.equal u v
+  let append x y =
+    if Array.length x = 0 then y
+    else if Array.length y = 0 then x 
+    else hcons (Array.append x y)
 
-let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
+  let of_array a = hcons a
 
-let check_univ_leq u v = 
-  Universe.for_all (fun u -> check_univ_leq_one u v) u
+  let to_array a = a
 
-let enforce_leq u v c =
-  match Huniv.node v with
-  | Universe.Huniv.Cons (v, n) when Universe.is_empty n -> 
-    Universe.Huniv.fold (fun u -> constraint_add_leq u v) u c
-  | _ -> anomaly (Pp.str"A universe bound can only be a variable")
+  let of_list a = of_array (Array.of_list a)
+  let to_list = Array.to_list
 
-let enforce_leq u v c =
-  if check_univ_leq u v then c
-  else enforce_leq u v c
+    
+  let eqeq = HInstancestruct.equal
 
-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 []
-  else Constraint.add (u,Eq,v) c
+  let subst_fn fn t = 
+    let t' = CArray.smartmap fn t in
+      if t' == t then t else hcons t'
 
-let enforce_eq u v c =
-  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 subst s t =
+    let t' = 
+      CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t
+    in if t' == t then t else hcons t'
 
-let enforce_eq u v c =
-  if check_univ_eq u v then c
-  else enforce_eq u v c
+  let levels x = LSet.of_array x
 
-let enforce_leq_level u v c =
-  if Level.equal u v then c else Constraint.add (u,Le,v) c
+  let pr =
+    prvect_with_sep spc Level.pr
+
+  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)
+
+end
 
 let enforce_eq_instances x y = 
   let ax = Instance.to_array x and ay = Instance.to_array y in
@@ -1720,314 +1852,174 @@ let enforce_eq_instances x y =
       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
-      
-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
+type universe_instance = Instance.t
 
-let check_constraints c g =
-  Constraint.for_all (check_constraint g) c
+type 'a puniverses = 'a * Instance.t
+let out_punivs (x, y) = x
+let in_punivs x = (x, Instance.empty)
 
-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
+(** A context of universe levels with universe constraints,
+    representiong local universe variables and constraints *)
 
-let subst_univs_constraints subst csts =
-  Constraint.fold 
-    (fun c -> Option.fold_right enforce_univ_constraint (subst_univs_constraint subst c))
-    csts Constraint.empty 
+module UContext =
+struct
+  type t = Instance.t constrained
 
-(** Substitute instance inst for ctx in csts *)
-let instantiate_univ_context subst (_, csts) = 
-  subst_univs_level_constraints subst csts
+  let make x = x
 
-(* Normalization *)
+  (** 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 lookup_level u g =
-  try Some (UMap.find u g) with Not_found -> None
+  let pr (univs, cst as ctx) =
+    if is_empty ctx then mt() else
+      Instance.pr univs ++ str " |= " ++ v 1 (Constraint.pr cst)
 
-(** [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;
-	predicative = false;
-      }
-  in
-  UMap.mapi canonicalize g
+  let hcons (univs, cst) =
+    (Instance.hcons univs, hcons_constraints cst)
 
-(** 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. *)
+  let instance (univs, cst) = univs
+  let constraints (univs, cst) = cst
 
-(** Adjacency graph *)
-type graph = constraint_type LMap.t LMap.t
+  let union (univs, cst) (univs', cst') =
+    Instance.append univs univs', Constraint.union cst cst'
+end
 
-exception Connected
+type universe_context = UContext.t
+let hcons_universe_context = UContext.hcons
 
-(** 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
+(** A set of universes with universe constraints.
+    We linearize the set to a list after typechecking. 
+    Beware, representation could change.
+*)
 
-let add_edge x y v (g : graph) =
-  try
-    let neighbours = LMap.find x g in
-    let () = assert (not (LMap.mem y neighbours)) 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
+module ContextSet =
+struct
+  type t = universe_set constrained
 
-(** 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
+  let empty = (LSet.empty, Constraint.empty)
+  let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst
 
-(** 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
-    let accu = List.fold_left fold_lt accu lt in
-    let accu = List.fold_left fold_le accu le in
-    accu
-  in
-  UMap.fold fold g (LMap.empty, LMap.empty)
+  let of_set s = (s, Constraint.empty)
+  let singleton l = of_set (LSet.singleton l)
+  let of_instance i = of_set (Instance.levels i)
 
-(** 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 union (univs, cst) (univs', cst') =
+    LSet.union univs univs', Constraint.union cst cst'
 
-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
+  let diff (univs, cst) (univs', cst') =
+    LSet.diff univs univs', Constraint.diff cst cst'
 
-(** Compute the longest path from any vertex. *)
-let constraint_cost = function
-| Eq | Le -> 0
-| Lt -> 1
+  let add_constraints (univs, cst) cst' =
+    univs, Constraint.union cst cst'
 
-(** 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)
+  let add_universes univs ctx =
+    union (of_instance univs) ctx
 
-(** [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 0 < i then
-      let pred = types.(i - 1) in
-      let arc = {univ = u; lt = [pred]; le = []; rank = 0; predicative = false} in
-      UMap.add u (Canonical arc) accu
-    else accu
-  in
-  Array.fold_left_i fold sorted types
+  let to_context (ctx, cst) =
+    (Instance.of_array (Array.of_list (LSet.elements ctx)), cst)
 
-(**********************************************************************)
-(* Tools for sort-polymorphic inductive types                         *)
+  let of_context (ctx, cst) =
+    (Instance.levels ctx, cst)
 
-(* Miscellaneous functions to remove or test local univ assumed to
-   occur only in the le constraints *)
+  let pr (univs, cst as ctx) =
+    if is_empty ctx then mt() else
+      LSet.pr univs ++ str " |= " ++ v 1 (Constraint.pr cst)
 
-let remove_large_constraint 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
+  let constraints (univs, cst) = cst
+  let levels (univs, cst) = univs
 
-(* [is_direct_constraint u v] if level [u] is a member of universe [v] *)
-let is_direct_constraint u v =
-  match Universe.level v with
-  | Some u' -> Level.equal u u'
-  | None -> 
-    let expr = Universe.Expr.make u in
-      Universe.exists (Universe.Expr.equal expr) v
+end
 
-(*
-   Solve a system of universe constraint of the form
+type universe_context_set = ContextSet.t
 
-   u_s11, ..., u_s1p1, w1 <= u1
-   ...
-   u_sn1, ..., u_snpn, wn <= un
+(** 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
 
-where
+(** Substitutions. *)
 
-  - 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.
-*)
+let make_universe_subst inst (ctx, csts) = 
+  try Array.fold_left2 (fun acc c i -> LMap.add c i acc)
+        LMap.empty (Instance.to_array ctx) (Instance.to_array inst)
+  with Invalid_argument _ -> 
+    anomaly (Pp.str "Mismatched instance and context when building universe substitution")
 
-let is_direct_sort_constraint s v = match s with
-  | Some u -> is_direct_constraint u v
-  | None -> false
+let empty_subst = LMap.empty
+let is_empty_subst = LMap.is_empty
 
-let solve_constraints_system levels level_bounds level_min =
-  let levels =
-    Array.map (Option.map (fun u -> match level u with Some u -> u | _ -> anomaly (Pp.str"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 not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
-	(v.(i) <- Universe.sup v.(i) level_bounds.(j);
-	 level_min.(i) <- Universe.sup level_min.(i) level_min.(j))
-    done;
-    for j=0 to nind-1 do
-      match levels.(j) with
-      | Some u -> v.(i) <- remove_large_constraint u v.(i) level_min.(i)
-      | None -> ()
-    done
-  done;
-  v
+let empty_level_subst = LMap.empty
+let is_empty_level_subst = LMap.is_empty
 
-let subst_large_constraint u u' v =
-  match level u with
-  | Some u ->
-      (* if is_direct_constraint u v then  *)
-	Universe.sup u' (remove_large_constraint u v type0m_univ)
-      (* else v *)
-  | _ ->
-      anomaly (Pp.str "expect a universe level")
+(** Substitution functions *)
 
-let subst_large_constraints =
-  List.fold_right (fun (u,u') -> subst_large_constraint u u')
+(** With level to level substitutions. *)
+let subst_univs_level_level subst l =
+  try LMap.find l subst
+  with Not_found -> l
 
-let no_upper_constraints u cst =
-  match level u with
-  | Some u ->
-    let test (u1, _, _) =
-      not (Int.equal (Level.compare u1 u) 0) in
-    Constraint.for_all test cst
-  | _ -> anomaly (Pp.str "no_upper_constraints")
+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_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')
 
-(* Is u mentionned in v (or equals to 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 
 
-let univ_depends u v =
-  match atom u with
-    | Some u -> Huniv.mem u v
-    | _ -> anomaly (Pp.str"univ_depends given a non-atomic 1st arg")
+(** Substitute instance inst for ctx in csts *)
+let instantiate_univ_context subst (_, csts) = 
+  subst_univs_level_constraints subst csts
 
-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
+(** With level to universe substitutions. *)
+type universe_subst_fn = universe_level -> universe
 
-let constraints_of_universes g =
-  constraints_of_universes (normalize_universes g)
+let make_subst subst = fun l -> LMap.find l subst
+
+let subst_univs_level fn l = 
+  try fn l
+  with Not_found -> make l
+
+let subst_univs_expr_opt fn (l,n) =
+  try Some (Universe.addn n (fn l))
+  with Not_found -> None
+
+let subst_univs_universe fn ul =
+  let subst, nosubst = 
+    Universe.Huniv.fold (fun u (subst,nosubst) -> 
+      match subst_univs_expr_opt fn u with
+      | Some a' -> (a' :: subst, nosubst)
+      | None -> (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_constraint fn (u,d,v) =
+  let u' = subst_univs_level fn u and v' = subst_univs_level fn v in
+    if d != Lt && Universe.equal u' v' then None
+    else Some (u',d,v')
+
+let subst_univs_constraints subst csts =
+  Constraint.fold 
+    (fun c -> Option.fold_right enforce_univ_constraint (subst_univs_constraint subst c))
+    csts Constraint.empty 
 
-(* Pretty-printing *)
+(** Pretty-printing *)
 
 let pr_arc = function
   | _, Canonical {univ=u; lt=[]; le=[]} ->
@@ -2050,6 +2042,18 @@ let pr_universes g =
   let graph = UMap.fold (fun u a l -> (u,a)::l) g [] in
   prlist pr_arc graph
 
+let pr_constraints = Constraint.pr
+
+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 =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 3fc2c7dc26..e43b19d305 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -52,45 +52,6 @@ end
 
 type universe_set = LSet.t
 
-(** Polymorphic maps from universe levels to 'a *)
-module LMap : 
-sig
-  include Map.S with type key = universe_level
-
-  val union : 'a t -> 'a t -> 'a t
-  (** [union x y] favors the bindings in the first map. *)
-
-  val diff : 'a t -> 'a t -> 'a t
-  (** [diff x y] removes bindings from x that appear in y (whatever the value). *)
-
-  val subst_union : 'a option t -> 'a option t -> 'a option t
-  (** [subst_union x y] favors the bindings of the first map that are [Some],
-      otherwise takes y's bindings. *)
-
-  val elements : 'a t -> (universe_level * 'a) list
-  (** As an association list *)
-
-  val of_list : (universe_level * 'a) list -> 'a t
-  (** From an association list *)
-
-  val of_set : universe_set -> 'a -> 'a t
-  (** Associates the same value to all levels in the set *)
-
-  val mem : universe_level -> 'a t -> bool
-  (** Is there a binding for the level? *)
-
-  val find_opt : universe_level -> 'a t -> 'a option
-  (** Find the value associated to the level, if any *)
-
-  val universes : 'a t -> universe_set
-  (** The domain of the map *)
-
-  val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
-  (** Pretty-printing *)
-end
-
-type 'a universe_map = 'a LMap.t
-
 module Universe :
 sig
   type t
@@ -187,6 +148,126 @@ val sort_universes : universes -> universes
 (** Adds a universe to the graph, ensuring it is >= Prop. *)
 val add_universe : universe_level -> universes -> universes
 
+(** {6 Constraints. } *)
+
+type constraint_type = Lt | Le | Eq
+type univ_constraint = universe_level * constraint_type * universe_level
+
+module Constraint : sig
+ include Set.S with type elt = univ_constraint
+end
+
+type constraints = Constraint.t
+
+val empty_constraint : constraints
+val union_constraint : constraints -> constraints -> constraints
+val eq_constraint : constraints -> constraints -> bool
+
+(** A value with universe constraints. *)
+type 'a constrained = 'a * constraints
+
+(** Constrained *)
+val constraints_of : 'a constrained -> constraints
+
+(** Enforcing constraints. *)
+
+type 'a constraint_function = 'a -> 'a -> constraints -> constraints
+
+val enforce_eq : universe constraint_function
+val enforce_leq : universe constraint_function
+val enforce_eq_level : universe_level constraint_function
+val enforce_leq_level : universe_level constraint_function
+
+(** {6 ... } *)
+(** Merge of constraints in a universes graph.
+  The function [merge_constraints] merges a set of constraints in a given
+  universes graph. It raises the exception [UniverseInconsistency] if the
+  constraints are not satisfiable. *)
+
+(** Type explanation is used to decorate error messages to provide
+  useful explanation why a given constraint is rejected. It is composed
+  of a path of universes and relation kinds [(r1,u1);..;(rn,un)] means
+   .. <(r1) u1 <(r2) ... <(rn) un (where <(ri) is the relation symbol
+  denoted by ri, currently only < and <=). The lowest end of the chain
+  is supposed known (see UniverseInconsistency exn). The upper end may
+  differ from the second univ of UniverseInconsistency because all
+  universes in the path are canonical. Note that each step does not
+  necessarily correspond to an actual constraint, but reflect how the
+  system stores the graph and may result from combination of several
+  constraints...
+*)
+type explanation = (constraint_type * universe) list
+type univ_inconsistency = constraint_type * universe * universe * explanation
+
+exception UniverseInconsistency of univ_inconsistency
+
+val enforce_constraint : univ_constraint -> universes -> universes
+val merge_constraints : constraints -> universes -> universes
+
+val constraints_of_universes : universes -> constraints
+
+val check_constraint  : universes -> univ_constraint -> bool
+val check_constraints : constraints -> universes -> bool
+
+(** {6 Support for old-style sort-polymorphism } *)
+
+val solve_constraints_system : universe option array -> universe array -> universe array ->
+  universe array
+
+val remove_large_constraint : universe_level -> universe -> universe -> universe
+
+val subst_large_constraint : universe -> universe -> universe -> universe
+
+val subst_large_constraints :
+  (universe * universe) list -> universe -> universe
+
+val no_upper_constraints : universe -> constraints -> bool
+
+(** Is u mentionned in v (or equals to v) ? *)
+
+val univ_depends : universe -> universe -> bool
+
+(** {6 Support for universe polymorphism } *)
+
+(** Polymorphic maps from universe levels to 'a *)
+module LMap : 
+sig
+  include Map.S with type key = universe_level
+
+  val union : 'a t -> 'a t -> 'a t
+  (** [union x y] favors the bindings in the first map. *)
+
+  val diff : 'a t -> 'a t -> 'a t
+  (** [diff x y] removes bindings from x that appear in y (whatever the value). *)
+
+  val subst_union : 'a option t -> 'a option t -> 'a option t
+  (** [subst_union x y] favors the bindings of the first map that are [Some],
+      otherwise takes y's bindings. *)
+
+  val elements : 'a t -> (universe_level * 'a) list
+  (** As an association list *)
+
+  val of_list : (universe_level * 'a) list -> 'a t
+  (** From an association list *)
+
+  val of_set : universe_set -> 'a -> 'a t
+  (** Associates the same value to all levels in the set *)
+
+  val mem : universe_level -> 'a t -> bool
+  (** Is there a binding for the level? *)
+
+  val find_opt : universe_level -> 'a t -> 'a option
+  (** Find the value associated to the level, if any *)
+
+  val universes : 'a t -> universe_set
+  (** The domain of the map *)
+
+  val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+  (** Pretty-printing *)
+end
+
+type 'a universe_map = 'a LMap.t
+
 (** {6 Substitution} *)
 
 type universe_subst_fn = universe_level -> universe
@@ -248,42 +329,24 @@ end
 
 type universe_instance = Instance.t
 
+val enforce_eq_instances : universe_instance constraint_function
+
 type 'a puniverses = 'a * universe_instance
 val out_punivs : 'a puniverses -> 'a
 val in_punivs : 'a -> 'a puniverses
 
-(** {6 Constraints. } *)
-
-type constraint_type = Lt | Le | Eq
-type univ_constraint = universe_level * constraint_type * universe_level
-
-module Constraint : sig
- include Set.S with type elt = univ_constraint
-end
-
-type constraints = Constraint.t
-
-val empty_constraint : constraints
-val union_constraint : constraints -> constraints -> constraints
-val eq_constraint : constraints -> constraints -> bool
-
-(** A value with universe constraints. *)
-type 'a constrained = 'a * constraints
-
-(** Constrained *)
-val constraints_of : 'a constrained -> constraints
-
-(** A list of universes with universe constraints,
-    representiong local universe variables and constraints *)
+(** A vector of universe levels with universe constraints,
+    representiong local universe variables and associated constraints *)
 
 module UContext :
 sig 
   type t
 
   val make : Instance.t constrained -> t
+
   val empty : t
   val is_empty : t -> bool
-
+    
   val instance : t -> Instance.t
   val constraints : t -> constraints
 
@@ -353,65 +416,6 @@ val subst_univs_level : universe_subst_fn -> universe_level -> universe
 val subst_univs_universe : universe_subst_fn -> universe -> universe
 val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
 
-(** Enforcing constraints. *)
-
-type 'a constraint_function = 'a -> 'a -> constraints -> constraints
-
-val enforce_eq : universe constraint_function
-val enforce_leq : universe constraint_function
-val enforce_eq_level : universe_level constraint_function
-val enforce_leq_level : universe_level constraint_function
-val enforce_eq_instances : universe_instance constraint_function
-
-(** {6 ... } *)
-(** Merge of constraints in a universes graph.
-  The function [merge_constraints] merges a set of constraints in a given
-  universes graph. It raises the exception [UniverseInconsistency] if the
-  constraints are not satisfiable. *)
-
-(** Type explanation is used to decorate error messages to provide
-  useful explanation why a given constraint is rejected. It is composed
-  of a path of universes and relation kinds [(r1,u1);..;(rn,un)] means
-   .. <(r1) u1 <(r2) ... <(rn) un (where <(ri) is the relation symbol
-  denoted by ri, currently only < and <=). The lowest end of the chain
-  is supposed known (see UniverseInconsistency exn). The upper end may
-  differ from the second univ of UniverseInconsistency because all
-  universes in the path are canonical. Note that each step does not
-  necessarily correspond to an actual constraint, but reflect how the
-  system stores the graph and may result from combination of several
-  constraints...
-*)
-type explanation = (constraint_type * universe) list
-type univ_inconsistency = constraint_type * universe * universe * explanation
-
-exception UniverseInconsistency of univ_inconsistency
-
-val enforce_constraint : univ_constraint -> universes -> universes
-val merge_constraints : constraints -> universes -> universes
-
-val constraints_of_universes : universes -> constraints
-
-val check_constraint  : universes -> univ_constraint -> bool
-val check_constraints : constraints -> universes -> bool
-
-(** {6 Support for sort-polymorphism } *)
-
-val solve_constraints_system : universe option array -> universe array -> universe array ->
-  universe array
-
-val remove_large_constraint : universe_level -> universe -> universe -> universe
-
-val subst_large_constraint : universe -> universe -> universe -> universe
-
-val subst_large_constraints :
-  (universe * universe) list -> universe -> universe
-
-val no_upper_constraints : universe -> constraints -> bool
-
-(** Is u mentionned in v (or equals to v) ? *)
-
-val univ_depends : universe -> universe -> bool
-
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : universes -> Pp.std_ppcmds
-- 
cgit v1.2.3