Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

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