(* *)
(*****************************************************************************)
-let universes_of_obj t =
+(* uri is the uri of the actual object that must be 'skipped' *)
+let universes_of_obj uri t =
+ let eq = UriManager.eq in
let don = ref [] in
let module C = Cic in
let rec aux t =
| 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))
+ aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))
| C.MutInd (u,_,exp_named_subst) ->
- if List.mem u !don then
+ if List.mem u !don || eq u uri then
[]
else
begin
don := u::!don;
- (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph) with
- | C.InductiveDefinition (l,_,_) ->
+ (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u)
+ with
+ | C.InductiveDefinition (l,_,_,_) ->
List.fold_left (
fun y (_,_,t,l') ->
y @ (aux t) @
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
+ if List.mem u !don || eq u uri then
[]
else
begin
don := u::!don;
- (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph) with
- | C.InductiveDefinition (l,_,_) ->
+ (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
+ | C.InductiveDefinition (l,_,_,_) ->
List.fold_left (
fun x (_,_,_t,l') ->
x @ aux t @
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 @
+ 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))
+ l @ if eq u uri then [] else
+ (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
[] v
- | C.Constant (_,None,ty,v) -> aux ty @
+ | 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))
+ l @ if eq u uri then [] else
+ (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
[] v
- | C.CurrentProof (_,conjs,te,ty,v) -> aux te @ aux ty @
+ | 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))
+ l @ if eq u uri then [] else
+ (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
[] v
- | C.Variable (_,Some bo,ty,v) -> aux bo @ aux ty @
+ | 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))
+ l @ if eq u uri then [] else
+ (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
[] v
- | C.Variable (_,None ,ty,v) -> aux ty @
+ | 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))
+ l @ if eq u uri then [] else
+ (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
[] v
- | C.InductiveDefinition (l,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))
+ (List.fold_left
+ (fun l u ->
+ l @ if eq u uri then [] else
+ (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
[] v)
)
in
aux_obj (t,CicUniv.empty_ugraph)
-
+let clean_and_fill uri obj ugraph =
+ let list_of_universes = universes_of_obj uri obj in
+ let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
+ let ugraph = CicUniv.fill_empty_nodes_with_uri ugraph uri in
+ ugraph