diff options
| -rw-r--r-- | kernel/uGraph.ml | 976 | ||||
| -rw-r--r-- | kernel/uGraph.mli | 3 | ||||
| -rw-r--r-- | kernel/univ.ml | 10 | ||||
| -rw-r--r-- | kernel/univ.mli | 4 | ||||
| -rw-r--r-- | lib/acyclicGraph.ml | 852 | ||||
| -rw-r--r-- | lib/acyclicGraph.mli | 82 | ||||
| -rw-r--r-- | lib/lib.mllib | 1 |
7 files changed, 1020 insertions, 908 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 5fc8d0297f..8187dea41b 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -8,749 +8,80 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pp -open Util open Univ -(* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *) -(* Functional code by Jean-Christophe Filliâtre for Coq V7.0 [1999] *) -(* Extension with algebraic universes by HH for Coq V7.0 [Sep 2001] *) -(* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *) -(* Support for universe polymorphism by MS [2014] *) +module G = AcyclicGraph.Make(struct + type t = Level.t + module Set = LSet + module Map = LMap + module Constraint = Constraint -(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu - Sozeau, Pierre-Marie Pédrot, Jacques-Henri Jourdan *) + let equal = Level.equal + let compare = Level.compare -let error_inconsistency o u v p = - raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p)) + type explanation = Univ.explanation + let error_inconsistency d u v p = + raise (UniverseInconsistency (d,Universe.make u, Universe.make v, p)) -(* Universes are stratified by a partial ordering $\le$. - Let $\~{}$ be the associated equivalence. We also have a strict ordering - $<$ between equivalence classes, and we maintain that $<$ is acyclic, - and contained in $\le$ in the sense that $[U]<[V]$ implies $U\le V$. + let pr = Level.pr + end) [@@inlined] (* without inline, +1% ish on HoTT, compcert. See jenkins 594 vs 596 *) +(* Do not include G to make it easier to control universe specific + code (eg add_universe with a constraint vs G.add with no + constraint) *) - At every moment, we have a finite number of universes, and we - maintain the ordering in the presence of assertions $U<V$ and $U\le V$. - - The equivalence $\~{}$ is represented by a tree structure, as in the - union-find algorithm. The assertions $<$ and $\le$ are represented by - adjacency lists. - - We use the algorithm described in the paper: - - Bender, M. A., Fineman, J. T., Gilbert, S., & Tarjan, R. E. (2011). A - new approach to incremental cycle detection and related - problems. arXiv preprint arXiv:1112.0784. - - *) - -open Universe - -module UMap = LMap - -type status = NoMark | Visited | WeakVisited | ToMerge - -(* Comparison on this type is pointer equality *) -type canonical_node = - { univ: Level.t; - ltle: bool UMap.t; (* true: strict (lt) constraint. - false: weak (le) constraint. *) - gtge: LSet.t; - rank : int; - klvl: int; - ilvl: int; - mutable status: status - } - -let big_rank = 1000000 - -(* A Level.t is either an alias for another one, or a canonical one, - for which we know the universes that are above *) - -type univ_entry = - Canonical of canonical_node - | Equiv of Level.t - -type universes = - { entries : univ_entry UMap.t; - index : int; - n_nodes : int; n_edges : int } - -type t = universes - -(** Used to cleanup universes if a traversal function is interrupted before it - has the opportunity to do it itself. *) -let unsafe_cleanup_universes g = - let iter _ n = match n with - | Equiv _ -> () - | Canonical n -> n.status <- NoMark - in - UMap.iter iter g.entries - -let rec cleanup_universes g = - try unsafe_cleanup_universes g - with e -> - (** The only way unsafe_cleanup_universes may raise an exception is when - a serious error (stack overflow, out of memory) occurs, or a signal is - sent. In this unlikely event, we relaunch the cleanup until we finally - succeed. *) - cleanup_universes g; raise e - -(* Every Level.t has a unique canonical arc representative *) - -(* Low-level function : makes u an alias for v. - Does not removes edges from n_edges, but decrements n_nodes. - u should be entered as canonical before. *) -let enter_equiv g u v = - { entries = - UMap.modify u (fun _ a -> - match a with - | Canonical n -> - n.status <- NoMark; - Equiv v - | _ -> assert false) g.entries; - index = g.index; - n_nodes = g.n_nodes - 1; - n_edges = g.n_edges } - -(* Low-level function : changes data associated with a canonical node. - Resets the mutable fields in the old record, in order to avoid breaking - invariants for other users of this record. - n.univ should already been inserted as a canonical node. *) -let change_node g n = - { g with entries = - UMap.modify n.univ - (fun _ a -> - match a with - | Canonical n' -> - n'.status <- NoMark; - Canonical n - | _ -> assert false) - g.entries } - -(* repr : universes -> Level.t -> canonical_node *) -(* canonical representative : we follow the Equiv links *) -let rec repr g u = - let a = - try UMap.find u g.entries - with Not_found -> CErrors.anomaly ~label:"Univ.repr" - (str"Universe " ++ Level.pr u ++ str" undefined.") - in - match a with - | Equiv v -> repr g v - | Canonical arc -> arc - -let get_set_arc g = repr g Level.set -let is_set_arc u = Level.is_set u.univ -let is_prop_arc u = Level.is_prop u.univ - -exception AlreadyDeclared - -(* Reindexes the given universe, using the next available index. *) -let use_index g u = - let u = repr g u in - let g = change_node g { u with ilvl = g.index } in - assert (g.index > min_int); - { g with index = g.index - 1 } - -(* [safe_repr] is like [repr] but if the graph doesn't contain the - searched universe, we add it. *) -let safe_repr g u = - let rec safe_repr_rec entries u = - match UMap.find u entries with - | Equiv v -> safe_repr_rec entries v - | Canonical arc -> arc - in - try g, safe_repr_rec g.entries u - with Not_found -> - let can = - { univ = u; - ltle = UMap.empty; gtge = LSet.empty; - rank = if Level.is_small u then big_rank else 0; - klvl = 0; ilvl = 0; - status = NoMark } - in - let g = { g with - entries = UMap.add u (Canonical can) g.entries; - n_nodes = g.n_nodes + 1 } - in - let g = use_index g u in - g, repr g u - -(* Returns 1 if u is higher than v in topological order. - -1 lower - 0 if u = v *) -let topo_compare u v = - if u.klvl > v.klvl then 1 - else if u.klvl < v.klvl then -1 - else if u.ilvl > v.ilvl then 1 - else if u.ilvl < v.ilvl then -1 - else (assert (u==v); 0) - -(* Checks most of the invariants of the graph. For debugging purposes. *) -let check_universes_invariants g = - let n_edges = ref 0 in - let n_nodes = ref 0 in - UMap.iter (fun l u -> - match u with - | Canonical u -> - UMap.iter (fun v _strict -> - incr n_edges; - let v = repr g v in - assert (topo_compare u v = -1); - if u.klvl = v.klvl then - assert (LSet.mem u.univ v.gtge || - LSet.exists (fun l -> u == repr g l) v.gtge)) - u.ltle; - LSet.iter (fun v -> - let v = repr g v in - assert (v.klvl = u.klvl && - (UMap.mem u.univ v.ltle || - UMap.exists (fun l _ -> u == repr g l) v.ltle)) - ) u.gtge; - assert (u.status = NoMark); - assert (Level.equal l u.univ); - assert (u.ilvl > g.index); - assert (not (UMap.mem u.univ u.ltle)); - incr n_nodes - | Equiv _ -> assert (not (Level.is_small l))) - g.entries; - assert (!n_edges = g.n_edges); - assert (!n_nodes = g.n_nodes) - -let clean_ltle g ltle = - UMap.fold (fun u strict acc -> - let uu = (repr g u).univ in - if Level.equal uu u then acc - else ( - let acc = UMap.remove u (fst acc) in - if not strict && UMap.mem uu acc then (acc, true) - else (UMap.add uu strict acc, true))) - ltle (ltle, false) - -let clean_gtge g gtge = - LSet.fold (fun u acc -> - let uu = (repr g u).univ in - if Level.equal uu u then acc - else LSet.add uu (LSet.remove u (fst acc)), true) - gtge (gtge, false) - -(* [get_ltle] and [get_gtge] return ltle and gtge arcs. - Moreover, if one of these lists is dirty (e.g. points to a - non-canonical node), these functions clean this node in the - graph by removing some duplicate edges *) -let get_ltle g u = - let ltle, chgt_ltle = clean_ltle g u.ltle in - if not chgt_ltle then u.ltle, u, g - else - let sz = UMap.cardinal u.ltle in - let sz2 = UMap.cardinal ltle in - let u = { u with ltle } in - let g = change_node g u in - let g = { g with n_edges = g.n_edges + sz2 - sz } in - u.ltle, u, g - -let get_gtge g u = - let gtge, chgt_gtge = clean_gtge g u.gtge in - if not chgt_gtge then u.gtge, u, g - else - let u = { u with gtge } in - let g = change_node g u in - u.gtge, u, g - -(* [revert_graph] rollbacks the changes made to mutable fields in - nodes in the graph. - [to_revert] contains the touched nodes. *) -let revert_graph to_revert g = - List.iter (fun t -> - match UMap.find t g.entries with - | Equiv _ -> () - | Canonical t -> - t.status <- NoMark) to_revert - -exception AbortBackward of universes -exception CycleDetected - -(* Implementation of the algorithm described in § 5.1 of the following paper: - - Bender, M. A., Fineman, J. T., Gilbert, S., & Tarjan, R. E. (2011). A - new approach to incremental cycle detection and related - problems. arXiv preprint arXiv:1112.0784. - - The "STEP X" comments contained in this file refers to the - corresponding step numbers of the algorithm described in Section - 5.1 of this paper. *) - -(* [delta] is the timeout for backward search. It might be - useful to tune a multiplicative constant. *) -let get_delta g = - int_of_float - (min (float_of_int g.n_edges ** 0.5) - (float_of_int g.n_nodes ** (2./.3.))) - -let rec backward_traverse to_revert b_traversed count g x = - let x = repr g x in - let count = count - 1 in - if count < 0 then begin - revert_graph to_revert g; - raise (AbortBackward g) - end; - if x.status = NoMark then begin - x.status <- Visited; - let to_revert = x.univ::to_revert in - let gtge, x, g = get_gtge g x in - let to_revert, b_traversed, count, g = - LSet.fold (fun y (to_revert, b_traversed, count, g) -> - backward_traverse to_revert b_traversed count g y) - gtge (to_revert, b_traversed, count, g) - in - to_revert, x.univ::b_traversed, count, g - end - else to_revert, b_traversed, count, g - -let rec forward_traverse f_traversed g v_klvl x y = - let y = repr g y in - if y.klvl < v_klvl then begin - let y = { y with klvl = v_klvl; - gtge = if x == y then LSet.empty - else LSet.singleton x.univ } - in - let g = change_node g y in - let ltle, y, g = get_ltle g y in - let f_traversed, g = - UMap.fold (fun z _ (f_traversed, g) -> - forward_traverse f_traversed g v_klvl y z) - ltle (f_traversed, g) - in - y.univ::f_traversed, g - end else if y.klvl = v_klvl && x != y then - let g = change_node g - { y with gtge = LSet.add x.univ y.gtge } in - f_traversed, g - else f_traversed, g - -let rec find_to_merge to_revert g x v = - let x = repr g x in - match x.status with - | Visited -> false, to_revert | ToMerge -> true, to_revert - | NoMark -> - let to_revert = x::to_revert in - if Level.equal x.univ v then - begin x.status <- ToMerge; true, to_revert end - else - begin - let merge, to_revert = LSet.fold - (fun y (merge, to_revert) -> - let merge', to_revert = find_to_merge to_revert g y v in - merge' || merge, to_revert) x.gtge (false, to_revert) - in - x.status <- if merge then ToMerge else Visited; - merge, to_revert - end - | _ -> assert false - -let get_new_edges g to_merge = - (* Computing edge sets. *) - let to_merge_lvl = - List.fold_left (fun acc u -> UMap.add u.univ u acc) - UMap.empty to_merge - in - let ltle = - let fold _ n acc = - let fold u strict acc = - if strict then UMap.add u strict acc - else if UMap.mem u acc then acc - else UMap.add u false acc - in - UMap.fold fold n.ltle acc - in - UMap.fold fold to_merge_lvl UMap.empty - in - let ltle, _ = clean_ltle g ltle in - let ltle = - UMap.merge (fun _ a strict -> - match a, strict with - | Some _, Some true -> - (* There is a lt edge inside the new component. This is a - "bad cycle". *) - raise CycleDetected - | Some _, Some false -> None - | _, _ -> strict - ) to_merge_lvl ltle - in - let gtge = - UMap.fold (fun _ n acc -> LSet.union acc n.gtge) - to_merge_lvl LSet.empty - in - let gtge, _ = clean_gtge g gtge in - let gtge = LSet.diff gtge (UMap.domain to_merge_lvl) in - (ltle, gtge) - - -let reorder g u v = - (* STEP 2: backward search in the k-level of u. *) - let delta = get_delta g in - - (* [v_klvl] is the chosen future level for u, v and all - traversed nodes. *) - let b_traversed, v_klvl, g = - try - let to_revert, b_traversed, _, g = backward_traverse [] [] delta g u in - revert_graph to_revert g; - let v_klvl = (repr g u).klvl in - b_traversed, v_klvl, g - with AbortBackward g -> - (* Backward search was too long, use the next k-level. *) - let v_klvl = (repr g u).klvl + 1 in - [], v_klvl, g - in - let f_traversed, g = - (* STEP 3: forward search. Contrary to what is described in - the paper, we do not test whether v_klvl = u.klvl nor we assign - v_klvl to v.klvl. Indeed, the first call to forward_traverse - will do all that. *) - forward_traverse [] g v_klvl (repr g v) v - in - - (* STEP 4: merge nodes if needed. *) - let to_merge, b_reindex, f_reindex = - if (repr g u).klvl = v_klvl then - begin - let merge, to_revert = find_to_merge [] g u v in - let r = - if merge then - List.filter (fun u -> u.status = ToMerge) to_revert, - List.filter (fun u -> (repr g u).status <> ToMerge) b_traversed, - List.filter (fun u -> (repr g u).status <> ToMerge) f_traversed - else [], b_traversed, f_traversed - in - List.iter (fun u -> u.status <- NoMark) to_revert; - r - end - else [], b_traversed, f_traversed - in - let to_reindex, g = - match to_merge with - | [] -> List.rev_append f_reindex b_reindex, g - | n0::q0 -> - (* Computing new root. *) - let root, rank_rest = - List.fold_left (fun ((best, _rank_rest) as acc) n -> - if n.rank >= best.rank then n, best.rank else acc) - (n0, min_int) q0 - in - let ltle, gtge = get_new_edges g to_merge in - (* Inserting the new root. *) - let g = change_node g - { root with ltle; gtge; - rank = max root.rank (rank_rest + 1); } - in - - (* Inserting shortcuts for old nodes. *) - let g = List.fold_left (fun g n -> - if Level.equal n.univ root.univ then g else enter_equiv g n.univ root.univ) - g to_merge - in - - (* Updating g.n_edges *) - let oldsz = - List.fold_left (fun sz u -> sz+UMap.cardinal u.ltle) - 0 to_merge - in - let sz = UMap.cardinal ltle in - let g = { g with n_edges = g.n_edges + sz - oldsz } in - - (* Not clear in the paper: we have to put the newly - created component just between B and F. *) - List.rev_append f_reindex (root.univ::b_reindex), g - - in - - (* STEP 5: reindex traversed nodes. *) - List.fold_left use_index g to_reindex - -(* Assumes [u] and [v] are already in the graph. *) -(* Does NOT assume that ucan != vcan. *) -let insert_edge strict ucan vcan g = - try - let u = ucan.univ and v = vcan.univ in - (* STEP 1: do we need to reorder nodes ? *) - let g = if topo_compare ucan vcan <= 0 then g else reorder g u v in - - (* STEP 6: insert the new edge in the graph. *) - let u = repr g u in - let v = repr g v in - if u == v then - if strict then raise CycleDetected else g - else - let g = - try let oldstrict = UMap.find v.univ u.ltle in - if strict && not oldstrict then - change_node g { u with ltle = UMap.add v.univ true u.ltle } - else g - with Not_found -> - { (change_node g { u with ltle = UMap.add v.univ strict u.ltle }) - with n_edges = g.n_edges + 1 } - in - if u.klvl <> v.klvl || LSet.mem u.univ v.gtge then g - else - let v = { v with gtge = LSet.add u.univ v.gtge } in - change_node g v - with - | CycleDetected as e -> raise e - | e -> - (** Unlikely event: fatal error or signal *) - let () = cleanup_universes g in - raise e - -let add_universe_gen vlev g = - try - let _arcv = UMap.find vlev g.entries in - raise AlreadyDeclared - with Not_found -> - assert (g.index > min_int); - let v = { - univ = vlev; - ltle = LMap.empty; - gtge = LSet.empty; - rank = 0; - klvl = 0; - ilvl = g.index; - status = NoMark; - } - in - let entries = UMap.add vlev (Canonical v) g.entries in - { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }, v - -let add_universe vlev strict g = - let g, v = add_universe_gen vlev g in - insert_edge strict (get_set_arc g) v g - -let add_universe_unconstrained vlev g = - fst (add_universe_gen vlev g) - -exception UndeclaredLevel of Univ.Level.t -let check_declared_universes g us = - let check l = if not (UMap.mem l g.entries) then raise (UndeclaredLevel l) in - Univ.LSet.iter check us - -exception Found_explanation of explanation - -let get_explanation strict u v g = - let v = repr g v in - let visited_strict = ref UMap.empty in - let rec traverse strict u = - if u == v then - if strict then None else Some [] - else if topo_compare u v = 1 then None - else - let visited = - try not (UMap.find u.univ !visited_strict) || strict - with Not_found -> false - in - if visited then None - else begin - visited_strict := UMap.add u.univ strict !visited_strict; - try - UMap.iter (fun u' strictu' -> - match traverse (strict && not strictu') (repr g u') with - | None -> () - | Some exp -> - let typ = if strictu' then Lt else Le in - raise (Found_explanation ((typ, make u') :: exp))) - u.ltle; - None - with Found_explanation exp -> Some exp - end - in - let u = repr g u in - if u == v then [(Eq, make v.univ)] - else match traverse strict u with Some exp -> exp | None -> assert false - -let get_explanation strict u v g = - Some (lazy (get_explanation strict u v g)) - -(* To compare two nodes, we simply do a forward search. - We implement two improvements: - - we ignore nodes that are higher than the destination; - - we do a BFS rather than a DFS because we expect to have a short - path (typically, the shortest path has length 1) -*) -exception Found of canonical_node list -let search_path strict u v g = - let rec loop to_revert todo next_todo = - match todo, next_todo with - | [], [] -> to_revert (* No path found *) - | [], _ -> loop to_revert next_todo [] - | (u, strict)::todo, _ -> - if u.status = Visited || (u.status = WeakVisited && strict) - then loop to_revert todo next_todo - else - let to_revert = - if u.status = NoMark then u::to_revert else to_revert - in - u.status <- if strict then WeakVisited else Visited; - if try UMap.find v.univ u.ltle || not strict - with Not_found -> false - then raise (Found to_revert) - else - begin - let next_todo = - UMap.fold (fun u strictu next_todo -> - let strict = not strictu && strict in - let u = repr g u in - if u == v && not strict then raise (Found to_revert) - else if topo_compare u v = 1 then next_todo - else (u, strict)::next_todo) - u.ltle next_todo - in - loop to_revert todo next_todo - end - in - if u == v then not strict - else - try - let res, to_revert = - try false, loop [] [u, strict] [] - with Found to_revert -> true, to_revert - in - List.iter (fun u -> u.status <- NoMark) to_revert; - res - with e -> - (** Unlikely event: fatal error or signal *) - let () = cleanup_universes g in - raise e - -(** Uncomment to debug the cycle detection algorithm. *) -(*let insert_edge strict ucan vcan g = - check_universes_invariants g; - let g = insert_edge strict ucan vcan g in - check_universes_invariants g; - let ucan = repr g ucan.univ in - let vcan = repr g vcan.univ in - assert (search_path strict ucan vcan g); - g*) - -(** First, checks on universe levels *) - -let check_equal g u v = - let arcu = repr g u and arcv = repr g v in - arcu == arcv - -let check_eq_level g u v = u == v || check_equal g u v - -let check_smaller g strict u v = - let arcu = repr g u and arcv = repr g v in - if strict then - search_path true arcu arcv g - else - is_prop_arc arcu - || (is_set_arc arcu && not (is_prop_arc arcv)) - || search_path false arcu arcv g - -(** Then, checks on universes *) - -type 'a check_function = universes -> 'a -> 'a -> bool +type t = G.t +type 'a check_function = 'a G.check_function let check_smaller_expr g (u,n) (v,m) = let diff = n - m in match diff with - | 0 -> check_smaller g false u v - | 1 -> check_smaller g true u v - | x when x < 0 -> check_smaller g false u v + | 0 -> G.check_leq g u v + | 1 -> G.check_lt g u v + | x when x < 0 -> G.check_leq g u v | _ -> false let exists_bigger g ul l = - Universe.exists (fun ul' -> + Universe.exists (fun ul' -> check_smaller_expr g ul ul') l let real_check_leq g u v = Universe.for_all (fun ul -> exists_bigger g ul v) u - + let check_leq g u v = Universe.equal u v || is_type0m_univ u || real_check_leq g u v -let check_eq_univs g l1 l2 = - real_check_leq g l1 l2 && real_check_leq g l2 l1 - let check_eq g u v = - Universe.equal u v || check_eq_univs g u v - -(* enforce_univ_eq g u v will force u=v if possible, will fail otherwise *) - -let rec enforce_univ_eq u v g = - let ucan = repr g u in - let vcan = repr g v in - if topo_compare ucan vcan = 1 then enforce_univ_eq v u g - else - let g = insert_edge false ucan vcan g in (* Cannot fail *) - try insert_edge false vcan ucan g - with CycleDetected -> - error_inconsistency Eq v u (get_explanation true u v g) - -(* enforce_univ_leq g u v will force u<=v if possible, will fail otherwise *) -let enforce_univ_leq u v g = - let ucan = repr g u in - let vcan = repr g v in - try insert_edge false ucan vcan g - with CycleDetected -> - error_inconsistency Le u v (get_explanation true v u g) - -(* enforce_univ_lt u v will force u<v if possible, will fail otherwise *) -let enforce_univ_lt u v g = - let ucan = repr g u in - let vcan = repr g v in - try insert_edge true ucan vcan g - with CycleDetected -> - error_inconsistency Lt u v (get_explanation false v u g) - -let empty_universes = - { entries = UMap.empty; index = 0; n_nodes = 0; n_edges = 0 } + Universe.equal u v || + (real_check_leq g u v && real_check_leq g v u) + +let check_eq_level = G.check_eq + +let empty_universes = G.empty let initial_universes = - let set_arc = Canonical { - univ = Level.set; - ltle = LMap.empty; - gtge = LSet.empty; - rank = big_rank; - klvl = 0; - ilvl = (-1); - status = NoMark; - } in - let prop_arc = Canonical { - univ = Level.prop; - ltle = LMap.empty; - gtge = LSet.empty; - rank = big_rank; - klvl = 0; - ilvl = 0; - status = NoMark; - } in - let entries = UMap.add Level.set set_arc (UMap.singleton Level.prop prop_arc) in - let empty = { entries; index = (-2); n_nodes = 2; n_edges = 0 } in - enforce_univ_lt Level.prop Level.set empty - -let is_initial_universes g = UMap.equal (==) g.entries initial_universes.entries - -let enforce_constraint cst g = - match cst with - | (u,Lt,v) -> enforce_univ_lt u v g - | (u,Le,v) -> enforce_univ_leq u v g - | (u,Eq,v) -> enforce_univ_eq u v g - -let merge_constraints c g = - Constraint.fold enforce_constraint c g - -let check_constraint g (l,d,r) = + let big_rank = 1000000 in + let g = G.empty in + let g = G.add ~rank:big_rank Level.prop g in + let g = G.add ~rank:big_rank Level.set g in + G.enforce_lt Level.prop Level.set g + +let enforce_constraint (u,d,v) g = + match d with + | Le -> G.enforce_leq u v g + | Lt -> G.enforce_lt u v g + | Eq -> G.enforce_eq u v g + +let merge_constraints csts g = Constraint.fold enforce_constraint csts g + +let check_constraint g (u,d,v) = match d with - | Eq -> check_equal g l r - | Le -> check_smaller g false l r - | Lt -> check_smaller g true l r + | Le -> G.check_leq g u v + | Lt -> G.check_lt g u v + | Eq -> G.check_eq g u v -let check_constraints c g = - Constraint.for_all (check_constraint g) c +let check_constraints csts g = Constraint.for_all (check_constraint g) csts let leq_expr (u,m) (v,n) = let d = match m - n with @@ -760,6 +91,7 @@ let leq_expr (u,m) (v,n) = (u,d,v) let enforce_leq_alg u v g = + let open Util in let enforce_one (u,v) = function | Inr _ as orig -> orig | Inl (cstrs,g) as orig -> @@ -791,148 +123,19 @@ let enforce_leq_alg u v g = assert (check_leq g u v); cg -(* Normalization *) - -(** [normalize_universes g] returns a graph where all edges point - directly to the canonical representent of their target. The output - graph should be equivalent to the input graph from a logical point - of view, but optimized. We maintain the invariant that the key of - a [Canonical] element is its own name, by keeping [Equiv] edges. *) -let normalize_universes g = - let g = - { g with - entries = UMap.map (fun entry -> - match entry with - | Equiv u -> Equiv ((repr g u).univ) - | Canonical ucan -> Canonical { ucan with rank = 1 }) - g.entries } - in - UMap.fold (fun _ u g -> - match u with - | Equiv _u -> g - | Canonical u -> - let _, u, g = get_ltle g u in - let _, _, g = get_gtge g u in - g) - g.entries g - -let constraints_of_universes g = - let module UF = Unionfind.Make (LSet) (LMap) in - let uf = UF.create () in - let constraints_of u v acc = - match v with - | Canonical {univ=u; ltle; _} -> - UMap.fold (fun v strict acc-> - let typ = if strict then Lt else Le in - Constraint.add (u,typ,v) acc) ltle acc - | Equiv v -> UF.union u v uf; acc - in - let csts = UMap.fold constraints_of g.entries Constraint.empty in - csts, UF.partition uf - -(* domain g.entries = kept + removed *) -let constraints_for ~kept g = - (* rmap: partial map from canonical universes to kept universes *) - let rmap, csts = LSet.fold (fun u (rmap,csts) -> - let arcu = repr g u in - if LSet.mem arcu.univ kept then - LMap.add arcu.univ arcu.univ rmap, enforce_eq_level u arcu.univ csts - else - match LMap.find arcu.univ rmap with - | v -> rmap, enforce_eq_level u v csts - | exception Not_found -> LMap.add arcu.univ u rmap, csts) - kept (LMap.empty,Constraint.empty) - in - let rec add_from u csts todo = match todo with - | [] -> csts - | (v,strict)::todo -> - let v = repr g v in - (match LMap.find v.univ rmap with - | v -> - let d = if strict then Lt else Le in - let csts = Constraint.add (u,d,v) csts in - add_from u csts todo - | exception Not_found -> - (* v is not equal to any kept universe *) - let todo = LMap.fold (fun v' strict' todo -> - (v',strict || strict') :: todo) - v.ltle todo - in - add_from u csts todo) - in - LSet.fold (fun u csts -> - let arc = repr g u in - LMap.fold (fun v strict csts -> add_from u csts [v,strict]) - arc.ltle csts) - kept csts - -let domain g = LMap.domain g.entries - -let choose p g u = - let exception Found of Level.t in - let ru = (repr g u).univ in - if p ru then Some ru - else - try LMap.iter (fun v -> function - | Canonical _ -> () (* we already tried [p ru] *) - | Equiv v' -> - let rv = (repr g v').univ in - if rv == ru && p v then raise (Found v) - (* NB: we could also try [p v'] but it will come up in the - rest of the iteration regardless. *) - ) g.entries; None - with Found v -> Some v - -(** [sort_universes g] builds a totally ordered universe graph. The - output graph should imply the input graph (and the implication - will be strict most of the time), but is not necessarily minimal. - Moreover, it adds levels [Type.n] to identify universes at level - n. An artificial constraint Set < Type.2 is added to ensure that - Type.n and small universes are not merged. Note: the result is - unspecified if the input graph already contains [Type.n] nodes - (calling a module Type is probably a bad idea anyway). *) -let sort_universes g = - let cans = - UMap.fold (fun _ u l -> - match u with - | Equiv _ -> l - | Canonical can -> can :: l - ) g.entries [] - in - let cans = List.sort topo_compare cans in - let lowest_levels = - UMap.mapi (fun u _ -> if Level.is_small u then 0 else 2) - (UMap.filter - (fun _ u -> match u with Equiv _ -> false | Canonical _ -> true) - g.entries) - in - let lowest_levels = - List.fold_left (fun lowest_levels can -> - let lvl = UMap.find can.univ lowest_levels in - UMap.fold (fun u' strict lowest_levels -> - let cost = if strict then 1 else 0 in - let u' = (repr g u').univ in - UMap.modify u' (fun _ lvl0 -> max lvl0 (lvl+cost)) lowest_levels) - can.ltle lowest_levels) - lowest_levels cans - in - let max_lvl = UMap.fold (fun _ a b -> max a b) lowest_levels 0 in - let mp = Names.DirPath.make [Names.Id.of_string "Type"] in - let types = Array.init (max_lvl + 1) (function - | 0 -> Level.prop - | 1 -> Level.set - | n -> Level.make (Level.UGlobal.make mp (n-2))) - in - let g = Array.fold_left (fun g u -> - let g, u = safe_repr g u in - change_node g { u with rank = big_rank }) g types - in - let g = if max_lvl >= 2 then enforce_univ_lt Level.set types.(2) g else g in - let g = - UMap.fold (fun u lvl g -> enforce_univ_eq u (types.(lvl)) g) - lowest_levels g - in - normalize_universes g +exception AlreadyDeclared = G.AlreadyDeclared +let add_universe u strict g = + let g = G.add u g in + let d = if strict then Lt else Le in + enforce_constraint (Level.set,d,u) g + +let add_universe_unconstrained u g = G.add u g + +exception UndeclaredLevel = G.Undeclared +let check_declared_universes = G.check_declared + +let constraints_of_universes = G.constraints_of +let constraints_for = G.constraints_for (** Subtyping of polymorphic contexts *) @@ -957,45 +160,23 @@ let check_eq_instances g t1 t2 = (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1)) in aux 0) -(** Pretty-printing *) - -let pr_umap sep pr map = - let cmp (u,_) (v,_) = Level.compare u v in - Pp.prlist_with_sep sep pr (List.sort cmp (UMap.bindings map)) - -let pr_arc prl = function - | _, Canonical {univ=u; ltle; _} -> - if UMap.is_empty ltle then mt () - else - prl u ++ str " " ++ - v 0 - (pr_umap Pp.spc (fun (v, strict) -> - (if strict then str "< " else str "<= ") ++ prl v) - ltle) ++ - fnl () - | u, Equiv v -> - prl u ++ str " = " ++ prl v ++ fnl () - -let pr_universes prl g = - pr_umap mt (pr_arc prl) g.entries - -(* Dumping constraints to a file *) - -let dump_universes output g = - let dump_arc u = function - | Canonical {univ=u; ltle; _} -> - UMap.iter (fun v strict -> - let typ = if strict then Lt else Le in - output typ u v) ltle; - | Equiv v -> - output Eq u v - in - UMap.iter dump_arc g.entries +let domain = G.domain +let choose = G.choose + +let dump_universes = G.dump + +let check_universes_invariants g = G.check_invariants ~required_canonical:Level.is_small g + +let pr_universes = G.pr + +let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] +let make_dummy i = Level.(make (UGlobal.make dummy_mp i)) +let sort_universes g = G.sort make_dummy [Level.prop;Level.set] g (** Profiling *) -let merge_constraints = - if Flags.profile then +let merge_constraints = + if Flags.profile then let key = CProfile.declare_profile "merge_constraints" in CProfile.profile2 key merge_constraints else merge_constraints @@ -1005,15 +186,14 @@ let check_constraints = CProfile.profile2 key check_constraints else check_constraints -let check_eq = +let check_eq = if Flags.profile then let check_eq_key = CProfile.declare_profile "check_eq" in CProfile.profile3 check_eq_key check_eq else check_eq -let check_leq = - if Flags.profile then +let check_leq = + if Flags.profile then let check_leq_key = CProfile.declare_profile "check_leq" in CProfile.profile3 check_leq_key check_leq else check_leq - diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 4dbfac5c73..e1a5d50425 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -22,9 +22,6 @@ val check_eq_level : Level.t check_function (** The initial graph of universes: Prop < Set *) val initial_universes : t -(** Check if we are in the initial case *) -val is_initial_universes : t -> bool - (** Check equality of instances w.r.t. a universe graph *) val check_eq_instances : Instance.t check_function diff --git a/kernel/univ.ml b/kernel/univ.ml index d7c0cf13ec..8940c0337e 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -533,9 +533,9 @@ open Universe let universe_level = Universe.level -type constraint_type = Lt | Le | Eq +type constraint_type = AcyclicGraph.constraint_type = Lt | Le | Eq -type explanation = (constraint_type * universe) list +type explanation = (constraint_type * Level.t) list let constraint_type_ord c1 c2 = match c1, c2 with | Lt, Lt -> 0 @@ -1269,7 +1269,7 @@ let hcons_universe_context_set (v, c) = let hcons_univ x = Universe.hcons x -let explain_universe_inconsistency prl (o,u,v,p) = +let explain_universe_inconsistency prl (o,u,v,p : univ_inconsistency) = let pr_uni = Universe.pr_with prl in let pr_rel = function | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" @@ -1281,9 +1281,9 @@ let explain_universe_inconsistency prl (o,u,v,p) = if p = [] then mt () else str " because" ++ spc() ++ pr_uni v ++ - prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v) + prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ prl v) p ++ - (if Universe.equal (snd (List.last p)) u then mt() else + (if Universe.equal (Universe.make (snd (List.last p))) u then mt() else (spc() ++ str "= " ++ pr_uni u)) in str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++ diff --git a/kernel/univ.mli b/kernel/univ.mli index d7097be570..b83251e983 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -166,7 +166,7 @@ val univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t (** {6 Constraints. } *) -type constraint_type = Lt | Le | Eq +type constraint_type = AcyclicGraph.constraint_type = Lt | Le | Eq type univ_constraint = Level.t * constraint_type * Level.t module Constraint : sig @@ -203,7 +203,7 @@ val enforce_leq_level : Level.t constraint_function system stores the graph and may result from combination of several Constraint.t... *) -type explanation = (constraint_type * Universe.t) list +type explanation = (constraint_type * Level.t) list type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Lazy.t option exception UniverseInconsistency of univ_inconsistency diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml new file mode 100644 index 0000000000..7d04c8f5a1 --- /dev/null +++ b/lib/acyclicGraph.ml @@ -0,0 +1,852 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type constraint_type = Lt | Le | Eq + +module type Point = sig + type t + + module Set : CSig.SetS with type elt = t + module Map : CMap.ExtS with type key = t and module Set := Set + + module Constraint : CSet.S with type elt = (t * constraint_type * t) + + val equal : t -> t -> bool + val compare : t -> t -> int + + type explanation = (constraint_type * t) list + val error_inconsistency : constraint_type -> t -> t -> explanation lazy_t option -> 'a + + val pr : t -> Pp.t +end + +module Make (Point:Point) = struct + + (* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *) + (* Functional code by Jean-Christophe Filliâtre for Coq V7.0 [1999] *) + (* Extension with algebraic universes by HH for Coq V7.0 [Sep 2001] *) + (* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *) + (* Support for universe polymorphism by MS [2014] *) + + (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu + Sozeau, Pierre-Marie Pédrot, Jacques-Henri Jourdan *) + + (* Points are stratified by a partial ordering $\le$. + Let $\~{}$ be the associated equivalence. We also have a strict ordering + $<$ between equivalence classes, and we maintain that $<$ is acyclic, + and contained in $\le$ in the sense that $[U]<[V]$ implies $U\le V$. + + At every moment, we have a finite number of points, and we + maintain the ordering in the presence of assertions $U<V$ and $U\le V$. + + The equivalence $\~{}$ is represented by a tree structure, as in the + union-find algorithm. The assertions $<$ and $\le$ are represented by + adjacency lists. + + We use the algorithm described in the paper: + + Bender, M. A., Fineman, J. T., Gilbert, S., & Tarjan, R. E. (2011). A + new approach to incremental cycle detection and related + problems. arXiv preprint arXiv:1112.0784. + + *) + + module PMap = Point.Map + module PSet = Point.Set + module Constraint = Point.Constraint + + type status = NoMark | Visited | WeakVisited | ToMerge + + (* Comparison on this type is pointer equality *) + type canonical_node = + { canon: Point.t; + ltle: bool PMap.t; (* true: strict (lt) constraint. + false: weak (le) constraint. *) + gtge: PSet.t; + rank : int; + klvl: int; + ilvl: int; + mutable status: status + } + + let big_rank = 1000000 + + (* A Point.t is either an alias for another one, or a canonical one, + for which we know the points that are above *) + + type entry = + | Canonical of canonical_node + | Equiv of Point.t + + type t = + { entries : entry PMap.t; + index : int; + n_nodes : int; n_edges : int } + + (** Used to cleanup mutable marks if a traversal function is + interrupted before it has the opportunity to do it itself. *) + let unsafe_cleanup_marks g = + let iter _ n = match n with + | Equiv _ -> () + | Canonical n -> n.status <- NoMark + in + PMap.iter iter g.entries + + let rec cleanup_marks g = + try unsafe_cleanup_marks g + with e -> + (* The only way unsafe_cleanup_marks may raise an exception is when + a serious error (stack overflow, out of memory) occurs, or a signal is + sent. In this unlikely event, we relaunch the cleanup until we finally + succeed. *) + cleanup_marks g; raise e + + (* Every Point.t has a unique canonical arc representative *) + + (* Low-level function : makes u an alias for v. + Does not removes edges from n_edges, but decrements n_nodes. + u should be entered as canonical before. *) + let enter_equiv g u v = + { entries = + PMap.modify u (fun _ a -> + match a with + | Canonical n -> + n.status <- NoMark; + Equiv v + | _ -> assert false) g.entries; + index = g.index; + n_nodes = g.n_nodes - 1; + n_edges = g.n_edges } + + (* Low-level function : changes data associated with a canonical node. + Resets the mutable fields in the old record, in order to avoid breaking + invariants for other users of this record. + n.canon should already been inserted as a canonical node. *) + let change_node g n = + { g with entries = + PMap.modify n.canon + (fun _ a -> + match a with + | Canonical n' -> + n'.status <- NoMark; + Canonical n + | _ -> assert false) + g.entries } + + (* canonical representative : we follow the Equiv links *) + let rec repr g u = + match PMap.find u g.entries with + | Equiv v -> repr g v + | Canonical arc -> arc + | exception Not_found -> + CErrors.anomaly ~label:"Univ.repr" + Pp.(str"Universe " ++ Point.pr u ++ str" undefined.") + + exception AlreadyDeclared + + (* Reindexes the given point, using the next available index. *) + let use_index g u = + let u = repr g u in + let g = change_node g { u with ilvl = g.index } in + assert (g.index > min_int); + { g with index = g.index - 1 } + + (* [safe_repr] is like [repr] but if the graph doesn't contain the + searched point, we add it. *) + let safe_repr g u = + let rec safe_repr_rec entries u = + match PMap.find u entries with + | Equiv v -> safe_repr_rec entries v + | Canonical arc -> arc + in + try g, safe_repr_rec g.entries u + with Not_found -> + let can = + { canon = u; + ltle = PMap.empty; gtge = PSet.empty; + rank = 0; + klvl = 0; ilvl = 0; + status = NoMark } + in + let g = { g with + entries = PMap.add u (Canonical can) g.entries; + n_nodes = g.n_nodes + 1 } + in + let g = use_index g u in + g, repr g u + + (* Returns 1 if u is higher than v in topological order. + -1 lower + 0 if u = v *) + let topo_compare u v = + if u.klvl > v.klvl then 1 + else if u.klvl < v.klvl then -1 + else if u.ilvl > v.ilvl then 1 + else if u.ilvl < v.ilvl then -1 + else (assert (u==v); 0) + + (* Checks most of the invariants of the graph. For debugging purposes. *) + let check_invariants ~required_canonical g = + let n_edges = ref 0 in + let n_nodes = ref 0 in + PMap.iter (fun l u -> + match u with + | Canonical u -> + PMap.iter (fun v _strict -> + incr n_edges; + let v = repr g v in + assert (topo_compare u v = -1); + if u.klvl = v.klvl then + assert (PSet.mem u.canon v.gtge || + PSet.exists (fun l -> u == repr g l) v.gtge)) + u.ltle; + PSet.iter (fun v -> + let v = repr g v in + assert (v.klvl = u.klvl && + (PMap.mem u.canon v.ltle || + PMap.exists (fun l _ -> u == repr g l) v.ltle)) + ) u.gtge; + assert (u.status = NoMark); + assert (Point.equal l u.canon); + assert (u.ilvl > g.index); + assert (not (PMap.mem u.canon u.ltle)); + incr n_nodes + | Equiv _ -> assert (not (required_canonical l))) + g.entries; + assert (!n_edges = g.n_edges); + assert (!n_nodes = g.n_nodes) + + let clean_ltle g ltle = + PMap.fold (fun u strict acc -> + let uu = (repr g u).canon in + if Point.equal uu u then acc + else ( + let acc = PMap.remove u (fst acc) in + if not strict && PMap.mem uu acc then (acc, true) + else (PMap.add uu strict acc, true))) + ltle (ltle, false) + + let clean_gtge g gtge = + PSet.fold (fun u acc -> + let uu = (repr g u).canon in + if Point.equal uu u then acc + else PSet.add uu (PSet.remove u (fst acc)), true) + gtge (gtge, false) + + (* [get_ltle] and [get_gtge] return ltle and gtge arcs. + Moreover, if one of these lists is dirty (e.g. points to a + non-canonical node), these functions clean this node in the + graph by removing some duplicate edges *) + let get_ltle g u = + let ltle, chgt_ltle = clean_ltle g u.ltle in + if not chgt_ltle then u.ltle, u, g + else + let sz = PMap.cardinal u.ltle in + let sz2 = PMap.cardinal ltle in + let u = { u with ltle } in + let g = change_node g u in + let g = { g with n_edges = g.n_edges + sz2 - sz } in + u.ltle, u, g + + let get_gtge g u = + let gtge, chgt_gtge = clean_gtge g u.gtge in + if not chgt_gtge then u.gtge, u, g + else + let u = { u with gtge } in + let g = change_node g u in + u.gtge, u, g + + (* [revert_graph] rollbacks the changes made to mutable fields in + nodes in the graph. + [to_revert] contains the touched nodes. *) + let revert_graph to_revert g = + List.iter (fun t -> + match PMap.find t g.entries with + | Equiv _ -> () + | Canonical t -> + t.status <- NoMark) to_revert + + exception AbortBackward of t + exception CycleDetected + + (* Implementation of the algorithm described in § 5.1 of the following paper: + + Bender, M. A., Fineman, J. T., Gilbert, S., & Tarjan, R. E. (2011). A + new approach to incremental cycle detection and related + problems. arXiv preprint arXiv:1112.0784. + + The "STEP X" comments contained in this file refers to the + corresponding step numbers of the algorithm described in Section + 5.1 of this paper. *) + + (* [delta] is the timeout for backward search. It might be + useful to tune a multiplicative constant. *) + let get_delta g = + int_of_float + (min (float_of_int g.n_edges ** 0.5) + (float_of_int g.n_nodes ** (2./.3.))) + + let rec backward_traverse to_revert b_traversed count g x = + let x = repr g x in + let count = count - 1 in + if count < 0 then begin + revert_graph to_revert g; + raise (AbortBackward g) + end; + if x.status = NoMark then begin + x.status <- Visited; + let to_revert = x.canon::to_revert in + let gtge, x, g = get_gtge g x in + let to_revert, b_traversed, count, g = + PSet.fold (fun y (to_revert, b_traversed, count, g) -> + backward_traverse to_revert b_traversed count g y) + gtge (to_revert, b_traversed, count, g) + in + to_revert, x.canon::b_traversed, count, g + end + else to_revert, b_traversed, count, g + + let rec forward_traverse f_traversed g v_klvl x y = + let y = repr g y in + if y.klvl < v_klvl then begin + let y = { y with klvl = v_klvl; + gtge = if x == y then PSet.empty + else PSet.singleton x.canon } + in + let g = change_node g y in + let ltle, y, g = get_ltle g y in + let f_traversed, g = + PMap.fold (fun z _ (f_traversed, g) -> + forward_traverse f_traversed g v_klvl y z) + ltle (f_traversed, g) + in + y.canon::f_traversed, g + end else if y.klvl = v_klvl && x != y then + let g = change_node g + { y with gtge = PSet.add x.canon y.gtge } in + f_traversed, g + else f_traversed, g + + let rec find_to_merge to_revert g x v = + let x = repr g x in + match x.status with + | Visited -> false, to_revert | ToMerge -> true, to_revert + | NoMark -> + let to_revert = x::to_revert in + if Point.equal x.canon v then + begin x.status <- ToMerge; true, to_revert end + else + begin + let merge, to_revert = PSet.fold + (fun y (merge, to_revert) -> + let merge', to_revert = find_to_merge to_revert g y v in + merge' || merge, to_revert) x.gtge (false, to_revert) + in + x.status <- if merge then ToMerge else Visited; + merge, to_revert + end + | _ -> assert false + + let get_new_edges g to_merge = + (* Computing edge sets. *) + let to_merge_lvl = + List.fold_left (fun acc u -> PMap.add u.canon u acc) + PMap.empty to_merge + in + let ltle = + let fold _ n acc = + let fold u strict acc = + if strict then PMap.add u strict acc + else if PMap.mem u acc then acc + else PMap.add u false acc + in + PMap.fold fold n.ltle acc + in + PMap.fold fold to_merge_lvl PMap.empty + in + let ltle, _ = clean_ltle g ltle in + let ltle = + PMap.merge (fun _ a strict -> + match a, strict with + | Some _, Some true -> + (* There is a lt edge inside the new component. This is a + "bad cycle". *) + raise CycleDetected + | Some _, Some false -> None + | _, _ -> strict + ) to_merge_lvl ltle + in + let gtge = + PMap.fold (fun _ n acc -> PSet.union acc n.gtge) + to_merge_lvl PSet.empty + in + let gtge, _ = clean_gtge g gtge in + let gtge = PSet.diff gtge (PMap.domain to_merge_lvl) in + (ltle, gtge) + + + let reorder g u v = + (* STEP 2: backward search in the k-level of u. *) + let delta = get_delta g in + + (* [v_klvl] is the chosen future level for u, v and all + traversed nodes. *) + let b_traversed, v_klvl, g = + try + let to_revert, b_traversed, _, g = backward_traverse [] [] delta g u in + revert_graph to_revert g; + let v_klvl = (repr g u).klvl in + b_traversed, v_klvl, g + with AbortBackward g -> + (* Backward search was too long, use the next k-level. *) + let v_klvl = (repr g u).klvl + 1 in + [], v_klvl, g + in + let f_traversed, g = + (* STEP 3: forward search. Contrary to what is described in + the paper, we do not test whether v_klvl = u.klvl nor we assign + v_klvl to v.klvl. Indeed, the first call to forward_traverse + will do all that. *) + forward_traverse [] g v_klvl (repr g v) v + in + + (* STEP 4: merge nodes if needed. *) + let to_merge, b_reindex, f_reindex = + if (repr g u).klvl = v_klvl then + begin + let merge, to_revert = find_to_merge [] g u v in + let r = + if merge then + List.filter (fun u -> u.status = ToMerge) to_revert, + List.filter (fun u -> (repr g u).status <> ToMerge) b_traversed, + List.filter (fun u -> (repr g u).status <> ToMerge) f_traversed + else [], b_traversed, f_traversed + in + List.iter (fun u -> u.status <- NoMark) to_revert; + r + end + else [], b_traversed, f_traversed + in + let to_reindex, g = + match to_merge with + | [] -> List.rev_append f_reindex b_reindex, g + | n0::q0 -> + (* Computing new root. *) + let root, rank_rest = + List.fold_left (fun ((best, _rank_rest) as acc) n -> + if n.rank >= best.rank then n, best.rank else acc) + (n0, min_int) q0 + in + let ltle, gtge = get_new_edges g to_merge in + (* Inserting the new root. *) + let g = change_node g + { root with ltle; gtge; + rank = max root.rank (rank_rest + 1); } + in + + (* Inserting shortcuts for old nodes. *) + let g = List.fold_left (fun g n -> + if Point.equal n.canon root.canon then g else enter_equiv g n.canon root.canon) + g to_merge + in + + (* Updating g.n_edges *) + let oldsz = + List.fold_left (fun sz u -> sz+PMap.cardinal u.ltle) + 0 to_merge + in + let sz = PMap.cardinal ltle in + let g = { g with n_edges = g.n_edges + sz - oldsz } in + + (* Not clear in the paper: we have to put the newly + created component just between B and F. *) + List.rev_append f_reindex (root.canon::b_reindex), g + + in + + (* STEP 5: reindex traversed nodes. *) + List.fold_left use_index g to_reindex + + (* Assumes [u] and [v] are already in the graph. *) + (* Does NOT assume that ucan != vcan. *) + let insert_edge strict ucan vcan g = + try + let u = ucan.canon and v = vcan.canon in + (* STEP 1: do we need to reorder nodes ? *) + let g = if topo_compare ucan vcan <= 0 then g else reorder g u v in + + (* STEP 6: insert the new edge in the graph. *) + let u = repr g u in + let v = repr g v in + if u == v then + if strict then raise CycleDetected else g + else + let g = + try let oldstrict = PMap.find v.canon u.ltle in + if strict && not oldstrict then + change_node g { u with ltle = PMap.add v.canon true u.ltle } + else g + with Not_found -> + { (change_node g { u with ltle = PMap.add v.canon strict u.ltle }) + with n_edges = g.n_edges + 1 } + in + if u.klvl <> v.klvl || PSet.mem u.canon v.gtge then g + else + let v = { v with gtge = PSet.add u.canon v.gtge } in + change_node g v + with + | CycleDetected as e -> raise e + | e -> + (* Unlikely event: fatal error or signal *) + let () = cleanup_marks g in + raise e + + let add ?(rank=0) v g = + try + let _arcv = PMap.find v g.entries in + raise AlreadyDeclared + with Not_found -> + assert (g.index > min_int); + let node = { + canon = v; + ltle = PMap.empty; + gtge = PSet.empty; + rank; + klvl = 0; + ilvl = g.index; + status = NoMark; + } + in + let entries = PMap.add v (Canonical node) g.entries in + { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges } + + exception Undeclared of Point.t + let check_declared g us = + let check l = if not (PMap.mem l g.entries) then raise (Undeclared l) in + PSet.iter check us + + exception Found_explanation of (constraint_type * Point.t) list + + let get_explanation strict u v g = + let v = repr g v in + let visited_strict = ref PMap.empty in + let rec traverse strict u = + if u == v then + if strict then None else Some [] + else if topo_compare u v = 1 then None + else + let visited = + try not (PMap.find u.canon !visited_strict) || strict + with Not_found -> false + in + if visited then None + else begin + visited_strict := PMap.add u.canon strict !visited_strict; + try + PMap.iter (fun u' strictu' -> + match traverse (strict && not strictu') (repr g u') with + | None -> () + | Some exp -> + let typ = if strictu' then Lt else Le in + raise (Found_explanation ((typ, u') :: exp))) + u.ltle; + None + with Found_explanation exp -> Some exp + end + in + let u = repr g u in + if u == v then [(Eq, v.canon)] + else match traverse strict u with Some exp -> exp | None -> assert false + + let get_explanation strict u v g = + Some (lazy (get_explanation strict u v g)) + + (* To compare two nodes, we simply do a forward search. + We implement two improvements: + - we ignore nodes that are higher than the destination; + - we do a BFS rather than a DFS because we expect to have a short + path (typically, the shortest path has length 1) + *) + exception Found of canonical_node list + let search_path strict u v g = + let rec loop to_revert todo next_todo = + match todo, next_todo with + | [], [] -> to_revert (* No path found *) + | [], _ -> loop to_revert next_todo [] + | (u, strict)::todo, _ -> + if u.status = Visited || (u.status = WeakVisited && strict) + then loop to_revert todo next_todo + else + let to_revert = + if u.status = NoMark then u::to_revert else to_revert + in + u.status <- if strict then WeakVisited else Visited; + if try PMap.find v.canon u.ltle || not strict + with Not_found -> false + then raise (Found to_revert) + else + begin + let next_todo = + PMap.fold (fun u strictu next_todo -> + let strict = not strictu && strict in + let u = repr g u in + if u == v && not strict then raise (Found to_revert) + else if topo_compare u v = 1 then next_todo + else (u, strict)::next_todo) + u.ltle next_todo + in + loop to_revert todo next_todo + end + in + if u == v then not strict + else + try + let res, to_revert = + try false, loop [] [u, strict] [] + with Found to_revert -> true, to_revert + in + List.iter (fun u -> u.status <- NoMark) to_revert; + res + with e -> + (* Unlikely event: fatal error or signal *) + let () = cleanup_marks g in + raise e + + (** Uncomment to debug the cycle detection algorithm. *) + (*let insert_edge strict ucan vcan g = + let check_invariants = check_invariants ~required_canonical:(fun _ -> false) in + check_invariants g; + let g = insert_edge strict ucan vcan g in + check_invariants g; + let ucan = repr g ucan.canon in + let vcan = repr g vcan.canon in + assert (search_path strict ucan vcan g); + g*) + + (** User interface *) + + type 'a check_function = t -> 'a -> 'a -> bool + + let check_eq g u v = + u == v || + let arcu = repr g u and arcv = repr g v in + arcu == arcv + + let check_smaller g strict u v = + search_path strict (repr g u) (repr g v) g + + let check_leq g u v = check_smaller g false u v + let check_lt g u v = check_smaller g true u v + + (* enforce_eq g u v will force u=v if possible, will fail otherwise *) + + let rec enforce_eq u v g = + let ucan = repr g u in + let vcan = repr g v in + if topo_compare ucan vcan = 1 then enforce_eq v u g + else + let g = insert_edge false ucan vcan g in (* Cannot fail *) + try insert_edge false vcan ucan g + with CycleDetected -> + Point.error_inconsistency Eq v u (get_explanation true u v g) + + (* enforce_leq g u v will force u<=v if possible, will fail otherwise *) + let enforce_leq u v g = + let ucan = repr g u in + let vcan = repr g v in + try insert_edge false ucan vcan g + with CycleDetected -> + Point.error_inconsistency Le u v (get_explanation true v u g) + + (* enforce_lt u v will force u<v if possible, will fail otherwise *) + let enforce_lt u v g = + let ucan = repr g u in + let vcan = repr g v in + try insert_edge true ucan vcan g + with CycleDetected -> + Point.error_inconsistency Lt u v (get_explanation false v u g) + + let empty = + { entries = PMap.empty; index = 0; n_nodes = 0; n_edges = 0 } + + (* Normalization *) + + (** [normalize g] returns a graph where all edges point + directly to the canonical representent of their target. The output + graph should be equivalent to the input graph from a logical point + of view, but optimized. We maintain the invariant that the key of + a [Canonical] element is its own name, by keeping [Equiv] edges. *) + let normalize g = + let g = + { g with + entries = PMap.map (fun entry -> + match entry with + | Equiv u -> Equiv ((repr g u).canon) + | Canonical ucan -> Canonical { ucan with rank = 1 }) + g.entries } + in + PMap.fold (fun _ u g -> + match u with + | Equiv _u -> g + | Canonical u -> + let _, u, g = get_ltle g u in + let _, _, g = get_gtge g u in + g) + g.entries g + + let constraints_of g = + let module UF = Unionfind.Make (PSet) (PMap) in + let uf = UF.create () in + let constraints_of u v acc = + match v with + | Canonical {canon=u; ltle; _} -> + PMap.fold (fun v strict acc-> + let typ = if strict then Lt else Le in + Constraint.add (u,typ,v) acc) ltle acc + | Equiv v -> UF.union u v uf; acc + in + let csts = PMap.fold constraints_of g.entries Constraint.empty in + csts, UF.partition uf + + (* domain g.entries = kept + removed *) + let constraints_for ~kept g = + (* rmap: partial map from canonical points to kept points *) + let rmap, csts = PSet.fold (fun u (rmap,csts) -> + let arcu = repr g u in + if PSet.mem arcu.canon kept then + PMap.add arcu.canon arcu.canon rmap, Constraint.add (u,Eq,arcu.canon) csts + else + match PMap.find arcu.canon rmap with + | v -> rmap, Constraint.add (u,Eq,v) csts + | exception Not_found -> PMap.add arcu.canon u rmap, csts) + kept (PMap.empty,Constraint.empty) + in + let rec add_from u csts todo = match todo with + | [] -> csts + | (v,strict)::todo -> + let v = repr g v in + (match PMap.find v.canon rmap with + | v -> + let d = if strict then Lt else Le in + let csts = Constraint.add (u,d,v) csts in + add_from u csts todo + | exception Not_found -> + (* v is not equal to any kept point *) + let todo = PMap.fold (fun v' strict' todo -> + (v',strict || strict') :: todo) + v.ltle todo + in + add_from u csts todo) + in + PSet.fold (fun u csts -> + let arc = repr g u in + PMap.fold (fun v strict csts -> add_from u csts [v,strict]) + arc.ltle csts) + kept csts + + let domain g = PMap.domain g.entries + + let choose p g u = + let exception Found of Point.t in + let ru = (repr g u).canon in + if p ru then Some ru + else + try PMap.iter (fun v -> function + | Canonical _ -> () (* we already tried [p ru] *) + | Equiv v' -> + let rv = (repr g v').canon in + if rv == ru && p v then raise (Found v) + (* NB: we could also try [p v'] but it will come up in the + rest of the iteration regardless. *) + ) g.entries; None + with Found v -> Some v + + let sort make_dummy first g = + let cans = + PMap.fold (fun _ u l -> + match u with + | Equiv _ -> l + | Canonical can -> can :: l + ) g.entries [] + in + let cans = List.sort topo_compare cans in + let lowest = + PMap.mapi (fun u _ -> if CList.mem_f Point.equal u first then 0 else 2) + (PMap.filter + (fun _ u -> match u with Equiv _ -> false | Canonical _ -> true) + g.entries) + in + let lowest = + List.fold_left (fun lowest can -> + let lvl = PMap.find can.canon lowest in + PMap.fold (fun u' strict lowest -> + let cost = if strict then 1 else 0 in + let u' = (repr g u').canon in + PMap.modify u' (fun _ lvl0 -> max lvl0 (lvl+cost)) lowest) + can.ltle lowest) + lowest cans + in + let max_lvl = PMap.fold (fun _ a b -> max a b) lowest 0 in + let types = Array.init (max_lvl + 1) (fun i -> + match List.nth_opt first i with + | Some u -> u + | None -> make_dummy (i-2)) + in + let g = Array.fold_left (fun g u -> + let g, u = safe_repr g u in + change_node g { u with rank = big_rank }) g types + in + let g = if max_lvl > List.length first && not (CList.is_empty first) then + enforce_lt (CList.last first) types.(List.length first) g + else g + in + let g = + PMap.fold (fun u lvl g -> enforce_eq u (types.(lvl)) g) + lowest g + in + normalize g + + (** Pretty-printing *) + + let pr_pmap sep pr map = + let cmp (u,_) (v,_) = Point.compare u v in + Pp.prlist_with_sep sep pr (List.sort cmp (PMap.bindings map)) + + let pr_arc prl = let open Pp in + function + | _, Canonical {canon=u; ltle; _} -> + if PMap.is_empty ltle then mt () + else + prl u ++ str " " ++ + v 0 + (pr_pmap spc (fun (v, strict) -> + (if strict then str "< " else str "<= ") ++ prl v) + ltle) ++ + fnl () + | u, Equiv v -> + prl u ++ str " = " ++ prl v ++ fnl () + + let pr prl g = + pr_pmap Pp.mt (pr_arc prl) g.entries + + (* Dumping constraints to a file *) + + let dump output g = + let dump_arc u = function + | Canonical {canon=u; ltle; _} -> + PMap.iter (fun v strict -> + let typ = if strict then Lt else Le in + output typ u v) ltle; + | Equiv v -> + output Eq u v + in + PMap.iter dump_arc g.entries + +end diff --git a/lib/acyclicGraph.mli b/lib/acyclicGraph.mli new file mode 100644 index 0000000000..b53a4c018f --- /dev/null +++ b/lib/acyclicGraph.mli @@ -0,0 +1,82 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Graphs representing strict orders *) + +type constraint_type = Lt | Le | Eq + +module type Point = sig + type t + + module Set : CSig.SetS with type elt = t + module Map : CMap.ExtS with type key = t and module Set := Set + + module Constraint : CSet.S with type elt = (t * constraint_type * t) + + val equal : t -> t -> bool + val compare : t -> t -> int + + type explanation = (constraint_type * t) list + val error_inconsistency : constraint_type -> t -> t -> explanation lazy_t option -> 'a + + val pr : t -> Pp.t +end + +module Make (Point:Point) : sig + + type t + + val empty : t + + val check_invariants : required_canonical:(Point.t -> bool) -> t -> unit + + exception AlreadyDeclared + val add : ?rank:int -> Point.t -> t -> t + (** All points must be pre-declared through this function before + they can be mentioned in the others. NB: use a large [rank] to + keep the node canonical *) + + exception Undeclared of Point.t + val check_declared : t -> Point.Set.t -> unit + (** @raise Undeclared if one of the points is not present in the graph. *) + + type 'a check_function = t -> 'a -> 'a -> bool + + val check_eq : Point.t check_function + val check_leq : Point.t check_function + val check_lt : Point.t check_function + + val enforce_eq : Point.t -> Point.t -> t -> t + val enforce_leq : Point.t -> Point.t -> t -> t + val enforce_lt : Point.t -> Point.t -> t -> t + + val constraints_of : t -> Point.Constraint.t * Point.Set.t list + + val constraints_for : kept:Point.Set.t -> t -> Point.Constraint.t + + val domain : t -> Point.Set.t + + val choose : (Point.t -> bool) -> t -> Point.t -> Point.t option + + val sort : (int -> Point.t) -> Point.t list -> t -> t + (** [sort mk first g] builds a totally ordered graph. The output + graph should imply the input graph (and the implication will be + strict most of the time), but is not necessarily minimal. The + lowest points in the result are identified with [first]. + Moreover, it adds levels [Type.n] to identify the points (not in + [first]) at level n. An artificial constraint (last first < mk + (length first)) is added to ensure that they are not merged. + Note: the result is unspecified if the input graph already + contains [mk n] nodes. *) + + val pr : (Point.t -> Pp.t) -> t -> Pp.t + + val dump : (constraint_type -> Point.t -> Point.t -> unit) -> t -> unit +end diff --git a/lib/lib.mllib b/lib/lib.mllib index 206b2504db..2db59712b9 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -11,6 +11,7 @@ Feedback CErrors CWarnings +AcyclicGraph Rtree System Explore |