The code for universes was not correct in many borderline cases.

The new code should be correct. For sure, it is much simpler, shorter,
characterized by better invariants and its interface has less functions.

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index c3695726bd37c20ed042d116f8ee2135f5ac86bf..63863ffe1326c4bc50bb239871a0cb1ce2d76494 100644 (file)
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -139,7 +139,7 @@ let _ =
   let _ = 
     let rec aux = function
       | a::b::tl ->
-         NCicEnvironment.add_lt_constraint (mk_type a) (mk_type b)
+         NCicEnvironment.add_le_constraint true (mk_type a) (mk_type b)
       | _ -> ()
     in
        aux lll

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 9b33de70184bfc3e3a1d32ff44aeb6c99f585a69..ddfe2ca52361506466db29377d5a3be13bd705ea 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -14,48 +14,44 @@
 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 &&
+   if strict then le_path_uri false a x else le_path_uri 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

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 9f828a11408cafb38136455c452798460699733e..7fa352901fd63ea2b949d6d80a8a5262b315dd19 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -14,16 +14,21 @@
 exception CircularDependency of string Lazy.t;;
 exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t;;
+exception BadConstraint of string Lazy.t;;
 
 val get_checked_obj: NUri.uri -> NCic.obj
 
 val get_relevance: NReference.reference -> bool list
 
 val type0: NCic.universe
+(* universe_* raise BadConstraints if the second arg. is an inferred universe *)
 val universe_eq: NCic.universe -> NCic.universe -> bool
 val universe_leq: NCic.universe -> NCic.universe -> bool
-val add_lt_constraint: NCic.universe -> NCic.universe -> unit
-val add_leq_constraint: NCic.universe -> NCic.universe -> unit
+(* add_le_constraint raise BadConstraint in case of universe inconsistency
+   or if the second argument is an inferred universe
+   true -> strict check (<); false -> loose check (<=)
+*)
+val add_le_constraint: bool -> NCic.universe -> NCic.universe -> unit
 
 val get_checked_def:
   NReference.reference ->