Bug fixed and further code semplification in management of universes.

[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..c2de425c6fbcf4a5bc046f0fd7794619df5012dc 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 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 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 (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
+  | 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 universe_eq a b = universe_leq b a || universe_leq a b
 
-let add_lt_constraint a b = 
+let add_le_constraint strict 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
+  | [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  
+  | _ -> raise (BadConstraint
+          (lazy "trying to add a constraint on an inferred universe"))
 ;;
 
-let add_leq_constraint 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
-;;
-
-
-
 let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;;
 let set_typecheck_obj f =
  if !already_set then