univ inconsistency error message gives evidence of a cycle

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15898 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 101 insertions, 51 deletions

diff --git a/.gitignore b/.gitignore
index 2b497f9a9..705967d0c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -50,6 +50,7 @@ dev/ocamldebug-coq
 plugins/micromega/csdpcert
 kernel/byterun/dllcoqrun.so
 coqdoc.sty
+csdp.cache
 test-suite/lia.cache
 test-suite/trace
 test-suite/misc/universes/all_stdlib.v
diff --git a/checker/checker.ml b/checker/checker.ml
index 8389803fc..8e0a2a1e5 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -252,12 +252,12 @@ let rec explain_exn = function
       hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
   | Sys.Break ->
       hov 0 (fnl () ++ str "User interrupt.")
-  | Univ.UniverseInconsistency (o,u,v) ->
+  | Univ.UniverseInconsistency (o,u,v,_) ->
       let msg =
 	if !Flags.debug (*!Constrextern.print_universes*) then
-	  spc() ++ str "(cannot enforce" ++ spc() ++ (*Univ.pr_uni u ++*) spc() ++
+	  spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
           str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=")
-	  ++ spc() ++ (*Univ.pr_uni v ++*) str")"
+	  ++ spc() ++ Univ.pr_uni v ++ str")"
 	else
 	  mt() in
       hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
diff --git a/kernel/univ.ml b/kernel/univ.ml
index f1fc8bda5..39cb6bc10 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -137,7 +137,9 @@ let sup u v =
 
 (* Comparison on this type is pointer equality *)
 type canonical_arc =
-    { univ: UniverseLevel.t; lt: UniverseLevel.t list; le: UniverseLevel.t list }
+    { univ: UniverseLevel.t;
+      lt: UniverseLevel.t list;
+      le: UniverseLevel.t list }
 
 let terminal u = {univ=u; lt=[]; le=[]}
 
@@ -267,8 +269,17 @@ let between g arcu arcv =
    Otherwise, between g u v = []
  *)
 
+type constraint_type = Lt | Le | Eq
+type explanation = (constraint_type * universe) list
+
+(* Assuming the current universe has been reached by [p] and [l]
+   correspond to the universes in (direct) relation [rel] with it,
+   make a list of canonical universe, updating the relation with
+   the starting point (path stored in reverse order). *)
+let canp g (p:explanation) rel l : (canonical_arc * explanation) list =
+  List.map (fun u -> (repr g u, (rel,Atom u)::p)) l
 
-type order = EQ | LT | LE | NLE
+type order = EQ | LT of explanation | LE of explanation | NLE
 
 (** [compare_neq] : is [arcv] in the transitive upward closure of [arcu] ?
 
@@ -291,43 +302,54 @@ type order = EQ | LT | LE | NLE
 *)
 
 let compare_neq 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 lt_done le_done = function
   | [],[] -> c
-  | arc::lt_todo, le_todo ->
+  | (arc,p)::lt_todo, le_todo ->
     if List.memq arc lt_done then
       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
-	if strict then LT else LE
-      else cmp c (arc::lt_done) le_done (lt_new@lt_todo,le_todo)
-  | [], arc::le_todo ->
+      let lt_new = canp g p Lt arc.lt@ canp g p Le arc.le in
+      (try
+	 let p = List.assq arcv lt_new in
+	 if strict then LT p else LE p
+       with Not_found ->
+	 cmp c (arc::lt_done) le_done (lt_new@lt_todo,le_todo))
+  | [], (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 LE lt_done le_done ([],le_todo) else LE
+      if strict then cmp (LE p) lt_done le_done ([],le_todo) else LE p
     else
       if (List.memq arc lt_done) || (List.memq arc le_done) then
 	cmp c lt_done le_done ([],le_todo)
       else
-	let lt_new = can g arc.lt in
-	if List.memq arcv lt_new then
-	  if strict then LT else LE
-	else
-	  let le_new = can g arc.le in
-	  cmp c lt_done (arc::le_done) (lt_new, le_new@le_todo)
+	let lt_new = canp g p Lt arc.lt in
+	(try
+	  let p = List.assq arcv lt_new in
+	  if strict then LT p else LE p
+	 with Not_found ->
+	   let le_new = canp g p Le arc.le in
+	   cmp c lt_done (arc::le_done) (lt_new, le_new@le_todo))
   in
-  cmp NLE [] [] ([],[arcu])
+  cmp NLE [] [] ([],[arcu,[]])
 
 let compare 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)
+  arcu == arcv ||
+ (match compare_neq false g arcu arcv with
+     NLE -> false
+   | (EQ|LE _|LT _) -> true)
 
-let is_lt g arcu arcv = (compare g arcu arcv = LT)
+let is_lt g arcu arcv =
+  match compare g arcu arcv with
+      LT _ -> true
+    | (EQ|LE _|NLE) -> false
 
 (* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ
                 compare(u,v) = LT or LE => compare(v,u) = NLE
@@ -385,7 +407,7 @@ let check_leq g u v =
 
 (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
 
-(* setlt : UniverseLevel.t -> UniverseLevel.t -> unit *)
+(* setlt : UniverseLevel.t -> UniverseLevel.t -> reason -> unit *)
 (* forces u > v *)
 (* this is normally an update of u in g rather than a creation. *)
 let setlt g arcu arcv =
@@ -443,11 +465,11 @@ let merge_disc g arcu arcv =
 (* Universe inconsistency: error raised when trying to enforce a relation
    that would create a cycle in the graph of universes. *)
 
-type constraint_type = Lt | Le | Eq
-
-exception UniverseInconsistency of constraint_type * universe * universe
+exception UniverseInconsistency of
+  constraint_type * universe * universe * explanation
 
-let error_inconsistency o u v = raise (UniverseInconsistency (o,Atom u,Atom v))
+let error_inconsistency o u v (p:explanation) =
+  raise (UniverseInconsistency (o,Atom u,Atom v,p))
 
 (* enforce_univ_leq : UniverseLevel.t -> UniverseLevel.t -> unit *)
 (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
@@ -456,8 +478,8 @@ let enforce_univ_leq u v g =
   let g,arcv = safe_repr g v in
   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
+    | LT p -> error_inconsistency Le u v (List.rev p)
+    | LE _ -> merge g arcv arcu
     | NLE -> fst (setleq g arcu arcv)
     | EQ -> anomaly "Univ.compare"
 
@@ -468,12 +490,12 @@ let enforce_univ_eq u v g =
   let g,arcv = safe_repr g v in
   match compare g arcu arcv with
     | EQ -> g
-    | LT -> error_inconsistency Eq u v
-    | LE -> merge g arcu arcv
+    | LT p -> error_inconsistency Eq u v (List.rev p)
+    | LE _ -> merge g arcu arcv
     | NLE ->
 	(match compare g arcv arcu with
-           | LT -> error_inconsistency Eq u v
-           | LE -> merge g arcv arcu
+           | LT p -> error_inconsistency Eq u v (List.rev p)
+           | LE _ -> merge g arcv arcu
            | NLE -> merge_disc g arcu arcv
            | EQ -> anomaly "Univ.compare")
 
@@ -482,12 +504,14 @@ let enforce_univ_lt 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
-    | LT -> g
-    | LE -> fst (setlt g arcu arcv)
-    | EQ -> error_inconsistency Lt u v
+    | LT _ -> g
+    | LE _ -> fst (setlt g arcu arcv)
+    | EQ -> error_inconsistency Lt u v [(Eq,Atom v)]
     | NLE ->
-      if is_leq g arcv arcu then error_inconsistency Lt u v
-      else fst (setlt g arcu arcv)
+      (match compare_neq false g arcv arcu with
+	  NLE -> fst (setlt g arcu arcv)
+	| EQ -> anomaly "Univ.compare"
+	| (LE p|LT p) -> error_inconsistency Lt u v (List.rev p))
 
 (* Constraints and sets of consrtaints. *)
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index a1c1bb206..c53a3c54d 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -71,7 +71,22 @@ val enforce_eq : constraint_function
 
 type constraint_type = Lt | Le | Eq
 
-exception UniverseInconsistency of constraint_type * universe * universe
+(** Type explanation is used to decorate error messages to provide
+  useful explanation why a given constraint is rejected. It is composed
+  of a path of universes and relation kinds [(r1,u1);..;(rn,un)] means
+   .. <(r1) u1 <(r2) ... <(rn) un (where <(ri) is the relation symbol
+  denoted by ri, currently only < and <=). The lowest end of the chain
+  is supposed known (see UniverseInconsistency exn). The upper end may
+  differ from the second univ of UniverseInconsistency because all
+  universes in the path are canonical. Note that each step does not
+  necessarily correspond to an actual constraint, but reflect how the
+  system stores the graph and may result from combination of several
+  constraints...
+*)
+type explanation = (constraint_type * universe) list
+
+exception UniverseInconsistency of
+    constraint_type * universe * universe * explanation
 
 val merge_constraints : constraints -> universes -> universes
 val normalize_universes : universes -> universes
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index cc6bd6150..dab4ee9c7 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -522,15 +522,15 @@ let set_leq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 =
       match s1, s2 with
       | Prop c, Prop c' -> 
 	  if c = Null && c' = Pos then d
-	  else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2)))
+	  else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2,[])))
      | Type u, Prop c -> 
 	  if c = Pos then 
 	    add_constraints d (Univ.enforce_leq u Univ.type0_univ Univ.empty_constraint)
-	  else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2))
+	  else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2,[]))
       | _, Type u ->
 	  if is_univ_var_or_set u then
 	    add_constraints d (Univ.enforce_leq u1 u2 Univ.empty_constraint)
-	  else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2))
+	  else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2,[]))
 
 let is_univ_level_var us u =
   match Univ.universe_level u with
@@ -553,7 +553,7 @@ let set_eq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 =
       | Type u, Prop c when is_univ_var_or_set u && Univ.check_eq sm u1 u2 -> d
       | Type u, Type v when is_univ_var_or_set u && is_univ_var_or_set v ->
 	  add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
-      | _, _ -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2))
+      | _, _ -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2, []))
 	    
 (**********************************************************)
 (* Accessing metas *)
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index c6e694902..0696299b3 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -63,15 +63,25 @@ let wrap_vernac_error strm =
   EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None)
 
 let rec process_vernac_interp_error = function
-  | Univ.UniverseInconsistency (o,u,v) ->
-      let msg =
-	if !Constrextern.print_universes then
-	  spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
-          str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=")
-	  ++ spc() ++ Univ.pr_uni v ++ str")"
-	else
-	  mt() in
-      wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".")
+  | Univ.UniverseInconsistency (o,u,v,p) ->
+    let pr_rel r =
+      match r with
+	  Univ.Eq -> str"=" | Univ.Lt -> str"<" | Univ.Le -> str"<=" in
+    let reason = match p with
+	[] -> mt()
+      | _::_ ->
+	str " because" ++ spc() ++ Univ.pr_uni v ++
+	  prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ Univ.pr_uni v)
+	  p ++
+	  (if snd (CList.last p)=u then mt() else
+	      (spc() ++ str "= " ++ Univ.pr_uni u)) in
+    let msg =
+      if !Constrextern.print_universes then
+	spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
+          pr_rel o ++ spc() ++ Univ.pr_uni v ++ reason ++ str")"
+      else
+	mt() in
+    wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".")
   | TypeError(ctx,te) ->
       wrap_vernac_error (Himsg.explain_type_error ctx Evd.empty te)
   | PretypeError(ctx,sigma,te) ->