From 864fda19d046428023851ba540b82c5ca24d06a4 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 25 Apr 2018 18:08:39 +0200 Subject: Deprecate most evarutil evdref functions clear_hyps remain with no alternative --- engine/evarutil.mli | 38 +++++++++++++++++------------- plugins/setoid_ring/newring.ml | 53 +++++++++++++++++++++++------------------- pretyping/cases.ml | 18 +++++++++----- pretyping/coercion.ml | 4 +++- pretyping/evarconv.ml | 10 ++++++++ pretyping/evarconv.mli | 3 +++ pretyping/program.ml | 4 +++- pretyping/unification.ml | 4 ++-- tactics/equality.ml | 36 ++++++++++++++-------------- tactics/tactics.ml | 3 ++- 10 files changed, 105 insertions(+), 68 deletions(-) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 3bbd2923c..7595de04c 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -50,13 +50,6 @@ val new_pure_evar : val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t -(** the same with side-effects *) -val e_new_evar : - env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> types -> constr - (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : @@ -65,13 +58,7 @@ val new_type_evar : ?principal:bool -> ?hypnaming:naming_mode -> rigid -> evar_map * (constr * Sorts.t) -val e_new_type_evar : env -> evar_map ref -> - ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t - val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr -val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr val restrict_evar : evar_map -> Evar.t -> Filter.t -> ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t @@ -79,7 +66,6 @@ val restrict_evar : evar_map -> Evar.t -> Filter.t -> (** Polymorphic constants *) val new_global : evar_map -> GlobRef.t -> evar_map * constr -val e_new_global : evar_map ref -> GlobRef.t -> constr (** Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context @@ -187,8 +173,6 @@ val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) [@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] -val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst -[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] (** Normalize the evar map w.r.t. universes, after simplification of constraints. Return the substitution function for constrs as well. *) @@ -276,3 +260,25 @@ type type_constraint = types option [@@ocaml.deprecated "use the version in Evardefine"] type val_constraint = constr option [@@ocaml.deprecated "use the version in Evardefine"] + +val e_new_evar : + env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> types -> constr +[@@ocaml.deprecated "Use [Evd.new_evar]"] + +val e_new_type_evar : env -> evar_map ref -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t +[@@ocaml.deprecated "Use [Evd.new_type_evar]"] + +val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr +[@@ocaml.deprecated "Use [Evd.new_Type]"] + +val e_new_global : evar_map ref -> GlobRef.t -> constr +[@@ocaml.deprecated "Use [Evd.new_global]"] + +val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 5facf2a80..b2ac3b5a4 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -247,9 +247,10 @@ let coq_nil = coq_reference "nil" let lapp f args = mkApp(Lazy.force f,args) -let plapp evd f args = - let fc = Evarutil.e_new_global evd (Lazy.force f) in - mkApp(fc,args) +let plapp evdref f args = + let evd, fc = Evarutil.new_global !evdref (Lazy.force f) in + evdref := evd; + mkApp(fc,args) let dest_rel0 sigma t = match EConstr.kind sigma t with @@ -586,48 +587,52 @@ let make_hyp env evd c = let t = Retyping.get_type_of env !evd c in plapp evd coq_mkhypo [|t;c|] -let make_hyp_list env evd lH = - let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in +let make_hyp_list env evdref lH = + let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in + evdref := evd; let l = List.fold_right - (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH - (plapp evd coq_nil [|carrier|]) + (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH + (plapp evdref coq_nil [|carrier|]) in - let l' = Typing.e_solve_evars env evd l in + let l' = Typing.e_solve_evars env evdref l in let l' = EConstr.Unsafe.to_constr l' in - Evarutil.nf_evars_universes !evd l' + Evarutil.nf_evars_universes !evdref l' -let interp_power env evd pow = - let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in +let interp_power env evdref pow = + let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in + evdref := evd; match pow with | None -> let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in - (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evd coq_None [|carrier|]) + (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evdref coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with | CstTac t -> Tacintern.glob_tactic t | Closed lc -> closed_term_ast (List.map Smartlocate.global_with_alias lc) in - let spec = make_hyp env evd (ic_unsafe spec) in - (tac, plapp evd coq_Some [|carrier; spec|]) + let spec = make_hyp env evdref (ic_unsafe spec) in + (tac, plapp evdref coq_Some [|carrier; spec|]) -let interp_sign env evd sign = - let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in +let interp_sign env evdref sign = + let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in + evdref := evd; match sign with - | None -> plapp evd coq_None [|carrier|] + | None -> plapp evdref coq_None [|carrier|] | Some spec -> - let spec = make_hyp env evd (ic_unsafe spec) in - plapp evd coq_Some [|carrier;spec|] + let spec = make_hyp env evdref (ic_unsafe spec) in + plapp evdref coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) -let interp_div env evd div = - let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in +let interp_div env evdref div = + let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in + evdref := evd; match div with - | None -> plapp evd coq_None [|carrier|] + | None -> plapp evdref coq_None [|carrier|] | Some spec -> - let spec = make_hyp env evd (ic_unsafe spec) in - plapp evd coq_Some [|carrier;spec|] + let spec = make_hyp env evdref (ic_unsafe spec) in + plapp evdref coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div = diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4c87b4e7e..16244d8c0 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -295,7 +295,8 @@ let inductive_template evdref env tmloc ind = | LocalAssum (na,ty) -> let ty = EConstr.of_constr ty in let ty' = substl subst ty in - let e = e_new_evar env evdref ~src:(hole_source n) ty' in + let evd, e = Evarutil.new_evar env !evdref ~src:(hole_source n) ty' in + evdref := evd; (e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> let b = EConstr.of_constr b in @@ -396,7 +397,9 @@ let coerce_to_indtype typing_fun evdref env lvar matx tomatchl = (* Utils *) let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref = - let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e + let evd, (e, u) = new_type_evar env !evdref univ_flexible_alg ~src:src in + evdref := evd; + e let evd_comb2 f evdref x y = let (evd',y) = f !evdref x y in @@ -1681,7 +1684,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in - let ev' = e_new_evar env evdref ~src ty in + let evd, ev' = Evarutil.new_evar env !evdref ~src ty in + evdref := evd; begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false @@ -1712,7 +1716,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in - let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in + let evd, ev = Evarutil.new_evar extenv !evdref ~src ~filter ~candidates ty in + evdref := evd; lift k ev in aux (0,extenv,subst0) t0 @@ -1724,8 +1729,9 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = we are in an impossible branch *) let n = Context.Rel.length (rel_context env) in let n' = Context.Rel.length (rel_context tycon_env) in - let impossible_case_type, u = - e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in + let evd, (impossible_case_type, u) = + new_type_evar (reset_context env) !evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in + evdref := evd; (lift (n'-n) impossible_case_type, mkSort u) | Some t -> let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 6dc3687a0..e8b17d694 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -94,7 +94,9 @@ open Program let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c = let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in - Evarutil.e_new_evar env evdref ~src c + let evd, v = Evarutil.new_evar env !evdref ~src c in + evdref := evd; + v let app_opt env evdref f t = whd_betaiota !evdref (app_opt f t) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 144166a34..2144639d5 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1394,6 +1394,16 @@ let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) +let make_opt = function + | Success evd -> Some evd + | UnifFailure _ -> None + +let conv env ?(ts=default_transparent_state env) evd t1 t2 = + make_opt(evar_conv_x ts env evd CONV t1 t2) + +let cumul env ?(ts=default_transparent_state env) evd t1 t2 = + make_opt(evar_conv_x ts env evd CUMUL t1 t2) + let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 = match evar_conv_x ts env !evdref CONV t1 t2 with | Success evd' -> evdref := evd'; true diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 9270d6e3a..da2b4d1b8 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -30,6 +30,9 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma val e_conv : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool +val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option +val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option + (** {6 Unification heuristics. } *) (** Try heuristics to solve pending unification problems and to solve diff --git a/pretyping/program.ml b/pretyping/program.ml index 52d940d8e..8cfb7966c 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -16,7 +16,9 @@ let init_reference dir s () = Coqlib.coq_reference "Program" dir s let papp evdref r args = let open EConstr in let gr = delayed_force r in - mkApp (Evarutil.e_new_global evdref gr, args) + let evd, hd = Evarutil.new_global !evdref gr in + evdref := evd; + mkApp (hd, args) let sig_typ = init_reference ["Init"; "Specif"] "sig" let sig_intro = init_reference ["Init"; "Specif"] "exist" diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d98ce9aba..1caa629ff 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -198,8 +198,8 @@ let pose_all_metas_as_evars env evd t = then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in let src = Evd.evar_source_of_meta mv !evdref in - let ev = Evarutil.e_new_evar env evdref ~src ty in - evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; + let evd, ev = Evarutil.new_evar env !evdref ~src ty in + evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd; ev) | _ -> EConstr.map !evdref aux t in diff --git a/tactics/equality.ml b/tactics/equality.ml index b6bbd0be4..d142e10a4 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1176,34 +1176,35 @@ let minimal_free_rels_rec env sigma = let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let sigdata = find_sigma_data env sort_of_ty in - let evdref = ref (Evd.clear_metas sigma) in - let rec sigrec_clausal_form siglen p_i = + let rec sigrec_clausal_form sigma siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) let dflt_typ = unsafe_type_of env sigma dflt in try - let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in - let () = - evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in - dflt + let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in + let sigma = + Evarconv.solve_unif_constraints_with_heuristics env sigma in + sigma, dflt with Evarconv.UnableToUnify _ -> user_err Pp.(str "Cannot solve a unification problem.") else - let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with + let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with | (_sigS,[a;p]) -> (a, p) | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in - let ev = Evarutil.e_new_evar env evdref a in + let sigma, ev = Evarutil.new_evar env sigma a in let rty = beta_applist sigma (p_i_minus_1,[ev]) in - let tuple_tail = sigrec_clausal_form (siglen-1) rty in - let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in + let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in + let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in match evopt with | Some w -> - let w_type = unsafe_type_of env !evdref w in - if Evarconv.e_cumul env evdref w_type a then - let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in - applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) - else + let w_type = unsafe_type_of env sigma w in + begin match Evarconv.cumul env sigma w_type a with + | Some sigma -> + let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in + sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + | None -> user_err Pp.(str "Cannot solve a unification problem.") + end | None -> (* This at least happens if what has been detected as a dependency is not one; use an evasive error message; @@ -1213,8 +1214,9 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = unsolved evars would mean not binding rel *) user_err Pp.(str "Cannot solve a unification problem.") in - let scf = sigrec_clausal_form siglen ty in - !evdref, Evarutil.nf_evar !evdref scf + let sigma = Evd.clear_metas sigma in + let sigma, scf = sigrec_clausal_form sigma siglen ty in + sigma, Evarutil.nf_evar sigma scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ee76ad077..178c10815 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3840,7 +3840,8 @@ let specialize_eqs id = | _ -> if in_eqs then acc, in_eqs, ctx, ty else - let e = e_new_evar (push_rel_context ctx env) evars t in + let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in + evars := sigma; aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) | t -> acc, in_eqs, ctx, ty in -- cgit v1.2.3