fixed clean_and_fill that now fills the object (used to fill only graph)

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
index 1f3b698d3485d182588e1303df0442d674edd367..ace4f844f78f44b32c987e6d844c2d319b039cbd 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
@@ -50,81 +50,76 @@ let universes_of_obj uri t =
   let add_result l = results := l :: !results in
   (* the iterators *)
   let rec aux = function
-    | C.Const (u,exp_named_subst) 
+    | C.Const (u,exp_named_subst) when is_not_visited u ->
+        aux_uri u;
+        visited u;
+        C.Const (u, List.map (fun (x,t) -> x,aux t) exp_named_subst)
     | C.Var (u,exp_named_subst) when is_not_visited u ->
         aux_uri u;
         visited u;
-        List.iter (fun (_,t) -> aux t) exp_named_subst
-    | C.Const (u,exp_named_subst) 
+        C.Var (u,  List.map (fun (x,t) -> x,aux t) exp_named_subst)
+    | C.Const (u,exp_named_subst) ->
+        C.Const (u, List.map (fun (x,t) -> x,aux t) exp_named_subst)
     | C.Var (u,exp_named_subst) ->
-        List.iter (fun (_,t) -> aux t) exp_named_subst
-    | C.MutInd (u,_,exp_named_subst) when is_not_visited u ->
+        C.Var (u,  List.map (fun (x,t) -> x,aux t) exp_named_subst)
+    | C.MutInd (u,x,exp_named_subst) when is_not_visited u ->
+        aux_uri u;
         visited u;
-        (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
-        | C.InductiveDefinition (l,_,_,_) -> 
-             List.iter 
-               (fun (_,_,t,l') -> 
-                 aux t;
-                 List.iter (fun (_,t) -> aux t) l')
-             l
-        | _ -> assert false);
-        List.iter (fun (_,t) -> aux t) exp_named_subst
-    | C.MutInd (_,_,exp_named_subst) ->
-        List.iter (fun (_,t) -> aux t) exp_named_subst
-    | C.MutConstruct (u,_,_,exp_named_subst) when is_not_visited u ->
+        C.MutInd (u,x,List.map (fun (x,t) -> x,aux t) exp_named_subst)
+    | C.MutInd (u,x,exp_named_subst) ->
+        C.MutInd (u,x, List.map (fun (x,t) -> x,aux t) exp_named_subst)
+    | C.MutConstruct (u,x,y,exp_named_subst) when is_not_visited u ->
+        aux_uri u;
         visited u;
-        (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
-           | C.InductiveDefinition (l,_,_,_) -> 
-               List.iter
-                 (fun (_,_,t,l') ->
-                   aux t;
-                   List.iter (fun (_,t) -> aux t) l')
-                 l
-           | _ -> assert false);
-        List.iter (fun (_,t) -> aux t) exp_named_subst
-    | C.MutConstruct (_,_,_,exp_named_subst) ->
-        List.iter (fun (_,t) -> aux t) exp_named_subst
-    | C.Meta (n,l1) -> 
-        List.iter (fun t -> match t with Some t' -> aux t' | _ -> ()) l1
-    | C.Sort ( C.Type i) -> add_result [i]
+        C.MutConstruct (u,x,y,List.map (fun (x,t) -> x,aux t) exp_named_subst)
+    | C.MutConstruct (x,y,z,exp_named_subst) ->
+        C.MutConstruct (x,y,z,List.map (fun (x,t) -> x,aux t) exp_named_subst)
+    | C.Meta (n,l1) -> C.Meta (n, List.map (HExtlib.map_option aux) l1)
+    | C.Sort (C.Type i) -> add_result [i]; 
+      C.Sort (C.Type (CicUniv.name_universe i uri))
     | C.Rel _ 
     | C.Sort _
-    | C.Implicit _ -> ()
-    | C.Cast (v,t) -> aux v; aux t
-    | C.Prod (b,s,t) 
-    | C.Lambda (b,s,t) 
-    | C.LetIn (b,s,t) -> aux s; aux t
-    | C.Appl li -> List.iter (fun t -> aux t) li
+    | C.Implicit _ as x -> x
+    | C.Cast (v,t) -> C.Cast (aux v, aux t)
+    | C.Prod (b,s,t) -> C.Prod (b,aux s, aux t)
+    | C.Lambda (b,s,t) ->  C.Lambda (b,aux s, aux t)
+    | C.LetIn (b,s,t) -> C.LetIn (b,aux s, aux t)
+    | C.Appl li -> C.Appl (List.map aux li)
     | C.MutCase (uri,n1,ty,te,patterns) ->
-        aux ty; aux te; (List.iter (fun t -> aux t) patterns)
-    | C.Fix (no, funs) -> List.iter (fun (_,_,b,c) -> aux b; aux c) funs
-    | C.CoFix (no,funs) -> List.iter (fun (_,b,c) -> aux b; aux c) funs
+        C.MutCase (uri,n1,aux ty,aux te, List.map aux patterns)
+    | C.Fix (no, funs) -> 
+        C.Fix(no, List.map (fun (x,y,b,c) -> (x,y,aux b,aux c)) funs)
+    | C.CoFix (no,funs) -> 
+        C.CoFix(no, List.map (fun (x,b,c) -> (x,aux b,aux c)) funs)
   and aux_uri u =
     if is_not_visited u then
       let _, _, l = 
         CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph u in 
       add_result l
   and aux_obj = function
-    | C.Constant (_,Some te,ty,v,_)
-    | C.Variable (_,Some te,ty,v,_) -> 
-        aux te; 
-        aux ty;
-        List.iter aux_uri v
-    | C.Constant (_,None, ty, v,_)
-    | C.Variable (_,None, ty, v,_) ->
-        aux ty;
-        List.iter aux_uri v
+    | C.Constant (x,Some te,ty,v,y) ->
+        List.iter aux_uri v;
+        C.Constant (x,Some (aux te),aux ty,v,y)
+    | C.Variable (x,Some te,ty,v,y) -> 
+        List.iter aux_uri v;
+        C.Variable (x,Some (aux te),aux ty,v,y)
+    | C.Constant (x,None, ty, v,y) ->
+        List.iter aux_uri v;
+        C.Constant (x,None, aux ty, v,y)
+    | C.Variable (x,None, ty, v,y) ->
+        List.iter aux_uri v;
+        C.Variable (x,None, aux ty, v,y)
     | C.CurrentProof (_,conjs,te,ty,v,_) -> assert false
-    | C.InductiveDefinition (l,v,_,_) -> 
-        List.iter
-           (fun (_,_,t,l') ->
-             aux t;
-             List.iter (fun (_,t) -> aux t) l') 
-        l; 
-        List.iter aux_uri v 
+    | C.InductiveDefinition (l,v,x,y) -> 
+        List.iter aux_uri v; 
+        C.InductiveDefinition (
+          List.map
+           (fun (x,y,t,l') ->
+             (x,y,aux t, List.map (fun (x,t) -> x,aux t) l'))
+          l,v,x,y)  
   in 
-  aux_obj t;
-  List.flatten !results
+  let o = aux_obj t in
+  List.flatten !results, o
 
 let rec list_uniq = function 
   | [] -> []
@@ -135,12 +130,22 @@ let rec list_uniq = function
 let list_uniq l = 
   list_uniq (List.fast_sort CicUniv.compare l)
   
+let profiler = (HExtlib.profile "clean_and_fill").HExtlib.profile
+  
 let clean_and_fill uri obj ugraph =
-  let list_of_universes = universes_of_obj uri obj in
+  (* universes of obj fills the universes of the obj with the right uri *)
+  let list_of_universes, obj = universes_of_obj uri obj in
   let list_of_universes = list_uniq list_of_universes in
+(*  CicUniv.print_ugraph ugraph;*)
+(*  List.iter (fun u -> prerr_endline (CicUniv.string_of_universe u))*)
+(*  list_of_universes;*)
   let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
+(*  CicUniv.print_ugraph ugraph;*)
   let ugraph, list_of_universes = 
     CicUniv.fill_empty_nodes_with_uri ugraph list_of_universes uri 
   in
-  ugraph, list_of_universes
+  ugraph, list_of_universes, obj
 
+let clean_and_fill u o g =
+  profiler (clean_and_fill u o) g
+  

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
index f3dfe3f09f970ed26dcd705864b79183b46640bc..eb55a47eb689e679128f930a48538faf291bb8d9 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
@@ -28,5 +28,5 @@
   *)
 val clean_and_fill:
   UriManager.uri -> Cic.obj -> CicUniv.universe_graph ->
-    CicUniv.universe_graph * CicUniv.universe list
+    CicUniv.universe_graph * CicUniv.universe list * Cic.obj