From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 12 Jan 2005 14:56:46 +0000 (+0000)
Subject: fixed bug in fill_and_clean (now the helper universes_of_obj knows that
X-Git-Tag: V_0_1_0~141
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=58bd1746df1d9dc734f8ac75220d25997c09bed1;p=helm.git

fixed bug in fill_and_clean (now the helper universes_of_obj knows that
the uri passed as the first parameter can't be in the environment and it
doesn't requests it)
---

diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile
index c8828a224..4d56f5b25 100644
--- a/helm/ocaml/cic_proof_checking/Makefile
+++ b/helm/ocaml/cic_proof_checking/Makefile
@@ -8,8 +8,8 @@ REDUCTION_IMPLEMENTATION = cicReductionMachine.ml
 INTERFACE_FILES = \
 	cicLogger.mli \
 	cicEnvironment.mli \
-	cicUnivUtils.mli \
 	cicPp.mli \
+	cicUnivUtils.mli \
 	cicSubstitution.mli \
 	cicMiniReduction.mli \
 	cicReductionNaif.mli \
diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
index 1c072bea5..1897772a8 100644
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
@@ -34,7 +34,9 @@
 (*                                                                           *)
 (*****************************************************************************)
 
-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 =
@@ -46,13 +48,14 @@ let universes_of_obj t =
          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  
-			 CicUniv.empty_ugraph) with
+                         CicUniv.empty_ugraph)
+              with
                | C.InductiveDefinition (l,_,_) -> 
 		   List.fold_left (
 		     fun y (_,_,t,l') -> 
@@ -65,7 +68,7 @@ let universes_of_obj 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
@@ -116,32 +119,37 @@ let universes_of_obj t =
 	 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 ->
-               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 ->
-               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 ->
-               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 ->
-               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 (
@@ -152,15 +160,16 @@ let universes_of_obj t =
 	      [] 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 =
-  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
diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
index 2af21f8c9..0184037a6 100644
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
@@ -23,9 +23,13 @@
  * 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) 
+ *)
 val universes_of_obj: 
-  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