- added attributes support

[helm.git] / helm / ocaml / cic_proof_checking / cicUnivUtils.ml

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
index 8182f72e3260e16c4dd76572d6893700a774c7d0..c027194543abc4cc0d4bc5aa4aa448eb7d996bf4 100644 (file)
--- 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 =
@@ -43,16 +45,15 @@ let universes_of_obj 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
+            (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u)
+              with
                | C.InductiveDefinition (l,_,_) -> 
                   List.fold_left (
                     fun y (_,_,t,l') -> 
@@ -65,13 +66,12 @@ 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
            don := u::!don;
-           (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u 
-                        CicUniv.empty_ugraph) with
+           (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
               | C.InductiveDefinition (l,_,_) -> 
                   List.fold_left (
                     fun x (_,_,_t,l') ->
@@ -116,32 +116,32 @@ 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 CicUniv.empty_ugraph 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 CicUniv.empty_ugraph 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 CicUniv.empty_ugraph 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 CicUniv.empty_ugraph 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 CicUniv.empty_ugraph u)))
             [] v
        | C.InductiveDefinition (l,v,_) -> 
           (List.fold_left (
@@ -150,14 +150,18 @@ let universes_of_obj t =
                  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