aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/critical-bugs12
-rw-r--r--doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst6
-rw-r--r--doc/sphinx/addendum/universe-polymorphism.rst33
-rw-r--r--kernel/inferCumulativity.ml (renamed from pretyping/inferCumulativity.ml)13
-rw-r--r--kernel/inferCumulativity.mli (renamed from pretyping/inferCumulativity.mli)0
-rw-r--r--kernel/kernel.mllib2
-rw-r--r--kernel/safe_typing.ml49
-rw-r--r--kernel/safe_typing.mli27
-rw-r--r--kernel/section.ml250
-rw-r--r--kernel/section.mli78
-rw-r--r--library/global.ml8
-rw-r--r--library/global.mli10
-rw-r--r--library/lib.ml169
-rw-r--r--library/lib.mli6
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--tactics/declare.ml32
16 files changed, 502 insertions, 194 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index d00c8cb11a..78d7061259 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -129,6 +129,18 @@ Universes
GH issue number: #9294
risk: moderate risk to be activated by chance
+ component: universe polymorphism, asynchronous proofs
+ summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section
+ introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one
+ impacted released: V8.5-V8.10
+ impacted development branches: none
+ impacted coqchk versions: immune
+ fixed in: PR#10664
+ found by: Pédrot
+ exploit: no test
+ GH issue number: none
+ risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc)
+
Primitive projections
component: primitive projections, guard condition
diff --git a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst
new file mode 100644
index 0000000000..bac08d12ea
--- /dev/null
+++ b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst
@@ -0,0 +1,6 @@
+- Section data is now part of the kernel. Solves a soundness issue
+ in interactive mode where global monomorphic universe constraints would be
+ dropped when forcing a delayed opaque proof inside a polymorphic section. Also
+ relaxes the nesting criterion for sections, as polymorphic sections can now
+ appear inside a monomorphic one
+ (#10664, <https://github.com/coq/coq/pull/10664> by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 7e698bfb66..1d0b732e7d 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -147,14 +147,7 @@ Many other commands support the ``Polymorphic`` flag, including:
- :cmd:`Section` will locally set the polymorphism flag inside the section.
- ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support
- polymorphism. This means that the universe variables (and associated
- constraints) are discharged polymorphically over definitions that use
- them. In other words, two definitions in the section sharing a common
- variable will both get parameterized by the universes produced by the
- variable declaration. This is in contrast to a “mononorphic” variable
- which introduces global universes and constraints, making the two
- definitions depend on the *same* global universes associated to the
- variable.
+ polymorphism. See :ref:`universe-polymorphism-in-sections` for more details.
- :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint
polymorphically, not at a single instance.
@@ -375,9 +368,7 @@ to universes and explicitly instantiate polymorphic definitions.
as well. Global universe names live in a separate namespace. The
command supports the ``Polymorphic`` flag only in sections, meaning the
universe quantification will be discharged on each section definition
- independently. One cannot mix polymorphic and monomorphic
- declarations in the same section.
-
+ independently.
.. cmd:: Constraint @universe_constraint
Polymorphic Constraint @universe_constraint
@@ -510,3 +501,23 @@ underscore or by omitting the annotation to a polymorphic definition.
Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed.
About baz.
+
+.. _universe-polymorphism-in-sections:
+
+Universe polymorphism and sections
+----------------------------------
+
+The universe polymorphic or monomorphic status is
+attached to each individual section, and all term or universe declarations
+contained inside must respect it, as described below. It is possible to nest a
+polymorphic section inside a monomorphic one, but the converse is not allowed.
+
+:cmd:`Variables`, :cmd:`Context`, :cmd:`Universe` and :cmd:`Constraint` in a section support
+polymorphism. This means that the universe variables and their associated
+constraints are discharged polymorphically over definitions that use
+them. In other words, two definitions in the section sharing a common
+variable will both get parameterized by the universes produced by the
+variable declaration. This is in contrast to a “mononorphic” variable
+which introduces global universes and constraints, making the two
+definitions depend on the *same* global universes associated to the
+variable.
diff --git a/pretyping/inferCumulativity.ml b/kernel/inferCumulativity.ml
index ed069eace0..3b8c2cd788 100644
--- a/pretyping/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -77,7 +77,7 @@ let infer_sort cv_pb variances s =
| CUMUL ->
LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances
-let infer_table_key infos variances c =
+let infer_table_key variances c =
let open Names in
match c with
| ConstKey (_, u) ->
@@ -103,7 +103,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
| FRel _ -> infer_stack infos variances stk
| FInt _ -> infer_stack infos variances stk
| FFlex fl ->
- let variances = infer_table_key infos variances fl in
+ let variances = infer_table_key variances fl in
infer_stack infos variances stk
| FProj (_,c) ->
let variances = infer_fterm CONV infos variances c [] in
@@ -152,7 +152,7 @@ and infer_stack infos variances (stk:CClosure.stack) =
| Zfix (fx,a) ->
let variances = infer_fterm CONV infos variances fx [] in
infer_stack infos variances a
- | ZcaseT (ci,p,br,e) ->
+ | ZcaseT (_, p, br, e) ->
let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
infer_vect infos variances (Array.map (mk_clos e) br)
| Zshift _ -> variances
@@ -195,7 +195,7 @@ let infer_inductive_core env params entries uctx =
Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances)
LMap.empty uarray
in
- let env, params = Typeops.check_context env params in
+ let env, _ = Typeops.check_context env params in
let variances = List.fold_left (fun variances entry ->
let variances = infer_arity_constructor true
env variances entry.mind_entry_arity
@@ -213,9 +213,8 @@ let infer_inductive_core env params entries uctx =
let infer_inductive env mie =
let open Entries in
- let { mind_entry_params = params;
- mind_entry_inds = entries; } = mie
- in
+ let params = mie.mind_entry_params in
+ let entries = mie.mind_entry_inds in
let variances =
match mie.mind_entry_variance with
| None -> None
diff --git a/pretyping/inferCumulativity.mli b/kernel/inferCumulativity.mli
index a234e334d1..a234e334d1 100644
--- a/pretyping/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 59c1d5890f..20e742d7f8 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -43,9 +43,11 @@ Inductive
Typeops
IndTyping
Indtypes
+InferCumulativity
Cooking
Term_typing
Subtyping
Mod_typing
Nativelibrary
+Section
Safe_typing
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6970a11e72..8d34f3a34f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -115,6 +115,7 @@ type module_parameters = (MBId.t * module_type_body) list
type safe_environment =
{ env : Environ.env;
+ sections : Section.t;
modpath : ModPath.t;
modvariant : modvariant;
modresolver : Mod_subst.delta_resolver;
@@ -151,6 +152,7 @@ let empty_environment =
revstruct = [];
modlabels = Label.Set.empty;
objlabels = Label.Set.empty;
+ sections = Section.empty;
future_cst = [];
univ = Univ.ContextSet.empty;
engagement = None;
@@ -317,11 +319,16 @@ let universes_of_private eff =
let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
+let sections_of_safe_env senv = senv.sections
+
type constraints_addition =
| Now of Univ.ContextSet.t
| Later of Univ.ContextSet.t Future.computation
let push_context_set poly cst senv =
+ let () = if Section.is_polymorphic senv.sections && not (Univ.ContextSet.is_empty cst) then
+ CErrors.user_err (Pp.str "Cannot add global universe constraints inside a polymorphic section.")
+ in
{ senv with
env = Environ.push_context_set ~strict:(not poly) cst senv.env;
univ = Univ.ContextSet.union cst senv.univ }
@@ -386,7 +393,7 @@ let check_current_library dir senv = match senv.modvariant with
(** When operating on modules, we're normally outside sections *)
let check_empty_context senv =
- assert (Environ.empty_context senv.env)
+ assert (Environ.empty_context senv.env && Section.is_empty senv.sections)
(** When adding a parameter to the current module/modtype,
it must have been freshly started *)
@@ -433,19 +440,30 @@ let safe_push_named d env =
with Not_found -> () in
Environ.push_named d env
-
let push_named_def (id,de) senv =
+ let sections = Section.push_local senv.sections in
let c, r, typ = Term_typing.translate_local_def senv.env id de in
let x = Context.make_annot id r in
let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in
- { senv with env = env'' }
+ { senv with sections; env = env'' }
let push_named_assum (x,t) senv =
+ let sections = Section.push_local senv.sections in
let t, r = Term_typing.translate_local_assum senv.env t in
let x = Context.make_annot x r in
let env'' = safe_push_named (LocalAssum (x,t)) senv.env in
- {senv with env=env''}
-
+ { senv with sections; env = env'' }
+
+let push_section_context (nas, ctx) senv =
+ let sections = Section.push_context (nas, ctx) senv.sections in
+ let senv = { senv with sections } in
+ let ctx = Univ.ContextSet.of_context ctx in
+ (* We check that the universes are fresh. FIXME: This should be done
+ implicitly, but we have to work around the API. *)
+ let () = assert (Univ.LSet.for_all (fun u -> not (Univ.LSet.mem u (fst senv.univ))) (fst ctx)) in
+ { senv with
+ env = Environ.push_context_set ~strict:false ctx senv.env;
+ univ = Univ.ContextSet.union ctx senv.univ }
(** {6 Insertion of new declarations to current environment } *)
@@ -527,8 +545,19 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
| SFBmodule mb, M -> Modops.add_module mb senv.env
| _ -> assert false
in
+ let sections = match sfb, gn with
+ | SFBconst cb, C con ->
+ let poly = Declareops.constant_is_polymorphic cb in
+ Section.push_constant ~poly con senv.sections
+ | SFBmind mib, I mind ->
+ let poly = Declareops.inductive_is_polymorphic mib in
+ Section.push_inductive ~poly mind senv.sections
+ | _, (M | MT) -> senv.sections
+ | _ -> assert false
+ in
{ senv with
env = env';
+ sections;
revstruct = field :: senv.revstruct;
modlabels = Label.Set.union mlabs senv.modlabels;
objlabels = Label.Set.union olabs senv.objlabels }
@@ -902,6 +931,16 @@ let add_module l me inl senv =
in
(mp,mb.mod_delta),senv''
+(** {6 Interactive sections *)
+
+let open_section ~poly senv =
+ let sections = Section.open_section ~poly senv.sections in
+ { senv with sections }
+
+let close_section senv =
+ (* TODO: implement me when discharging in kernel *)
+ let sections = Section.close_section senv.sections in
+ { senv with sections }
(** {6 Starting / ending interactive modules and module types } *)
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index fa53fa33fa..10fedc2faf 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -33,6 +33,8 @@ val is_initial : safe_environment -> bool
val env_of_safe_env : safe_environment -> Environ.env
+val sections_of_safe_env : safe_environment -> Section.t
+
(** The safe_environment state monad *)
type safe_transformer0 = safe_environment -> safe_environment
@@ -67,15 +69,6 @@ val join_safe_environment :
val is_joined_environment : safe_environment -> bool
(** {6 Enriching a safe environment } *)
-(** Insertion of local declarations (Local or Variables) *)
-
-val push_named_assum : (Id.t * Constr.types) -> safe_transformer0
-
-(** Returns the full universe context necessary to typecheck the definition
- (futures are forced) *)
-val push_named_def :
- Id.t * Entries.section_def_entry -> safe_transformer0
-
(** Insertion of global axioms or definitions *)
type 'a effect_entry =
@@ -140,6 +133,22 @@ val set_allow_sprop : bool -> safe_transformer0
val check_engagement : Environ.env -> Declarations.set_predicativity -> unit
+(** {6 Interactive section functions } *)
+
+val open_section : poly:bool -> safe_transformer0
+
+val close_section : safe_transformer0
+
+(** Insertion of local declarations (Local or Variables) *)
+
+val push_named_assum : (Id.t * Constr.types) -> safe_transformer0
+
+val push_named_def :
+ Id.t * Entries.section_def_entry -> safe_transformer0
+
+(** Add local universes to a polymorphic section *)
+val push_section_context : (Name.t array * Univ.UContext.t) -> safe_transformer0
+
(** {6 Interactive module functions } *)
val start_module : Label.t -> ModPath.t safe_transformer
diff --git a/kernel/section.ml b/kernel/section.ml
new file mode 100644
index 0000000000..12e9c2fd60
--- /dev/null
+++ b/kernel/section.ml
@@ -0,0 +1,250 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Util
+open Names
+open Univ
+
+module NamedDecl = Context.Named.Declaration
+
+type _ section_kind =
+| SecMono : [ `mono ] section_kind
+| SecPoly : [ `poly ] section_kind
+
+type _ section_universes =
+| SecMonoUniv : [ `mono ] section_universes
+| SecPolyUniv : Name.t array * UContext.t -> [ `poly ] section_universes
+
+type section_entry =
+| SecDefinition of Constant.t
+| SecInductive of MutInd.t
+
+type 'a entry_map = 'a Cmap.t * 'a Mindmap.t
+
+type 'a section = {
+ sec_context : int;
+ (** Length of the named context suffix that has been introduced locally *)
+ sec_universes : 'a section_universes;
+ (** Universes local to the section *)
+ sec_entries : section_entry list;
+ (** Definitions introduced in the section *)
+ sec_data : 'a section_universes entry_map;
+}
+
+(** Sections can be nested with the proviso that no monomorphic section can be
+ opened inside a polymorphic one. The reverse is allowed. *)
+type t = {
+ sec_poly : [ `poly ] section list;
+ sec_mono : [ `mono ] section list;
+}
+
+let empty = {
+ sec_poly = [];
+ sec_mono = [];
+}
+
+let is_empty s =
+ List.is_empty s.sec_poly && List.is_empty s.sec_mono
+
+let is_polymorphic s =
+ not (List.is_empty s.sec_poly)
+
+let find_emap e (cmap, imap) = match e with
+| SecDefinition con -> Cmap.find con cmap
+| SecInductive ind -> Mindmap.find ind imap
+
+let add_emap e v (cmap, imap) = match e with
+| SecDefinition con -> (Cmap.add con v cmap, imap)
+| SecInductive ind -> (cmap, Mindmap.add ind v imap)
+
+type on_sec = { on_sec : 'a. 'a section_kind -> 'a section -> 'a section }
+
+let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
+| [], [] -> CErrors.user_err (Pp.str "No opened section")
+| sec :: rem, _ ->
+ let sec_poly = f.on_sec SecPoly sec :: rem in
+ { sec_mono; sec_poly }
+| [], sec :: rem ->
+ let sec_mono = f.on_sec SecMono sec :: rem in
+ { sec_mono; sec_poly }
+
+type 'r with_sec = { with_sec : 'a. ('a section_kind * 'a section) option -> 'r }
+
+let with_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
+| [], [] -> f.with_sec None
+| sec :: _, _ -> f.with_sec (Some (SecPoly, sec))
+| [], sec :: _ -> f.with_sec (Some (SecMono, sec))
+
+let push_local s =
+ let on_sec _ sec = { sec with sec_context = sec.sec_context + 1 } in
+ on_last_section { on_sec } s
+
+let push_context (nas, ctx) s =
+ let on_sec (type a) (kind : a section_kind) (sec : a section) : a section = match kind with
+ | SecMono ->
+ CErrors.anomaly (Pp.str "Adding polymorphic constraints to monomorphic section")
+ | SecPoly ->
+ let SecPolyUniv (snas, sctx) = sec.sec_universes in
+ let sec_universes = SecPolyUniv (Array.append snas nas, UContext.union sctx ctx) in
+ { sec with sec_universes }
+ in
+ on_last_section { on_sec } s
+
+let open_section ~poly sections =
+ if poly then
+ let sec = {
+ sec_context = 0;
+ sec_universes = SecPolyUniv ([||], Univ.UContext.empty);
+ sec_entries = [];
+ sec_data = (Cmap.empty, Mindmap.empty);
+ } in
+ { sections with sec_poly = sec :: sections.sec_poly }
+ else if List.is_empty sections.sec_poly then
+ let sec = {
+ sec_context = 0;
+ sec_universes = SecMonoUniv;
+ sec_entries = [];
+ sec_data = (Cmap.empty, Mindmap.empty);
+ } in
+ { sections with sec_mono = sec :: sections.sec_mono }
+ else
+ CErrors.user_err (Pp.str "Cannot open a monomorphic section inside a polymorphic one")
+
+let close_section sections =
+ (* TODO: implement me correctly when discharging in kernel *)
+ match sections.sec_poly, sections.sec_mono with
+ | _sec :: psecs, _ ->
+ let sections = { sections with sec_poly = psecs } in
+ sections
+ | [], _sec :: msecs ->
+ let sections = { sections with sec_mono = msecs } in
+ sections
+ | [], [] ->
+ CErrors.user_err (Pp.str "No opened section.")
+
+let same_poly (type a) ~poly (knd : a section_kind) = match knd with
+| SecPoly -> poly
+| SecMono -> not poly
+
+let push_global ~poly e s =
+ if is_empty s then s
+ else
+ let on_sec knd sec =
+ if same_poly ~poly knd then { sec with
+ sec_entries = e :: sec.sec_entries;
+ sec_data = add_emap e sec.sec_universes sec.sec_data;
+ } else
+ CErrors.user_err (Pp.str "Cannot mix universe polymorphic and \
+ monomorphic declarations in sections.")
+ in
+ on_last_section { on_sec } s
+
+let push_constant ~poly con s = push_global ~poly (SecDefinition con) s
+
+let push_inductive ~poly ind s = push_global ~poly (SecInductive ind) s
+
+type abstr_info = {
+ abstr_ctx : Constr.named_context;
+ abstr_subst : Univ.Instance.t;
+ abstr_uctx : Univ.AUContext.t;
+}
+
+let empty_segment = {
+ abstr_ctx = [];
+ abstr_subst = Instance.empty;
+ abstr_uctx = AUContext.empty;
+}
+
+let extract_hyps sec vars hyps =
+ (* FIXME: this code is fishy. It is supposed to check that declared section
+ variables are an ordered subset of the ambient ones, but it doesn't check
+ e.g. uniqueness of naming nor convertibility of the section data. *)
+ let rec aux ids hyps = match ids, hyps with
+ | id :: ids, decl :: hyps when Names.Id.equal id (NamedDecl.get_id decl) ->
+ decl :: aux ids hyps
+ | _ :: ids, hyps ->
+ aux ids hyps
+ | [], _ -> []
+ in
+ let ids = List.map NamedDecl.get_id @@ List.firstn sec.sec_context vars in
+ aux ids hyps
+
+let section_segment_of_entry vars e hyps sections =
+ (* [vars] are the named hypotheses, [hyps] the subset that is declared by the
+ global *)
+ let with_sec (type a) (s : (a section_kind * a section) option) = match s with
+ | None ->
+ CErrors.user_err (Pp.str "No opened section.")
+ | Some (knd, sec) ->
+ let hyps = extract_hyps sec vars hyps in
+ let inst, auctx = match knd, find_emap e sec.sec_data with
+ | SecMono, SecMonoUniv ->
+ Instance.empty, AUContext.empty
+ | SecPoly, SecPolyUniv (nas, ctx) ->
+ Univ.abstract_universes nas ctx
+ in
+ {
+ abstr_ctx = hyps;
+ abstr_subst = inst;
+ abstr_uctx = auctx;
+ }
+ in
+ with_last_section { with_sec } sections
+
+let segment_of_constant env con s =
+ let body = Environ.lookup_constant con env in
+ let vars = Environ.named_context env in
+ section_segment_of_entry vars (SecDefinition con) body.Declarations.const_hyps s
+
+let segment_of_inductive env mind s =
+ let mib = Environ.lookup_mind mind env in
+ let vars = Environ.named_context env in
+ section_segment_of_entry vars (SecInductive mind) mib.Declarations.mind_hyps s
+
+let instance_from_variable_context =
+ List.rev %> List.filter NamedDecl.is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
+
+let extract_worklist info =
+ let args = instance_from_variable_context info.abstr_ctx in
+ info.abstr_subst, args
+
+let replacement_context env s =
+ let with_sec sec = match sec with
+ | None -> CErrors.user_err (Pp.str "No opened section.")
+ | Some (_, sec) ->
+ let cmap, imap = sec.sec_data in
+ let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con s) cmap in
+ let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind s) imap in
+ (cmap, imap)
+ in
+ with_last_section { with_sec } s
+
+let is_in_section env gr s =
+ let with_sec sec = match sec with
+ | None -> false
+ | Some (_, sec) ->
+ let open GlobRef in
+ match gr with
+ | VarRef id ->
+ let vars = List.firstn sec.sec_context (Environ.named_context env) in
+ List.exists (fun decl -> Id.equal id (NamedDecl.get_id decl)) vars
+ | ConstRef con ->
+ Cmap.mem con (fst sec.sec_data)
+ | IndRef (ind, _) | ConstructRef ((ind, _), _) ->
+ Mindmap.mem ind (snd sec.sec_data)
+ in
+ with_last_section { with_sec } s
+
+let is_polymorphic_univ u s =
+ let check sec =
+ let SecPolyUniv (_, uctx) = sec.sec_universes in
+ Array.mem u (Instance.to_array (UContext.instance uctx))
+ in
+ List.exists check s.sec_poly
diff --git a/kernel/section.mli b/kernel/section.mli
new file mode 100644
index 0000000000..4b23115ca2
--- /dev/null
+++ b/kernel/section.mli
@@ -0,0 +1,78 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Univ
+
+(** Kernel implementation of sections. *)
+
+type t
+(** Type of sections *)
+
+val empty : t
+
+val is_empty : t -> bool
+(** Checks whether there is no opened section *)
+
+val is_polymorphic : t -> bool
+(** Checks whether last opened section is polymorphic *)
+
+(** {6 Manipulating sections} *)
+
+val open_section : poly:bool -> t -> t
+(** Open a new section with the provided universe polymorphic status. Sections
+ can be nested, with the proviso that polymorphic sections cannot appear
+ inside a monomorphic one. *)
+
+val close_section : t -> t
+
+(** {6 Extending sections} *)
+
+val push_local : t -> t
+(** Extend the current section with a local definition (cf. push_named). *)
+
+val push_context : Name.t array * UContext.t -> t -> t
+(** Extend the current section with a local universe context. Assumes that the
+ last opened section is polymorphic. *)
+
+val push_constant : poly:bool -> Constant.t -> t -> t
+(** Make the constant as having been defined in this section. *)
+
+val push_inductive : poly:bool -> MutInd.t -> t -> t
+(** Make the inductive block as having been defined in this section. *)
+
+(** {6 Retrieving section data} *)
+
+type abstr_info = private {
+ abstr_ctx : Constr.named_context;
+ (** Section variables of this prefix *)
+ abstr_subst : Univ.Instance.t;
+ (** Actual names of the abstracted variables *)
+ abstr_uctx : Univ.AUContext.t;
+ (** Universe quantification, same length as the substitution *)
+}
+(** Data needed to abstract over the section variable and universe hypotheses *)
+
+
+val empty_segment : abstr_info
+(** Nothing to abstract *)
+
+val segment_of_constant : Environ.env -> Constant.t -> t -> abstr_info
+(** Section segment at the time of the constant declaration *)
+
+val segment_of_inductive : Environ.env -> MutInd.t -> t -> abstr_info
+(** Section segment at the time of the inductive declaration *)
+
+val replacement_context : Environ.env -> t -> Opaqueproof.work_list
+(** Section segments of all declarations from this section. *)
+
+val is_in_section : Environ.env -> GlobRef.t -> t -> bool
+
+val is_polymorphic_univ : Level.t -> t -> bool
diff --git a/library/global.ml b/library/global.ml
index 6bb4614aa4..3d28178d7b 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -83,6 +83,7 @@ let i2l = Label.of_id
let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
let push_named_def d = globalize0 (Safe_typing.push_named_def d)
+let push_section_context c = globalize0 (Safe_typing.push_section_context c)
let add_constraints c = globalize0 (Safe_typing.add_constraints c)
let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
@@ -104,6 +105,13 @@ let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
+let open_section ~poly = globalize0 (Safe_typing.open_section ~poly)
+let close_section fs =
+ (* TODO: use globalize0_with_summary *)
+ Summary.unfreeze_summaries fs;
+ let env = Safe_typing.close_section (safe_env ()) in
+ GlobalSafeEnv.set_safe_env env
+
let start_module id = globalize (Safe_typing.start_module (i2l id))
let start_modtype id = globalize (Safe_typing.start_modtype (i2l id))
diff --git a/library/global.mli b/library/global.mli
index d0bd556d70..b809e9b241 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -44,6 +44,7 @@ val sprop_allowed : unit -> bool
val push_named_assum : (Id.t * Constr.types) -> unit
val push_named_def : (Id.t * Entries.section_def_entry) -> unit
+val push_section_context : (Name.t array * Univ.UContext.t) -> unit
val export_private_constants : in_section:bool ->
Safe_typing.private_constants Entries.proof_output ->
@@ -71,6 +72,15 @@ val add_include :
Entries.module_struct_entry -> bool -> Declarations.inline ->
Mod_subst.delta_resolver
+(** Sections *)
+
+val open_section : poly:bool -> unit
+(** [poly] is true when the section should be universe polymorphic *)
+
+val close_section : Summary.frozen -> unit
+(** Close the section and reset the global state to the one at the time when
+ the section what opened. *)
+
(** Interactive modules and module types *)
val start_module : Id.t -> ModPath.t
diff --git a/library/lib.ml b/library/lib.ml
index 851f086961..1c6f82e8a6 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -410,87 +410,11 @@ let find_opening_node id =
- the list of substitution to do at section closing
*)
-type abstr_info = {
+type abstr_info = Section.abstr_info = private {
abstr_ctx : Constr.named_context;
abstr_subst : Univ.Instance.t;
abstr_uctx : Univ.AUContext.t;
}
-type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
-
-type secentry =
- | Variable of {
- id:Names.Id.t;
- }
- | Context of Univ.ContextSet.t
-
-type section_data = {
- sec_entry : secentry list;
- sec_abstr : abstr_list;
- sec_poly : bool;
-}
-
-let empty_section_data ~poly = {
- sec_entry = [];
- sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty);
- sec_poly = poly;
-}
-
-let sectab =
- Summary.ref ([] : section_data list) ~name:"section-context"
-
-let check_same_poly p sec =
- if p != sec.sec_poly then
- user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.")
-
-let add_section ~poly () =
- List.iter (fun tab -> check_same_poly poly tab) !sectab;
- sectab := empty_section_data ~poly :: !sectab
-
-let add_section_variable ~name ~poly =
- match !sectab with
- | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
- | s :: sl ->
- List.iter (fun tab -> check_same_poly poly tab) !sectab;
- let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in
- sectab := s :: sl
-
-let add_section_context ctx =
- match !sectab with
- | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
- | s :: sl ->
- check_same_poly true s;
- let s = { s with sec_entry = Context ctx :: s.sec_entry } in
- sectab := s :: sl
-
-exception PolyFound (* make this a let exception once possible *)
-let is_polymorphic_univ u =
- try
- let open Univ in
- List.iter (fun s ->
- let vars = s.sec_entry in
- List.iter (function
- | Variable _ -> ()
- | Context (univs,_) ->
- if LSet.mem u univs then raise PolyFound
- ) vars
- ) !sectab;
- false
- with PolyFound -> true
-
-let extract_hyps poly (secs,ohyps) =
- let rec aux = function
- | (Variable {id}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
- let l, r = aux (idl,hyps) in
- decl :: l, r
- | (Variable _::idl,hyps) ->
- let l, r = aux (idl,hyps) in
- l, r
- | (Context ctx :: idl, hyps) ->
- let () = assert poly in
- let l, r = aux (idl, hyps) in
- l, Univ.ContextSet.union r ctx
- | [], _ -> [],Univ.ContextSet.empty
- in aux (secs,ohyps)
let instance_from_variable_context =
List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
@@ -499,66 +423,21 @@ let extract_worklist info =
let args = instance_from_variable_context info.abstr_ctx in
info.abstr_subst, args
-let make_worklist (cmap, mmap) =
- Cmap.map extract_worklist cmap, Mindmap.map extract_worklist mmap
-
-let name_instance inst =
- (* FIXME: this should probably be done at an upper level, by storing the
- name information in the section data structure. *)
- let map lvl = match Univ.Level.name lvl with
- | None -> (* Having Prop/Set/Var as section universes makes no sense *)
- assert false
- | Some na ->
- try
- let qid = Nametab.shortest_qualid_of_universe na in
- Name (Libnames.qualid_basename qid)
- with Not_found ->
- (* Best-effort naming from the string representation of the level.
- See univNames.ml for a similar hack. *)
- Name (Id.of_string_soft (Univ.Level.to_string lvl))
- in
- Array.map map (Univ.Instance.to_array inst)
-
-let add_section_replacement g poly hyps =
- match !sectab with
- | [] -> ()
- | s :: sl ->
- let () = check_same_poly poly s in
- let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in
- let ctx = Univ.ContextSet.to_context ctx in
- let nas = name_instance (Univ.UContext.instance ctx) in
- let subst, ctx = Univ.abstract_universes nas ctx in
- let info = {
- abstr_ctx = sechyps;
- abstr_subst = subst;
- abstr_uctx = ctx;
- } in
- let s = { s with
- sec_abstr = g info s.sec_abstr;
- } in
- sectab := s :: sl
-
-let add_section_kn ~poly kn =
- let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
- add_section_replacement f poly
-
-let add_section_constant ~poly kn =
- let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
- add_section_replacement f poly
-
-let replacement_context () = make_worklist (List.hd !sectab).sec_abstr
+let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env ()
+
+let is_polymorphic_univ u =
+ Section.is_polymorphic_univ u (sections ())
+
+let replacement_context () =
+ Section.replacement_context (Global.env ()) (sections ())
let section_segment_of_constant con =
- Names.Cmap.find con (fst (List.hd !sectab).sec_abstr)
+ Section.segment_of_constant (Global.env ()) con (sections ())
let section_segment_of_mutual_inductive kn =
- Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr)
+ Section.segment_of_inductive (Global.env ()) kn (sections ())
-let empty_segment = {
- abstr_ctx = [];
- abstr_subst = Univ.Instance.empty;
- abstr_uctx = Univ.AUContext.empty;
-}
+let empty_segment = Section.empty_segment
let section_segment_of_reference = let open GlobRef in function
| ConstRef c -> section_segment_of_constant c
@@ -569,28 +448,24 @@ let section_segment_of_reference = let open GlobRef in function
let variable_section_segment_of_reference gr =
(section_segment_of_reference gr).abstr_ctx
+let is_in_section ref =
+ Section.is_in_section (Global.env ()) ref (sections ())
+
let section_instance = let open GlobRef in function
| VarRef id ->
- let eq = function
- | Variable {id=id'} -> Names.Id.equal id id'
- | Context _ -> false
- in
- if List.exists eq (List.hd !sectab).sec_entry
- then Univ.Instance.empty, [||]
- else raise Not_found
+ if is_in_section (VarRef id) then (Univ.Instance.empty, [||])
+ else raise Not_found
| ConstRef con ->
- let data = Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) in
+ let data = section_segment_of_constant con in
extract_worklist data
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
- let data = Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) in
+ let data = section_segment_of_mutual_inductive kn in
extract_worklist data
-let is_in_section ref =
- try ignore (section_instance ref); true with Not_found -> false
-
(*************)
(* Sections. *)
let open_section ~poly id =
+ let () = Global.open_section ~poly in
let opp = !lib_state.path_prefix in
let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
@@ -600,9 +475,7 @@ let open_section ~poly id =
add_entry (make_foname id) (OpenedSection (prefix, fs));
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
- lib_state := { !lib_state with path_prefix = prefix };
- add_section ~poly ()
-
+ lib_state := { !lib_state with path_prefix = prefix }
(* Restore lib_stk and summaries as before the section opening, and
add a ClosedSection object. *)
@@ -631,7 +504,7 @@ let close_section () =
lib_state := { !lib_state with lib_stk = before };
pop_path_prefix ();
let newdecls = List.map discharge_item secdecls in
- Summary.unfreeze_summaries fs;
+ let () = Global.close_section fs in
List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls
(* State and initialization. *)
diff --git a/library/lib.mli b/library/lib.mli
index 9ffa69ef93..5ce601f2d3 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -163,7 +163,7 @@ val drop_objects : frozen -> frozen
val init : unit -> unit
(** {6 Section management for discharge } *)
-type abstr_info = private {
+type abstr_info = Section.abstr_info = private {
abstr_ctx : Constr.named_context;
(** Section variables of this prefix *)
abstr_subst : Univ.Instance.t;
@@ -181,10 +181,6 @@ val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context
val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
val is_in_section : GlobRef.t -> bool
-val add_section_variable : name:Id.t -> poly:bool -> unit
-val add_section_context : Univ.ContextSet.t -> unit
-val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit
-val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit
val replacement_context : unit -> Opaqueproof.work_list
val is_polymorphic_univ : Univ.Level.t -> bool
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 0ca39f0404..7e140f4399 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -4,7 +4,6 @@ Locusops
Pretype_errors
Reductionops
Inductiveops
-InferCumulativity
Arguments_renaming
Retyping
Vnorm
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 3a02e5451a..208b8e28a7 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -40,9 +40,30 @@ let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
~discharge:(fun (_, x) -> Some x)
+let name_instance inst =
+ let map lvl = match Univ.Level.name lvl with
+ | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+ assert false
+ | Some na ->
+ try
+ let qid = Nametab.shortest_qualid_of_universe na in
+ Name (Libnames.qualid_basename qid)
+ with Not_found ->
+ (* Best-effort naming from the string representation of the level.
+ See univNames.ml for a similar hack. *)
+ Name (Id.of_string_soft (Univ.Level.to_string lvl))
+ in
+ Array.map map (Univ.Instance.to_array inst)
+
let declare_universe_context ~poly ctx =
if poly then
- (Global.push_context_set true ctx; Lib.add_section_context ctx)
+ (* FIXME: some upper layers declare universes several times, we hack around
+ by checking whether the universes already exist. *)
+ let (univs, cstr) = ctx in
+ let univs = Univ.LSet.filter (fun u -> not (Lib.is_polymorphic_univ u)) univs in
+ let uctx = Univ.ContextSet.to_context (univs, cstr) in
+ let nas = name_instance (Univ.UContext.instance uctx) in
+ Global.push_section_context (nas, uctx)
else
Lib.add_anonymous_leaf (input_universe_context ctx)
@@ -118,8 +139,6 @@ let cache_constant ((sp,kn), obj) =
in
assert (Constant.equal kn' (Constant.make1 kn));
Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
- let cst = Global.lookup_constant kn' in
- add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
let discharge_constant ((sp, kn), obj) =
@@ -352,7 +371,6 @@ let declare_variable ~name ~kind d =
poly
in
Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
- add_section_variable ~name ~poly;
Decls.(add_variable_data name {opaque;kind});
add_anonymous_leaf (inVariable ());
Impargs.declare_var_implicits ~impl name;
@@ -401,8 +419,6 @@ let cache_inductive ((sp,kn),mie) =
let id = Libnames.basename sp in
let kn' = Global.add_mind id mie in
assert (MutInd.equal kn' (MutInd.make1 kn));
- let mind = Global.lookup_mind kn' in
- add_section_kn ~poly:(Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
let discharge_inductive ((sp,kn),mie) =
@@ -632,9 +648,9 @@ let do_universe ~poly l =
let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
Univ.LSet.empty l, Univ.Constraint.empty
in
- let () = declare_universe_context ~poly ctx in
let src = if poly then BoundUniv else UnqualifiedUniv in
- Lib.add_anonymous_leaf (input_univ_names (src, l))
+ let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
+ declare_universe_context ~poly ctx
let do_constraint ~poly l =
let open Univ in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:01:00 +0000