diff options
Diffstat (limited to 'kernel')
| -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 |
4 files changed, 85 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 |