renamed add_le_constraint to add_constraint since it adds both le and lt constraints

[helm.git] / helm / software / components / ng_kernel / nCicEnvironment.ml

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 9b33de70184bfc3e3a1d32ff44aeb6c99f585a69..de785bde8b4b009f5bc39526ec601ab43cbd8732 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -14,48 +14,43 @@
 exception CircularDependency of string Lazy.t;;
 exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t;;
+exception BadConstraint of string Lazy.t;;
 
 let type0 = [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
 
-let u_eq (a1,a2) (b1,b2) = a1=b1 && NUri.eq a2 b2
+let le_constraints = ref [] (* strict,a,b *)
 
-let u_lt a b = 
-  match a,b with
-  | (false,a2), (true,b2) -> NUri.eq a2 b2
-  | _ -> false
+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_constraints = ref []
 
-let rec path a b = 
-  List.exists (fun (x,y) -> u_eq y b && (u_eq a x || u_lt a x || path a x))
-    !leq_constraints
+let leq_path a b = le_path_uri [b] (fst a) (snd a) b;;
 
 let universe_leq a b = 
   match a, b with
-  | a,[b] -> List.for_all (fun a -> path a b) a
-  | _ -> assert false
-
-let universe_eq a b = universe_leq b a || universe_leq a b
+  | a,[(false,b)] -> List.for_all (fun a -> leq_path a b) a
+  | _,_ ->
+     raise (BadConstraint
+      (lazy "trying to check if a universe is less or equal than an inferred universe"))
 
-let add_lt_constraint a b = 
-  match a,b with
-  | [false,a2 as a],[false,_ as b] -> 
-      if path b a then (raise (Failure "universe inconsistency"));
-      leq_constraints := ((true,a2),b) :: !leq_constraints  
-  | _ -> assert false
-;;
+let universe_eq a b = universe_leq b a && universe_leq a b
 
-let add_leq_constraint a b = 
+let add_constraint strict a b = 
   match a,b with
-  | [false,_ as a],[false,b2 as b] -> 
-      if path (true,b2) a then (raise (Failure "universe inconsistency"));
-      leq_constraints := (a,b) :: !leq_constraints  
-  | _ -> assert false
+  | [false,a2],[false,b2] -> 
+      if not (le_path_uri [] strict 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"))
 ;;
 
-
-
 let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;;
 let set_typecheck_obj f =
  if !already_set then