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) ->
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 _ -> ()
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
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