From 3530497aed9b6ef2cd057cf7fc89ceae1d524fc1 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 11 Jan 2005 16:03:13 +0000 Subject: [PATCH] added clean_and_fill, to be invoked on qed --- helm/ocaml/cic_proof_checking/cicUnivUtils.ml | 10 +++++++--- helm/ocaml/cic_proof_checking/cicUnivUtils.mli | 9 +++++++++ 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml index 8182f72e3..1c072bea5 100644 --- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml +++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml @@ -150,8 +150,8 @@ let universes_of_obj t = fun y (_,t) -> y @ aux t) [] l') [] l) @ - (List.fold_left ( - fun l u -> + (List.fold_left + (fun l u -> l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u CicUniv.empty_ugraph)) [] v) @@ -159,5 +159,9 @@ let universes_of_obj t = in aux_obj (t,CicUniv.empty_ugraph) - +let clean_and_fill uri obj ugraph = + let list_of_universes = universes_of_obj obj in + let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in + let ugraph = CicUniv.fill_empty_nodes_with_uri ugraph uri in + ugraph diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli index e39ac0ab5..2af21f8c9 100644 --- a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli +++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli @@ -22,6 +22,15 @@ * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) + (* traverses recursively a type and lists the referenced universes *) val universes_of_obj: Cic.obj -> CicUniv.universe list + + (** cleans the universe graph for a given object and fills universes with URI. + * to be used on qed + *) +val clean_and_fill: + UriManager.uri -> Cic.obj -> CicUniv.universe_graph -> + CicUniv.universe_graph + -- 2.39.2