clean_and_fill optimization

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index c16385e5d4597c5785ec2fd298f11f872972345e..c499d29d277c0f4a9928bcc58f31daa8a20ed86a 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -31,6 +31,9 @@ open Printf
 exception AssertFailure of string;;
 exception TypeCheckerFailure of string;;
 
+let profiler_clean_fill = 
+  (CicUtil.profile "add_obj.typecheck_obj.clean_and_fill").CicUtil.profile
+
 let fdebug = ref 0;;
 let debug t context =
  let rec debug_aux t i =
@@ -2146,9 +2149,12 @@ let typecheck uri =
              uobj,ugraph
 ;;
 
+let clean_and_fill u o g = 
+  (profiler_clean_fill (CicUnivUtils.clean_and_fill u o)) g
+
 let typecheck_obj ~logger uri obj =
  let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
- let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
+ let ugraph = clean_and_fill uri obj ugraph in
   CicEnvironment.add_type_checked_obj uri (obj,ugraph)
 
 (** wrappers which instantiate fresh loggers *)
@@ -2160,3 +2166,4 @@ let type_of_aux' ?(subst = []) metasenv context t ugraph =
 let typecheck_obj uri obj =
  let logger = new CicLogger.logger in
  typecheck_obj ~logger uri obj
+

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
index a7861444ef5c43d4961d5a7f790fea67b8acfa08..4e8387cf587a90489e7828c130dd61d42404e989 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
@@ -34,130 +34,105 @@
 (*                                                                           *)
 (*****************************************************************************)
 
+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) 
+    | C.Var (u,exp_named_subst) when is_not_visited 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,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]
+        List.iter (fun (_,t) -> aux t) exp_named_subst
+    | C.MutInd (u,_,exp_named_subst) when is_not_visited 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 ->
+        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.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 _ -> ()
+    | 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.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)
-    )
+        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
+    | _ -> ()
+  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.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
   in 
-    aux_obj (t,CicUniv.empty_ugraph) 
+  aux_obj t;
+  !results
 
 let clean_and_fill uri obj ugraph =
   let list_of_universes = universes_of_obj uri obj in

diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml
index 1ca99d9726eef6df41c10c97eca771d02073abda..f0bc5795892891ac813b14ed0d45c2e8396df871 100644 (file)
--- a/helm/ocaml/urimanager/uriManager.ml
+++ b/helm/ocaml/urimanager/uriManager.ml
@@ -200,3 +200,13 @@ end
 
 module UriSet = Set.Make (OrderedUri)
 
+module HashedUri =
+struct
+  type t = uri
+  let equal = eq
+  let hash = snd
+end
+
+module UriHashtbl = Hashtbl.Make (HashedUri)
+
+

diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli
index 8691600a9af45146109fa8e21eac1faf5deec54e..5f0600c7e077a840d2ce2067e1cb396f532358ee 100644 (file)
--- a/helm/ocaml/urimanager/uriManager.mli
+++ b/helm/ocaml/urimanager/uriManager.mli
@@ -65,3 +65,5 @@ val uri_of_uriref :  uri -> int -> int option -> uri
 
 module UriSet: Set.S with type elt = uri
 
+module UriHashtbl : Hashtbl.S with type key = uri
+