diff options
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 834 |
1 files changed, 0 insertions, 834 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 34eb283d7..7e6d4de23 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -653,170 +653,6 @@ open Universe let universe_level = Universe.level -type status = Unset | SetLe | SetLt - -(* Comparison on this type is pointer equality *) -type canonical_arc = - { univ: Level.t; - lt: Level.t list; - le: Level.t list; - rank : int; - mutable status : status; - (** Guaranteed to be unset out of the [compare_neq] functions. It is used - to do an imperative traversal of the graph, ensuring a O(1) check that - a node has already been visited. Quite performance critical indeed. *) - } - -let arc_is_le arc = match arc.status with -| Unset -> false -| SetLe | SetLt -> true - -let arc_is_lt arc = match arc.status with -| Unset | SetLe -> false -| SetLt -> true - -let terminal u = {univ=u; lt=[]; le=[]; rank=0; status = Unset} - -module UMap : -sig - type key = Level.t - type +'a t - val empty : 'a t - val add : key -> 'a -> 'a t -> 'a t - val find : key -> 'a t -> 'a - val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool - val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b - val iter : (key -> 'a -> unit) -> 'a t -> unit - val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t -end = HMap.Make(Level) - -(* 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_arc - | Equiv of Level.t - -type universes = univ_entry UMap.t - -(** 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 _ arc = match arc with - | Equiv _ -> () - | Canonical arc -> arc.status <- Unset - in - UMap.iter iter g - -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 - -let enter_equiv_arc u v g = - UMap.add u (Equiv v) g - -let enter_arc ca g = - UMap.add ca.univ (Canonical ca) g - -(* Every Level.t has a unique canonical arc representative *) - -(** The graph always contains nodes for Prop and Set. *) - -let terminal_lt u v = - {(terminal u) with lt=[v]} - -let empty_universes = - let g = enter_arc (terminal Level.set) UMap.empty in - let g = enter_arc (terminal_lt Level.prop Level.set) g in - g - -(* repr : universes -> Level.t -> canonical_arc *) -(* canonical representative : we follow the Equiv links *) - -let rec repr g u = - let a = - try UMap.find u g - with Not_found -> 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_prop_arc g = repr g Level.prop -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 - -let add_universe vlev strict g = - try - let _arcv = UMap.find vlev g in - raise AlreadyDeclared - with Not_found -> - let v = terminal vlev in - let arc = - let arc = get_set_arc g in - if strict then - { arc with lt=vlev::arc.lt} - else - { arc with le=vlev::arc.le} - in - let g = enter_arc arc g in - enter_arc v g - -(* reprleq : canonical_arc -> canonical_arc list *) -(* All canonical arcv such that arcu<=arcv with arcv#arcu *) -let reprleq g arcu = - let rec searchrec w = function - | [] -> w - | v :: vl -> - let arcv = repr g v in - if List.memq arcv w || arcu==arcv then - searchrec w vl - else - searchrec (arcv :: w) vl - in - searchrec [] arcu.le - - -(* between : Level.t -> canonical_arc -> canonical_arc list *) -(* between u v = { w | u<=w<=v, w canonical } *) -(* between is the most costly operation *) - -let between g arcu arcv = - (* good are all w | u <= w <= v *) - (* bad are all w | u <= w ~<= v *) - (* find good and bad nodes in {w | u <= w} *) - (* explore b u = (b or "u is good") *) - let rec explore ((good, bad, b) as input) arcu = - if List.memq arcu good then - (good, bad, true) (* b or true *) - else if List.memq arcu bad then - input (* (good, bad, b or false) *) - else - let leq = reprleq g arcu in - (* is some universe >= u good ? *) - let good, bad, b_leq = - List.fold_left explore (good, bad, false) leq - in - if b_leq then - arcu::good, bad, true (* b or true *) - else - good, arcu::bad, b (* b or false *) - in - let good,_,_ = explore ([arcv],[],false) arcu in - good -(* We assume compare(u,v) = LE with v canonical (see compare below). - In this case List.hd(between g u v) = repr u - Otherwise, between g u v = [] - *) type constraint_type = Lt | Le | Eq @@ -831,343 +667,6 @@ let constraint_type_ord c1 c2 = match c1, c2 with | Eq, Eq -> 0 | Eq, _ -> 1 -(** [fast_compare_neq] : is [arcv] in the transitive upward closure of [arcu] ? - - In [strict] mode, we fully distinguish between LE and LT, while in - non-strict mode, we simply answer LE for both situations. - - If [arcv] is encountered in a LT part, we could directly answer - without visiting unneeded parts of this transitive closure. - In [strict] mode, if [arcv] is encountered in a LE part, we could only - change the default answer (1st arg [c]) from NLE to LE, since a strict - constraint may appear later. During the recursive traversal, - [lt_done] and [le_done] are universes we have already visited, - they do not contain [arcv]. The 4rd arg is [(lt_todo,le_todo)], - two lists of universes not yet considered, known to be above [arcu], - strictly or not. - - We use depth-first search, but the presence of [arcv] in [new_lt] - is checked as soon as possible : this seems to be slightly faster - on a test. - - We do the traversal imperatively, setting the [status] flag on visited nodes. - This ensures O(1) check, but it also requires unsetting the flag when leaving - the function. Some special care has to be taken in order to ensure we do not - recover a messed up graph at the end. This occurs in particular when the - traversal raises an exception. Even though the code below is exception-free, - OCaml may still raise random exceptions, essentially fatal exceptions or - signal handlers. Therefore we ensure the cleanup by a catch-all clause. Note - also that the use of an imperative solution does make this function - thread-unsafe. For now we do not check universes in different threads, but if - ever this is to be done, we would need some lock somewhere. - -*) - -let get_explanation strict g arcu arcv = - (* [c] characterizes whether (and how) arcv has already been related - to arcu among the lt_done,le_done universe *) - let rec cmp c to_revert lt_todo le_todo = match lt_todo, le_todo with - | [],[] -> (to_revert, c) - | (arc,p)::lt_todo, le_todo -> - if arc_is_lt arc then - cmp c to_revert lt_todo le_todo - else - let rec find lt_todo lt le = match le with - | [] -> - begin match lt with - | [] -> - let () = arc.status <- SetLt in - cmp c (arc :: to_revert) lt_todo le_todo - | u :: lt -> - let arc = repr g u in - let p = (Lt, make u) :: p in - if arc == arcv then - if strict then (to_revert, p) else (to_revert, p) - else find ((arc, p) :: lt_todo) lt le - end - | u :: le -> - let arc = repr g u in - let p = (Le, make u) :: p in - if arc == arcv then - if strict then (to_revert, p) else (to_revert, p) - else find ((arc, p) :: lt_todo) lt le - in - find lt_todo arc.lt arc.le - | [], (arc,p)::le_todo -> - if arc == arcv then - (* No need to continue inspecting universes above arc: - if arcv is strictly above arc, then we would have a cycle. - But we cannot answer LE yet, a stronger constraint may - come later from [le_todo]. *) - if strict then cmp p to_revert [] le_todo else (to_revert, p) - else - if arc_is_le arc then - cmp c to_revert [] le_todo - else - let rec find lt_todo lt = match lt with - | [] -> - let fold accu u = - let p = (Le, make u) :: p in - let node = (repr g u, p) in - node :: accu - in - let le_new = List.fold_left fold le_todo arc.le in - let () = arc.status <- SetLe in - cmp c (arc :: to_revert) lt_todo le_new - | u :: lt -> - let arc = repr g u in - let p = (Lt, make u) :: p in - if arc == arcv then - if strict then (to_revert, p) else (to_revert, p) - else find ((arc, p) :: lt_todo) lt - in - find [] arc.lt - in - let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in - try - let (to_revert, c) = cmp start [] [] [(arcu, [])] in - (** Reset all the touched arcs. *) - let () = List.iter (fun arc -> arc.status <- Unset) to_revert in - List.rev c - with e -> - (** Unlikely event: fatal error or signal *) - let () = cleanup_universes g in - raise e - -let get_explanation strict g arcu arcv = - if !Flags.univ_print then Some (get_explanation strict g arcu arcv) - else None - -type fast_order = FastEQ | FastLT | FastLE | FastNLE - -let fast_compare_neq strict g arcu arcv = - (* [c] characterizes whether arcv has already been related - to arcu among the lt_done,le_done universe *) - let rec cmp c to_revert lt_todo le_todo = match lt_todo, le_todo with - | [],[] -> (to_revert, c) - | arc::lt_todo, le_todo -> - if arc_is_lt arc then - cmp c to_revert lt_todo le_todo - else - let () = arc.status <- SetLt in - process_lt c (arc :: to_revert) lt_todo le_todo arc.lt arc.le - | [], arc::le_todo -> - if arc == arcv then - (* No need to continue inspecting universes above arc: - if arcv is strictly above arc, then we would have a cycle. - But we cannot answer LE yet, a stronger constraint may - come later from [le_todo]. *) - if strict then cmp FastLE to_revert [] le_todo else (to_revert, FastLE) - else - if arc_is_le arc then - cmp c to_revert [] le_todo - else - let () = arc.status <- SetLe in - process_le c (arc :: to_revert) [] le_todo arc.lt arc.le - - and process_lt c to_revert lt_todo le_todo lt le = match le with - | [] -> - begin match lt with - | [] -> cmp c to_revert lt_todo le_todo - | u :: lt -> - let arc = repr g u in - if arc == arcv then - if strict then (to_revert, FastLT) else (to_revert, FastLE) - else process_lt c to_revert (arc :: lt_todo) le_todo lt le - end - | u :: le -> - let arc = repr g u in - if arc == arcv then - if strict then (to_revert, FastLT) else (to_revert, FastLE) - else process_lt c to_revert (arc :: lt_todo) le_todo lt le - - and process_le c to_revert lt_todo le_todo lt le = match lt with - | [] -> - let fold accu u = - let node = repr g u in - node :: accu - in - let le_new = List.fold_left fold le_todo le in - cmp c to_revert lt_todo le_new - | u :: lt -> - let arc = repr g u in - if arc == arcv then - if strict then (to_revert, FastLT) else (to_revert, FastLE) - else process_le c to_revert (arc :: lt_todo) le_todo lt le - - in - try - let (to_revert, c) = cmp FastNLE [] [] [arcu] in - (** Reset all the touched arcs. *) - let () = List.iter (fun arc -> arc.status <- Unset) to_revert in - c - with e -> - (** Unlikely event: fatal error or signal *) - let () = cleanup_universes g in - raise e - -let get_explanation_strict g arcu arcv = get_explanation true g arcu arcv - -let fast_compare g arcu arcv = - if arcu == arcv then FastEQ else fast_compare_neq true g arcu arcv - -let is_leq g arcu arcv = - arcu == arcv || - (match fast_compare_neq false g arcu arcv with - | FastNLE -> false - | (FastEQ|FastLE|FastLT) -> true) - -let is_lt g arcu arcv = - if arcu == arcv then false - else - match fast_compare_neq true g arcu arcv with - | FastLT -> true - | (FastEQ|FastLE|FastNLE) -> false - -(* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ - compare(u,v) = LT or LE => compare(v,u) = NLE - compare(u,v) = NLE => compare(v,u) = NLE or LE or LT - - Adding u>=v is consistent iff compare(v,u) # LT - and then it is redundant iff compare(u,v) # NLE - Adding u>v is consistent iff compare(v,u) = NLE - and then it is redundant iff compare(u,v) = LT *) - -(** * Universe checks [check_eq] and [check_leq], used in coqchk *) - -(** 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 - is_lt g arcu arcv - else - is_prop_arc arcu - || (is_set_arc arcu && not (is_prop_arc arcv)) - || is_leq g arcu arcv - -(** Then, checks on universes *) - -type 'a check_function = universes -> 'a -> 'a -> bool - -let check_equal_expr g x y = - x == y || (let (u, n) = x and (v, m) = y in - Int.equal n m && check_equal g u v) - -let check_eq_univs g l1 l2 = - let f x1 x2 = check_equal_expr g x1 x2 in - let exists x1 l = Huniv.exists (fun x2 -> f x1 x2) l in - Huniv.for_all (fun x1 -> exists x1 l2) l1 - && Huniv.for_all (fun x2 -> exists x2 l1) l2 - -let check_eq g u v = - Universe.equal u v || check_eq_univs g u v - -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 - | _ -> false - -let exists_bigger g ul l = - Huniv.exists (fun ul' -> - check_smaller_expr g ul ul') l - -let real_check_leq g u v = - Huniv.for_all (fun ul -> exists_bigger g ul v) u - -let check_leq g u v = - Universe.equal u v || - Universe.is_type0m u || - check_eq_univs g u v || real_check_leq g u v - -(** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *) - -(* setlt : Level.t -> Level.t -> reason -> unit *) -(* forces u > v *) -(* this is normally an update of u in g rather than a creation. *) -let setlt g arcu arcv = - let arcu' = {arcu with lt=arcv.univ::arcu.lt} in - enter_arc arcu' g, arcu' - -(* checks that non-redundant *) -let setlt_if (g,arcu) v = - let arcv = repr g v in - if is_lt g arcu arcv then g, arcu - else setlt g arcu arcv - -(* setleq : Level.t -> Level.t -> unit *) -(* forces u >= v *) -(* this is normally an update of u in g rather than a creation. *) -let setleq g arcu arcv = - let arcu' = {arcu with le=arcv.univ::arcu.le} in - enter_arc arcu' g, arcu' - -(* checks that non-redundant *) -let setleq_if (g,arcu) v = - let arcv = repr g v in - if is_leq g arcu arcv then g, arcu - else setleq g arcu arcv - -(* merge : Level.t -> Level.t -> unit *) -(* we assume compare(u,v) = LE *) -(* merge u v forces u ~ v with repr u as canonical repr *) -let merge g arcu arcv = - (* we find the arc with the biggest rank, and we redirect all others to it *) - let arcu, g, v = - let best_ranked (max_rank, old_max_rank, best_arc, rest) arc = - if Level.is_small arc.univ || - (arc.rank >= max_rank && not (Level.is_small best_arc.univ)) - then (arc.rank, max_rank, arc, best_arc::rest) - else (max_rank, old_max_rank, best_arc, arc::rest) - in - match between g arcu arcv with - | [] -> anomaly (str "Univ.between") - | arc::rest -> - let (max_rank, old_max_rank, best_arc, rest) = - List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in - if max_rank > old_max_rank then best_arc, g, rest - else begin - (* one redirected node also has max_rank *) - let arcu = {best_arc with rank = max_rank + 1} in - arcu, enter_arc arcu g, rest - end - in - let redirect (g,w,w') arcv = - let g' = enter_equiv_arc arcv.univ arcu.univ g in - (g',List.unionq arcv.lt w,arcv.le@w') - in - let (g',w,w') = List.fold_left redirect (g,[],[]) v in - let g_arcu = (g',arcu) in - let g_arcu = List.fold_left setlt_if g_arcu w in - let g_arcu = List.fold_left setleq_if g_arcu w' in - fst g_arcu - -(* merge_disc : Level.t -> Level.t -> unit *) -(* we assume compare(u,v) = compare(v,u) = NLE *) -(* merge_disc u v forces u ~ v with repr u as canonical repr *) -let merge_disc g arc1 arc2 = - let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in - let arcu, g = - if not (Int.equal arc1.rank arc2.rank) then arcu, g - else - let arcu = {arcu with rank = succ arcu.rank} in - arcu, enter_arc arcu g - in - let g' = enter_equiv_arc arcv.univ arcu.univ g in - let g_arcu = (g',arcu) in - let g_arcu = List.fold_left setlt_if g_arcu arcv.lt in - let g_arcu = List.fold_left setleq_if g_arcu arcv.le in - fst g_arcu - (* Universe inconsistency: error raised when trying to enforce a relation that would create a cycle in the graph of universes. *) @@ -1178,70 +677,10 @@ exception UniverseInconsistency of univ_inconsistency let error_inconsistency o u v (p:explanation option) = raise (UniverseInconsistency (o,make u,make v,p)) -(* enforce_univ_eq : Level.t -> Level.t -> unit *) -(* enforce_univ_eq u v will force u=v if possible, will fail otherwise *) - -let enforce_univ_eq u v g = - let arcu = repr g u and arcv = repr g v in - match fast_compare g arcu arcv with - | FastEQ -> g - | FastLT -> - let p = get_explanation_strict g arcu arcv in - error_inconsistency Eq v u p - | FastLE -> merge g arcu arcv - | FastNLE -> - (match fast_compare g arcv arcu with - | FastLT -> - let p = get_explanation_strict g arcv arcu in - error_inconsistency Eq u v p - | FastLE -> merge g arcv arcu - | FastNLE -> merge_disc g arcu arcv - | FastEQ -> anomaly (Pp.str "Univ.compare")) - -(* enforce_univ_leq : Level.t -> Level.t -> unit *) -(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *) -let enforce_univ_leq u v g = - let arcu = repr g u and arcv = repr g v in - if is_leq g arcu arcv then g - else - match fast_compare g arcv arcu with - | FastLT -> - let p = get_explanation_strict g arcv arcu in - error_inconsistency Le u v p - | FastLE -> merge g arcv arcu - | FastNLE -> fst (setleq g arcu arcv) - | FastEQ -> anomaly (Pp.str "Univ.compare") - -(* enforce_univ_lt u v will force u<v if possible, will fail otherwise *) -let enforce_univ_lt u v g = - let arcu = repr g u and arcv = repr g v in - match fast_compare g arcu arcv with - | FastLT -> g - | FastLE -> fst (setlt g arcu arcv) - | FastEQ -> error_inconsistency Lt u v (Some [(Eq,make v)]) - | FastNLE -> - match fast_compare_neq false g arcv arcu with - FastNLE -> fst (setlt g arcu arcv) - | FastEQ -> anomaly (Pp.str "Univ.compare") - | (FastLE|FastLT) -> - let p = get_explanation false g arcv arcu in - error_inconsistency Lt u v p - -(* Prop = Set is forbidden here. *) -let initial_universes = empty_universes - -let is_initial_universes g = UMap.equal (==) g initial_universes - (* Constraints and sets of constraints. *) type univ_constraint = Level.t * constraint_type * Level.t -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 pr_constraint_type op = let op_str = match op with | Lt -> " < " @@ -1276,8 +715,6 @@ end let empty_constraint = Constraint.empty let union_constraint = Constraint.union let eq_constraint = Constraint.equal -let merge_constraints c g = - Constraint.fold enforce_constraint c g type constraints = Constraint.t @@ -1378,218 +815,12 @@ let enforce_leq u v c = let enforce_leq_level u v c = if Level.equal u v then c else Constraint.add (u,Le,v) c -let check_constraint g (l,d,r) = - match d with - | Eq -> check_equal g l r - | Le -> check_smaller g false l r - | Lt -> check_smaller g true l r - -let check_constraints c g = - Constraint.for_all (check_constraint g) c - let enforce_univ_constraint (u,d,v) = match d with | Eq -> enforce_eq u v | Le -> enforce_leq u v | Lt -> enforce_leq (super u) v -(* Normalization *) - -let lookup_level u g = - try Some (UMap.find u g) with Not_found -> None - -(** [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 - (see the assertion)... I (Stéphane Glondu) am not sure if this - plays a role in the rest of the module. *) -let normalize_universes g = - let rec visit u arc cache = match lookup_level u cache with - | Some x -> x, cache - | None -> match Lazy.force arc with - | None -> - u, UMap.add u u cache - | Some (Canonical {univ=v; lt=_; le=_}) -> - v, UMap.add u v cache - | Some (Equiv v) -> - let v, cache = visit v (lazy (lookup_level v g)) cache in - v, UMap.add u v cache - in - let cache = UMap.fold - (fun u arc cache -> snd (visit u (Lazy.lazy_from_val (Some arc)) cache)) - g UMap.empty - in - let repr x = UMap.find x cache in - let lrepr us = List.fold_left - (fun e x -> LSet.add (repr x) e) LSet.empty us - in - let canonicalize u = function - | Equiv _ -> Equiv (repr u) - | Canonical {univ=v; lt=lt; le=le; rank=rank} -> - assert (u == v); - (* avoid duplicates and self-loops *) - let lt = lrepr lt and le = lrepr le in - let le = LSet.filter - (fun x -> x != u && not (LSet.mem x lt)) le - in - LSet.iter (fun x -> assert (x != u)) lt; - Canonical { - univ = v; - lt = LSet.elements lt; - le = LSet.elements le; - rank = rank; - status = Unset; - } - in - UMap.mapi canonicalize g - -let constraints_of_universes g = - let constraints_of u v acc = - match v with - | Canonical {univ=u; lt=lt; le=le} -> - let acc = List.fold_left (fun acc v -> Constraint.add (u,Lt,v) acc) acc lt in - let acc = List.fold_left (fun acc v -> Constraint.add (u,Le,v) acc) acc le in - acc - | Equiv v -> Constraint.add (u,Eq,v) acc - in - UMap.fold constraints_of g Constraint.empty - -let constraints_of_universes g = - constraints_of_universes (normalize_universes g) - -(** Longest path algorithm. This is used to compute the minimal number of - universes required if the only strict edge would be the Lt one. This - algorithm assumes that the given universes constraints are a almost DAG, in - the sense that there may be {Eq, Le}-cycles. This is OK for consistent - universes, which is the only case where we use this algorithm. *) - -(** Adjacency graph *) -type graph = constraint_type LMap.t LMap.t - -exception Connected - -(** Check connectedness *) -let connected x y (g : graph) = - let rec connected x target seen g = - if Level.equal x target then raise Connected - else if not (LSet.mem x seen) then - let seen = LSet.add x seen in - let fold z _ seen = connected z target seen g in - let neighbours = try LMap.find x g with Not_found -> LMap.empty in - LMap.fold fold neighbours seen - else seen - in - try ignore(connected x y LSet.empty g); false with Connected -> true - -let add_edge x y v (g : graph) = - try - let neighbours = LMap.find x g in - let neighbours = LMap.add y v neighbours in - LMap.add x neighbours g - with Not_found -> - LMap.add x (LMap.singleton y v) g - -(** We want to keep the graph DAG. If adding an edge would cause a cycle, that - would necessarily be an {Eq, Le}-cycle, otherwise there would have been a - universe inconsistency. Therefore we may omit adding such a cycling edge - without changing the compacted graph. *) -let add_eq_edge x y v g = if connected y x g then g else add_edge x y v g - -(** Construct the DAG and its inverse at the same time. *) -let make_graph g : (graph * graph) = - let fold u arc accu = match arc with - | Equiv v -> - let (dir, rev) = accu in - (add_eq_edge u v Eq dir, add_eq_edge v u Eq rev) - | Canonical { univ; lt; le; } -> - let () = assert (u == univ) in - let fold_lt (dir, rev) v = (add_edge u v Lt dir, add_edge v u Lt rev) in - let fold_le (dir, rev) v = (add_eq_edge u v Le dir, add_eq_edge v u Le rev) in - (** Order is important : lt after le, because of the possible redundancy - between [le] and [lt] in a canonical arc. This way, the [lt] constraint - is the last one set, which is correct because it implies [le]. *) - let accu = List.fold_left fold_le accu le in - let accu = List.fold_left fold_lt accu lt in - accu - in - UMap.fold fold g (LMap.empty, LMap.empty) - -(** Construct a topological order out of a DAG. *) -let rec topological_fold u g rem seen accu = - let is_seen = - try - let status = LMap.find u seen in - assert status; (** If false, not a DAG! *) - true - with Not_found -> false - in - if not is_seen then - let rem = LMap.remove u rem in - let seen = LMap.add u false seen in - let neighbours = try LMap.find u g with Not_found -> LMap.empty in - let fold v _ (rem, seen, accu) = topological_fold v g rem seen accu in - let (rem, seen, accu) = LMap.fold fold neighbours (rem, seen, accu) in - (rem, LMap.add u true seen, u :: accu) - else (rem, seen, accu) - -let rec topological g rem seen accu = - let node = try Some (LMap.choose rem) with Not_found -> None in - match node with - | None -> accu - | Some (u, _) -> - let rem, seen, accu = topological_fold u g rem seen accu in - topological g rem seen accu - -(** Compute the longest path from any vertex. *) -let constraint_cost = function -| Eq | Le -> 0 -| Lt -> 1 - -(** This algorithm browses the graph in topological order, computing for each - encountered node the length of the longest path leading to it. Should be - O(|V|) or so (modulo map representation). *) -let rec flatten_graph rem (rev : graph) map mx = match rem with -| [] -> map, mx -| u :: rem -> - let prev = try LMap.find u rev with Not_found -> LMap.empty in - let fold v cstr accu = - let v_cost = LMap.find v map in - max (v_cost + constraint_cost cstr) accu - in - let u_cost = LMap.fold fold prev 0 in - let map = LMap.add u u_cost map in - flatten_graph rem rev map (max mx u_cost) - -(** [sort_universes g] builds a map from universes in [g] to natural - numbers. It outputs a graph containing equivalence edges from each - level appearing in [g] to [Type.n], and [lt] edges between the - [Type.n]s. The output graph should imply the input graph (and the - [Type.n]s. The output graph should imply the input graph (and the - implication will be strict most of the time), but is not - necessarily minimal. 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 orig = - let (dir, rev) = make_graph orig in - let order = topological dir dir LMap.empty [] in - let compact, max = flatten_graph order rev LMap.empty 0 in - let mp = Names.DirPath.make [Names.Id.of_string "Type"] in - let types = Array.init (max + 1) (fun n -> Level.make mp n) in - (** Old universes are made equal to [Type.n] *) - let fold u level accu = UMap.add u (Equiv types.(level)) accu in - let sorted = LMap.fold fold compact UMap.empty in - (** Add all [Type.n] nodes *) - let fold i accu u = - if i < max then - let pred = types.(i + 1) in - let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in - UMap.add u (Canonical arc) accu - else accu - in - Array.fold_left_i fold sorted types - (* Miscellaneous functions to remove or test local univ assumed to occur in a universe *) @@ -1645,7 +876,6 @@ module Instance : sig val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds val levels : t -> LSet.t - val check_eq : t check_function end = struct type t = Level.t array @@ -1729,13 +959,6 @@ struct (* Necessary as universe instances might come from different modules and unmarshalling doesn't preserve sharing *)) - let check_eq g t1 t2 = - t1 == t2 || - (Int.equal (Array.length t1) (Array.length t2) && - let rec aux i = - (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1)) - in aux 0) - end let enforce_eq_instances x y = @@ -1985,27 +1208,6 @@ let abstract_universes poly ctx = (** Pretty-printing *) -let pr_arc prl = function - | _, Canonical {univ=u; lt=[]; le=[]} -> - mt () - | _, Canonical {univ=u; lt=lt; le=le} -> - let opt_sep = match lt, le with - | [], _ | _, [] -> mt () - | _ -> spc () - in - prl u ++ str " " ++ - v 0 - (pr_sequence (fun v -> str "< " ++ prl v) lt ++ - opt_sep ++ - pr_sequence (fun v -> str "<= " ++ prl v) le) ++ - fnl () - | u, Equiv v -> - prl u ++ str " = " ++ prl v ++ fnl () - -let pr_universes prl g = - let graph = UMap.fold (fun u a l -> (u,a)::l) g [] in - prlist (pr_arc prl) graph - let pr_constraints prl = Constraint.pr prl let pr_universe_context = UContext.pr @@ -2018,19 +1220,6 @@ let pr_universe_subst = let pr_universe_level_subst = LMap.pr (fun u -> str" := " ++ Level.pr u ++ spc ()) -(* Dumping constraints to a file *) - -let dump_universes output g = - let dump_arc u = function - | Canonical {univ=u; lt=lt; le=le} -> - let u_str = Level.to_string u in - List.iter (fun v -> output Lt (Level.to_string v) u_str) lt; - List.iter (fun v -> output Le (Level.to_string v) u_str) le - | Equiv v -> - output Eq (Level.to_string u) (Level.to_string v) - in - UMap.iter dump_arc g - module Huniverse_set = Hashcons.Make( struct @@ -2078,26 +1267,3 @@ let subst_instance_constraints = let key = Profile.declare_profile "subst_instance_constraints" in Profile.profile2 key subst_instance_constraints else subst_instance_constraints - -let merge_constraints = - if Flags.profile then - let key = Profile.declare_profile "merge_constraints" in - Profile.profile2 key merge_constraints - else merge_constraints -let check_constraints = - if Flags.profile then - let key = Profile.declare_profile "check_constraints" in - Profile.profile2 key check_constraints - else check_constraints - -let check_eq = - if Flags.profile then - let check_eq_key = Profile.declare_profile "check_eq" in - Profile.profile3 check_eq_key check_eq - else check_eq - -let check_leq = - if Flags.profile then - let check_leq_key = Profile.declare_profile "check_leq" in - Profile.profile3 check_leq_key check_leq - else check_leq |