From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 17 May 2008 11:14:46 +0000 (+0000)
Subject: The code for universes was not correct in many borderline cases.
X-Git-Tag: make_still_working~5186
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b5f64556ec797a92c2c79d9d1c6aefa4dcf880b1;p=helm.git

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 c3695726b..63863ffe1 100644
--- 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 9b33de701..ddfe2ca52 100644
--- 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 9f828a114..7fa352901 100644
--- 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 ->