From e792b4a6b0a9a279293ff7ff5748bc61d2116ce6 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Tue, 22 Oct 2013 17:26:28 +0000 Subject: Optimizing evar filters. It seems to cost quite a lot in unification, as witnessed by profiling on time-consuming files. I suspect we can do better by using a smarter representation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16912 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/cList.ml | 10 +++++----- pretyping/evarconv.ml | 2 +- pretyping/evarsolve.ml | 4 ++-- pretyping/evarutil.ml | 3 +-- pretyping/evd.ml | 2 +- 5 files changed, 10 insertions(+), 11 deletions(-) diff --git a/lib/cList.ml b/lib/cList.ml index 643ef7f2b..2cc5e4cfd 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -600,11 +600,11 @@ let map_filter_i f = match f i x with None -> l' | Some y -> y::l' in aux 0 -let filter_along f filter l = - snd (filter2 (fun b c -> f b) filter l) - -let filter_with filter l = - filter_along (fun x -> x) filter l +let rec filter_with filter l = match filter, l with +| [], [] -> [] +| true :: filter, x :: l -> x :: filter_with filter l +| false :: filter, _ :: l -> filter_with filter l +| _ -> invalid_arg "List.filter_with" let subset l1 l2 = let t2 = Hashtbl.create 151 in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b4388ff08..44138a8ee 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -720,7 +720,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | Some _ -> error "Selection of specific occurrences not supported" | None -> let evty = set_holes evdref cty subst in - let _, instance = List.filter2 (fun b c -> b) filter instance in + let instance = List.filter_with filter instance in let evd,ev = new_evar_instance sign !evdref evty ~filter instance in evdref := evd; evsref := (fst (destEvar ev),evty)::!evsref; diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index c8122c4dc..7ae44faf8 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -45,7 +45,7 @@ let test_success conv_algo env evd c c' rhs = (************************) let extract_subfilter initial_filter refined_filter = - snd (List.filter2 (fun b1 b2 -> b1) initial_filter refined_filter) + List.filter_with initial_filter refined_filter let apply_subfilter filter subfilter = fst (List.fold_right (fun oldb (l,filter) -> @@ -82,7 +82,7 @@ let restrict_evar_key evd evk filter candidates = let sign = evar_hyps evi in let src = evi.evar_source in let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in - let _, ctxt = List.filter2 (fun b c -> b) filter (evar_context evi) in + let ctxt = List.filter_with filter (evar_context evi) in let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk end diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 920fb5418..de394e660 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -239,8 +239,7 @@ let non_instantiated sigma = (* Manipulating filters *) (************************) -let extract_subfilter initial_filter refined_filter = - snd (List.filter2 (fun b1 b2 -> b1) initial_filter refined_filter) +let extract_subfilter = List.filter_with let make_pure_subst evi args = snd (List.fold_right diff --git a/pretyping/evd.ml b/pretyping/evd.ml index df02975ce..751809bc5 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -57,7 +57,7 @@ let evar_filter evi = evi.evar_filter let evar_body evi = evi.evar_body let evar_context evi = named_context_of_val evi.evar_hyps let evar_filtered_context evi = - snd (List.filter2 (fun b c -> b) (evar_filter evi) (evar_context evi)) + List.filter_with (evar_filter evi) (evar_context evi) let evar_hyps evi = evi.evar_hyps let evar_filtered_hyps evi = List.fold_right push_named_context_val (evar_filtered_context evi) -- cgit v1.2.3