From 396da69dc2716971741c90230ba3f65631a849d2 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 18 Dec 2010 16:35:18 +0000 Subject: Univ: try to avoid a few lookup in the universe graph Sometimes the same (repr g u) was done in different functions after being passed u as argument. We rather try to compute (repr g u) as soon as possible, and then pass it instead of u. Beware of sync issues : if g changes, arcu might become obsolete (cf. setlt, setleq, merge ...) Typical code around occurences of declare_univ was doing up to 3 lookups: - is u in g ? - if not we descend again in g to add it - and then later repr is called on the same u. With my safe_repr, we do one lookup if u is in g, and a lookup and an addition otherwise. Ok, declare_univ was rarely used, but it seems nicer this way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13726 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/univ.ml | 144 +++++++++++++++++++++++++++++++-------------------------- 1 file changed, 79 insertions(+), 65 deletions(-) diff --git a/kernel/univ.ml b/kernel/univ.ml index 8db4484b6..7f49e6e76 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -130,12 +130,6 @@ let enter_equiv_arc u v g = let enter_arc ca g = UniverseLMap.add ca.univ (Canonical ca) g -let declare_univ u g = - if not (UniverseLMap.mem u g) then - enter_arc (terminal u) g - else - g - (* The lower predicative level of the hierarchy that contains (impredicative) Prop and singleton inductive types *) let type0m_univ = Max ([],[]) @@ -167,6 +161,7 @@ let initial_universes = UniverseLMap.empty (* repr : universes -> universe_level -> canonical_arc *) (* canonical representative : we follow the Equiv links *) + let repr g u = let rec repr_rec u = let a = @@ -182,6 +177,20 @@ let repr g u = let can g = List.map (repr g) +(* [safe_repr] also search for the canonical representative, but + if the graph doesn't contain the searched universe, we add it. *) + +let safe_repr g u = + let rec safe_repr_rec u = + match UniverseLMap.find u g with + | Equiv v -> safe_repr_rec v + | Canonical arc -> arc + in + try g, safe_repr_rec u + with Not_found -> + let can = terminal u in + enter_arc can g, can + (* reprleq : canonical_arc -> canonical_arc list *) (* All canonical arcv such that arcu<=arcv with arcv#arcu *) let reprleq g arcu = @@ -201,7 +210,7 @@ let reprleq g arcu = (* between u v = {w|u<=w<=v, w canonical} *) (* between is the most costly operation *) -let between g u arcv = +let between g arcu arcv = (* good are all w | u <= w <= v *) (* bad are all w | u <= w ~<= v *) (* find good and bad nodes in {w | u <= w} *) @@ -222,7 +231,7 @@ let between g u arcv = else good, arcu::bad, b (* b or false *) in - let good,_,_ = explore ([arcv],[],false) (repr g u) in + let good,_,_ = explore ([arcv],[],false) arcu in good (* We assume compare(u,v) = LE with v canonical (see compare below). @@ -273,9 +282,7 @@ let compare_neq g arcu arcv = in cmp [] [] ([],[arcu]) -let compare g u v = - let arcu = repr g u - and arcv = repr g v in +let compare g arcu arcv = if arcu == arcv then EQ else compare_neq g arcu arcv (* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ @@ -287,11 +294,12 @@ let compare g u v = Adding u>v is consistent iff compare(v,u) = NLE and then it is redundant iff compare(u,v) = LT *) -let compare_eq g u v = - let g = declare_univ u g in - let g = declare_univ v g in - repr g u == repr g v +(** * Universe checks [check_eq] and [check_geq], used in coqchk *) +let compare_eq g u v = + let g, arcu = safe_repr g u in + let _, arcv = safe_repr g v in + arcu == arcv type check_function = universes -> universe -> universe -> bool @@ -311,10 +319,10 @@ let rec check_eq g u v = | _ -> anomaly "check_eq" (* not complete! (Atom(u) = Max([u],[]) *) let compare_greater g strict u v = - let g = declare_univ u g in - let g = declare_univ v g in - if not strict && compare_eq g v Set then true else - match compare g v u with + let g, arcu = safe_repr g u in + let g, arcv = safe_repr g v in + if not strict && arcv == snd (safe_repr g Set) then true else + match compare g arcv arcu with | (EQ|LE) -> not strict | LT -> true | NLE -> false @@ -324,44 +332,50 @@ let compare_greater g strict u v = ppnl(str (if b then if strict then ">" else ">=" else "NOT >=")); b *) -let rec check_greater g strict u v = +let check_geq g u v = match u, v with - | Atom ul, Atom vl -> compare_greater g strict ul vl + | Atom ul, Atom vl -> compare_greater g false ul vl | Atom ul, Max(le,lt) -> - List.for_all (fun vl -> compare_greater g strict ul vl) le && + List.for_all (fun vl -> compare_greater g false ul vl) le && List.for_all (fun vl -> compare_greater g true ul vl) lt | _ -> anomaly "check_greater" -let check_geq g = check_greater g false +(** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *) (* setlt : universe_level -> universe_level -> unit *) (* forces u > v *) -let setlt g u v = - let arcu = repr g u in - enter_arc {arcu with lt=v::arcu.lt} g +(* this is normally an update of u in g rather than a creation. *) +let setlt g arcu arcv = + let arcu' = {arcu with lt=arcv.univ::arcu.lt} in + enter_arc arcu' g, arcu' (* checks that non-redundant *) -let setlt_if g u v = match compare g u v with - | LT -> g - | _ -> setlt g u v +let setlt_if (g,arcu) v = + let arcv = repr g v in + match compare g arcu arcv with + | LT -> g, arcu + | _ -> setlt g arcu arcv (* setleq : universe_level -> universe_level -> unit *) (* forces u >= v *) -let setleq g u v = - let arcu = repr g u in - enter_arc {arcu with le=v::arcu.le} g +(* this is normally an update of u in g rather than a creation. *) +let setleq g arcu arcv = + let arcu' = {arcu with le=arcv.univ::arcu.le} in + enter_arc arcu' g, arcu' (* checks that non-redundant *) -let setleq_if g u v = match compare g u v with - | NLE -> setleq g u v - | _ -> g +let setleq_if (g,arcu) v = + let arcv = repr g v in + match compare g arcu arcv with + | NLE -> setleq g arcu arcv + | _ -> g, arcu (* merge : universe_level -> universe_level -> unit *) (* we assume compare(u,v) = LE *) (* merge u v forces u ~ v with repr u as canonical repr *) -let merge g u v = - match between g u (repr g v) with +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 = @@ -369,21 +383,21 @@ let merge g u v = (g',list_unionq arcv.lt w,arcv.le@w') in let (g',w,w') = List.fold_left redirect (g,[],[]) v in - let g'' = List.fold_left (fun g -> setlt_if g arcu.univ) g' w in - let g''' = List.fold_left (fun g -> setleq_if g arcu.univ) g'' w' in - g''' + 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" (* merge_disc : universe_level -> universe_level -> 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 u v = - let arcu = repr g u in - let arcv = repr g v in +let merge_disc g arcu arcv = let g' = enter_equiv_arc arcv.univ arcu.univ g in - let g'' = List.fold_left (fun g -> setlt_if g arcu.univ) g' arcv.lt in - let g''' = List.fold_left (fun g -> setleq_if g arcu.univ) g'' arcv.le in - g''' + let g_arcu = (g',arcu) in + let g_arcu = List.fold_left setlt_if g_arcu arcv.lt in + let g_arcu = List.fold_left setleq_if g_arcu arcv.le in + fst g_arcu (* Universe inconsistency: error raised when trying to enforce a relation that would create a cycle in the graph of universes. *) @@ -397,44 +411,44 @@ let error_inconsistency o u v = raise (UniverseInconsistency (o,Atom u,Atom v)) (* enforce_univ_leq : universe_level -> universe_level -> unit *) (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *) let enforce_univ_leq u v g = - let g = declare_univ u g in - let g = declare_univ v g in - match compare g u v with + let g,arcu = safe_repr g u in + let g,arcv = safe_repr g v in + match compare g arcu arcv with | NLE -> - (match compare g v u with + (match compare g arcv arcu with | LT -> error_inconsistency Le u v - | LE -> merge g v u - | NLE -> setleq g u v + | LE -> merge g arcv arcu + | NLE -> fst (setleq g arcu arcv) | EQ -> anomaly "Univ.compare") | _ -> g (* enforc_univ_eq : universe_level -> universe_level -> unit *) (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) let enforce_univ_eq u v g = - let g = declare_univ u g in - let g = declare_univ v g in - match compare g u v with + let g,arcu = safe_repr g u in + let g,arcv = safe_repr g v in + match compare g arcu arcv with | EQ -> g | LT -> error_inconsistency Eq u v - | LE -> merge g u v + | LE -> merge g arcu arcv | NLE -> - (match compare g v u with + (match compare g arcv arcu with | LT -> error_inconsistency Eq u v - | LE -> merge g v u - | NLE -> merge_disc g u v + | LE -> merge g arcv arcu + | NLE -> merge_disc g arcu arcv | EQ -> anomaly "Univ.compare") (* enforce_univ_lt u v will force u g - | LE -> setlt g u v + | LE -> fst (setlt g arcu arcv) | EQ -> error_inconsistency Lt u v | NLE -> - (match compare g v u with - | NLE -> setlt g u v + (match compare g arcv arcu with + | NLE -> fst (setlt g arcu arcv) | _ -> error_inconsistency Lt u v) (* Constraints and sets of consrtaints. *) -- cgit v1.2.3