(* *)
(*****************************************************************************)
-let universes_of_obj t =
- let don = ref [] in
- let module C = Cic in
- let rec aux t =
- match t with
- C.Const (u,exp_named_subst)
+module C = Cic
+module H = UriManager.UriHashtbl
+let eq = UriManager.eq
+
+(* uri is the uri of the actual object that must be 'skipped' *)
+let universes_of_obj uri t =
+ (* don't the same work twice *)
+ let visited_objs = H.create 31 in
+ let visited u = H.replace visited_objs u true in
+ let is_not_visited u = not (H.mem visited_objs u) in
+ visited uri;
+ (* the result *)
+ let results = ref [] in
+ let add_result l = results := l :: !results in
+ (* the iterators *)
+ 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;
+ List.iter (fun (_,t) -> aux t) exp_named_subst
+ | C.Const (u,exp_named_subst)
| C.Var (u,exp_named_subst) ->
- if List.mem u !don then [] else
- (don := u::!don;
- aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- | C.MutInd (u,_,exp_named_subst) ->
- if List.mem u !don then
- []
- else
- begin
- don := u::!don;
- (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph) with
- | C.InductiveDefinition (l,_,_) ->
- List.fold_left (
- fun y (_,_,t,l') ->
- y @ (aux t) @
- (List.fold_left (
- fun x (_,t) -> x @ (aux t) )
- [] l'))
- [] l
- | _ -> assert false) @
- List.fold_left (fun x (uri,t) -> x @ (aux t) ) [] exp_named_subst
- end
- | C.MutConstruct (u,_,_,exp_named_subst) ->
- if List.mem u !don then
- []
- else
- begin
- don := u::!don;
- (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph) with
- | C.InductiveDefinition (l,_,_) ->
- List.fold_left (
- fun x (_,_,_t,l') ->
- x @ aux t @
- (List.fold_left (
- fun y (_,t) -> y @ (aux t) )
- [] l'))
- [] l
- | _ -> assert false) @
- List.fold_left (fun x (uri,t) -> x @ (aux t) ) [] exp_named_subst
- end
- | C.Meta (n,l1) ->
- List.fold_left
- (fun x t ->
- match t with
- Some t' -> x @ (aux t')
- | _ -> x)
- [] l1
- | C.Sort ( C.Type i) -> [i]
+ List.iter (fun (_,t) -> aux t) exp_named_subst
+ | C.MutInd (u,_,exp_named_subst) when is_not_visited 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 ->
+ 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.Rel _
| C.Sort _
- | C.Implicit _ -> []
- | C.Prod (b,s,t) ->
- aux s @ aux t
- | C.Cast (v,t) ->
- aux v @ aux t
- | C.Lambda (b,s,t) ->
- aux s @ aux t
- | C.LetIn (b,s,t) ->
- aux s @ aux t
- | C.Appl li ->
- List.fold_left (fun x t -> x @ (aux t)) [] li
+ | 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.MutCase (uri,n1,ty,te,patterns) ->
- aux ty @ aux te @
- (List.fold_left (fun x t -> x @ (aux t)) [] patterns)
- | C.Fix (no, funs) ->
- List.fold_left (fun x (_,_,b,c) -> x @ (aux b) @ (aux c)) [] funs
- | C.CoFix (no,funs) ->
- List.fold_left (fun x (_,b,c) -> x @ (aux b) @ (aux c)) [] funs
- and aux_obj ?(boo=false) (t,_) =
- (match t with
- C.Constant (_,Some te,ty,v) -> aux te @ aux ty @
- List.fold_left (
- fun l u ->
- l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- [] v
- | C.Constant (_,None,ty,v) -> aux ty @
- List.fold_left (
- fun l u ->
- l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- [] v
- | C.CurrentProof (_,conjs,te,ty,v) -> aux te @ aux ty @
- List.fold_left (
- fun l u ->
- l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- [] v
- | C.Variable (_,Some bo,ty,v) -> aux bo @ aux ty @
- List.fold_left (
- fun l u ->
- l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- [] v
- | C.Variable (_,None ,ty,v) -> aux ty @
- List.fold_left (
- fun l u ->
- l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- [] v
- | C.InductiveDefinition (l,v,_) ->
- (List.fold_left (
- fun x (_,_,t,l') ->
- x @ aux t @ List.fold_left (
- fun y (_,t) -> y @ aux t)
- [] l')
- [] l) @
- (List.fold_left (
- fun l u ->
- l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- [] v)
- )
+ 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 aux_uri v
+ | C.Constant (_,None, ty, v,_)
+ | C.Variable (_,None, ty, v,_) ->
+ aux ty;
+ List.iter aux_uri v
+ | 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 aux_uri v
in
- aux_obj (t,CicUniv.empty_ugraph)
+ aux_obj t;
+ 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, list_of_universes =
+ CicUniv.fill_empty_nodes_with_uri ugraph list_of_universes uri
+ in
+ ugraph, list_of_universes
projects / helm.git / blobdiff