From dac8b249e95d376de587d7b527fd17f70e4942fc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 4 Oct 2018 23:21:57 +0200 Subject: [api] Deprecate `evar_map` ref combinators. All the `evar_map` APIs were deprecated in 8.9, thus we deprecate the combinators to discourage this style of programming. Still a few places do use imperative style, but they are pretty localized and should be cleaned up separately. As these are the last bits of `e_` API remaining this PR closes #6342. --- engine/evarutil.mli | 3 +++ plugins/funind/functional_principles_types.ml | 8 +++++--- pretyping/cases.ml | 3 ++- pretyping/evarsolve.ml | 3 ++- pretyping/indrec.ml | 4 ++-- tactics/inv.ml | 15 ++++++++++----- 6 files changed, 24 insertions(+), 12 deletions(-) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 1046fdc8d8..11e07175e3 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -258,8 +258,11 @@ val generalize_evar_over_rels : evar_map -> existential -> types * constr list (** Evar combinators *) val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a +[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"] val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a +[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"] val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a +[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"] val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 839915631d..f7094ebe51 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -322,7 +322,8 @@ let generate_functional_principle (evd: Evd.evar_map ref) try let f = funs.(i) in - let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in + let sigma, type_sort = Evd.fresh_sort_in_family !evd InType in + evd := sigma; let new_sorts = match sorts with | None -> Array.make (Array.length funs) (type_sort) @@ -507,8 +508,9 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let i = ref (-1) in let sorts = List.rev_map (fun (_,x) -> - Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x - ) + let sigma, fs = Evd.fresh_sort_in_family !evd x in + evd := sigma; fs + ) fas in (* We create the first priciple by tactic *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 2c821c96ba..9fa8442f8a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1713,7 +1713,8 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = let vl = List.map pi1 good in let ty = let ty = get_type_of !!env sigma t in - Evarutil.evd_comb1 (refresh_universes (Some false) !!env) evdref ty + let sigma, res = refresh_universes (Some false) !!env !evdref ty in + evdref := sigma; res in let dummy_subst = List.init k (fun _ -> mkProp) in let ty = substl dummy_subst (aux x ty) in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index c0565f4f47..44bfe4b6cc 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -46,7 +46,8 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) (* direction: true for fresh universes lower than the existing ones *) let refresh_sort status ~direction s = let s = ESorts.kind !evdref s in - let s' = evd_comb0 (new_sort_variable status) evdref in + let sigma, s' = new_sort_variable status !evdref in + evdref := sigma; let evd = if direction then set_leq_sort env !evdref s' s else set_leq_sort env !evdref s s' diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 4ee7e667fe..e49ba75b3f 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -455,8 +455,8 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = | ((indi,u),_,_,dep,kinds)::rest -> let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list mkRel i lnamesparrec) in let s = - Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg) - evdref kinds + let sigma, res = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg !evdref kinds in + evdref := sigma; res in let typP = make_arity env !evdref dep indf s in let typP = EConstr.Unsafe.to_constr typP in diff --git a/tactics/inv.ml b/tactics/inv.ml index f718b13a63..5ac4284b43 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -70,6 +70,11 @@ type inversion_kind = | FullInversion | FullInversionClear +let evd_comb1 f evdref x = + let (evd',y) = f !evdref x in + evdref := evd'; + y + let compute_eqn env sigma n i ai = (mkRel (n-i),get_type_of env sigma (mkRel (n-i))) @@ -94,7 +99,7 @@ let make_inv_predicate env evd indf realargs id status concl = | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*) | None -> let sort = get_sort_family_of env !evd concl in - let sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd sort in + let sort = evd_comb1 Evd.fresh_sort_in_family evd sort in let p = make_arity env !evd true indf sort in let evd',(p,ptyp) = Unification.abstract_list_all env !evd p concl (realargs@[mkVar id]) @@ -124,19 +129,19 @@ let make_inv_predicate env evd indf realargs id status concl = evd := sigma; res in let eq_term = eqdata.Coqlib.eq in - let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in + let eq = evd_comb1 (Evd.fresh_global env) evd eq_term in let eqn = applist (eq,[eqnty;lhs;rhs]) in let eqns = (Anonymous, lift n eqn) :: eqns in let refl_term = eqdata.Coqlib.refl in - let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in + let refl_term = evd_comb1 (Evd.fresh_global env) evd refl_term in let refl = mkApp (refl_term, [|eqnty; rhs|]) in - let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in + let _ = evd_comb1 (Typing.type_of env) evd refl in let args = refl :: args in build_concl eqns args (succ n) restlist in let (newconcl, args) = build_concl [] [] 0 realargs in let predicate = it_mkLambda_or_LetIn newconcl (name_context env !evd hyps) in - let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in + let _ = evd_comb1 (Typing.type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) predicate, args -- cgit v1.2.3