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=a7861444ef5c43d4961d5a7f790fea67b8acfa08;hpb=e8236af508187f6446f5af481d545d433628ee00;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
index a7861444e..ace4f844f 100644
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
@@ -34,134 +34,118 @@
 (*                                                                           *)
 (*****************************************************************************)
 
+module C = Cic
+module H = UriManager.UriHashtbl 
+let eq  = UriManager.eq
+
 (* 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 =
-    match t with
-      C.Const (u,exp_named_subst) 
+  (* don't the same work twice *)
+  let visited_objs = H.create 31 in
+  let visited u = H.replace visited_objs u true in 
+  let is_not_visited u = not (H.mem visited_objs u) in 
+  visited uri;
+  (* the result *)
+  let results = ref [] in
+  let add_result l = results := l :: !results in
+  (* the iterators *)
+  let rec aux = function
+    | 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;
+        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) ->
-        if List.mem u !don then [] else
-        (don := u::!don;
-         aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))
-    | C.MutInd (u,_,exp_named_subst) ->
-	if List.mem u !don || eq u uri then 
-	  [] 
-	else
-          begin
-	    don := u::!don;
-            (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u)
-              with
-               | C.InductiveDefinition (l,_,_,_) -> 
-		   List.fold_left (
-		     fun y (_,_,t,l') -> 
-		       y @ (aux t) @ 
-		       (List.fold_left (
-			  fun x (_,t) -> x @ (aux t) )
-			  [] l'))
-		     [] l
-	      | _ -> assert false) @ 
-	    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 || eq u uri then 
-	  [] 
-	else
-	  begin
-	    don := u::!don;
-	    (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
-	       | C.InductiveDefinition (l,_,_,_) -> 
-		   List.fold_left (
-		     fun x (_,_,_t,l') ->
-		       x @ aux t @  
-		       (List.fold_left (
-			  fun y (_,t) -> y @ (aux t) )
-			  []  l')) 
-		     [] l
-	       | _ -> assert false) @ 
-	    List.fold_left (fun x (uri,t) -> x @ (aux t) ) [] exp_named_subst
-	  end
-    | C.Meta (n,l1) ->
-        List.fold_left 
-          (fun x t -> 
-             match t with 
-		 Some t' -> x @ (aux t') 
-               | _ -> x) 
-          [] l1
-    | C.Sort ( C.Type i) -> [i]
+        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;
+        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;
+        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.Prod (b,s,t) ->
-	aux s @ aux t
-    | C.Cast (v,t) -> 
-	aux v @ aux t
-    | C.Lambda (b,s,t) ->
-	aux s @ aux t 
-    | C.LetIn (b,s,t) ->
-	aux s @ aux t
-    | C.Appl li ->
-	List.fold_left (fun x t -> x @  (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.fold_left (fun x t -> x @ (aux t)) [] patterns)
-    | C.Fix (no, funs) ->
-	List.fold_left (fun x (_,_,b,c) -> x @ (aux b) @ (aux c)) [] funs
-    | C.CoFix (no,funs) ->
-	List.fold_left (fun x (_,b,c) -> x @ (aux b) @ (aux c)) [] funs
-  and aux_obj ?(boo=false) (t,_)  = 
-    (match t with
-	 C.Constant (_,Some te,ty,v,_) -> aux te @ aux ty @
-           List.fold_left (
-             fun l u ->
-               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 @ 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 @ 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 @ 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 @ if eq u uri then [] else 
-                 (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
-	     [] v
-       | C.InductiveDefinition (l,v,_,_) -> 
-	   (List.fold_left (
-	      fun x (_,_,t,l') ->
-		x @ aux t @ List.fold_left (
-		  fun y (_,t) -> y @ aux t) 
-		[] l') 
-	      [] l) @ 
-	   (List.fold_left
-              (fun l u -> 
-	       l @ if eq u uri then [] else 
-                 (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
-	      [] v)
-    )
+        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 (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,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,CicUniv.empty_ugraph) 
+  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
+