diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 70 |
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 |