summaryrefslogtreecommitdiff
path: root/kernel/univ.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/univ.ml')
-rw-r--r--kernel/univ.ml111
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