From 1f6887596563bfbf43af858bd951ee986d059aa8 Mon Sep 17 00:00:00 2001 From: notin Date: Tue, 30 Jan 2007 22:15:57 +0000 Subject: Nouvelle implantation de clear_hyps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9560 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarutil.ml | 110 +++++++++++++++++++++++++++++++------------------ pretyping/evarutil.mli | 9 ++-- 2 files changed, 76 insertions(+), 43 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 3c93e5882..1d0273260 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -306,47 +306,77 @@ let do_restrict_hyps env k evd ev args = evd := Evd.evar_define ev nc !evd; let (evn,_) = destEvar nc in mkEvar(evn,Array.of_list ncargs) + -let clear_evar_hyps_in_evar evd evn args ids = - (* Creates a new evar ev' from ev such that all ids are removed from - the context of ev' *) - (* ATTN: il faut vérifier que le type associé à ev ne dépend pas de - l'un des ids *) - let args = Array.to_list args in - let evi = Evd.find (evars_of !evd) evn in - let hyps = evar_context evi in - let (hyps',args') = list_filter2 - (fun _ c -> match kind_of_term c with Var id -> not (List.mem id ids) | _ -> true) - (hyps,args) in - let env = Sign.fold_named_context push_named hyps' ~init:(empty_env) in - let ev' = e_new_evar evd env ~src:(evar_source evn !evd) evi.evar_concl in - evd := Evd.evar_define evn ev' !evd; - let (evn',_) = destEvar ev' in - mkEvar(evn',Array.of_list args') - -let clear_evar_hyps_in_constr evd c ids = - let rec aux c = - match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c - | Evar (e,l) -> - (* aux may have defined e earlier, so we have to check *) - if Evd.is_defined_evar !evd (e,l) then - let nc = nf_evar (evars_of !evd) c in aux nc - else - clear_evar_hyps_in_evar evd e l ids - | _ -> map_constr aux c - in - aux c - -let clear_evar_hyps sigma evi ids = - let evd = Evd.create_evar_defs sigma in - let aux c = clear_evar_hyps_in_constr (ref evd) c ids in - let goal = evar_concl evi in - let hyps = evar_hyps evi in - ({ evi with - evar_concl = aux goal; - evar_hyps = map_named_val aux hyps}, evars_of evd) +type ch_error_loc = + | InGoal + | InHyps of identifier + | InEvar of existential_key + +let rec check_and_clear_in_constr evd loc c ids = + (* returns a new constr where all the evars have been 'cleaned' + (ie the hypotheses ids have been removed from the contexts of + evars *) + match kind_of_term c with + | ( Rel _ | Meta _ | Sort _ ) -> c + | ( Const _ | Ind _ | Construct _ ) -> + let vars = Environ.vars_of_global (Global.env()) c in + let check id' = + if List.mem id' ids then + match loc with + InGoal -> error (string_of_id id' ^ " is used in conclusion") + | InHyps id -> error (string_of_id id' ^ " is used in hypothesis " + ^ string_of_id id) + | InEvar n -> error (string_of_id id' ^ " is used in " + ^ string_of_existential n) + in + List.iter check vars; c + | Var id' -> + (if List.mem id' ids then + match loc with + InGoal -> error (string_of_id id' ^ " is used in conclusion") + | InHyps id -> error (string_of_id id' ^ " is used in hypothesis " + ^ string_of_id id) + | InEvar n -> error (string_of_id id' ^ " is used in " + ^ string_of_existential n)); + mkVar id' + | Evar (e,l) -> + (* If e is already defined we replace it by its definition *) + if Evd.is_defined_evar !evd (e,l) then + let nc = nf_evar (evars_of !evd) c in + (check_and_clear_in_constr evd loc nc ids) + else + let evi = Evd.find (evars_of !evd) e in + let evi' = clear_evar_hyps_in_evi evd (InEvar e) evi ids in + let env = Sign.fold_named_context push_named (evar_context evi') ~init:(empty_env) in + let ev'= e_new_evar evd env ~src:(evar_source e !evd) (evar_concl evi') in + evd := Evd.evar_define e ev' !evd; + ev' + | _ -> map_constr (fun c -> check_and_clear_in_constr evd loc c ids) c + +and clear_evar_hyps_in_evi evd loc evi ids = + (* clear_evar_hyps erases hypotheses ids in evi, checking if some + hypothesis does not depend on a element of ids, and erases ids in + the contexts of the evars occuring in evi *) + let nconcl = check_and_clear_in_constr evd loc (evar_concl evi) ids in + let (nhyps,_) = + let aux (id,ob,c) = + let loc' = match loc with + InGoal -> InHyps id + | _ -> loc + in + (id, + (match ob with + None -> None + | Some b -> Some (check_and_clear_in_constr evd loc' b ids)), + check_and_clear_in_constr evd loc' c ids) + in + remove_hyps ids aux (evar_hyps evi) + in + { evi with + evar_concl = nconcl; + evar_hyps = nhyps} + let need_restriction k args = not (array_for_all (closedn k) args) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 9ad7b6e58..e8f3bf6f0 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -162,6 +162,9 @@ val pr_tycon : env -> type_constraint -> Pp.std_ppcmds (**********************************) (* Removing hyps in evars'context *) -val clear_evar_hyps_in_evar : evar_defs ref -> evar -> constr array -> identifier list -> constr -val clear_evar_hyps_in_constr : evar_defs ref -> constr -> identifier list -> constr -val clear_evar_hyps : evar_map -> evar_info -> identifier list -> evar_info * evar_map +type ch_error_loc = + | InGoal + | InHyps of Names.identifier + | InEvar of Term.existential_key + +val clear_evar_hyps_in_evi : evar_defs ref -> ch_error_loc -> evar_info -> identifier list -> evar_info -- cgit v1.2.3