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

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)