From 5d926b0279f70250db1ee54edcdb4e855ac96f0f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Mar 2018 14:58:00 +0100 Subject: Deprecate UState aliases in Evd. --- tactics/eqschemes.ml | 12 ++++++------ tactics/ind_tables.ml | 4 ++-- 2 files changed, 8 insertions(+), 8 deletions(-) (limited to 'tactics') diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 45926551b..477de6452 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -214,7 +214,7 @@ let build_sym_scheme env ind = rel_vect (2*nrealargs+2) nrealargs])), mkRel 1 (* varH *), [|cstr (nrealargs+1)|])))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" @@ -285,7 +285,7 @@ let build_sym_involutive_scheme env ind = mkRel 1|])), mkRel 1 (* varH *), [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))) - in (c, Evd.evar_universe_context_of ctx), eff + in (c, UState.of_context_set ctx), eff let sym_involutive_scheme_kind = declare_individual_scheme_object "_sym_involutive" @@ -439,7 +439,7 @@ let build_l2r_rew_scheme dep env ind kind = [|main_body|]) else main_body)))))) - in (c, Evd.evar_universe_context_of ctx), + in (c, UState.of_context_set ctx), Safe_typing.concat_private eff' eff (**********************************************************************) @@ -528,7 +528,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s) (mkNamedLambda varHC applied_PC' (mkVar varHC))|]))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx (**********************************************************************) (* Build the right-to-left rewriting lemma for hypotheses associated *) @@ -601,7 +601,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = lift (nrealargs+3) applied_PC, mkRel 1)|]), [|mkVar varHC|])))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx (**********************************************************************) (* This function "repairs" the non-dependent r2l forward rewriting *) @@ -808,7 +808,7 @@ let build_congr env (eq,refl,ctx) ind = [|mkApp (refl, [|mkVar varB; mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index b960a845c..71e2d5820 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -122,8 +122,8 @@ let compute_name internal id = let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in - let ctx = Evd.normalize_evar_universe_context univs in - let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in + let ctx = UState.normalize univs in + let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) else Monomorphic_const_entry (UState.context_set ctx) -- cgit v1.2.3 From 66973ce17e32a3c692a5b0032f38300ec8cc36d3 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Mar 2018 15:10:39 +0100 Subject: Rename some universe minimizing "normalize" functions to "minimize" UState normalize -> minimize, Evd nf_constraints -> minimize_universes --- engine/evarutil.ml | 6 +++--- engine/evd.ml | 7 ++++--- engine/evd.mli | 5 ++++- engine/uState.ml | 5 ++++- engine/uState.mli | 3 +++ plugins/ltac/rewrite.ml | 2 +- proofs/proof_global.ml | 2 +- tactics/ind_tables.ml | 2 +- tactics/leminv.ml | 2 +- vernac/comAssumption.ml | 2 +- vernac/comDefinition.ml | 2 +- vernac/vernacentries.ml | 2 +- 12 files changed, 25 insertions(+), 15 deletions(-) (limited to 'tactics') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 7674cf67a..6b3ce048f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -89,15 +89,15 @@ let nf_evars_universes evm = (Evd.universe_subst evm) let nf_evars_and_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in evm, nf_evars_universes evm let e_nf_evars_and_universes evdref = - evdref := Evd.nf_constraints !evdref; + evdref := Evd.minimize_universes !evdref; nf_evars_universes !evdref, Evd.universe_subst !evdref let nf_evar_map_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in let subst = Evd.universe_subst evm in if Univ.LMap.is_empty subst then evm, nf_evar0 evm else diff --git a/engine/evd.ml b/engine/evd.ml index 47fa48d4f..185cab101 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -900,9 +900,9 @@ let nf_univ_variables evd = let evd' = {evd with universes = uctx'} in evd', subst -let nf_constraints evd = +let minimize_universes evd = let subst, uctx' = UState.normalize_variables evd.universes in - let uctx' = UState.normalize uctx' in + let uctx' = UState.minimize uctx' in {evd with universes = uctx'} let universe_of_name evd s = UState.universe_of_name evd.universes s @@ -1167,4 +1167,5 @@ let make_evar_universe_context e l = | Some l -> UState.make_with_initial_binders g l let normalize_evar_universe_context_variables = UState.normalize_variables let abstract_undefined_variables = UState.abstract_undefined_variables -let normalize_evar_universe_context = UState.normalize +let normalize_evar_universe_context = UState.minimize +let nf_constraints = minimize_universes diff --git a/engine/evd.mli b/engine/evd.mli index 25dc8c993..7957eaa01 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -533,7 +533,7 @@ val normalize_evar_universe_context_variables : UState.t -> [@@ocaml.deprecated "Alias of UState.normalize_variables"] val normalize_evar_universe_context : UState.t -> UState.t -[@@ocaml.deprecated "Alias of UState.normalize"] +[@@ocaml.deprecated "Alias of UState.minimize"] val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t @@ -598,7 +598,10 @@ val fix_undefined_variables : evar_map -> evar_map val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst +(** Universe minimization *) +val minimize_universes : evar_map -> evar_map val nf_constraints : evar_map -> evar_map +[@@ocaml.deprecated "Alias of Evd.minimize_universes"] val update_sigma_env : evar_map -> env -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index 67479351a..e57afd743 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -585,7 +585,7 @@ let refresh_undefined_univ_variables uctx = uctx_initial_universes = initial } in uctx', subst -let normalize uctx = +let minimize uctx = let ((vars',algs'), us') = Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic @@ -613,3 +613,6 @@ let update_sigma_env uctx env = uctx_universes = univs } in merge true univ_rigid eunivs eunivs.uctx_local + +(** Deprecated *) +let normalize = minimize diff --git a/engine/uState.mli b/engine/uState.mli index ef7cee32e..9a2bc706b 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -133,7 +133,10 @@ val fix_undefined_variables : t -> t val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst +(** Universe minimization *) +val minimize : t -> t val normalize : t -> t +[@@ocaml.deprecated "Alias of UState.minimize"] type universe_decl = (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 6e38b4641..e0368153e 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1922,7 +1922,7 @@ let build_morphism_signature env sigma m = in let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in let evd = solve_constraints env !evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m); Evd.evar_universe_context evd, m diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index b290a20ff..8b5b739a3 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -436,7 +436,7 @@ let return_proof ?(allow_partial=false) () = | Proof.HasUnresolvedEvar-> error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in let eff = Evd.eval_side_effects evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 71e2d5820..62ead57f3 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -122,7 +122,7 @@ let compute_name internal id = let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in - let ctx = UState.normalize univs in + let ctx = UState.minimize univs in let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 655283c20..a4cdc1592 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -218,7 +218,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = end in let avoid = ref Id.Set.empty in let _,_,_,_,sigma = Proof.proof pf in - let sigma = Evd.nf_constraints sigma in + let sigma = Evd.minimize_universes sigma in let rec fill_holes c = match EConstr.kind sigma c with | Evar (e,args) -> diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 1712634da..6a590758f 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -160,7 +160,7 @@ let do_assumptions kind nl l = in let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in (* The universe constraints come from the whole telescope. *) - let sigma = Evd.nf_constraints sigma in + let sigma = Evd.minimize_universes sigma in let nf_evar c = EConstr.to_constr sigma c in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 01dbe0a0d..b18a60a1f 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -85,7 +85,7 @@ let interp_definition pl bl poly red_option c ctypopt = evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty in (* universe minimization *) - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in (* Substitute evars and universes, and add parameters. Note: in program mode some evars may remain. *) let ctx = List.map (EConstr.to_rel_decl evd) ctx in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0ff6d9c17..26c6a8cbe 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -72,7 +72,7 @@ let show_top_evars () = let show_universes () = let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in - let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in + let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx -- cgit v1.2.3