diff options
author | 2006-04-28 12:24:14 +0000 | |
---|---|---|
committer | 2006-04-28 12:24:14 +0000 | |
commit | a184d54b95c40bc2890fc91f236bbdf983ebc83d (patch) | |
tree | d95ef613b68e96c0e7de041baae4c721bd48cd25 | |
parent | 11aaf97fa5f773c8a81d12255414cd3f5d189d25 (diff) |
Standardisation du nom des méthodes de Evd
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | CHANGES | 4 | ||||
-rw-r--r-- | contrib/correctness/ptactic.ml | 4 | ||||
-rw-r--r-- | contrib/xml/doubleTypeInference.ml | 2 | ||||
-rw-r--r-- | contrib/xml/proof2aproof.ml | 2 | ||||
-rw-r--r-- | dev/db | 1 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 21 | ||||
-rw-r--r-- | pretyping/evd.ml | 24 | ||||
-rw-r--r-- | pretyping/evd.mli | 7 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 6 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 6 | ||||
-rw-r--r-- | pretyping/unification.ml | 2 | ||||
-rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
-rw-r--r-- | proofs/refiner.ml | 2 | ||||
-rw-r--r-- | tactics/evar_tactics.ml | 2 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 4 | ||||
-rw-r--r-- | theories/Logic/ClassicalChoice.v | 2 |
16 files changed, 46 insertions, 45 deletions
@@ -96,9 +96,11 @@ Notations - no more automatic printing box in case of user-provided printing "format". - new notation "exists! x:A, P" for unique existence. -Library +Libraries - Small extension of Zmin.V, new Zmax.v, new Zminmax.v +- Reworking of the files on classical logic and description principles + (possible incompatibilities) - New library on String and Ascii characters (contributed by L. Thery) - Few other improvements in ZArith potentially exceptionally breaking the compatibility (useless hypothesys of Zgt_square_simpl and diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index 5994fb38d..e7610923c 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -208,8 +208,8 @@ let reduce_open_constr (em0,c) = | Cast (c',t) -> (match kind_of_term c' with | Evar (ev,_) -> - if not (Evd.in_dom em ev) then - Evd.add em ev (Evd.map em0 ev) + if not (Evd.mem em ev) then + Evd.add em ev (Evd.find em0 ev) else em | _ -> fold_constr collect em c) diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index 518f6c115..a3336817e 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -93,7 +93,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = let jty = execute env sigma ty None in let jty = assumption_of_judgment env sigma jty in let evar_context = - E.named_context_of_val (Evd.map sigma n).Evd.evar_hyps in + E.named_context_of_val (Evd.find sigma n).Evd.evar_hyps in let rec iter actual_args evar_context = match actual_args,evar_context with [],[] -> () diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index dff546c94..678b650cc 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -47,7 +47,7 @@ let nf_evar sigma ~preserve = | _ -> T.mkApp (c', l') ) | _ -> T.mkApp (c', l')) - | T.Evar (e,l) when Evd.in_dom sigma e & Evd.is_defined sigma e -> + | T.Evar (e,l) when Evd.mem sigma e & Evd.is_defined sigma e -> aux (Evd.existential_value sigma (e,l)) | T.Evar (e,l) -> T.mkEvar (e, Array.map aux l) | T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl) @@ -28,6 +28,7 @@ install_printer Top_printers.ppgoal install_printer Top_printers.ppsigmagoal install_printer Top_printers.pproof install_printer Top_printers.ppevd +install_printer Top_printers.ppevm install_printer Top_printers.ppclenv install_printer Top_printers.pptac diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 2785d0838..658bf407f 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -35,7 +35,7 @@ exception Uninstantiated_evar of existential_key let rec whd_ise sigma c = match kind_of_term c with - | Evar (ev,args) when Evd.in_dom sigma ev -> + | Evar (ev,args) when Evd.mem sigma ev -> if Evd.is_defined sigma ev then whd_ise sigma (existential_value sigma (ev,args)) else raise (Uninstantiated_evar ev) @@ -46,7 +46,7 @@ let rec whd_ise sigma c = let whd_castappevar_stack sigma c = let rec whrec (c, l as s) = match kind_of_term c with - | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> + | Evar (ev,args) when Evd.mem sigma ev & Evd.is_defined sigma ev -> whrec (existential_value sigma (ev,args), l) | Cast (c,_,_) -> whrec (c, l) | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l) @@ -93,7 +93,7 @@ let collect_evars emap c = let rec collrec acc c = match kind_of_term c with | Evar (k,_) -> - if Evd.in_dom emap k & not (Evd.is_defined emap k) then k::acc + if Evd.mem emap k & not (Evd.is_defined emap k) then k::acc else (* No recursion on the evar instantiation *) acc | _ -> fold_constr collrec acc c in @@ -103,13 +103,14 @@ let push_dependent_evars sigma emap = Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') -> List.fold_left (fun (sigma',emap') ev -> - (Evd.add sigma' ev (Evd.map emap' ev),Evd.rmv emap' ev)) + (Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev)) (sigma',emap') (collect_evars emap' ccl)) emap (sigma,emap) (* replaces a mapping of existentials into a mapping of metas. Problem if an evar appears in the type of another one (pops anomaly) *) let evars_to_metas sigma (emap, c) = + let emap = nf_evars emap in let sigma',emap' = push_dependent_evars sigma emap in let change_exist evar = let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in @@ -117,7 +118,7 @@ let evars_to_metas sigma (emap, c) = mkCast (mkMeta n, DEFAULTcast, ty) in let rec replace c = match kind_of_term c with - Evar (k,_ as ev) when Evd.in_dom emap' k -> change_exist ev + Evar (k,_ as ev) when Evd.mem emap' k -> change_exist ev | _ -> map_constr replace c in (sigma', replace c) @@ -297,7 +298,7 @@ let is_defined_equation env evd (ev,inst) rhs = is_pattern inst && not (occur_evar ev rhs) && try - let evi = Evd.map (evars_of evd) ev in + let evi = Evd.find (evars_of evd) ev in let (evd',body) = inverse_instance env evd ev evi inst rhs in evar_well_typed_body evd' ev evi body with Failure _ -> false @@ -313,7 +314,7 @@ let is_defined_equation env evd (ev,inst) rhs = let do_restrict_hyps evd ev args = let args = Array.to_list args in - let evi = Evd.map (evars_of !evd) ev in + let evi = Evd.find (evars_of !evd) ev in let env = evar_env evi in let hyps = evar_context evi in let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in @@ -395,7 +396,7 @@ let evar_define env (ev,argsv) rhs isevars = if occur_evar ev rhs then error_occur_check env (evars_of isevars) ev rhs; let args = Array.to_list argsv in - let evi = Evd.map (evars_of isevars) ev in + let evi = Evd.find (evars_of isevars) ev in (* the bindings to invert *) let worklist = make_subst (evar_env evi) args in let (isevars',body) = real_clean env isevars ev evi worklist rhs in @@ -502,7 +503,7 @@ let status_changed lev (pbty,t1,t2) = let solve_refl conv_algo env isevars ev argsv1 argsv2 = if argsv1 = argsv2 then (isevars,[]) else - let evd = Evd.map (evars_of isevars) ev in + let evd = Evd.find (evars_of isevars) ev in let hyps = evar_context evd in let (isevars',_,rsign) = array_fold_left2 @@ -599,7 +600,7 @@ let mk_valcon c = Some c cumulativity now includes Prop and Set in Type... It is, but that's not too bad *) let define_evar_as_abstraction abs evd (ev,args) = - let evi = Evd.map (evars_of evd) ev in + let evi = Evd.find (evars_of evd) ev in let evenv = evar_env evi in let (evd1,dom) = new_evar evd evenv (new_Type()) in let nvar = diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 5da0a1a99..713995641 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -48,17 +48,16 @@ let empty = Evarmap.empty let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc [] let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc [] -let map evc k = Evarmap.find k evc -let rmv evc k = Evarmap.remove k evc -let remap evc k i = Evarmap.add k i evc -let in_dom evc k = Evarmap.mem k evc +let find evc k = Evarmap.find k evc +let remove evc k = Evarmap.remove k evc +let mem evc k = Evarmap.mem k evc let fold = Evarmap.fold let add evd ev newinfo = Evarmap.add ev newinfo evd let define evd ev body = let oldinfo = - try map evd ev + try find evd ev with Not_found -> error "Evd.define: cannot define undeclared evar" in let newinfo = { evar_concl = oldinfo.evar_concl; @@ -68,10 +67,10 @@ let define evd ev body = | Evar_empty -> Evarmap.add ev newinfo evd | _ -> anomaly "Evd.define: cannot define an isevar twice" -let is_evar sigma ev = in_dom sigma ev +let is_evar sigma ev = mem sigma ev let is_defined sigma ev = - let info = map sigma ev in + let info = find sigma ev in not (info.evar_body = Evar_empty) let evar_body ev = ev.evar_body @@ -112,7 +111,7 @@ let instantiate_evar sign c args = let existential_type sigma (n,args) = let info = - try map sigma n + try find sigma n with Not_found -> anomaly ("Evar "^(string_of_existential n)^" was not declared") in let hyps = evar_context info in @@ -121,7 +120,7 @@ let existential_type sigma (n,args) = exception NotInstantiatedEvar let existential_value sigma (n,args) = - let info = map sigma n in + let info = find sigma n in let hyps = evar_context info in match evar_body info with | Evar_defined c -> @@ -270,10 +269,9 @@ type evar_map = evar_map1 * sort_constraints let empty = empty, UniverseMap.empty let add (sigma,sm) k v = (add sigma k v, sm) let dom (sigma,_) = dom sigma -let map (sigma,_) = map sigma -let rmv (sigma,sm) k = (rmv sigma k, sm) -let remap (sigma,sm) k v = (remap sigma k v, sm) -let in_dom (sigma,_) = in_dom sigma +let find (sigma,_) = find sigma +let remove (sigma,sm) k = (remove sigma k, sm) +let mem (sigma,_) = mem sigma let to_list (sigma,_) = to_list sigma let fold f (sigma,_) = fold f sigma let define (sigma,sm) k v = (define sigma k v, sm) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 35bcb67c7..6481ff201 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -43,10 +43,9 @@ val empty : evar_map val add : evar_map -> evar -> evar_info -> evar_map val dom : evar_map -> evar list -val map : evar_map -> evar -> evar_info -val rmv : evar_map -> evar -> evar_map -val remap : evar_map -> evar -> evar_info -> evar_map -val in_dom : evar_map -> evar -> bool +val find : evar_map -> evar -> evar_info +val remove : evar_map -> evar -> evar_map +val mem : evar_map -> evar -> bool val to_list : evar_map -> (evar * evar_info) list val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 82a45ad44..01841641c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -273,7 +273,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | REvar (loc, ev, instopt) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) - let hyps = evar_context (Evd.map (evars_of !isevars) ev) in + let hyps = evar_context (Evd.find (evars_of !isevars) ev) in let args = match instopt with | None -> instance_from_named_context hyps | Some inst -> failwith "Evar subtitutions not implemented" in @@ -657,8 +657,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct let rec proc_rec c = match kind_of_term c with | Evar (ev,args) -> - assert (Evd.in_dom sigma ev); - if not (Evd.in_dom initial_sigma ev) then + assert (Evd.mem sigma ev); + if not (Evd.mem initial_sigma ev) then let (loc,k) = evar_source ev !isevars in error_unsolvable_implicit loc env sigma k | _ -> iter_constr proc_rec c diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 20b48a01a..9a0125025 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -428,13 +428,13 @@ let whd_betadeltaiota_nolet env sigma x = let rec whd_evar sigma c = match kind_of_term c with | Evar (ev,args) - when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> + when Evd.mem sigma ev & Evd.is_defined sigma ev -> whd_evar sigma (Evd.existential_value sigma (ev,args)) | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c | _ -> collapse_appl c -let nf_evar evd = - local_strong (whd_evar evd) +let nf_evar sigma = + local_strong (whd_evar sigma) (* lazy reduction functions. The infos must be created for each term *) let clos_norm_flags flgs env sigma t = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0c5d7d672..f231c728b 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -259,7 +259,7 @@ let w_merge env with_types mod_delta metas evars evd = end and mimick_evar evd mod_delta hdc nargs sp = - let ev = Evd.map (evars_of evd) sp in + let ev = Evd.find (evars_of evd) sp in let sp_env = Global.env_of_context ev.evar_hyps in let (evd', c) = applyHead sp_env evd nargs hdc in let (mc,ec) = diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 0f3fa7584..d5ea25bd3 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -25,7 +25,7 @@ open Refiner let w_refine env ev rawc evd = if Evd.is_defined (evars_of evd) ev then error "Instantiate called on already-defined evar"; - let e_info = Evd.map (evars_of evd) ev in + let e_info = Evd.find (evars_of evd) ev in let env = Evd.evar_env e_info in let sigma,typed_c = Pretyping.Default.understand_tcc (evars_of evd) env diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 0bb4a9735..ee4b672a1 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -263,7 +263,7 @@ let extract_open_proof sigma pf = let meta_cnt = ref 0 in let rec f () = incr meta_cnt; - if in_dom sigma (existential_of_int !meta_cnt) then f () + if Evd.mem sigma (existential_of_int !meta_cnt) then f () else !meta_cnt in f in diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index a321b9f1b..d01cd8ca2 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -23,7 +23,7 @@ open Termops let evar_list evc c = let rec evrec acc c = match kind_of_term c with - | Evar (n, _) when Evd.in_dom evc n -> c :: acc + | Evar (n, _) when Evd.mem evc n -> c :: acc | _ -> fold_constr evrec acc c in evrec [] c diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 2eb2d88f4..56aaee4fe 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1194,11 +1194,11 @@ let solve_remaining_evars env initial_sigma evars c = let isevars = ref evars in let rec proc_rec c = match kind_of_term (Reductionops.whd_evar (evars_of !isevars) c) with - | Evar (ev,args as k) when not (Evd.in_dom initial_sigma ev) -> + | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) -> let (loc,src) = evar_source ev !isevars in let sigma = evars_of !isevars in (try - let evi = Evd.map sigma ev in + let evi = Evd.find sigma ev in let c = solvable_by_tactic env evi k src in isevars := Evd.evar_define ev c !isevars; c diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index 69887a540..5b347b1be 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -14,7 +14,7 @@ As ClassicalDescription.v, it implies the double-negation of excluded-middle in Set and implies a strongly classical world. Especially it conflicts with impredicativity of Set, knowing - that true<>false in Set. + that [true<>false] in Set. *) Require Export ClassicalDescription. |