new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_as...

[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 df1fc849d6ffaa199b56c559a4ee9369d6c6ae7d..738329689988176b57ecc0b7243f021792cc5c20 100644 (file)
--- 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
@@ -154,7 +152,7 @@ let typeof_sort = function
   | 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 = 
@@ -172,8 +170,10 @@ 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 ->
@@ -182,7 +182,6 @@ let sup l =
      (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 ->
@@ -192,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),_)::_ | [])