From dbc820f0df53218e730eba34b44a3b1901f13b9e Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Mar 2018 15:50:32 +0100 Subject: Deprecate mixing univ minimization and evm normalization functions. Normalization sounds like it should be semantically noop. --- engine/evarutil.mli | 3 +++ plugins/funind/glob_termops.ml | 4 ++-- plugins/funind/recdef.ml | 10 ++++------ plugins/setoid_ring/newring.ml | 8 ++++---- tactics/elimschemes.ml | 4 ++-- tactics/tactics.ml | 4 ++-- vernac/classes.ml | 6 +++--- vernac/comFixpoint.ml | 2 +- vernac/comInductive.ml | 10 ++++++---- vernac/lemmas.ml | 2 +- vernac/record.ml | 2 +- vernac/vernacentries.ml | 9 ++++----- 12 files changed, 33 insertions(+), 31 deletions(-) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 40c1ee082..8bb0d2f61 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -178,11 +178,14 @@ val nf_evar_map_undefined : evar_map -> evar_map 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. *) val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evar_map and nf_evars_universes"] (** Replacing all evars, possibly raising [Uninstantiated_evar] *) exception Uninstantiated_evar of Evar.t diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 845104c3c..e331dc014 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -563,8 +563,8 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *) let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in - let ctx, f = Evarutil.nf_evars_and_universes ctx in - let f c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in + let ctx = Evd.minimize_universes ctx in + let f c = EConstr.of_constr (Evarutil.nf_evars_universes ctx (EConstr.Unsafe.to_constr c)) in (* then we map [rt] to replace the implicit holes by their values *) let rec change rt = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index fb9ae64bf..e41bf71dd 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1533,14 +1533,12 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let env = Global.env() in let evd = Evd.from_env env in let evd, function_type = interp_type_evars env evd type_of_f in - let function_type = EConstr.Unsafe.to_constr function_type in - let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in + let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in - let ty = EConstr.Unsafe.to_constr ty in - let evd, nf = Evarutil.nf_evars_and_universes evd in - let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in - let function_type = nf function_type in + let evd = Evd.minimize_universes evd in + let equation_lemma_type = nf_betaiotazeta (Evarutil.nf_evar evd ty) in + let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 99bb8440c..33c30e4d3 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -186,8 +186,8 @@ let dummy_goal env sigma = Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in {Evd.it = gl; Evd.sigma = sigma} -let constr_of v = match Value.to_constr v with - | Some c -> EConstr.Unsafe.to_constr c +let constr_of evd v = match Value.to_constr v with + | Some c -> EConstr.to_constr evd c | None -> failwith "Ring.exec_tactic: anomaly" let tactic_res = ref [||] @@ -221,8 +221,8 @@ let exec_tactic env evd n f args = (** Evaluate the whole result *) let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in - let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in - let nf c = nf (constr_of c) in + let evd = Evd.minimize_universes (Refiner.project gls) in + let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd let stdlib_modules = diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 6bd4866c6..70f73df5c 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -46,8 +46,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = mib.mind_nparams in let sigma, sort = Evd.fresh_sort_in_family env sigma sort in let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in - let sigma, nf = Evarutil.nf_evars_and_universes sigma in - (nf c', Evd.evar_universe_context sigma), eff + let sigma = Evd.minimize_universes sigma in + (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff else let sigma, pind = Evd.fresh_inductive_instance env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index aae4bc088..482571ea8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4929,9 +4929,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let evd, ctx, concl = (* FIXME: should be done only if the tactic succeeds *) - let evd, nf = nf_evars_and_universes !evdref in + let evd = Evd.minimize_universes !evdref in let ctx = Evd.universe_context_set evd in - evd, ctx, nf concl + evd, ctx, Evarutil.nf_evars_universes evd concl in let concl = EConstr.of_constr concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in diff --git a/vernac/classes.ml b/vernac/classes.ml index 3c133f317..a98fc15ce 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -196,7 +196,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma,_ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in Pretyping.check_evars env Evd.empty sigma termtype; let univs = Evd.check_univ_decl ~poly sigma decl in let termtype = to_constr sigma termtype in @@ -289,7 +289,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in let sigma = Evarutil.nf_evar_map_undefined sigma in (* Beware of this step, it is required as to minimize universes. *) - let sigma, _nf = Evarutil.nf_evar_map_universes sigma in + let sigma = Evd.minimize_universes sigma in (* Check that the type is free of evars now. *) Pretyping.check_evars env Evd.empty sigma termtype; let termtype = to_constr sigma termtype in @@ -365,7 +365,7 @@ let context poly l = let sigma = Evd.from_env env in let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in (* Note, we must use the normalized evar from now on! *) - let sigma,_ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in let ce t = Pretyping.check_evars env Evd.empty sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in let ctx = diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 1466fa243..7b382dacc 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -224,7 +224,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Instantiate evars and check all are resolved *) let sigma = solve_unif_constraints_with_heuristics env_rec sigma in - let sigma, _ = nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in (* XXX: We still have evars here in Program *) let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 05c40dbdd..101298ef4 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -304,14 +304,16 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = (* Try further to solve evars, and instantiate them *) let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in (* Compute renewed arities *) - let sigma, nf = nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in + let nf = Evarutil.nf_evars_universes sigma in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let arities = List.map EConstr.(to_constr sigma) arities in let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in - let sigma, nf' = nf_evars_and_universes sigma in - let arities = List.map nf' arities in - let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in + let sigma = Evd.minimize_universes sigma in + let nf = Evarutil.nf_evars_universes sigma in + let arities = List.map nf arities in + let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in let uctx = Evd.check_univ_decl ~poly sigma decl in List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 30dd6ec74..aba5e32db 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -451,7 +451,7 @@ let start_proof_com ?inference_hook kind thms hook = (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps')))) evd thms in let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in - let evd, _nf = Evarutil.nf_evars_and_universes evd in + let evd = Evd.minimize_universes evd in (* XXX: This nf_evar is critical too!! We are normalizing twice if you look at the previous lines... *) let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in diff --git a/vernac/record.ml b/vernac/record.ml index 78e68e8a3..b89c0060d 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -168,7 +168,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = EConstr.mkSort (Sorts.sort_of_univ univ) else sigma, typ in - let sigma, _ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in let newfs = List.map (EConstr.to_rel_decl sigma) newfs in let newps = List.map (EConstr.to_rel_decl sigma) newps in let typ = EConstr.to_constr sigma typ in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a9d1631ba..b9600d23d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1619,17 +1619,16 @@ let vernac_check_may_eval ~atts redexp glopt rc = let glopt = query_command_selector ?loc:atts.loc glopt in let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr env sigma rc in - let c = EConstr.Unsafe.to_constr c in let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in Evarconv.check_problems_are_solved env sigma'; - let sigma',nf = Evarutil.nf_evars_and_universes sigma' in + let sigma' = Evd.minimize_universes sigma' in let uctx = Evd.universe_context_set sigma' in let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in - let c = nf c in let j = - if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then - Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c)) + if Evarutil.has_undefined_evars sigma' c then + Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) else + let c = EConstr.to_constr sigma' c in (* OK to call kernel which does not support evars *) Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c) in -- cgit v1.2.3