X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicUnivUtils.ml;h=ace4f844f78f44b32c987e6d844c2d319b039cbd;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d36c1ee350219d6974f88b32d0655565534704ea;hpb=ffefcfede36fec9a9dfdb0911557dbb67849c1ea;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
index d36c1ee35..ace4f844f 100644
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
@@ -50,92 +50,102 @@ 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;
-        aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph 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
-          (fun u ->
-            if is_not_visited u then 
-              (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
-        v
-    | C.Constant (_,None, ty, v,_)
-    | C.Variable (_,None, ty, v,_) ->
-        aux ty;
-        List.iter
-          (fun u ->
-            if is_not_visited u then
-              (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
-        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
-           (fun u -> 
-             if is_not_visited u then
-              (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
-        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;
-  !results
+  let o = aux_obj t in
+  List.flatten !results, o
+
+let rec list_uniq = function 
+  | [] -> []
+  | h::[] -> [h]
+  | h1::h2::tl when CicUniv.eq h1 h2 -> list_uniq (h2 :: tl) 
+  | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
 
+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
-  let ugraph = CicUniv.fill_empty_nodes_with_uri ugraph uri in
-  ugraph
+(*  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, obj
 
+let clean_and_fill u o g =
+  profiler (clean_and_fill u o) g
+