Bug fixed: since circular <= graphs are allowed, added an avoid list to

avoid looping.
Even more code semplification.
Little optimization: adding x <= x does nothing

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index c2de425c6fbcf4a5bc046f0fd7794619df5012dc..8f76f4a0f25628c0947617d0144091e871cdd7e3 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -20,17 +20,16 @@ let type0 = [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
 
 let le_constraints = ref [] (* strict,a,b *)
 
-let rec le_path_uri strict a b =
- if strict then
-  List.exists (fun (strict,x,y) -> NUri.eq y b && le_path_uri (not strict) a x)
-    !le_constraints
- else
-  NUri.eq a b ||
-   List.exists (fun (_,x,y) -> NUri.eq y b && le_path_uri false a x)
-     !le_constraints
+let rec le_path_uri avoid strict a b =
+ (not strict && NUri.eq a b) ||
+ List.exists
+  (fun (strict',x,y) ->
+     NUri.eq y b && not (List.exists (NUri.eq x) avoid) &&
+       le_path_uri (x::avoid) (strict && not strict') a x
+  ) !le_constraints
 ;;
 
-let leq_path a b = le_path_uri (fst a) (snd a) b;;
+let leq_path a b = le_path_uri [b] (fst a) (snd a) b;;
 
 let universe_leq a b = 
   match a, b with
@@ -44,9 +43,10 @@ let universe_eq a b = universe_leq b a || universe_leq a b
 let add_le_constraint strict a b = 
   match a,b with
   | [false,a2],[false,b2] -> 
-      if le_path_uri (not strict) b2 a2 then
-       (raise (BadConstraint (lazy "universe inconsistency")));
-      le_constraints := (strict,a2,b2) :: !le_constraints  
+      if not (NUri.eq a2 b2) then (
+        if le_path_uri [] (not strict) b2 a2 then
+         (raise (BadConstraint (lazy "universe inconsistency")));
+        le_constraints := (strict,a2,b2) :: !le_constraints)
   | _ -> raise (BadConstraint
           (lazy "trying to add a constraint on an inferred universe"))
 ;;