From 60770e86f4ec925fce52ad3565a92beb98d253c1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 22:21:46 +0200 Subject: Stop exposing UState.universe_context and its Evd wrapper. We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former). --- API/API.mli | 4 ++-- engine/evd.ml | 3 +-- engine/evd.mli | 9 +++++++-- engine/uState.mli | 23 +++++++++-------------- interp/modintern.ml | 2 +- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/recdef.ml | 2 +- plugins/ltac/rewrite.ml | 2 +- plugins/setoid_ring/newring.ml | 2 +- proofs/proof_global.ml | 2 +- tactics/ind_tables.ml | 2 +- tactics/leminv.ml | 2 +- test-suite/success/polymorphism.v | 2 ++ vernac/class.ml | 2 +- vernac/command.ml | 4 +--- vernac/indschemes.ml | 2 +- vernac/lemmas.ml | 15 ++++++++------- vernac/obligations.ml | 13 +++++++------ 18 files changed, 47 insertions(+), 46 deletions(-) diff --git a/API/API.mli b/API/API.mli index 889050d90..5c7860671 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2881,12 +2881,12 @@ sig val universe_context_set : evar_map -> Univ.ContextSet.t val evar_ident : evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list - val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> - Univ.UContext.t val universe_binders : evar_map -> Universes.universe_binders val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map + val to_universe_context : evar_map -> Univ.UContext.t + val meta_list : evar_map -> (Constr.metavariable * clbinding) list val meta_defined : evar_map -> Constr.metavariable -> bool diff --git a/engine/evd.ml b/engine/evd.ml index 67ae73ceb..eb0f2e3e7 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -756,8 +756,7 @@ let evar_universe_context d = d.universes let universe_context_set d = UState.context_set d.universes -let universe_context ~names ~extensible evd = - UState.universe_context ~names ~extensible evd.universes +let to_universe_context evd = UState.context evd.universes let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl diff --git a/engine/evd.mli b/engine/evd.mli index b6157202d..49b6a7583 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -492,6 +492,8 @@ type 'a in_evar_universe_context = 'a * UState.t val evar_universe_context_set : UState.t -> Univ.ContextSet.t val evar_universe_context_constraints : UState.t -> Univ.constraints val evar_context_universe_context : UState.t -> Univ.UContext.t +[@@ocaml.deprecated "alias of UState.context"] + val evar_universe_context_of : Univ.ContextSet.t -> UState.t val empty_evar_universe_context : UState.t val union_evar_universe_context : UState.t -> UState.t -> @@ -552,11 +554,14 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t -val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> - Univ.UContext.t val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t +(** [to_universe_context evm] extracts the local universes and + constraints of [evm] and orders the universes the same as + [Univ.ContextSet.to_context]. *) +val to_universe_context : evar_map -> Univ.UContext.t + val check_univ_decl : evar_map -> UState.universe_decl -> Univ.UContext.t diff --git a/engine/uState.mli b/engine/uState.mli index 38af08f91..5279c6388 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -125,23 +125,18 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst val normalize : t -> t -(** [universe_context names extensible ctx] - - Return a universe context containing the local universes of [ctx] - and their constraints. The universes corresponding to [names] come - first in the order defined by that list. - - If [extensible] is false, check that the universes of [names] are - the only local universes. - - Also return the association list of universe names and universes - (including those not in [names]). *) -val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t -> - Univ.UContext.t - type universe_decl = (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl +(** [check_univ_decl ctx decl] + + If non extensible in [decl], check that the local universes (resp. + universe constraints) in [ctx] are implied by [decl]. + + Return a universe context containing the local universes of [ctx] + and their constraints. The universes corresponding to + [decl.univdecl_instance] come first in the order defined by that + list. *) val check_univ_decl : t -> universe_decl -> Univ.UContext.t (** {5 TODO: Document me} *) diff --git a/interp/modintern.ml b/interp/modintern.ml index 08657936e..3eb91d8cd 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -62,7 +62,7 @@ let transl_with_decl env = function WithMod (fqid,lookup_module qid) | CWith_Definition ((_,fqid),c) -> let c, ectx = interp_constr env (Evd.from_env env) c in - let ctx = Evd.evar_context_universe_context ectx in + let ctx = UState.context ectx in WithDef (fqid,(c,ctx)) let loc_of_module l = l.CAst.loc diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d5bff57af..076fba861 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -348,7 +348,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = Evd.universe_context ~names:[] ~extensible:true evd' in + let univs = Evd.to_universe_context evd' in let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in ignore( Declare.declare_constant diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 63896bb56..320f7c7f3 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1556,7 +1556,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let ctx = Evd.universe_context ~names:[] ~extensible:true evm in + let ctx = Evd.to_universe_context evm in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in (* Refresh the global universes, now including those of _F *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2eb660219..f6523d28c 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1884,7 +1884,7 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let ctx = Evd.universe_context ~names:[] ~extensible:true sigma in + let ctx = Evd.to_universe_context sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index a37b35b3d..6d0b6fd09 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = 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 - Array.map nf !tactic_res, Evd.universe_context ~names:[] ~extensible:true evd + Array.map nf !tactic_res, Evd.to_universe_context evd let stdlib_modules = [["Coq";"Setoids";"Setoid"]; diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 9faff3211..ea0408169 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -353,7 +353,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let used_univs_typ = Univops.universes_of_constr typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then - let initunivs = Evd.evar_context_universe_context initial_euctx in + let initunivs = UState.context initial_euctx in let ctx = constrain_variables initunivs universes in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e7fa555c2..92c326b1e 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -123,7 +123,7 @@ let define internal id c p univs = let ctx = Evd.normalize_evar_universe_context univs in let c = Vars.subst_univs_fn_constr (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in - let univs = Evd.evar_context_universe_context ctx in + let univs = UState.context ctx in let univs = if p then Polymorphic_const_entry univs else Monomorphic_const_entry univs diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 4d1b271d6..1ee873e0f 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -232,7 +232,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let invProof = it_mkNamedLambda_or_LetIn c !ownSign in let invProof = EConstr.Unsafe.to_constr invProof in let p = Evarutil.nf_evars_universes sigma invProof in - p, Evd.universe_context ~names:[] ~extensible:true sigma + p, Evd.to_universe_context sigma let add_inversion_lemma name env sigma t sort dep inv_op = let invProof, univs = inversion_scheme env sigma t sort dep inv_op in diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 7eaafc354..00cab744e 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -190,6 +190,8 @@ Module binders. Fail Defined. Abort. + Fail Lemma bar@{u v | } : let x := (fun x => x) : Type@{u} -> Type@{v} in nat. + Lemma bar@{i j| i < j} : Type@{j}. Proof. exact Type@{i}. diff --git a/vernac/class.ml b/vernac/class.ml index e59482b71..68fd22cb6 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -212,7 +212,7 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = Evd.universe_context ~names:[] ~extensible:true sigma in + let univs = Evd.to_universe_context sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry (definition_entry ~types:typ_f ~poly ~univs diff --git a/vernac/command.ml b/vernac/command.ml index 5a063f173..80599c534 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -1022,8 +1022,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let binders_rel = nf_evar_context !evdref binders_rel in let binders = nf_evar_context !evdref binders in let top_arity = Evarutil.nf_evar !evdref top_arity in - let pl, plext = Option.cata - (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in let hook, recname, typ = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in @@ -1031,7 +1029,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in - let univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in + let univs = Evd.check_univ_decl !evdref decl in (*FIXME poly? *) let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in (** FIXME: include locality *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 58f39e303..c728c2671 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -109,7 +109,7 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in - let univs = Evd.universe_context ~names:[] ~extensible:true ctx in + let univs = Evd.to_universe_context ctx in let univs = if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs else Monomorphic_const_entry univs diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index cd30c7a68..71d80c4db 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -49,7 +49,8 @@ let retrieve_first_recthm uctx = function (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - let uctx = UState.universe_context ~names:[] ~extensible:true uctx in + (* we get the right order somehow but surely it could be enforced in a better way *) + let uctx = UState.context uctx in let inst = Univ.UContext.instance uctx in let map (c, ctx) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body cb), is_opaque cb) @@ -420,8 +421,8 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in - let body = Option.map norm body in + let ctx = UState.check_univ_decl ctx decl in + let body = Option.map norm body in List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> @@ -453,9 +454,9 @@ let start_proof_com ?inference_hook kind thms hook = let evd, nf = Evarutil.nf_evars_and_universes !evdref in let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in let () = - if not decl.Misctypes.univdecl_extensible_instance then - ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false) - else () + let open Misctypes in + if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then + ignore (Evd.check_univ_decl evd decl) in let evd = if pi2 kind then evd @@ -490,7 +491,7 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = Evd.evar_context_universe_context (fst universes) in + let ctx = UState.context (fst universes) in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) | None -> diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 216801811..43af8968f 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -479,7 +479,7 @@ let declare_definition prg = let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) - ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) + ~univs:(UState.context prg.prg_ctx) (nf body) in let () = progmap_remove prg in let ubinders = UState.universe_binders prg.prg_ctx in @@ -549,7 +549,7 @@ let declare_mutual_definition l = mk_proof (mkCoFix (i,fixdecls))) 0 l in (* Declare the recursive definitions *) - let ctx = Evd.evar_context_universe_context first.prg_ctx in + let ctx = UState.context first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx) fixnames fixdecls fixtypes fiximps in @@ -855,7 +855,7 @@ let obligation_terminator name num guard hook auto pf = | (_, status), Vernacexpr.Transparent -> status in let obl = { obl with obl_status = false, status } in - let uctx = Evd.evar_context_universe_context ctx in + let uctx = UState.context ctx in let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in @@ -890,7 +890,8 @@ in let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in Univ.Instance.empty, Evd.evar_universe_context ctx' else - let uctx = UState.universe_context ~names:[] ~extensible:true ctx' in + (* We get the right order somehow, but surely it could be enforced in a clearer way. *) + let uctx = UState.context ctx' in Univ.UContext.instance uctx, ctx' in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in @@ -969,7 +970,7 @@ and solve_obligation_by_tac prg obls i tac = solve_by_tac obl.obl_name (evar_of_obligation obl) tac (pi2 prg.prg_kind) (Evd.evar_universe_context evd) in - let uctx = Evd.evar_context_universe_context ctx in + let uctx = UState.context ctx in let prg = {prg with prg_ctx = ctx} in let def, obl' = declare_obligation prg obl t ty uctx in obls.(i) <- obl'; @@ -1120,7 +1121,7 @@ let admit_prog prg = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let ctx = Evd.evar_context_universe_context prg.prg_ctx in + let ctx = UState.context prg.prg_ctx in let kn = Declare.declare_constant x.obl_name ~local:true (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural) in -- cgit v1.2.3