diff options
-rw-r--r-- | kernel/environ.ml | 2 | ||||
-rw-r--r-- | kernel/environ.mli | 2 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 56 | ||||
-rw-r--r-- | pretyping/evarutil.mli | 2 | ||||
-rw-r--r-- | proofs/goal.mli | 2 | ||||
-rw-r--r-- | proofs/logic.ml | 3 |
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) |