Fix minimization to be insensitive to redundant arcs.

The new algorithm produces different sets of arcs than in 8.5, hence
existing developments may fail to pass now because they relied on
the (correct but more approximate) result of minimization in 8.5 which
wasn't insensitive.

The algorithm works bottom-up on the (well-founded) graph to
find lower levels that an upper level can be minimized to. We
filter said lower levels according to the lower sets of the other levels
we consider. If they appear in any of them then we don't need their
constraints. Does not seem to have a huge impact on performance in HoTT,
but this should be evaluated further.

Adapt test-suite files accordingly.

2 files changed, 105 insertions, 41 deletions

diff --git a/library/universes.ml b/library/universes.ml
index db95607f1..08ff2ced8 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -702,12 +702,43 @@ let pr_universe_body = function
 
 let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
 
-exception Found of Level.t
+let compare_constraint_type d d' =
+  match d, d' with
+  | Eq, Eq | Le, Le | Lt, Lt -> 0
+  | Eq, _ -> -1
+  | Le, Eq -> 1
+  | Le, Lt -> -1
+  | Lt, (Eq | Le) -> 1
+
+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
+
+exception Found of Level.t * lowermap
 let find_inst insts v =
-  try LMap.iter (fun k (enf,alg,v') ->
-    if not alg && enf && Universe.equal v' v then raise (Found k))
+  try LMap.iter (fun k (enf,alg,v',lower) ->
+    if not alg && enf && Universe.equal v' v then raise (Found (k, lower)))
 	insts; raise Not_found
-  with Found l -> l
+  with Found (f,l) -> (f,l)
 
 let compute_lbound left =
  (** The universe variable was not fixed yet.
@@ -726,27 +757,33 @@ let compute_lbound left =
 	 else None))
       None left
   
-let instantiate_with_lbound u lbound alg enforce (ctx, us, algs, insts, cstrs) =
+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) insts, cstrs'), (enforce, alg, inst)
+       LMap.add u (enforce,alg,lbound,lower) insts, cstrs'),
+      (enforce, alg, inst, lower)
   else (* Actually instantiate *)
     (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
-     LMap.add u (enforce,alg,lbound) insts, cstrs), (enforce, alg, lbound)
+     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 =
   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)
+      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 remove_lower u lower =
+  let levels = Universe.levels u in
+  LSet.fold (fun l acc -> LMap.remove l acc) levels lower
     
 let minimize_univ_variables ctx us algs left right cstrs =
   let left, lbounds = 
@@ -756,22 +793,44 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	let lbounds' = 
 	  match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
 	  | None -> lbounds
-	  | Some lbound -> LMap.add r (true, false, lbound) lbounds
+	  | Some lbound -> LMap.add r (true, false, lbound, 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 = 
+    let acc, left, lower =
       try let l = LMap.find u left in
-	    List.fold_left
-	      (fun (acc, left') (d, l) -> 
-	       let acc', (enf,alg,l') = aux acc l in
-	       let l' = 
-		 if enf then Universe.make l 
-		 else l' 
-	       in acc', (d, l') :: left')
-	      (acc, []) l
-      with Not_found -> acc, []
+	  let acc, left, newlow, lower =
+            List.fold_left
+	      (fun (acc, left', newlow, lower') (d, l) ->
+	        let acc', (enf,alg,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 not_lower (d,l) =
+            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
+          in
+          let left = List.uniquize (List.filter not_lower left) in
+          (acc, left, LMap.union newlow lower)
+      with Not_found -> acc, [], LMap.empty
     and right =
       try Some (LMap.find u right)
       with Not_found -> None
@@ -779,31 +838,33 @@ let minimize_univ_variables ctx us algs left right cstrs =
     let instantiate_lbound lbound =
       let alg = LSet.mem u algs in
 	if alg then
-	  (* u is algebraic: we instantiate it with it's lower bound, if any, 
+	  (* u is algebraic: we instantiate it with its lower bound, if any,
               or enforce the constraints if it is bounded from the top. *)
-	  instantiate_with_lbound u lbound true false acc
+          let lower = remove_lower lbound lower in
+	  instantiate_with_lbound u lbound lower true 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 false false acc'
-	     else acc, (true, false, lbound)
-	| None -> 
-	  try 
-	    (* if right <> None then raise Not_found; *)
-	    (* Another universe represents the same lower bound, 
-	       we can share them with no harm. *)
-	    let can = find_inst insts lbound in
-	      instantiate_with_lbound u (Universe.make can) false false acc
+		 instantiate_with_lbound u lbound lower false false acc'
+	     else acc, (true, false, lbound, lower)
+	  | None ->
+	     try
+	       (* Another universe represents the same lower bound,
+                  we can share them with no harm. *)
+	       let can, lower = find_inst insts lbound in
+               let lower = LMap.remove can lower in
+	       instantiate_with_lbound u (Universe.make can) lower false false acc
 	  with Not_found -> 
 	    (* We set u as the canonical universe representing lbound *)
-	    instantiate_with_lbound u lbound false true acc
+	    instantiate_with_lbound u lbound lower false true acc
     in
     let acc' acc = 
       match right with
@@ -812,7 +873,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in
 	  if List.is_empty dangling then acc
 	  else
-	    let ((ctx', us, algs, insts, cstrs), (enf,_,inst as b)) = acc in
+	    let ((ctx', us, algs, insts, cstrs), (enf,_,inst,lower as b)) = acc in
 	    let cstrs' = List.fold_left (fun cstrs (d, r) -> 
 	      if d == Univ.Le then
 		enforce_leq inst (Universe.make r) cstrs
@@ -824,15 +885,15 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	    in
 	      (ctx', us, algs, insts, cstrs'), b
     in
-      if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u))
+      if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower))
       else
 	let lbound = compute_lbound left in
 	  match lbound with
 	  | None -> (* Nothing to do *)
-	    acc' (acc, (true, false, Universe.make u))
+	    acc' (acc, (true, false, Universe.make u, lower))
 	  | Some lbound ->
 	     try acc' (instantiate_lbound lbound) 
-	     with Failure _ -> acc' (acc, (true, false, Universe.make u))
+	     with Failure _ -> acc' (acc, (true, false, 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
diff --git a/library/universes.mli b/library/universes.mli
index a5740ec49..c8cf7047e 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -243,28 +243,31 @@ val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> univ
     
 val compute_lbound : (constraint_type * Univ.universe) list -> universe option
 
+type lowermap = constraint_type Univ.LMap.t
+
 val instantiate_with_lbound : 
   Univ.LMap.key ->
   Univ.universe ->
+  lowermap ->
   bool ->
   bool ->
   Univ.LSet.t * Univ.universe option Univ.LMap.t *
     Univ.LSet.t *
-    (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints ->
+    (bool * bool * Univ.universe * lowermap) Univ.LMap.t * Univ.constraints ->
   (Univ.LSet.t * Univ.universe option Univ.LMap.t *
     Univ.LSet.t *
-     (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) *
-    (bool * bool * Univ.universe)
+     (bool * bool * Univ.universe * lowermap) Univ.LMap.t * Univ.constraints) *
+    (bool * bool * Univ.universe * lowermap)
 
 val minimize_univ_variables : 
            Univ.LSet.t ->
            Univ.universe option Univ.LMap.t ->
            Univ.LSet.t ->
-  constraints_map -> constraints_map ->
+           constraints_map -> constraints_map ->
            Univ.constraints ->
            Univ.LSet.t * Univ.universe option Univ.LMap.t *
 	     Univ.LSet.t *
-           (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints
+           (bool * bool * Univ.universe * lowermap) Univ.LMap.t * Univ.constraints
 
 (** {6 Support for old-style sort-polymorphism } *)