summaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/univ.ml70
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