From 45c8cad0524aa224f530ac3829adc8a1adfef4d5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 21 Sep 2005 12:16:29 +0000 Subject: [PATCH] clean_and_fill optimization --- .../cic_proof_checking/cicTypeChecker.ml | 9 +- helm/ocaml/cic_proof_checking/cicUnivUtils.ml | 209 ++++++++---------- helm/ocaml/urimanager/uriManager.ml | 10 + helm/ocaml/urimanager/uriManager.mli | 2 + 4 files changed, 112 insertions(+), 118 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index c16385e5d..c499d29d2 100644 --- 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 a7861444e..4e8387cf5 100644 --- 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 1ca99d972..f0bc57958 100644 --- 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 8691600a9..5f0600c7e 100644 --- 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 + -- 2.39.2