diff options
Diffstat (limited to 'kernel/univ.ml')
-rw-r--r-- | kernel/univ.ml | 113 |
1 files changed, 69 insertions, 44 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 0646a501..869a60e2 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: univ.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: univ.ml 15019 2012-03-02 17:27:18Z letouzey $ *) (* Initial Caml version originates from CoC 4.8 [Dec 1988] *) (* Extension with algebraic universes by HH [Sep 2001] *) @@ -234,48 +234,66 @@ 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 u v = let arcu = repr g u and arcv = repr g v in - 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 u v = + let arcu = repr g u + and arcv = repr g v in + arcu == arcv || (compare_neq false g arcu arcv = LE) + +let is_lt g u v = (compare g u v = LT) (* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ compare(u,v) = LT or LE => compare(v,u) = NLE @@ -312,11 +330,11 @@ let rec check_eq g u v = let compare_greater g strict u v = let g = declare_univ u g in let g = declare_univ v g in - if not strict && compare_eq g v Set then true else - match compare g v u with - | (EQ|LE) -> not strict - | LT -> true - | NLE -> false + if strict then + is_lt g v u + else + compare_eq g v Set || is_leq g v u + (* let compare_greater g strict u v = let b = compare_greater g strict u v in @@ -340,9 +358,7 @@ let setlt g u v = enter_arc {arcu with lt=v::arcu.lt} g (* checks that non-redundant *) -let setlt_if g u v = match compare g u v with - | LT -> g - | _ -> setlt g u v +let setlt_if g u v = if is_lt g u v then g else setlt g u v (* setleq : universe_level -> universe_level -> unit *) (* forces u >= v *) @@ -352,9 +368,7 @@ let setleq g u v = (* checks that non-redundant *) -let setleq_if g u v = match compare g u v with - | NLE -> setleq g u v - | _ -> g +let setleq_if g u v = if is_leq g u v then g else setleq g u v (* merge : universe_level -> universe_level -> unit *) (* we assume compare(u,v) = LE *) @@ -398,14 +412,12 @@ let error_inconsistency o u v = raise (UniverseInconsistency (o,Atom u,Atom v)) let enforce_univ_leq u v g = let g = declare_univ u g in let g = declare_univ v g in - match compare g u v with - | NLE -> - (match compare g v u with - | LT -> error_inconsistency Le u v - | LE -> merge g v u - | NLE -> setleq g u v - | EQ -> anomaly "Univ.compare") - | _ -> g + if is_leq g u v then g + else match compare g v u with + | LT -> error_inconsistency Le u v + | LE -> merge g v u + | NLE -> setleq g u v + | EQ -> anomaly "Univ.compare" (* enforc_univ_eq : universe_level -> universe_level -> unit *) (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) @@ -432,9 +444,8 @@ let enforce_univ_lt u v g = | LE -> setlt g u v | EQ -> error_inconsistency Lt u v | NLE -> - (match compare g v u with - | NLE -> setlt g u v - | _ -> error_inconsistency Lt u v) + if is_leq g v u then error_inconsistency Lt u v + else setlt g u v (* Constraints and sets of consrtaints. *) @@ -452,7 +463,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' = cmp_univ_level u u' in + if i' <> 0 then i' + else cmp_univ_level v v' end) type constraints = Constraint.t @@ -557,6 +574,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 num_universes g = |