the uri passed as the first parameter can't be in the environment and it
doesn't requests it)
INTERFACE_FILES = \
cicLogger.mli \
cicEnvironment.mli \
INTERFACE_FILES = \
cicLogger.mli \
cicEnvironment.mli \
cicSubstitution.mli \
cicMiniReduction.mli \
cicReductionNaif.mli \
cicSubstitution.mli \
cicMiniReduction.mli \
cicReductionNaif.mli \
(* *)
(*****************************************************************************)
(* *)
(*****************************************************************************)
-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 =
let don = ref [] in
let module C = Cic in
let rec aux t =
aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
CicUniv.empty_ugraph))
| C.MutInd (u,_,exp_named_subst) ->
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
+ if List.mem u !don || eq u uri then
[]
else
begin
don := u::!don;
(match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
[]
else
begin
don := u::!don;
(match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph) with
+ CicUniv.empty_ugraph)
+ with
| C.InductiveDefinition (l,_,_) ->
List.fold_left (
fun y (_,_,t,l') ->
| C.InductiveDefinition (l,_,_) ->
List.fold_left (
fun y (_,_,t,l') ->
List.fold_left (fun x (uri,t) -> x @ (aux t) ) [] exp_named_subst
end
| C.MutConstruct (u,_,_,exp_named_subst) ->
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
C.Constant (_,Some te,ty,v) -> aux te @ aux ty @
List.fold_left (
fun l u ->
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 ~not_jet_cooked:true u
+ CicUniv.empty_ugraph)))
[] v
| C.Constant (_,None,ty,v) -> aux ty @
List.fold_left (
fun l u ->
[] 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))
+ l @ if eq u uri then [] else
+ (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 ->
[] 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))
+ l @ if eq u uri then [] else
+ (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 ->
[] 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))
+ l @ if eq u uri then [] else
+ (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 ->
[] 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))
+ l @ if eq u uri then [] else
+ (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
+ CicUniv.empty_ugraph)))
[] v
| C.InductiveDefinition (l,v,_) ->
(List.fold_left (
[] v
| C.InductiveDefinition (l,v,_) ->
(List.fold_left (
[] l) @
(List.fold_left
(fun l u ->
[] l) @
(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 ~not_jet_cooked:true u
+ CicUniv.empty_ugraph)))
[] v)
)
in
aux_obj (t,CicUniv.empty_ugraph)
let clean_and_fill uri obj ugraph =
[] v)
)
in
aux_obj (t,CicUniv.empty_ugraph)
let clean_and_fill uri obj ugraph =
- let list_of_universes = universes_of_obj obj in
+ 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
let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
let ugraph = CicUniv.fill_empty_nodes_with_uri ugraph uri in
ugraph
* http://cs.unibo.it/helm/.
*)
* http://cs.unibo.it/helm/.
*)
-(* traverses recursively a type and lists the referenced universes *)
+(** traverses recursively a type and lists the referenced universes
+ * skipping uri (that should be the object we are working on and
+ * that can't be in the environment since we are in a Qed-like state)
+ *)
- Cic.obj -> CicUniv.universe list
+ UriManager.uri -> Cic.obj -> CicUniv.universe list
+
(** cleans the universe graph for a given object and fills universes with URI.
* to be used on qed
(** cleans the universe graph for a given object and fills universes with URI.
* to be used on qed