Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg

1 files changed, 49 insertions, 21 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6aeb7390..028eaeb4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -125,9 +125,12 @@ let sup u v =
 
 (* Comparison on this type is pointer equality *)
 type canonical_arc =
-    { univ: UniverseLevel.t; lt: UniverseLevel.t list; le: UniverseLevel.t list }
+    { univ: UniverseLevel.t;
+      lt: UniverseLevel.t list;
+      le: UniverseLevel.t list;
+      rank: int }
 
-let terminal u = {univ=u; lt=[]; le=[]}
+let terminal u = {univ=u; lt=[]; le=[]; rank=0}
 
 (* A UniverseLevel.t is either an alias for another one, or a canonical one,
    for which we know the universes that are above *)
@@ -405,24 +408,46 @@ let setleq_if (g,arcu) v =
 (* we assume  compare(u,v) = LE *)
 (* merge u v  forces u ~ v with repr u as canonical repr *)
 let merge g arcu arcv =
-  match between g arcu arcv with
-    | arcu::v -> (* arcu is chosen as canonical and all others (v) are *)
-                 (* redirected to it *)
-	let redirect (g,w,w') arcv =
- 	  let g' = enter_equiv_arc arcv.univ arcu.univ g in
- 	  (g',list_unionq arcv.lt w,arcv.le@w')
-	in
-	let (g',w,w') = List.fold_left redirect (g,[],[]) v in
-	let g_arcu = (g',arcu) in
-	let g_arcu = List.fold_left setlt_if g_arcu w in
-	let g_arcu = List.fold_left setleq_if g_arcu w' in
-	fst g_arcu
-    | [] -> anomaly "Univ.between"
+  (* we find the arc with the biggest rank, and we redirect all others to it *)
+  let arcu, g, v =
+    let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
+      if arc.rank >= max_rank
+      then (arc.rank, max_rank, arc, best_arc::rest)
+      else (max_rank, old_max_rank, best_arc, arc::rest)
+    in
+    match between g arcu arcv with
+      | [] -> anomaly "Univ.between"
+      | arc::rest ->
+        let (max_rank, old_max_rank, best_arc, rest) =
+          List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in
+        if max_rank > old_max_rank then best_arc, g, rest
+        else begin
+          (* one redirected node also has max_rank *)
+          let arcu = {best_arc with rank = max_rank + 1} in
+          arcu, enter_arc arcu g, rest
+        end
+  in
+  let redirect (g,w,w') arcv =
+    let g' = enter_equiv_arc arcv.univ arcu.univ g in
+    (g',list_unionq arcv.lt w,arcv.le@w')
+  in
+  let (g',w,w') = List.fold_left redirect (g,[],[]) v in
+  let g_arcu = (g',arcu) in
+  let g_arcu = List.fold_left setlt_if g_arcu w in
+  let g_arcu = List.fold_left setleq_if g_arcu w' in
+  fst g_arcu
 
 (* merge_disc : UniverseLevel.t -> UniverseLevel.t -> unit *)
 (* we assume  compare(u,v) = compare(v,u) = NLE *)
 (* merge_disc u v  forces u ~ v with repr u as canonical repr *)
-let merge_disc g arcu arcv =
+let merge_disc g arc1 arc2 =
+  let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
+  let arcu, g = 
+    if arc1.rank <> arc2.rank then arcu, g
+    else
+      let arcu = {arcu with rank = succ arcu.rank} in 
+      arcu, enter_arc arcu g
+  in
   let g' = enter_equiv_arc arcv.univ arcu.univ g in
   let g_arcu = (g',arcu) in
   let g_arcu = List.fold_left setlt_if g_arcu arcv.lt in
@@ -563,7 +588,7 @@ let normalize_universes g =
   in
   let canonicalize u = function
     | Equiv _ -> Equiv (repr u)
-    | Canonical {univ=v; lt=lt; le=le} ->
+    | 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
@@ -575,6 +600,7 @@ let normalize_universes g =
         univ = v;
         lt = UniverseLSet.elements lt;
         le = UniverseLSet.elements le;
+	rank = rank
       }
   in
   UniverseLMap.mapi canonicalize g
@@ -632,7 +658,8 @@ let bellman_ford bottom g =
     let node = Canonical {
       univ = bottom;
       lt = [];
-      le = UniverseLSet.elements vertices
+      le = UniverseLSet.elements vertices;
+      rank = 0
     } in UniverseLMap.add bottom node g
   in
   let rec iter count accu =
@@ -692,12 +719,12 @@ let sort_universes orig =
           | false, true -> push res v
           | false, false -> res
         end
-      | Canonical {univ=v; lt=lt; le=le} ->
+      | Canonical {univ=v; lt=lt; le=le; rank=r} ->
         assert (u == v);
         if filter u then
           let lt = List.filter filter lt in
           let le = List.filter filter le in
-          UniverseLMap.add u (Canonical {univ=u; lt=lt; le=le}) res
+          UniverseLMap.add u (Canonical {univ=u; lt=lt; le=le; rank=r}) res
         else
           let res = List.fold_left (fun g u -> if filter u then push g u else g) res lt in
           let res = List.fold_left (fun g u -> if filter u then push g u else g) res le in
@@ -717,7 +744,8 @@ let sort_universes orig =
         let g = UniverseLMap.add u (Canonical {
           univ = u;
           le = [];
-          lt = [types.(i+1)]
+          lt = [types.(i+1)];
+	  rank = 1
         }) g in aux (i+1) g
       else g
     in aux 0 g