Fix issue #88: restrict_universe_context was wrongly forgetting about constraints,

and keeping spurious equalities. simplify_universe_context is correct, although
it might keep unused universes around (it's the responsibility of the tactics to
not produce unused universes then).
Add printer for future universe contexts for debugging.

2 files changed, 34 insertions, 3 deletions

diff --git a/library/universes.ml b/library/universes.ml
index d8fa563a0..2b42e3fe8 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -251,7 +251,7 @@ type universe_full_subst = (universe_level * universe) list
 (** Precondition: flexible <= ctx *)
 let choose_canonical ctx flexible algs s =
   let global = LSet.diff s ctx in
-  let flexible, rigid = LSet.partition (fun x -> LMap.mem x flexible) (LSet.inter 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
@@ -589,8 +589,9 @@ let normalize_context_set ctx us algs =
     csts Constraint.empty
   in
   let partition = UF.partition uf in
+  let flex x = LMap.mem x us in
   let subst, eqs = List.fold_left (fun (subst, cstrs) s -> 
-    let canon, (global, rigid, flexible) = choose_canonical ctx us algs s in
+    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, Univ.Eq, g) cst) global cstrs 
@@ -675,6 +676,34 @@ let restrict_universe_context (univs,csts) s =
       csts Constraint.empty
   in (univs', csts')
 
+let simplify_universe_context (univs,csts) s =
+  let uf = UF.create () in
+  let noneqs =
+    Constraint.fold (fun (l,d,r) noneqs ->
+      if d == Eq && (LSet.mem l univs || LSet.mem r univs) then 
+	(UF.union l r uf; noneqs)
+      else Constraint.add (l,d,r) noneqs)
+      csts Constraint.empty
+  in
+  let partition = UF.partition uf in
+  let flex x = LSet.mem x univs in
+  let subst, univs', csts' = List.fold_left (fun (subst, univs, cstrs) s -> 
+    let canon, (global, rigid, flexible) = choose_canonical univs flex LSet.empty s in
+    (* Add equalities for globals which can't be merged anymore. *)
+    let cstrs = LSet.fold (fun g cst -> 
+      Constraint.add (canon, Univ.Eq, g) cst) (LSet.union global rigid)
+      cstrs 
+    in
+    let subst = LSet.fold (fun f -> LMap.add f canon)
+      flexible subst
+    in (subst, LSet.diff univs flexible, cstrs))
+    (LMap.empty, univs, noneqs) partition
+  in
+  (* Noneqs is now in canonical form w.r.t. equality constraints, 
+     and contains only inequality constraints. *)
+  let csts' = subst_univs_level_constraints subst csts' in
+    (univs', csts'), subst
+
 let is_small_leq (l,d,r) =
   Level.is_small l && d == Univ.Le
 
diff --git a/library/universes.mli b/library/universes.mli
index a41b07362..150686d73 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -78,7 +78,7 @@ val make_opt_subst : universe_opt_subst -> universe_subst_fn
 
 val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
 
-val choose_canonical : universe_set -> universe_opt_subst -> universe_set -> universe_set -> 
+val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> universe_set -> universe_set -> 
   universe_level * (universe_set * universe_set * universe_set)
 
 val instantiate_with_lbound : 
@@ -171,6 +171,8 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
 val universes_of_constr : constr -> universe_set
 val shrink_universe_context : universe_context_set -> universe_set -> universe_context_set
 val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set
+val simplify_universe_context : universe_context_set -> universe_set -> 
+  universe_context_set * universe_level_subst
 
 val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes