X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;h=738329689988176b57ecc0b7243f021792cc5c20;hb=491d4b52a73ec28b4c8f28414d87d146e8caa40d;hp=893e514b1fef9f642a212997aa92e54be2c0533c;hpb=8b1a49bbee9eea86eb74c040defe701370ca5893;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 893e514b1..738329689 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -27,8 +27,6 @@ let frozen_list = ref [];;
 let get_obj = ref (fun _ -> assert false);;
 let set_get_obj f = get_obj := f;;
 
-let type0 = []
-
 module F = Format 
 
 let rec ppsort f = function
@@ -146,14 +144,15 @@ let typeof_sort = function
   | C.Type ([(`Type|`CProp),u] as univ) ->
      if is_declared univ then (C.Type [`Succ, u])
      else 
+      let universes = !universes in
        raise (UntypableSort (lazy ("undeclared universe " ^
          NUri.string_of_uri u ^ "\ndeclared ones are: " ^ 
-         String.concat ", " (List.map NUri.string_of_uri !universes)
+         String.concat ", " (List.map NUri.string_of_uri universes)
      )))
   | C.Type t -> 
       raise (AssertFailure (lazy (
               "Cannot type an inferred type: "^ string_of_univ t)))
-  | C.Prop -> (C.Type type0)
+  | C.Prop -> (C.Type [])
 ;;
 
 let add_lt_constraint a b = 
@@ -171,16 +170,18 @@ let add_lt_constraint a b =
   | _ -> raise (BadConstraint
           (lazy "trying to add a constraint on an inferred universe"))
 ;;
+   
+let family_of = function (`CProp,_)::_ -> `CProp | _ -> `Type ;;
 
-let sup l =
+let sup fam l =
   match l with
   | [(`Type|`CProp),_] -> Some l
   | l ->
-   let bigger_than acc (_s1,n1) = 
-     List.filter (fun x -> lt_path_uri [] n1 x || NUri.eq n1 x) acc 
+   let bigger_than acc (s1,n1) = 
+    List.filter
+     (fun x -> lt_path_uri [] n1 x || (s1 <> `Succ && NUri.eq n1 x)) acc 
    in
    let solutions = List.fold_left bigger_than !universes l in
-   let fam = match l with (`CProp,_)::_ -> `CProp | _ -> `Type in
    let rec aux = function
      | [] -> None
      | u :: tl ->
@@ -190,6 +191,47 @@ let sup l =
     aux solutions
 ;;
 
+let sup l = sup (family_of l) l;;
+
+let inf ~strict fam l =
+  match l with
+  | [(`Type|`CProp),_] -> Some l
+  | [] -> None
+  | l ->
+   let smaller_than acc (_s1,n1) = 
+    List.filter
+     (fun x -> lt_path_uri [] x n1 || (not strict && NUri.eq n1 x)) acc 
+   in
+   let solutions = List.fold_left smaller_than !universes l in
+   let rec aux = function
+     | [] -> None
+     | u :: tl ->
+         if List.exists (lt_path_uri [] u) solutions then aux tl
+         else Some [fam,u]
+   in
+    aux solutions
+;;
+
+let inf ~strict l = inf ~strict (family_of l) l;;
+
+let rec universe_lt a b = 
+  match a, b with
+  | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
+  | l, ([((`Type|`CProp),b)] as orig_b) -> 
+       List.for_all 
+         (function 
+         | `Succ,_ as a -> 
+             (match sup [a] with
+             | None -> false
+             | Some x -> universe_lt x orig_b) 
+         | _, a -> lt_path a b) l
+  | _, ([] | [`Succ,_] | _::_::_) -> 
+     raise (BadConstraint (lazy (
+       "trying to check if "^string_of_univ a^
+       " is lt than the inferred universe " ^ string_of_univ b)))
+;;
+
+
 let allowed_sort_elimination s1 s2 =
   match s1, s2 with
   | C.Type (((`Type|`Succ),_)::_ | []), C.Type (((`Type|`Succ),_)::_ | [])