diff options
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 111 |
1 files changed, 68 insertions, 43 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index a8934544..0193542a 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -260,46 +260,62 @@ type order = EQ | LT | LE | NLE (** [compare_neq] : is [arcv] in the transitive upward closure of [arcu] ? - We try to avoid visiting unneeded parts of this transitive closure, - by stopping as soon as [arcv] is encountered. During the recursive - traversal, [lt_done] and [le_done] are universes we have already - visited, they do not contain [arcv]. The 3rd arg is - [(lt_todo,le_todo)], two lists of universes not yet considered, - known to be above [arcu], strictly or not. + 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. *) -let compare_neq g arcu arcv = - let rec cmp lt_done le_done = function - | [],[] -> NLE +let compare_neq strict g arcu arcv = + let rec cmp c lt_done le_done = function + | [],[] -> c | arc::lt_todo, le_todo -> if List.memq arc lt_done then - cmp lt_done le_done (lt_todo,le_todo) + cmp c lt_done le_done (lt_todo,le_todo) else let lt_new = can g (arc.lt@arc.le) in - if List.memq arcv lt_new then LT - else cmp (arc::lt_done) le_done (lt_new@lt_todo,le_todo) + if List.memq arcv lt_new then + if strict then LT else LE + else cmp c (arc::lt_done) le_done (lt_new@lt_todo,le_todo) | [], arc::le_todo -> - if arc == arcv then LE - (* No need to continue inspecting universes above arc: - if arcv is strictly above arc, then we would have a cycle *) + 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 LE lt_done le_done ([],le_todo) else LE else if (List.memq arc lt_done) || (List.memq arc le_done) then - cmp lt_done le_done ([],le_todo) + cmp c lt_done le_done ([],le_todo) else let lt_new = can g arc.lt in - if List.memq arcv lt_new then LT + if List.memq arcv lt_new then + if strict then LT else LE else let le_new = can g arc.le in - cmp lt_done (arc::le_done) (lt_new, le_new@le_todo) + cmp c lt_done (arc::le_done) (lt_new, le_new@le_todo) in - cmp [] [] ([],[arcu]) + cmp NLE [] [] ([],[arcu]) let compare g arcu arcv = - if arcu == arcv then EQ else compare_neq g arcu arcv + if arcu == arcv then EQ else compare_neq true g arcu arcv + +let is_leq g arcu arcv = + arcu == arcv || (compare_neq false g arcu arcv = LE) + +let is_lt g arcu arcv = (compare g arcu arcv = LT) (* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ compare(u,v) = LT or LE => compare(v,u) = NLE @@ -337,11 +353,11 @@ let rec check_eq g u v = let compare_greater g strict u v = let g, arcu = safe_repr g u in let g, arcv = safe_repr g v in - if not strict && arcv == snd (safe_repr g UniverseLevel.Set) then true else - match compare g arcv arcu with - | (EQ|LE) -> not strict - | LT -> true - | NLE -> false + if strict then + is_lt g arcv arcu + else + arcv == snd (safe_repr g UniverseLevel.Set) || is_leq g arcv arcu + (* let compare_greater g strict u v = let b = compare_greater g strict u v in @@ -368,9 +384,8 @@ let setlt g arcu arcv = (* checks that non-redundant *) let setlt_if (g,arcu) v = let arcv = repr g v in - match compare g arcu arcv with - | LT -> g, arcu - | _ -> setlt g arcu arcv + if is_lt g arcu arcv then g, arcu + else setlt g arcu arcv (* setleq : UniverseLevel.t -> UniverseLevel.t -> unit *) (* forces u >= v *) @@ -383,9 +398,8 @@ let setleq g arcu arcv = (* checks that non-redundant *) let setleq_if (g,arcu) v = let arcv = repr g v in - match compare g arcu arcv with - | NLE -> setleq g arcu arcv - | _ -> g, arcu + if is_leq g arcu arcv then g, arcu + else setleq g arcu arcv (* merge : UniverseLevel.t -> UniverseLevel.t -> unit *) (* we assume compare(u,v) = LE *) @@ -429,14 +443,12 @@ let error_inconsistency o u v = raise (UniverseInconsistency (o,Atom u,Atom v)) let enforce_univ_leq u v g = let g,arcu = safe_repr g u in let g,arcv = safe_repr g v in - match compare g arcu arcv with - | NLE -> - (match compare g arcv arcu with - | LT -> error_inconsistency Le u v - | LE -> merge g arcv arcu - | NLE -> fst (setleq g arcu arcv) - | EQ -> anomaly "Univ.compare") - | _ -> g + if is_leq g arcu arcv then g + else match compare g arcv arcu with + | LT -> error_inconsistency Le u v + | LE -> merge g arcv arcu + | NLE -> fst (setleq g arcu arcv) + | EQ -> anomaly "Univ.compare" (* enforc_univ_eq : UniverseLevel.t -> UniverseLevel.t -> unit *) (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) @@ -463,9 +475,8 @@ let enforce_univ_lt u v g = | LE -> fst (setlt g arcu arcv) | EQ -> error_inconsistency Lt u v | NLE -> - (match compare g arcv arcu with - | NLE -> fst (setlt g arcu arcv) - | _ -> error_inconsistency Lt u v) + if is_leq g arcv arcu then error_inconsistency Lt u v + else fst (setlt g arcu arcv) (* Constraints and sets of consrtaints. *) @@ -480,7 +491,13 @@ let enforce_constraint cst g = module Constraint = Set.Make( struct type t = univ_constraint - let compare = Pervasives.compare + let compare (u,c,v) (u',c',v') = + let i = Pervasives.compare c c' in + if i <> 0 then i + else + let i' = UniverseLevel.compare u u' in + if i' <> 0 then i' + else UniverseLevel.compare v v' end) type constraints = Constraint.t @@ -784,6 +801,14 @@ let no_upper_constraints u cst = | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst | Max _ -> anomaly "no_upper_constraints" +(* Is u mentionned in v (or equals to v) ? *) + +let univ_depends u v = + match u, v with + | Atom u, Atom v -> u = v + | Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl + | _ -> anomaly "univ_depends given a non-atomic 1st arg" + (* Pretty-printing *) let pr_arc = function |