Replacing lists by sets in clear tactic.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16734 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 35 insertions, 32 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 8a4871a1d..9b18db78e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -362,7 +362,7 @@ let insert_after_hyp (ctxt,vals) id d check =
 (* To be used in Logic.clear_hyps *)
 let remove_hyps ids check_context check_value (ctxt, vals) =
   List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals) ->
-      if List.mem id ids then
+      if Id.Set.mem id ids then
 	(ctxt,vals)
       else
 	let nd = check_context d in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 0dcc291b5..54e88f646 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -212,7 +212,7 @@ val insert_after_hyp : named_context_val -> variable ->
   named_declaration ->
     (named_context -> unit) -> named_context_val
 
-val remove_hyps : Id.t list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
+val remove_hyps : Id.Set.t -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
 
 
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 14c102cbc..60c4e88bc 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -374,12 +374,14 @@ exception ClearDependencyError of Id.t * clear_dependency_error
 
 let cleared = Store.field ()
 
+exception Depends of Id.t
+
 let rec check_and_clear_in_constr evdref err ids c =
   (* returns a new constr where all the evars have been 'cleaned'
      (ie the hypotheses ids have been removed from the contexts of
      evars) *)
   let check id' =
-    if List.mem id' ids then
+    if Id.Set.mem id' ids then
       raise (ClearDependencyError (id',err))
   in
     match kind_of_term c with
@@ -404,35 +406,36 @@ let rec check_and_clear_in_constr evdref err ids c =
 	    let evi = Evd.find_undefined !evdref evk in
 	    let ctxt = Evd.evar_filtered_context evi in
 	    let (nhyps,nargs,rids) =
-	      List.fold_right2
-		(fun (rid,ob,c as h) a (hy,ar,ri) ->
-		  (* Check if some id to clear occurs in the instance
-		     a of rid in ev and remember the dependency *)
-		  match
-		    List.filter (fun id -> List.mem id ids) (Id.Set.elements (collect_vars a))
-		  with
-		  | id :: _ -> (hy,ar,(rid,id)::ri)
-		  | _ ->
-		  (* Check if some rid to clear in the context of ev
-		     has dependencies in another hyp of the context of ev
-		     and transitively remember the dependency *)
-		  match List.filter (fun (id,_) -> occur_var_in_decl (Global.env()) id h) ri with
-		  | (_,id') :: _ -> (hy,ar,(rid,id')::ri)
-		  | _ ->
-		  (* No dependency at all, we can keep this ev's context hyp *)
-		      (h::hy,a::ar,ri))
-		ctxt (Array.to_list l) ([],[],[]) in
+              List.fold_right2
+                (fun (rid, ob,c as h) a (hy,ar,ri) ->
+                  try
+                  (* Check if some id to clear occurs in the instance
+                     a of rid in ev and remember the dependency *)
+                    let check id = if Id.Set.mem id ids then raise (Depends id) in
+                    let () = Id.Set.iter check (collect_vars a) in
+                  (* Check if some rid to clear in the context of ev
+                     has dependencies in another hyp of the context of ev
+                     and transitively remember the dependency *)
+                    let check id _ =
+                      if occur_var_in_decl (Global.env ()) id h
+                      then raise (Depends id)
+                    in
+                    let () = Id.Map.iter check ri in
+                  (* No dependency at all, we can keep this ev's context hyp *)
+                    (h::hy, a::ar, ri)
+                  with Depends id -> (hy, ar, Id.Map.add rid id ri))
+		ctxt (Array.to_list l) ([],[],Id.Map.empty) in
 	    (* Check if some rid to clear in the context of ev has dependencies
 	       in the type of ev and adjust the source of the dependency *)
 	    let nconcl =
-	      try check_and_clear_in_constr evdref (EvarTypingBreak ev)
-		    (List.map fst rids) (evar_concl evi)
+	      try
+                let nids = Id.Map.fold (fun x _ accu -> Id.Set.add x accu) rids Id.Set.empty in
+                check_and_clear_in_constr evdref (EvarTypingBreak ev) nids (evar_concl evi)
 	      with ClearDependencyError (rid,err) ->
-		raise (ClearDependencyError (List.assoc rid rids,err)) in
+		raise (ClearDependencyError (Id.Map.find rid rids,err)) in
 
-            begin match rids with
-            | [] -> c
-            | _ ->
+            if Id.Map.is_empty rids then c
+            else
 	      let env = Context.fold_named_context push_named nhyps ~init:(empty_env) in
 	      let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
 	      evdref := Evd.define evk ev' !evdref;
@@ -445,7 +448,6 @@ let rec check_and_clear_in_constr evdref err ids c =
 	      evdref := Evd.add !evdref evk evi' ;
 	    (* spiwack: /hacking session *)
 	      mkEvar(evk', Array.of_list nargs)
-            end
 
       | _ -> map_constr (check_and_clear_in_constr evdref err ids) c
 
@@ -465,7 +467,7 @@ let clear_hyps_in_evi evdref hyps concl ids =
       match !vk with
 	| VKnone -> vk
 	| VKvalue (v,d) ->
-	    if (List.for_all (fun e -> not (Id.Set.mem e d)) ids) then
+	    if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then
 	      (* v does depend on any of ids, it's ok *)
 	      vk
 	    else
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 8e344860f..5f8a4bd37 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -193,7 +193,7 @@ exception ClearDependencyError of Id.t * clear_dependency_error
 val cleared : bool Store.field
 
 val clear_hyps_in_evi : evar_map ref -> named_context_val -> types ->
-  Id.t list -> named_context_val * types
+  Id.Set.t -> named_context_val * types
 
 val push_rel_context_to_named_context : Environ.env -> types ->
   named_context_val * types * constr list * constr list
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 345f46abf..267d26493 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -103,7 +103,7 @@ val refine : refinable -> subgoals sensitive
 (*** Cleaning  goals ***)
 
 (* Implements the [clear] tactic *)
-val clear : Names.Id.t list -> subgoals sensitive
+val clear : Names.Id.Set.t -> subgoals sensitive
 
 (* Implements the [clearbody] tactic *)
 val clear_body : Names.Id.t list -> subgoals sensitive
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 68031e2b5..84bbd9751 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -529,7 +529,7 @@ let prim_refiner r sigma goal =
 	let sign,cl,sigma =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
-	    let sign,cl,sigma = clear_hyps sigma [id] sign cl in
+	    let sign,cl,sigma = clear_hyps sigma (Id.Set.singleton id) sign cl in
 	    move_hyp true false ([],(id,None,t),named_context_of_val sign)
 	      nexthyp,
 	      cl,sigma
@@ -654,6 +654,7 @@ let prim_refiner r sigma goal =
 
     (* And now the structural rules *)
     | Thin ids ->
+        let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
 	let (hyps,concl,nsigma) = clear_hyps sigma ids sign cl in
 	let (gl,ev,sigma) =
 	  Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal)