diff options
33 files changed, 313 insertions, 92 deletions
diff --git a/CHANGES.md b/CHANGES.md index 5ff90b5123..1f88b77b51 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -120,6 +120,10 @@ Universes - Added `Print Universes Subgraph` variant of `Print Universes`. Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).` +- Added private universes for opaque polymorphic constants, see doc + for the "Private Polymorphic Universes" option (and Unset it to get + the previous behaviour). + Misc - Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances. diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 77f4cea0c6..b83fe831bb 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -19,7 +19,13 @@ let check_constant_declaration env kn cb = | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env | Polymorphic_const auctx -> let ctx = Univ.AUContext.repr auctx in - true, push_context ~strict:false ctx env + let env = push_context ~strict:false ctx env in + true, env + in + let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with + | None, _ -> env' + | Some local, (OpaqueDef _, true) -> push_subgraph local env' + | Some _, _ -> assert false in let ty = cb.const_type in let _ = infer_type env' ty in diff --git a/checker/values.ml b/checker/values.ml index 628089433a..dcb2bca81a 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -227,6 +227,7 @@ let v_cb = v_tuple "constant_body" v_constr; Any; v_const_univs; + Opt v_context_set; v_bool; v_typing_flags|] diff --git a/dev/ci/user-overlays/08850-poly-local-univs.sh b/dev/ci/user-overlays/08850-poly-local-univs.sh new file mode 100644 index 0000000000..482792d7cd --- /dev/null +++ b/dev/ci/user-overlays/08850-poly-local-univs.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8850" ] || [ "$CI_BRANCH" = "poly-local-univs" ]; then + formal_topology_CI_REF=poly-local-univs + formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology + + paramcoq_CI_REF=poly-local-univs + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq +fi diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 99b883d23c..04aedd0cf6 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -443,3 +443,60 @@ underscore or by omitting the annotation to a polymorphic definition. semantics that the first use declares it. In this mode, the universe names are not associated with the definition or proof once it has been defined. This is meant mainly for debugging purposes. + +.. flag:: Private Polymorphic Universes + + This option, on by default, removes universes which appear only in + the body of an opaque polymorphic definition from the definition's + universe arguments. As such, no value needs to be provided for + these universes when instanciating the definition. Universe + constraints are automatically adjusted. + + Consider the following definition: + + .. coqtop:: all + + Lemma foo@{i} : Type@{i}. + Proof. exact Type. Qed. + Print foo. + + The universe :g:`Top.xxx` for the :g:`Type` in the body cannot be accessed, we + only care that one exists for any instantiation of the universes + appearing in the type of :g:`foo`. This is guaranteed when the + transitive constraint ``Set <= Top.xxx < i`` is verified. Then when + using the constant we don't need to put a value for the inner + universe: + + .. coqtop:: all + + Check foo@{_}. + + and when not looking at the body we don't mention the private + universe: + + .. coqtop:: all + + About foo. + + To recover the same behaviour with regard to universes as + :g:`Defined`, the option :flag:`Private Polymorphic Universes` may + be unset: + + .. coqtop:: all + + Unset Private Polymorphic Universes. + + Lemma bar : Type. Proof. exact Type. Qed. + About bar. + Fail Check bar@{_}. + Check bar@{_ _}. + + Note that named universes are always public. + + .. coqtop:: all + + Set Private Polymorphic Universes. + Unset Strict Universe Declaration. + + Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed. + About baz. diff --git a/engine/uState.ml b/engine/uState.ml index 5747ae2ad4..5b0671c06e 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -441,11 +441,13 @@ let restrict_universe_context (univs, csts) keep = if LSet.is_empty removed then univs, csts else let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in - let g = UGraph.empty_universes in - let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in + let g = UGraph.initial_universes in + let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in let g = UGraph.merge_constraints csts g in - let allkept = LSet.diff allunivs removed in + let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in let csts = UGraph.constraints_for ~kept:allkept g in + let csts = Constraint.filter (fun (l,d,r) -> + not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in (LSet.inter univs keep, csts) let restrict ctx vars = diff --git a/kernel/cooking.ml b/kernel/cooking.ml index b39aed01e8..f4b4834d98 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -158,6 +158,7 @@ type result = { cook_body : constant_def; cook_type : types; cook_universes : constant_universes; + cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; } @@ -204,7 +205,8 @@ let lift_univs cb subst auctx0 = else let ainst = Univ.make_abstract_instance auctx in let subst = Instance.append subst ainst in - let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in + let substf = Univ.make_instance_subst subst in + let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in subst, (Polymorphic_const (AUContext.union auctx0 auctx')) let cook_constant ~hcons { from = cb; info } = @@ -229,10 +231,15 @@ let cook_constant ~hcons { from = cb; info } = hyps) hyps0 ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in + let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints + (Univ.make_instance_subst usubst))) + cb.const_private_poly_univs + in { cook_body = body; cook_type = typ; cook_universes = univs; + cook_private_univs = private_univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; } diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 6ebe691b83..7ff4b657d3 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,6 +21,7 @@ type result = { cook_body : constant_def; cook_type : types; cook_universes : constant_universes; + cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; } diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 94832726fe..016b63be09 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -92,6 +92,7 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; + const_private_poly_univs : Univ.ContextSet.t option; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for diff --git a/kernel/declareops.ml b/kernel/declareops.ml index d1d184df69..707c46048b 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -102,6 +102,7 @@ let subst_const_body sub cb = const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; + const_private_poly_univs = cb.const_private_poly_univs; const_inline_code = cb.const_inline_code; const_typing_flags = cb.const_typing_flags } @@ -127,14 +128,20 @@ let hcons_const_universes cbu = match cbu with | Monomorphic_const ctx -> Monomorphic_const (Univ.hcons_universe_context_set ctx) - | Polymorphic_const ctx -> + | Polymorphic_const ctx -> Polymorphic_const (Univ.hcons_abstract_universe_context ctx) +let hcons_const_private_univs = function + | None -> None + | Some univs -> Some (Univ.hcons_universe_context_set univs) + let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; const_type = Constr.hcons cb.const_type; - const_universes = hcons_const_universes cb.const_universes } + const_universes = hcons_const_universes cb.const_universes; + const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs; + } (** {6 Inductive types } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 7835a807ba..38a428d9a1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -382,6 +382,18 @@ let add_universes_set strict ctx g = let push_context_set ?(strict=false) ctx env = map_universes (add_universes_set strict ctx) env +let push_subgraph (levels,csts) env = + let add_subgraph g = + let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in + let newg = UGraph.merge_constraints csts newg in + (if not (Univ.Constraint.is_empty csts) then + let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in + (if not (UGraph.check_constraints restricted g) then + CErrors.anomaly Pp.(str "Local constraints imply new transitive constraints."))); + newg + in + map_universes add_subgraph env + let set_engagement c env = (* Unsafe *) { env with env_stratification = { env.env_stratification with env_engagement = c } } diff --git a/kernel/environ.mli b/kernel/environ.mli index 91b28bfcbc..8a2efb2477 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -269,6 +269,12 @@ val push_context : ?strict:bool -> Univ.UContext.t -> env -> env val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env val push_constraints_to_env : 'a Univ.constrained -> env -> env +val push_subgraph : Univ.ContextSet.t -> env -> env +(** [push_subgraph univs env] adds the universes and constraints in + [univs] to [env] as [push_context_set ~strict:false univs env], and + also checks that they do not imply new transitive constraints + between pre-existing universes in [env]. *) + val set_engagement : engagement -> env -> env val set_typing_flags : typing_flags -> env -> env diff --git a/kernel/modops.ml b/kernel/modops.ml index 0dde1c7e75..f43dbd88f9 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -338,7 +338,8 @@ let strengthen_const mp_from l cb resolver = | Polymorphic_const ctx -> Univ.make_abstract_instance ctx in { cb with - const_body = Def (Mod_subst.from_val (mkConstU (con,u))); + const_body = Def (Mod_subst.from_val (mkConstU (con,u))); + const_private_poly_univs = None; const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) } let rec strengthen_mod mp_from mp_to mb = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index b7f1e93062..df9e253135 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -612,7 +612,7 @@ let inline_side_effects env body side_eff = let subst = Cmap_env.add c (Inr var) subst in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) - | Polymorphic_const _auctx -> + | Polymorphic_const _ -> (** Inline the term to emulate universe polymorphism *) let subst = Cmap_env.add c (Inl b) subst in (subst, var, ctx, args) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 35fa871b4e..f9fdbdd68e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -88,6 +88,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = Undef nl; cook_type = t; cook_universes = univs; + cook_private_univs = None; cook_inline = false; cook_context = ctx; } @@ -130,6 +131,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = Monomorphic_const univs; + cook_private_univs = None; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } @@ -145,24 +147,25 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let body, ctx', _ = handle env body side_eff in body, Univ.ContextSet.union ctx ctx' in - let env, usubst, univs = match c.const_entry_universes with + let env, usubst, univs, private_univs = match c.const_entry_universes with | Monomorphic_const_entry univs -> let ctx = Univ.ContextSet.union univs ctx in let env = push_context_set ~strict:true ctx env in - env, Univ.empty_level_subst, Monomorphic_const ctx + env, Univ.empty_level_subst, Monomorphic_const ctx, None | Polymorphic_const_entry (nas, uctx) -> - (** Ensure not to generate internal constraints in polymorphic mode. - The only way for this to happen would be that either the body - contained deferred universes, or that it contains monomorphic - side-effects. The first property is ruled out by upper layers, - and the second one is ensured by the fact we currently - unconditionally export side-effects from polymorphic definitions, - i.e. [trust] is always [Pure]. *) - let () = assert (Univ.ContextSet.is_empty ctx) in + (** [ctx] must contain local universes, such that it has no impact + on the rest of the graph (up to transitivity). *) let env = push_context ~strict:false uctx env in let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in - env, sbst, Polymorphic_const auctx + let env, local = + if opaque then + push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx) + else + if Univ.ContextSet.is_empty ctx then env, None + else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") + in + env, sbst, Polymorphic_const auctx, local in let j = infer env body in let typ = match typ with @@ -183,6 +186,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = univs; + cook_private_univs = private_univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } @@ -277,6 +281,7 @@ let build_constant_declaration _kn env result = const_type = typ; const_body_code = tps; const_universes = univs; + const_private_poly_univs = result.cook_private_univs; const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 9083156745..fe07a1c90e 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -866,6 +866,8 @@ let constraints_for ~kept g = arc.ltle csts) kept csts +let domain g = LMap.domain g.entries + (** [sort_universes g] builds a totally ordered universe graph. The output graph should imply the input graph (and the implication will be strict most of the time), but is not necessarily minimal. diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index a2cc5b3116..a389b35993 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -79,6 +79,9 @@ val constraints_of_universes : t -> Constraint.t * LSet.t list eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *) val constraints_for : kept:LSet.t -> t -> Constraint.t +val domain : t -> LSet.t +(** Known universes *) + val check_subtype : AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 1cf952576d..5ba9735690 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -322,7 +322,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* end; *) let open Proof_global in - let { id; entries; persistence } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in + let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in match entries with | [entry] -> discard_current (); diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 712eb21ee6..f9f4d7f7f8 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -96,8 +96,9 @@ let print_ref reduce ref udecl = then Printer.pr_universe_instance sigma inst else mt () in + let priv = None in (* We deliberately don't print private univs in About. *) hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_abstract_universe_ctx sigma ?variance univs) + Printer.pr_abstract_universe_ctx sigma ?variance univs ~priv) (********************************) (** Printing implicit arguments *) @@ -580,11 +581,11 @@ let print_constant with_values sep sp udecl = str"*** [ " ++ print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_constant_universes sigma univs + Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs | Some (c, ctx) -> print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ - Printer.pr_constant_universes sigma univs) + Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs) let gallina_print_constant_with_infos sp udecl = print_constant true " = " sp udecl ++ diff --git a/printing/printer.ml b/printing/printer.ml index 4840577cbf..94b514239a 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -143,7 +143,7 @@ let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) let _ = Termops.Internal.set_print_constr (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t)) -let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" +let pr_in_comment x = str "(* " ++ x ++ str " *)" (** Term printers resilient to [Nametab] errors *) @@ -199,42 +199,43 @@ let safe_pr_constr_env = safe_gen pr_constr_env let pr_universe_ctx_set sigma c = if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then - fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c + fnl()++pr_in_comment (v 0 (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) else mt() let pr_universe_ctx sigma ?variance c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then - fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) c + fnl()++pr_in_comment (v 0 (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) else mt() -let pr_abstract_universe_ctx sigma ?variance c = - if !Detyping.print_universes && not (Univ.AUContext.is_empty c) then - fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c)) c +let pr_abstract_universe_ctx sigma ?variance c ~priv = + let open Univ in + let priv = Option.default Univ.ContextSet.empty priv in + let has_priv = not (ContextSet.is_empty priv) in + if !Detyping.print_universes && (not (Univ.AUContext.is_empty c) || has_priv) then + let prlev u = Termops.pr_evd_level sigma u in + let pub = (if has_priv then str "Public universes:" ++ fnl() else mt()) ++ v 0 (Univ.pr_abstract_universe_context prlev ?variance c) in + let priv = if has_priv then fnl() ++ str "Private universes:" ++ fnl() ++ v 0 (Univ.pr_universe_context_set prlev priv) else mt() in + fnl()++pr_in_comment (pub ++ priv) else mt() -let pr_constant_universes sigma = function +let pr_constant_universes sigma ~priv = function | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx - | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx + | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx ~priv let pr_cumulativity_info sigma cumi = if !Detyping.print_universes && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then - fnl()++pr_in_comment (fun uii -> v 0 - (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi + fnl()++pr_in_comment (v 0 (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) cumi)) else mt() let pr_abstract_cumulativity_info sigma cumi = if !Detyping.print_universes && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then - fnl()++pr_in_comment (fun uii -> v 0 - (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi + fnl()++pr_in_comment (v 0 (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) cumi)) else mt() diff --git a/printing/printer.mli b/printing/printer.mli index cefc005c74..b0232ec4ac 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -87,10 +87,10 @@ val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t -val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> - Univ.AUContext.t -> Pp.t +val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> + Univ.AUContext.t -> priv:Univ.ContextSet.t option -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t -val pr_constant_universes : evar_map -> Declarations.constant_universes -> Pp.t +val pr_constant_universes : evar_map -> priv:Univ.ContextSet.t option -> Declarations.constant_universes -> Pp.t val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t val pr_abstract_cumulativity_info : evar_map -> Univ.ACumulativityInfo.t -> Pp.t diff --git a/printing/printmod.ml b/printing/printmod.ml index 2c3ab46670..1360ad4af4 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -310,7 +310,7 @@ let print_body is_impl extent env mp (l,body) = hov 2 (str ":= " ++ Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l)) | _ -> mt ()) ++ str "." ++ - Printer.pr_abstract_universe_ctx sigma ctx) + Printer.pr_abstract_universe_ctx sigma ctx ~priv:cb.const_private_poly_univs) | SFBmind mib -> match extent with | WithContents -> diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 81122e6858..647e87150b 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -138,7 +138,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo try let status = by tac in let open Proof_global in - let { entries; universes } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in + let { entries; universes } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in match entries with | [entry] -> discard_current (); diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index cb4b5759dc..af97d40579 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -318,10 +318,23 @@ let get_open_goals () = type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t -let close_proof ~keep_body_ucst_separate ?feedback_id ~now +let private_poly_univs = + let b = ref true in + let _ = Goptions.(declare_bool_option { + optdepr = false; + optname = "use private polymorphic universes for Qed constants"; + optkey = ["Private";"Polymorphic";"Universes"]; + optread = (fun () -> !b); + optwrite = ((:=) b); + }) + in + fun () -> !b + +let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (fpl : closed_proof_output Future.computation) = let { pid; section_vars; strength; proof; terminator; universe_decl } = cur_pstate () in + let opaque = match opaque with Opaque -> true | Transparent -> false in let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let initial_euctx = Proof.initial_euctx proof in @@ -358,6 +371,16 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let ctx_body = UState.restrict ctx used_univs in let univs = UState.check_mono_univ_decl ctx_body universe_decl in (initunivs, typ), ((body, univs), eff) + else if poly && opaque && private_poly_univs () then + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let universes = UState.restrict universes used_univs in + let typus = UState.restrict universes used_univs_typ in + let udecl = UState.check_univ_decl ~poly typus universe_decl in + let ubody = Univ.ContextSet.diff + (UState.context_set universes) + (UState.context_set typus) + in + (udecl, typ), ((body, ubody), eff) else (* Since the proof is computed now, we can simply have 1 set of constraints in which we merge the ones for the body and the ones @@ -394,7 +417,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now const_entry_feedback = feedback_id; const_entry_type = Some typ; const_entry_inline_code = false; - const_entry_opaque = true; + const_entry_opaque = opaque; const_entry_universes = univs; } in let entries = Future.map2 entry_fn fpl initial_goals in @@ -425,10 +448,10 @@ let return_proof ?(allow_partial=false) () = List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in proofs, Evd.evar_universe_context evd -let close_future_proof ~feedback_id proof = - close_proof ~keep_body_ucst_separate:true ~feedback_id ~now:false proof -let close_proof ~keep_body_ucst_separate fix_exn = - close_proof ~keep_body_ucst_separate ~now:true +let close_future_proof ~opaque ~feedback_id proof = + close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof +let close_proof ~opaque ~keep_body_ucst_separate fix_exn = + close_proof ~opaque ~keep_body_ucst_separate ~now:true (Future.from_val ~fix_exn (return_proof ())) (** Gets the current terminator without checking that the proof has diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index e3808bc36d..d9c32cf9d5 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -86,7 +86,7 @@ val update_global_env : unit -> unit (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) -val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof +val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof (* Intermediate step necessary to delegate the future. * Both access the current proof state. The former is supposed to be @@ -97,7 +97,7 @@ type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * USt (* If allow_partial is set (default no) then an incomplete proof * is allowed (no error), and a warn is given if the proof is complete. *) val return_proof : ?allow_partial:bool -> unit -> closed_proof_output -val close_future_proof : feedback_id:Stateid.t -> +val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> closed_proof_output Future.computation -> closed_proof (** Gets the current terminator without checking that the proof has diff --git a/stm/stm.ml b/stm/stm.ml index 9359ab15e2..3324df3066 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -27,6 +27,9 @@ open Feedback open Vernacexpr open Vernacextend +let is_vtkeep = function VtKeep _ -> true | _ -> false +let get_vtkeep = function VtKeep x -> x | _ -> assert false + module AsyncOpts = struct type cache = Force @@ -1532,12 +1535,13 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in if not drop then begin let checked_proof = Future.chain future_proof (fun p -> + let opaque = Proof_global.Opaque in (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) Vernacstate.unfreeze_interp_state st; let pobject, _ = - Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in + Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in @@ -1545,7 +1549,7 @@ end = struct (* {{{ *) stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }) in + expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1680,9 +1684,10 @@ end = struct (* {{{ *) (* The original terminator, a hook, has not been saved in the .vio*) Proof_global.set_terminator (Lemmas.standard_proof_terminator [] - (Lemmas.mk_hook (fun _ _ -> ()))); + (Lemmas.mk_hook (fun _ _ -> ()))); + let opaque = Proof_global.Opaque in let proof = - Proof_global.close_proof ~keep_body_ucst_separate:true (fun x -> x) in + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No start; @@ -1695,7 +1700,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }); + expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }); `OK proof end with e -> @@ -2252,7 +2257,7 @@ let collect_proof keep cur hd brkind id = else let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc - else if (keep == VtKeep || keep == VtKeepAsAxiom) && + else if (is_vtkeep keep) && (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -2440,9 +2445,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ), `Yes, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function - | `ASync (block_start, nodes, name, delegate) -> (fun () -> - assert(keep == VtKeep || keep == VtKeepAsAxiom); - let drop_pt = keep == VtKeepAsAxiom in + | `ASync (block_start, nodes, name, delegate) -> (fun () -> + let keep' = get_vtkeep keep in + let drop_pt = keep' == VtKeepAxiom in let block_stop, exn_info, loc = eop, (id, eop), x.loc in log_processing_async id name; VCS.create_proof_task_box nodes ~qed:id ~block_start; @@ -2450,11 +2455,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | { VCS.kind = `Edit _ }, None -> assert false | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> assert(redefine_qed = true); - if okeep != keep then + if okeep <> keep then msg_warning(strbrk("The command closing the proof changed. " ^"The kernel cannot take this into account and will " - ^(if keep == VtKeep then "not check " else "reject ") - ^"the "^(if keep == VtKeep then "new" else "incomplete") + ^(if not drop_pt then "not check " else "reject ") + ^"the "^(if not drop_pt then "new" else "incomplete") ^" proof. Reprocess the command declaring " ^"the proof's statement to avoid that.")); let fp, cancel = @@ -2477,8 +2482,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ~drop_pt exn_info block_stop, ref false in qed.fproof <- Some (fp, cancel); + let opaque = match keep' with + | VtKeepAxiom | VtKeepOpaque -> + Proof_global.Opaque (* Admitted -> Opaque should be OK. *) + | VtKeepDefined -> Proof_global.Transparent + in let proof = - Proof_global.close_future_proof ~feedback_id:id fp in + Proof_global.close_future_proof ~opaque ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; let st = Vernacstate.freeze_interp_state `No in @@ -2502,15 +2512,19 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let proof = match keep with | VtDrop -> None - | VtKeepAsAxiom -> + | VtKeep VtKeepAxiom -> let ctx = UState.empty in let fp = Future.from_val ([],ctx) in qed.fproof <- Some (fp, ref false); None - | VtKeep -> - Some(Proof_global.close_proof + | VtKeep opaque -> + let opaque = let open Proof_global in match opaque with + | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent + | VtKeepAxiom -> assert false + in + Some(Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (State.exn_on id ~valid:eop)) in - if keep != VtKeepAsAxiom then + if keep <> VtKeep VtKeepAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in let st = Vernacstate.freeze_interp_state `No in @@ -2714,7 +2728,7 @@ let rec join_admitted_proofs id = if Stateid.equal id Stateid.initial then () else let view = VCS.visit id in match view.step with - | `Qed ({ keep = VtKeepAsAxiom; fproof = Some (fp,_) },_) -> + | `Qed ({ keep = VtKeep VtKeepAxiom; fproof = Some (fp,_) },_) -> ignore(Future.force fp); join_admitted_proofs view.next | _ -> join_admitted_proofs view.next diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 526858bd73..44d07279fc 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -26,8 +26,8 @@ let string_of_vernac_type = function | VtUnknown -> "Unknown" | VtStartProof _ -> "StartProof" | VtSideff _ -> "Sideff" - | VtQed VtKeep -> "Qed(keep)" - | VtQed VtKeepAsAxiom -> "Qed(admitted)" + | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)" + | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)" | VtQed VtDrop -> "Qed(drop)" | VtProofStep { parallel; proof_block_detection } -> "ProofStep " ^ string_of_parallel parallel ^ @@ -43,6 +43,10 @@ let string_of_vernac_when = function let string_of_vernac_classification (t,w) = string_of_vernac_type t ^ " " ^ string_of_vernac_when w +let vtkeep_of_opaque = let open Proof_global in function + | Opaque -> VtKeepOpaque + | Transparent -> VtKeepDefined + let idents_of_name : Names.Name.t -> Names.Id.t list = function | Names.Anonymous -> [] @@ -65,8 +69,9 @@ let classify_vernac e = VtSideff [], VtNow (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater - | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater - | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater + | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom), VtLater + | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque)), VtLater + | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque), VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ | VernacCheckMayEval _ -> VtQuery, VtLater diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index d76b307914..339f798240 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -165,19 +165,13 @@ Module binders. exact A. Defined. - Definition nomoreu@{i j | i < j +} (A : Type@{i}) : Type@{j}. - pose(foo:=Type). - exact A. - Fail Defined. - Abort. - - Polymorphic Definition moreu@{i j +} (A : Type@{i}) : Type@{j}. - pose(foo:=Type). - exact A. - Defined. + Polymorphic Lemma hidden_strict_type : Type. + Proof. + exact Type. + Qed. + Check hidden_strict_type@{_}. + Fail Check hidden_strict_type@{Set}. - Check moreu@{_ _ _ _}. - Fail Definition morec@{i j|} (A : Type@{i}) : Type@{j} := A. (* By default constraints are extensible *) diff --git a/test-suite/success/private_univs.v b/test-suite/success/private_univs.v new file mode 100644 index 0000000000..5c30b33435 --- /dev/null +++ b/test-suite/success/private_univs.v @@ -0,0 +1,50 @@ +Set Universe Polymorphism. Set Printing Universes. + +Definition internal_defined@{i j | i < j +} (A : Type@{i}) : Type@{j}. + pose(foo:=Type). (* 1 universe for the let body + 1 for the type *) + exact A. + Fail Defined. +Abort. + +Definition internal_defined@{i j +} (A : Type@{i}) : Type@{j}. +pose(foo:=Type). +exact A. +Defined. +Check internal_defined@{_ _ _ _}. + +Module M. +Lemma internal_qed@{i j|i<=j} (A:Type@{i}) : Type@{j}. +Proof. + pose (foo := Type). + exact A. +Qed. +Check internal_qed@{_ _}. +End M. +Include M. +(* be careful to remove const_private_univs in Include! will be coqchk'd *) + +Unset Strict Universe Declaration. +Lemma private_transitivity@{i j} (A:Type@{i}) : Type@{j}. +Proof. + pose (bar := Type : Type@{j}). + pose (foo := Type@{i} : bar). + exact bar. +Qed. + +Definition private_transitivity'@{i j|i < j} := private_transitivity@{i j}. +Fail Definition dummy@{i j|j <= i +} := private_transitivity@{i j}. + +Unset Private Polymorphic Universes. +Lemma internal_noprivate_qed@{i j|i<=j} (A:Type@{i}) : Type@{j}. +Proof. + pose (foo := Type). + exact A. + Fail Qed. +Abort. + +Lemma internal_noprivate_qed@{i j +} (A:Type@{i}) : Type@{j}. +Proof. + pose (foo := Type). + exact A. +Qed. +Check internal_noprivate_qed@{_ _ _ _}. diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v index 49b9e4c951..81a087b525 100644 --- a/theories/Compat/Coq89.v +++ b/theories/Compat/Coq89.v @@ -10,3 +10,5 @@ (** Compatibility file for making Coq act similar to Coq v8.9 *) Local Set Warnings "-deprecated". + +Unset Private Polymorphic Universes. diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 2443c5d12a..46d7892bf6 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -311,7 +311,7 @@ let universe_proof_terminator compute_guard hook = | Transparent -> false, true | Opaque -> true, false in - let const = {const with const_entry_opaque = is_opaque} in + assert (is_opaque == const.const_entry_opaque); let id = match idopt with | None -> id | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in @@ -498,13 +498,13 @@ let save_proof ?proof = function Admitted(id,k,(sec_vars, (typ, ctx), None), universes) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe - | Vernacexpr.Proved (is_opaque,idopt) -> + | Vernacexpr.Proved (opaque,idopt) -> let (proof_obj,terminator) = match proof with | None -> - Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x) + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) | Some proof -> proof in (* if the proof is given explicitly, nothing has to be deleted *) if Option.is_empty proof then Proof_global.discard_current (); - Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) + Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj))) diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 35f26cab4d..2541f73582 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -12,6 +12,10 @@ open Util open Pp open CErrors +type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque + +type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop + type vernac_type = (* Start of a proof *) | VtStartProof of vernac_start @@ -33,7 +37,6 @@ type vernac_type = (* To be removed *) | VtMeta | VtUnknown -and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 7feaccd9a3..8b07be8b16 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -27,6 +27,11 @@ considered safe to delegate to a worker. *) + +type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque + +type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop + type vernac_type = (* Start of a proof *) | VtStartProof of vernac_start @@ -48,7 +53,6 @@ type vernac_type = (* To be removed *) | VtMeta | VtUnknown -and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = |