Split off Universes functions for minimization.

This finishes the splitting of Universes.

6 files changed, 438 insertions, 405 deletions

diff --git a/engine/engine.mllib b/engine/engine.mllib
index befd49dc9..37e83b623 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -2,6 +2,7 @@ UnivNames
 UnivGen
 UnivSubst
 UnivProblem
+UnivMinim
 Universes
 Univops
 UState
diff --git a/engine/uState.ml b/engine/uState.ml
index dbf5d48aa..844eb390b 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -20,7 +20,7 @@ type uinfo = {
   uloc : Loc.t option;
 }
 
-module UPairSet = Universes.UPairSet
+module UPairSet = UnivMinim.UPairSet
 
 (* 2nd part used to check consistency on the fly. *)
 type t =
@@ -630,7 +630,7 @@ let refresh_undefined_univ_variables uctx =
     uctx', subst
 
 let minimize uctx =
-  let open Universes in
+  let open UnivMinim in
   let ((vars',algs'), us') =
     normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
       uctx.uctx_univ_algebraic uctx.uctx_weak_constraints
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
new file mode 100644
index 000000000..f10e6d2ec
--- /dev/null
+++ b/engine/univMinim.ml
@@ -0,0 +1,383 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Univ
+open UnivSubst
+
+(* To disallow minimization to Set *)
+let set_minimization = ref true
+let is_set_minimization () = !set_minimization
+
+let _ =
+  Goptions.(declare_bool_option
+          { optdepr  = false;
+            optname  = "minimization to Set";
+            optkey   = ["Universe";"Minimization";"ToSet"];
+            optread  = is_set_minimization;
+            optwrite = (:=) set_minimization })
+
+
+(** Simplification *)
+
+let add_list_map u t map =
+  try
+    let l = LMap.find u map in
+    LMap.set u (t :: l) map
+  with Not_found ->
+    LMap.add u [t] map
+
+(** Precondition: flexible <= ctx *)
+let choose_canonical ctx flexible algs s =
+  let global = LSet.diff s ctx in
+  let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in
+    (** If there is a global universe in the set, choose it *)
+    if not (LSet.is_empty global) then
+      let canon = LSet.choose global in
+        canon, (LSet.remove canon global, rigid, flexible)
+    else (** No global in the equivalence class, choose a rigid one *)
+        if not (LSet.is_empty rigid) then
+          let canon = LSet.choose rigid in
+            canon, (global, LSet.remove canon rigid, flexible)
+        else (** There are only flexible universes in the equivalence
+                 class, choose a non-algebraic. *)
+          let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in
+            if not (LSet.is_empty nonalgs) then
+              let canon = LSet.choose nonalgs in
+                canon, (global, rigid, LSet.remove canon flexible)
+            else
+              let canon = LSet.choose algs in
+                canon, (global, rigid, LSet.remove canon flexible)
+
+(* Eq < Le < Lt *)
+let compare_constraint_type d d' =
+  match d, d' with
+  | Eq, Eq -> 0
+  | Eq, _ -> -1
+  | _, Eq -> 1
+  | Le, Le -> 0
+  | Le, _ -> -1
+  | _, Le -> 1
+  | Lt, Lt -> 0
+
+type lowermap = constraint_type LMap.t
+
+let lower_union =
+  let merge k a b =
+    match a, b with
+    | Some _, None -> a
+    | None, Some _ -> b
+    | None, None -> None
+    | Some l, Some r ->
+       if compare_constraint_type l r >= 0 then a
+       else b
+  in LMap.merge merge
+
+let lower_add l c m =
+  try let c' = LMap.find l m in
+      if compare_constraint_type c c' > 0 then
+        LMap.add l c m
+      else m
+  with Not_found -> LMap.add l c m
+
+let lower_of_list l =
+  List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l
+
+type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap }
+
+exception Found of Level.t * lowermap
+let find_inst insts v =
+  try LMap.iter (fun k {enforce;alg;lbound=v';lower} ->
+    if not alg && enforce && Universe.equal v' v then raise (Found (k, lower)))
+        insts; raise Not_found
+  with Found (f,l) -> (f,l)
+
+let compute_lbound left =
+ (** The universe variable was not fixed yet.
+     Compute its level using its lower bound. *)
+  let sup l lbound =
+    match lbound with
+    | None -> Some l
+    | Some l' -> Some (Universe.sup l l')
+  in
+    List.fold_left (fun lbound (d, l) ->
+      if d == Le (* l <= ?u *) then sup l lbound
+      else (* l < ?u *)
+        (assert (d == Lt);
+         if not (Universe.level l == None) then
+           sup (Universe.super l) lbound
+         else None))
+      None left
+
+let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, cstrs) =
+  if enforce then
+    let inst = Universe.make u in
+    let cstrs' = enforce_leq lbound inst cstrs in
+      (ctx, us, LSet.remove u algs,
+       LMap.add u {enforce;alg;lbound;lower} insts, cstrs'),
+      {enforce; alg; lbound=inst; lower}
+  else (* Actually instantiate *)
+    (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
+     LMap.add u {enforce;alg;lbound;lower} insts, cstrs),
+    {enforce; alg; lbound; lower}
+
+type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
+
+let _pr_constraints_map (cmap:constraints_map) =
+  let open Pp in
+  LMap.fold (fun l cstrs acc ->
+    Level.pr l ++ str " => " ++
+      prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++
+      fnl () ++ acc)
+    cmap (mt ())
+
+let remove_alg l (ctx, us, algs, insts, cstrs) =
+  (ctx, us, LSet.remove l algs, insts, cstrs)
+
+let not_lower lower (d,l) =
+  (* We're checking if (d,l) is already implied by the lower
+     constraints on some level u. If it represents l < u (d is Lt
+     or d is Le and i > 0, the i < 0 case is impossible due to
+     invariants of Univ), and the lower constraints only have l <=
+     u then it is not implied. *)
+  Univ.Universe.exists
+    (fun (l,i) ->
+       let d =
+         if i == 0 then d
+         else match d with
+           | Le -> Lt
+           | d -> d
+       in
+       try let d' = LMap.find l lower in
+         (* If d is stronger than the already implied lower
+          * constraints we must keep it. *)
+         compare_constraint_type d d' > 0
+       with Not_found ->
+         (** No constraint existing on l *) true) l
+
+exception UpperBoundedAlg
+(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper
+   constraints to [lbound], adding them to [cstrs].
+
+    @raise UpperBoundedAlg if any [upper] constraints are strict and
+   [lbound] algebraic. *)
+let enforce_uppers upper lbound cstrs =
+  List.fold_left (fun cstrs (d, r) ->
+      if d == Univ.Le then
+        enforce_leq lbound (Universe.make r) cstrs
+      else
+        match Universe.level lbound with
+        | Some lev -> Constraint.add (lev, d, r) cstrs
+        | None -> raise UpperBoundedAlg)
+    cstrs upper
+
+let minimize_univ_variables ctx us algs left right cstrs =
+  let left, lbounds =
+    Univ.LMap.fold (fun r lower (left, lbounds as acc)  ->
+      if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc
+      else (* Fixed universe, just compute its glb for sharing *)
+        let lbounds =
+          match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
+          | None -> lbounds
+          | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower}
+                                   lbounds
+        in (Univ.LMap.remove r left, lbounds))
+      left (left, Univ.LMap.empty)
+  in
+  let rec instance (ctx, us, algs, insts, cstrs as acc) u =
+    let acc, left, lower =
+      match LMap.find u left with
+      | exception Not_found -> acc, [], LMap.empty
+      | l ->
+        let acc, left, newlow, lower =
+          List.fold_left
+          (fun (acc, left, newlow, lower') (d, l) ->
+           let acc', {enforce=enf;alg;lbound=l';lower} = aux acc l in
+           let l' =
+             if enf then Universe.make l
+             else l'
+           in acc', (d, l') :: left,
+              lower_add l d newlow, lower_union lower lower')
+          (acc, [], LMap.empty, LMap.empty) l
+        in
+        let left = CList.uniquize (List.filter (not_lower lower) left) in
+        (acc, left, LMap.union newlow lower)
+    in
+    let instantiate_lbound lbound =
+      let alg = LSet.mem u algs in
+        if alg then
+          (* u is algebraic: we instantiate it with its lower bound, if any,
+              or enforce the constraints if it is bounded from the top. *)
+          let lower = LSet.fold LMap.remove (Universe.levels lbound) lower in
+          instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc
+        else (* u is non algebraic *)
+          match Universe.level lbound with
+          | Some l -> (* The lowerbound is directly a level *)
+             (* u is not algebraic but has no upper bounds,
+                we instantiate it with its lower bound if it is a
+                different level, otherwise we keep it. *)
+             let lower = LMap.remove l lower in
+             if not (Level.equal l u) then
+               (* Should check that u does not
+                  have upper constraints that are not already in right *)
+               let acc = remove_alg l acc in
+                 instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc
+             else acc, {enforce=true; alg=false; lbound; lower}
+          | None ->
+            begin match find_inst insts lbound with
+              | can, lower ->
+                (* Another universe represents the same lower bound,
+                   we can share them with no harm. *)
+                let lower = LMap.remove can lower in
+                instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc
+              | exception Not_found ->
+                (* We set u as the canonical universe representing lbound *)
+                instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc
+            end
+    in
+    let enforce_uppers ((ctx,us,algs,insts,cstrs), b as acc) =
+      match LMap.find u right with
+      | exception Not_found -> acc
+      | upper ->
+        let upper = List.filter (fun (d, r) -> not (LMap.mem r us)) upper in
+        let cstrs = enforce_uppers upper b.lbound cstrs in
+        (ctx, us, algs, insts, cstrs), b
+    in
+    if not (LSet.mem u ctx)
+    then enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
+    else
+      let lbound = compute_lbound left in
+      match lbound with
+      | None -> (* Nothing to do *)
+        enforce_uppers (acc, {enforce=true;alg=false;lbound=Universe.make u; lower})
+      | Some lbound ->
+        try enforce_uppers (instantiate_lbound lbound)
+        with UpperBoundedAlg ->
+          enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
+  and aux (ctx, us, algs, seen, cstrs as acc) u =
+    try acc, LMap.find u seen
+    with Not_found -> instance acc u
+  in
+    LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) ->
+      if v == None then fst (aux acc u)
+      else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs)
+      us (ctx, us, algs, lbounds, cstrs)
+
+module UPairs = OrderedType.UnorderedPair(Univ.Level)
+module UPairSet = Set.Make (UPairs)
+
+let normalize_context_set g ctx us algs weak =
+  let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
+  (** Keep the Prop/Set <= i constraints separate for minimization *)
+  let smallles, csts =
+    Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
+  in
+  let smallles = if is_set_minimization ()
+    then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
+    else Constraint.empty
+  in
+  let csts, partition =
+    (* We first put constraints in a normal-form: all self-loops are collapsed
+       to equalities. *)
+    let g = LSet.fold (fun v g -> UGraph.add_universe v false g)
+                           ctx UGraph.initial_universes
+    in
+    let add_soft u g =
+      if not (Level.is_small u || LSet.mem u ctx)
+      then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g
+      else g
+    in
+    let g = Constraint.fold
+        (fun (l, d, r) g -> add_soft r (add_soft l g))
+        csts g
+    in
+    let g = UGraph.merge_constraints csts g in
+      UGraph.constraints_of_universes g
+  in
+  (* We ignore the trivial Prop/Set <= i constraints. *)
+  let noneqs =
+    Constraint.filter
+      (fun (l,d,r) -> not ((d == Le && Level.is_small l) ||
+                           (Level.is_prop l && d == Lt && Level.is_set r)))
+      csts
+  in
+  let noneqs = Constraint.union noneqs smallles in
+  let flex x = LMap.mem x us in
+  let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s ->
+    let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
+    (* Add equalities for globals which can't be merged anymore. *)
+    let cstrs = LSet.fold (fun g cst ->
+      Constraint.add (canon, Eq, g) cst) global
+      cstrs
+    in
+    (* Also add equalities for rigid variables *)
+    let cstrs = LSet.fold (fun g cst ->
+      Constraint.add (canon, Eq, g) cst) rigid
+      cstrs
+    in
+    let canonu = Some (Universe.make canon) in
+    let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in
+      (LSet.diff ctx flexible, us, cstrs))
+    (ctx, us, Constraint.empty) partition
+  in
+  (* Process weak constraints: when one side is flexible and the 2
+     universes are unrelated unify them. *)
+  let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) ->
+      let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
+      let u = norm u and v = norm v in
+      let set_to a b =
+        (LSet.remove a ctx,
+         LMap.add a (Some (Universe.make b)) us,
+         UGraph.enforce_constraint (a,Eq,b) g)
+      in
+      if UGraph.check_constraint g (u,Le,v) || UGraph.check_constraint g (v,Le,u)
+      then acc
+      else
+      if LMap.mem u us
+      then set_to u v
+      else if LMap.mem v us
+      then set_to v u
+      else acc)
+      weak (ctx, us, g)  in
+  (* Noneqs is now in canonical form w.r.t. equality constraints,
+     and contains only inequality constraints. *)
+  let noneqs =
+    let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
+    Constraint.fold (fun (u,d,v) noneqs ->
+        let u = norm u and v = norm v in
+        if d != Lt && Level.equal u v then noneqs
+        else Constraint.add (u,d,v) noneqs)
+      noneqs Constraint.empty
+  in
+  (* Compute the left and right set of flexible variables, constraints
+     mentionning other variables remain in noneqs. *)
+  let noneqs, ucstrsl, ucstrsr =
+    Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) ->
+      let lus = LMap.mem l us and rus = LMap.mem r us in
+      let ucstrsl' =
+        if lus then add_list_map l (d, r) ucstrsl
+        else ucstrsl
+      and ucstrsr' =
+        add_list_map r (d, l) ucstrsr
+      in
+      let noneqs =
+        if lus || rus then noneq
+        else Constraint.add cstr noneq
+      in (noneqs, ucstrsl', ucstrsr'))
+    noneqs (Constraint.empty, LMap.empty, LMap.empty)
+  in
+  (* Now we construct the instantiation of each variable. *)
+  let ctx', us, algs, inst, noneqs =
+    minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs
+  in
+  let us = normalize_opt_subst us in
+    (us, algs), (ctx', Constraint.union noneqs eqs)
+
+(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *)
+(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *)
diff --git a/engine/univMinim.mli b/engine/univMinim.mli
new file mode 100644
index 000000000..9f80b7acb
--- /dev/null
+++ b/engine/univMinim.mli
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Univ
+open UnivSubst
+
+(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *)
+module UPairSet : CSet.S with type elt = (Level.t * Level.t)
+
+(** Simplification and pruning of constraints:
+    [normalize_context_set ctx us]
+
+    - Instantiate the variables in [us] with their most precise
+    universe levels respecting the constraints.
+
+    - Normalizes the context [ctx] w.r.t. equality constraints,
+    choosing a canonical universe in each equivalence class
+    (a global one if there is one) and transitively saturate
+    the constraints w.r.t to the equalities. *)
+
+val normalize_context_set : UGraph.t -> ContextSet.t ->
+  universe_opt_subst (* The defined and undefined variables *) ->
+  LSet.t (* univ variables that can be substituted by algebraics *) ->
+  UPairSet.t (* weak equality constraints *) ->
+  (universe_opt_subst * LSet.t) in_universe_context_set
diff --git a/engine/universes.ml b/engine/universes.ml
index e3b661770..70601987c 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -8,381 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Univ
-open UnivSubst
-
-(* To disallow minimization to Set *)
-
-let set_minimization = ref true
-let is_set_minimization () = !set_minimization
-
-let _ =
-  Goptions.(declare_bool_option
-          { optdepr  = false;
-            optname  = "minimization to Set";
-            optkey   = ["Universe";"Minimization";"ToSet"];
-            optread  = is_set_minimization;
-            optwrite = (:=) set_minimization })
-
-
-(** Simplification *)
-
-let add_list_map u t map =
-  try
-    let l = LMap.find u map in
-    LMap.set u (t :: l) map
-  with Not_found ->
-    LMap.add u [t] map
-
-(** Precondition: flexible <= ctx *)
-let choose_canonical ctx flexible algs s =
-  let global = LSet.diff s ctx in
-  let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in
-    (** If there is a global universe in the set, choose it *)
-    if not (LSet.is_empty global) then
-      let canon = LSet.choose global in
-	canon, (LSet.remove canon global, rigid, flexible)
-    else (** No global in the equivalence class, choose a rigid one *)
-	if not (LSet.is_empty rigid) then
-	  let canon = LSet.choose rigid in
-	    canon, (global, LSet.remove canon rigid, flexible)
-	else (** There are only flexible universes in the equivalence
-		 class, choose a non-algebraic. *)
-	  let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in
-	    if not (LSet.is_empty nonalgs) then
-	      let canon = LSet.choose nonalgs in
-		canon, (global, rigid, LSet.remove canon flexible)
-	    else
-	      let canon = LSet.choose algs in
-		canon, (global, rigid, LSet.remove canon flexible)
-
-(* Eq < Le < Lt *)
-let compare_constraint_type d d' =
-  match d, d' with
-  | Eq, Eq -> 0
-  | Eq, _ -> -1
-  | _, Eq -> 1
-  | Le, Le -> 0
-  | Le, _ -> -1
-  | _, Le -> 1
-  | Lt, Lt -> 0
-
-type lowermap = constraint_type LMap.t
-
-let lower_union =
-  let merge k a b =
-    match a, b with
-    | Some _, None -> a
-    | None, Some _ -> b
-    | None, None -> None
-    | Some l, Some r ->
-       if compare_constraint_type l r >= 0 then a
-       else b
-  in LMap.merge merge
-
-let lower_add l c m =
-  try let c' = LMap.find l m in
-      if compare_constraint_type c c' > 0 then
-        LMap.add l c m
-      else m
-  with Not_found -> LMap.add l c m
-
-let lower_of_list l =
-  List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l
-
-type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap }
-
-exception Found of Level.t * lowermap
-let find_inst insts v =
-  try LMap.iter (fun k {enforce;alg;lbound=v';lower} ->
-    if not alg && enforce && Universe.equal v' v then raise (Found (k, lower)))
-	insts; raise Not_found
-  with Found (f,l) -> (f,l)
-
-let compute_lbound left =
- (** The universe variable was not fixed yet.
-     Compute its level using its lower bound. *)
-  let sup l lbound = 
-    match lbound with
-    | None -> Some l
-    | Some l' -> Some (Universe.sup l l')
-  in
-    List.fold_left (fun lbound (d, l) -> 
-      if d == Le (* l <= ?u *) then sup l lbound
-      else (* l < ?u *) 
-	(assert (d == Lt); 
-	 if not (Universe.level l == None) then
-	   sup (Universe.super l) lbound
-	 else None))
-      None left
-
-let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, cstrs) =
-  if enforce then
-    let inst = Universe.make u in
-    let cstrs' = enforce_leq lbound inst cstrs in
-      (ctx, us, LSet.remove u algs, 
-       LMap.add u {enforce;alg;lbound;lower} insts, cstrs'),
-      {enforce; alg; lbound=inst; lower}
-  else (* Actually instantiate *)
-    (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
-     LMap.add u {enforce;alg;lbound;lower} insts, cstrs),
-    {enforce; alg; lbound; lower}
-
-type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
-
-let _pr_constraints_map (cmap:constraints_map) =
-  let open Pp in
-  LMap.fold (fun l cstrs acc -> 
-    Level.pr l ++ str " => " ++ 
-      prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++
-      fnl () ++ acc)
-    cmap (mt ())
-
-let remove_alg l (ctx, us, algs, insts, cstrs) =
-  (ctx, us, LSet.remove l algs, insts, cstrs)
-
-let not_lower lower (d,l) =
-  (* We're checking if (d,l) is already implied by the lower
-     constraints on some level u. If it represents l < u (d is Lt
-     or d is Le and i > 0, the i < 0 case is impossible due to
-     invariants of Univ), and the lower constraints only have l <=
-     u then it is not implied. *)
-  Univ.Universe.exists
-    (fun (l,i) ->
-       let d =
-         if i == 0 then d
-         else match d with
-           | Le -> Lt
-           | d -> d
-       in
-       try let d' = LMap.find l lower in
-         (* If d is stronger than the already implied lower
-          * constraints we must keep it. *)
-         compare_constraint_type d d' > 0
-       with Not_found ->
-         (** No constraint existing on l *) true) l
-
-exception UpperBoundedAlg
-(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper
-   constraints to [lbound], adding them to [cstrs].
-
-    @raise UpperBoundedAlg if any [upper] constraints are strict and
-   [lbound] algebraic. *)
-let enforce_uppers upper lbound cstrs =
-  List.fold_left (fun cstrs (d, r) ->
-      if d == Univ.Le then
-        enforce_leq lbound (Universe.make r) cstrs
-      else
-        match Universe.level lbound with
-        | Some lev -> Constraint.add (lev, d, r) cstrs
-        | None -> raise UpperBoundedAlg)
-    cstrs upper
-
-let minimize_univ_variables ctx us algs left right cstrs =
-  let left, lbounds = 
-    Univ.LMap.fold (fun r lower (left, lbounds as acc)  ->
-      if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc
-      else (* Fixed universe, just compute its glb for sharing *)
-        let lbounds =
-	  match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
-	  | None -> lbounds
-          | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower}
-                                   lbounds
-        in (Univ.LMap.remove r left, lbounds))
-      left (left, Univ.LMap.empty)
-  in
-  let rec instance (ctx, us, algs, insts, cstrs as acc) u =
-    let acc, left, lower =
-      match LMap.find u left with
-      | exception Not_found -> acc, [], LMap.empty
-      | l ->
-	let acc, left, newlow, lower =
-          List.fold_left
-          (fun (acc, left, newlow, lower') (d, l) ->
-           let acc', {enforce=enf;alg;lbound=l';lower} = aux acc l in
-	   let l' =
-	     if enf then Universe.make l
-	     else l'
-           in acc', (d, l') :: left,
-              lower_add l d newlow, lower_union lower lower')
-	  (acc, [], LMap.empty, LMap.empty) l
-        in
-        let left = List.uniquize (List.filter (not_lower lower) left) in
-        (acc, left, LMap.union newlow lower)
-    in
-    let instantiate_lbound lbound =
-      let alg = LSet.mem u algs in
-	if alg then
-	  (* u is algebraic: we instantiate it with its lower bound, if any,
-              or enforce the constraints if it is bounded from the top. *)
-          let lower = LSet.fold LMap.remove (Universe.levels lbound) lower in
-          instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc
-	else (* u is non algebraic *)
-	  match Universe.level lbound with
-	  | Some l -> (* The lowerbound is directly a level *) 
-	     (* u is not algebraic but has no upper bounds,
-  	        we instantiate it with its lower bound if it is a 
-	        different level, otherwise we keep it. *)
-             let lower = LMap.remove l lower in
-	     if not (Level.equal l u) then
-	       (* Should check that u does not 
-  	          have upper constraints that are not already in right *)
-               let acc = remove_alg l acc in
-                 instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc
-             else acc, {enforce=true; alg=false; lbound; lower}
-	  | None ->
-            begin match find_inst insts lbound with
-              | can, lower ->
-                (* Another universe represents the same lower bound,
-                   we can share them with no harm. *)
-                let lower = LMap.remove can lower in
-                instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc
-              | exception Not_found ->
-                (* We set u as the canonical universe representing lbound *)
-                instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc
-            end
-    in
-    let enforce_uppers ((ctx,us,algs,insts,cstrs), b as acc) =
-      match LMap.find u right with
-      | exception Not_found -> acc
-      | upper ->
-        let upper = List.filter (fun (d, r) -> not (LMap.mem r us)) upper in
-        let cstrs = enforce_uppers upper b.lbound cstrs in
-        (ctx, us, algs, insts, cstrs), b
-    in
-    if not (LSet.mem u ctx)
-    then enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
-    else
-      let lbound = compute_lbound left in
-      match lbound with
-      | None -> (* Nothing to do *)
-        enforce_uppers (acc, {enforce=true;alg=false;lbound=Universe.make u; lower})
-      | Some lbound ->
-        try enforce_uppers (instantiate_lbound lbound)
-        with UpperBoundedAlg ->
-          enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
-  and aux (ctx, us, algs, seen, cstrs as acc) u =
-    try acc, LMap.find u seen 
-    with Not_found -> instance acc u
-  in
-    LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) ->
-      if v == None then fst (aux acc u)
-      else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs)
-      us (ctx, us, algs, lbounds, cstrs)
-
-module UPairs = OrderedType.UnorderedPair(Univ.Level)
-module UPairSet = Set.Make (UPairs)
-
-let normalize_context_set g ctx us algs weak =
-  let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
-  (** Keep the Prop/Set <= i constraints separate for minimization *)
-  let smallles, csts =
-    Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
-  in
-  let smallles = if is_set_minimization ()
-    then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
-    else Constraint.empty
-  in
-  let csts, partition =
-    (* We first put constraints in a normal-form: all self-loops are collapsed
-       to equalities. *)
-    let g = LSet.fold (fun v g -> UGraph.add_universe v false g)
-			   ctx UGraph.initial_universes
-    in
-    let add_soft u g =
-      if not (Level.is_small u || LSet.mem u ctx)
-      then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g
-      else g
-    in
-    let g = Constraint.fold
-        (fun (l, d, r) g -> add_soft r (add_soft l g))
-        csts g
-    in
-    let g = UGraph.merge_constraints csts g in
-      UGraph.constraints_of_universes g
-  in
-  (* We ignore the trivial Prop/Set <= i constraints. *)
-  let noneqs =
-    Constraint.filter
-      (fun (l,d,r) -> not ((d == Le && Level.is_small l) ||
-                           (Level.is_prop l && d == Lt && Level.is_set r)))
-      csts
-  in
-  let noneqs = Constraint.union noneqs smallles in
-  let flex x = LMap.mem x us in
-  let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s ->
-    let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
-    (* Add equalities for globals which can't be merged anymore. *)
-    let cstrs = LSet.fold (fun g cst -> 
-      Constraint.add (canon, Eq, g) cst) global
-      cstrs 
-    in
-    (* Also add equalities for rigid variables *)
-    let cstrs = LSet.fold (fun g cst -> 
-      Constraint.add (canon, Eq, g) cst) rigid
-      cstrs
-    in
-    let canonu = Some (Universe.make canon) in
-    let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in
-      (LSet.diff ctx flexible, us, cstrs))
-    (ctx, us, Constraint.empty) partition
-  in
-  (* Process weak constraints: when one side is flexible and the 2
-     universes are unrelated unify them. *)
-  let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) ->
-      let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
-      let u = norm u and v = norm v in
-      let set_to a b =
-        (LSet.remove a ctx,
-         LMap.add a (Some (Universe.make b)) us,
-         UGraph.enforce_constraint (a,Eq,b) g)
-      in
-      if UGraph.check_constraint g (u,Le,v) || UGraph.check_constraint g (v,Le,u)
-      then acc
-      else
-      if LMap.mem u us
-      then set_to u v
-      else if LMap.mem v us
-      then set_to v u
-      else acc)
-      weak (ctx, us, g)  in
-  (* Noneqs is now in canonical form w.r.t. equality constraints, 
-     and contains only inequality constraints. *)
-  let noneqs =
-    let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
-    Constraint.fold (fun (u,d,v) noneqs ->
-        let u = norm u and v = norm v in
-        if d != Lt && Level.equal u v then noneqs
-        else Constraint.add (u,d,v) noneqs)
-      noneqs Constraint.empty
-  in
-  (* Compute the left and right set of flexible variables, constraints
-     mentionning other variables remain in noneqs. *)
-  let noneqs, ucstrsl, ucstrsr = 
-    Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> 
-      let lus = LMap.mem l us and rus = LMap.mem r us in
-      let ucstrsl' = 
-	if lus then add_list_map l (d, r) ucstrsl
-	else ucstrsl
-      and ucstrsr' = 
-	add_list_map r (d, l) ucstrsr
-      in 
-      let noneqs = 
-	if lus || rus then noneq 
-	else Constraint.add cstr noneq
-      in (noneqs, ucstrsl', ucstrsr'))
-    noneqs (Constraint.empty, LMap.empty, LMap.empty)
-  in
-  (* Now we construct the instantiation of each variable. *)
-  let ctx', us, algs, inst, noneqs = 
-    minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs
-  in
-  let us = normalize_opt_subst us in
-    (us, algs), (ctx', Constraint.union noneqs eqs)
-
-(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *)
-(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *)
 
 (** Deprecated *)
 
@@ -464,3 +90,8 @@ let subst_univs_universe_constraints = UnivProblem.Set.subst_univs
 let enforce_eq_instances_univs = UnivProblem.enforce_eq_instances_univs
 let to_constraints = UnivProblem.to_constraints
 let eq_constr_univs_infer_with = UnivProblem.eq_constr_univs_infer_with
+
+(** UnivMinim *)
+module UPairSet = UnivMinim.UPairSet
+
+let normalize_context_set = UnivMinim.normalize_context_set
diff --git a/engine/universes.mli b/engine/universes.mli
index 4d7105e72..46ff33a47 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -12,37 +12,11 @@ open Names
 open Constr
 open Environ
 open Univ
-open UnivSubst
-
-(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *)
-module UPairSet : CSet.S with type elt = (Level.t * Level.t)
-
-(** Universes *)
-
-(** Simplification and pruning of constraints:
-    [normalize_context_set ctx us]
-
-    - Instantiate the variables in [us] with their most precise
-    universe levels respecting the constraints.
-
-    - Normalizes the context [ctx] w.r.t. equality constraints, 
-    choosing a canonical universe in each equivalence class 
-    (a global one if there is one) and transitively saturate
-    the constraints w.r.t to the equalities. *)
-
-val normalize_context_set : UGraph.t -> ContextSet.t ->
-  universe_opt_subst (* The defined and undefined variables *) ->
-  LSet.t (* univ variables that can be substituted by algebraics *) ->
-  UPairSet.t (* weak equality constraints *) ->
-  (universe_opt_subst * LSet.t) in_universe_context_set
-
-(** *********************************** Deprecated *)
 
+(** ************************************** *)
+(** This entire module is deprecated. **** *)
+(** ************************************** *)
 [@@@ocaml.warning "-3"]
-val set_minimization : bool ref
-[@@ocaml.deprecated "Becoming internal."]
-val is_set_minimization : unit -> bool
-[@@ocaml.deprecated "Becoming internal."]
 
 (** ****** Deprecated: moved to [UnivNames] *)
 
@@ -250,3 +224,15 @@ val eq_constr_univs_infer_with :
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
   UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
 [@@ocaml.deprecated "Use [UnivProblem.eq_constr_univs_infer_with]"]
+
+(** ****** Deprecated: moved to [UnivMinim] *)
+
+module UPairSet = UnivMinim.UPairSet
+[@@ocaml.deprecated "Use [UnivMinim.UPairSet]"]
+
+val normalize_context_set : UGraph.t -> ContextSet.t ->
+  universe_opt_subst (* The defined and undefined variables *) ->
+  LSet.t (* univ variables that can be substituted by algebraics *) ->
+  UPairSet.t (* weak equality constraints *) ->
+  (universe_opt_subst * LSet.t) in_universe_context_set
+[@@ocaml.deprecated "Use [UnivMinim.normalize_context_set]"]