added universes list handling

[helm.git] / helm / ocaml / cic_proof_checking / cicUnivUtils.ml

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
index d36c1ee350219d6974f88b32d0655565534704ea..cf9e8249649d3afc3af5dcc5ed71fa956406cb44 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
@@ -52,8 +52,8 @@ let universes_of_obj uri t =
   let rec aux = function
     | C.Const (u,exp_named_subst) 
     | C.Var (u,exp_named_subst) when is_not_visited u ->
+        aux_uri u;
         visited u;
-        aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u));
         List.iter (fun (_,t) -> aux t) exp_named_subst
     | C.Const (u,exp_named_subst) 
     | C.Var (u,exp_named_subst) ->
@@ -86,7 +86,7 @@ let universes_of_obj uri t =
         List.iter (fun (_,t) -> aux t) exp_named_subst
     | C.Meta (n,l1) -> 
         List.iter (fun t -> match t with Some t' -> aux t' | _ -> ()) l1
-    | C.Sort ( C.Type i) -> add_result i
+    | C.Sort ( C.Type i) -> add_result [i]
     | C.Rel _ 
     | C.Sort _
     | C.Implicit _ -> ()
@@ -99,24 +99,22 @@ let universes_of_obj uri t =
         aux ty; aux te; (List.iter (fun t -> aux t) patterns)
     | C.Fix (no, funs) -> List.iter (fun (_,_,b,c) -> aux b; aux c) funs
     | C.CoFix (no,funs) -> List.iter (fun (_,b,c) -> aux b; aux c) funs
+    | _ -> ()
+  and aux_uri u =
+    if is_not_visited u then
+      let _, _, l = 
+        CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph u in 
+      add_result l
   and aux_obj = function
     | C.Constant (_,Some te,ty,v,_)
     | C.Variable (_,Some te,ty,v,_) -> 
         aux te; 
         aux ty;
-        List.iter
-          (fun u ->
-            if is_not_visited u then 
-              (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
-        v
+        List.iter aux_uri v
     | C.Constant (_,None, ty, v,_)
     | C.Variable (_,None, ty, v,_) ->
         aux ty;
-        List.iter
-          (fun u ->
-            if is_not_visited u then
-              (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
-        v
+        List.iter aux_uri v
     | C.CurrentProof (_,conjs,te,ty,v,_) -> assert false
     | C.InductiveDefinition (l,v,_,_) -> 
         List.iter
@@ -124,18 +122,26 @@ let universes_of_obj uri t =
              aux t;
              List.iter (fun (_,t) -> aux t) l') 
         l; 
-        List.iter
-           (fun u -> 
-             if is_not_visited u then
-              (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
-        v
+        List.iter aux_uri v 
   in 
   aux_obj t;
-  !results
+  List.flatten !results
+
+let rec list_uniq = function 
+  | [] -> []
+  | h::[] -> [h]
+  | h1::h2::tl when CicUniv.eq h1 h2 -> list_uniq (h2 :: tl) 
+  | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
 
+let list_uniq l = 
+  list_uniq (List.fast_sort CicUniv.compare l)
+  
 let clean_and_fill uri obj ugraph =
   let list_of_universes = universes_of_obj uri obj in
+  let list_of_universes = list_uniq list_of_universes in
   let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
-  let ugraph = CicUniv.fill_empty_nodes_with_uri ugraph uri in
-  ugraph
+  let ugraph, list_of_universes = 
+    CicUniv.fill_empty_nodes_with_uri ugraph list_of_universes uri 
+  in
+  ugraph, list_of_universes