let add_result l = results := l :: !results in
(* the iterators *)
let rec aux = function
- | C.Const (u,exp_named_subst)
+ | C.Const (u,exp_named_subst) when is_not_visited u ->
+ aux_uri u;
+ visited u;
+ C.Const (u, List.map (fun (x,t) -> x,aux t) 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, List.map (fun (x,t) -> x,aux t) exp_named_subst)
+ | C.Const (u,exp_named_subst) ->
+ C.Const (u, List.map (fun (x,t) -> x,aux t) exp_named_subst)
| C.Var (u,exp_named_subst) ->
- List.iter (fun (_,t) -> aux t) exp_named_subst
- | C.MutInd (u,_,exp_named_subst) when is_not_visited u ->
+ C.Var (u, List.map (fun (x,t) -> x,aux t) exp_named_subst)
+ | C.MutInd (u,x,exp_named_subst) when is_not_visited u ->
+ aux_uri u;
visited u;
- (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
- | C.InductiveDefinition (l,_,_,_) ->
- List.iter
- (fun (_,_,t,l') ->
- aux t;
- List.iter (fun (_,t) -> aux t) l')
- l
- | _ -> assert false);
- List.iter (fun (_,t) -> aux t) exp_named_subst
- | C.MutInd (_,_,exp_named_subst) ->
- List.iter (fun (_,t) -> aux t) exp_named_subst
- | C.MutConstruct (u,_,_,exp_named_subst) when is_not_visited u ->
+ C.MutInd (u,x,List.map (fun (x,t) -> x,aux t) exp_named_subst)
+ | C.MutInd (u,x,exp_named_subst) ->
+ C.MutInd (u,x, List.map (fun (x,t) -> x,aux t) exp_named_subst)
+ | C.MutConstruct (u,x,y,exp_named_subst) when is_not_visited u ->
+ aux_uri u;
visited u;
- (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
- | C.InductiveDefinition (l,_,_,_) ->
- List.iter
- (fun (_,_,t,l') ->
- aux t;
- List.iter (fun (_,t) -> aux t) l')
- l
- | _ -> assert false);
- List.iter (fun (_,t) -> aux t) exp_named_subst
- | C.MutConstruct (_,_,_,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.MutConstruct (u,x,y,List.map (fun (x,t) -> x,aux t) exp_named_subst)
+ | C.MutConstruct (x,y,z,exp_named_subst) ->
+ C.MutConstruct (x,y,z,List.map (fun (x,t) -> x,aux t) exp_named_subst)
+ | C.Meta (n,l1) -> C.Meta (n, List.map (HExtlib.map_option aux) l1)
+ | C.Sort (C.Type i) -> add_result [i];
+ C.Sort (C.Type (CicUniv.name_universe i uri))
| C.Rel _
| C.Sort _
- | C.Implicit _ -> ()
- | C.Cast (v,t) -> aux v; aux t
- | C.Prod (b,s,t)
- | C.Lambda (b,s,t)
- | C.LetIn (b,s,t) -> aux s; aux t
- | C.Appl li -> List.iter (fun t -> aux t) li
+ | C.Implicit _ as x -> x
+ | C.Cast (v,t) -> C.Cast (aux v, aux t)
+ | C.Prod (b,s,t) -> C.Prod (b,aux s, aux t)
+ | C.Lambda (b,s,t) -> C.Lambda (b,aux s, aux t)
+ | C.LetIn (b,s,t) -> C.LetIn (b,aux s, aux t)
+ | C.Appl li -> C.Appl (List.map aux li)
| C.MutCase (uri,n1,ty,te,patterns) ->
- 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
+ C.MutCase (uri,n1,aux ty,aux te, List.map aux patterns)
+ | C.Fix (no, funs) ->
+ C.Fix(no, List.map (fun (x,y,b,c) -> (x,y,aux b,aux c)) funs)
+ | C.CoFix (no,funs) ->
+ C.CoFix(no, List.map (fun (x,b,c) -> (x,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
- | 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
+ | C.Constant (x,Some te,ty,v,y) ->
+ List.iter aux_uri v;
+ C.Constant (x,Some (aux te),aux ty,v,y)
+ | C.Variable (x,Some te,ty,v,y) ->
+ List.iter aux_uri v;
+ C.Variable (x,Some (aux te),aux ty,v,y)
+ | C.Constant (x,None, ty, v,y) ->
+ List.iter aux_uri v;
+ C.Constant (x,None, aux ty, v,y)
+ | C.Variable (x,None, ty, v,y) ->
+ List.iter aux_uri v;
+ C.Variable (x,None, aux ty, v,y)
| C.CurrentProof (_,conjs,te,ty,v,_) -> assert false
- | C.InductiveDefinition (l,v,_,_) ->
- List.iter
- (fun (_,_,t,l') ->
- 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
+ | C.InductiveDefinition (l,v,x,y) ->
+ List.iter aux_uri v;
+ C.InductiveDefinition (
+ List.map
+ (fun (x,y,t,l') ->
+ (x,y,aux t, List.map (fun (x,t) -> x,aux t) l'))
+ l,v,x,y)
in
- aux_obj t;
- !results
+ let o = aux_obj t in
+ List.flatten !results, o
+
+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 profiler = (HExtlib.profile "clean_and_fill").HExtlib.profile
+
let clean_and_fill uri obj ugraph =
- let list_of_universes = universes_of_obj uri obj in
+ (* universes of obj fills the universes of the obj with the right uri *)
+ let list_of_universes, obj = universes_of_obj uri obj in
+ let list_of_universes = list_uniq list_of_universes in
+(* CicUniv.print_ugraph ugraph;*)
+(* List.iter (fun u -> prerr_endline (CicUniv.string_of_universe u))*)
+(* list_of_universes;*)
let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
- let ugraph = CicUniv.fill_empty_nodes_with_uri ugraph uri in
- ugraph
+(* CicUniv.print_ugraph ugraph;*)
+ let ugraph, list_of_universes =
+ CicUniv.fill_empty_nodes_with_uri ugraph list_of_universes uri
+ in
+ ugraph, list_of_universes, obj
+let clean_and_fill u o g =
+ profiler (clean_and_fill u o) g
+
projects / helm.git / blobdiff