From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 17 May 2008 13:21:45 +0000 (+0000)
Subject: Bug fixed: since circular <= graphs are allowed, added an avoid list to
X-Git-Tag: make_still_working~5183
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ecc3dad340e2369f5f226713513e0704e5349ab0;p=helm.git

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 c2de425c6..8f76f4a0f 100644
--- 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"))
 ;;