diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 93 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 7 | ||||
| -rw-r--r-- | kernel/section.ml | 63 | ||||
| -rw-r--r-- | kernel/section.mli | 46 |
4 files changed, 153 insertions, 56 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8d34f3a34f..ddaed6c941 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -113,9 +113,16 @@ type library_info = DirPath.t * vodigest (** Functor and funsig parameters, most recent first *) type module_parameters = (MBId.t * module_type_body) list +(** Part of the safe_env at a section opening time to be backtracked *) +type section_data = { + rev_env : Environ.env; + rev_univ : Univ.ContextSet.t; + rev_objlabels : Label.Set.t; +} + type safe_environment = { env : Environ.env; - sections : Section.t; + sections : section_data Section.t; modpath : ModPath.t; modvariant : modvariant; modresolver : Mod_subst.delta_resolver; @@ -326,12 +333,18 @@ type constraints_addition = | 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 + if Univ.ContextSet.is_empty cst then senv + else if Section.is_polymorphic senv.sections 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 } + else + let sections = + if Section.is_empty senv.sections then senv.sections + else Section.push_constraints cst senv.sections + in + { senv with + env = Environ.push_context_set ~strict:(not poly) cst senv.env; + univ = Univ.ContextSet.union cst senv.univ; + sections } let add_constraints cst senv = match cst with @@ -819,11 +832,10 @@ let export_private_constants ~in_section ce senv = let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in (ce, exported), senv -let add_recipe ~in_section l r senv = - let kn = Constant.make2 senv.modpath l in +let add_recipe ~in_section kn r senv = let cb = Term_typing.translate_recipe senv.env kn r in let senv = add_constant_aux ~in_section senv (kn, cb) in - kn, senv + senv let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment = let kn = Constant.make2 senv.modpath l in @@ -934,13 +946,68 @@ let add_module l me inl senv = (** {6 Interactive sections *) let open_section ~poly senv = - let sections = Section.open_section ~poly senv.sections in + let custom = { + rev_env = senv.env; + rev_univ = senv.univ; + rev_objlabels = senv.objlabels; + } in + let sections = Section.open_section ~poly ~custom 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 } + let open Section in + let sections0 = senv.sections in + let env0 = senv.env in + (* First phase: revert the declarations added in the section *) + let sections, entries, cstrs, revert = Section.close_section sections0 in + let () = assert (not (Section.is_polymorphic sections0) || Univ.ContextSet.is_empty cstrs) in + let rec pop_revstruct accu entries revstruct = match entries, revstruct with + | [], revstruct -> accu, revstruct + | _ :: _, [] -> + CErrors.anomaly (Pp.str "Unmatched section data") + | entry :: entries, (lbl, leaf) :: revstruct -> + let data = match entry, leaf with + | SecDefinition kn, SFBconst cb -> + let () = assert (Label.equal lbl (Constant.label kn)) in + `Definition (kn, cb) + | SecInductive ind, SFBmind mib -> + let () = assert (Label.equal lbl (MutInd.label ind)) in + `Inductive (ind, mib) + | (SecDefinition _ | SecInductive _), (SFBconst _ | SFBmind _) -> + CErrors.anomaly (Pp.str "Section content mismatch") + | (SecDefinition _ | SecInductive _), (SFBmodule _ | SFBmodtype _) -> + CErrors.anomaly (Pp.str "Module inside a section") + in + pop_revstruct (data :: accu) entries revstruct + in + let redo, revstruct = pop_revstruct [] entries senv.revstruct in + (* Don't revert the delayed constraints. If some delayed constraints were + forced inside the section, they have been turned into global monomorphic + that are going to be replayed. FIXME: the other ones are added twice. *) + let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels } = revert in + let senv = { senv with env; revstruct; sections; univ; objlabels; } in + (* Second phase: replay the discharged section contents *) + let senv = add_constraints (Now cstrs) senv in + let modlist = Section.replacement_context env0 sections0 in + let cooking_info seg = + let { abstr_ctx; abstr_subst; abstr_uctx } = seg in + let abstract = (abstr_ctx, abstr_subst, abstr_uctx) in + { Opaqueproof.modlist; abstract } + in + let fold senv = function + | `Definition (kn, cb) -> + let in_section = not (Section.is_empty senv.sections) in + let info = cooking_info (Section.segment_of_constant env0 kn sections0) in + let r = { Cooking.from = cb; info } in + add_recipe ~in_section kn r senv + | `Inductive (ind, mib) -> + let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in + let mie = Cooking.cook_inductive info mib in + let mie = InferCumulativity.infer_inductive senv.env mie in + let _, senv = add_mind (MutInd.label ind) mie senv in + senv + in + List.fold_left fold senv redo (** {6 Starting / ending interactive modules and module types } *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 10fedc2faf..d3ca642a89 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -27,13 +27,15 @@ val digest_match : actual:vodigest -> required:vodigest -> bool type safe_environment +type section_data + val empty_environment : safe_environment val is_initial : safe_environment -> bool val env_of_safe_env : safe_environment -> Environ.env -val sections_of_safe_env : safe_environment -> Section.t +val sections_of_safe_env : safe_environment -> section_data Section.t (** The safe_environment state monad *) @@ -89,9 +91,6 @@ val add_constant : side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration -> (Constant.t * 'a) safe_transformer -val add_recipe : - in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer - (** Adding an inductive type *) val add_mind : diff --git a/kernel/section.ml b/kernel/section.ml index 12e9c2fd60..188249e77e 100644 --- a/kernel/section.ml +++ b/kernel/section.ml @@ -18,9 +18,9 @@ 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 (_, 'a) section_universes = +| SecMonoUniv : 'a -> ([ `mono ], 'a) section_universes +| SecPolyUniv : Name.t array * UContext.t -> ([ `poly ], 'a) section_universes type section_entry = | SecDefinition of Constant.t @@ -28,21 +28,23 @@ type section_entry = type 'a entry_map = 'a Cmap.t * 'a Mindmap.t -type 'a section = { +type ('a, 'b) section = { sec_context : int; (** Length of the named context suffix that has been introduced locally *) - sec_universes : 'a section_universes; + sec_universes : ('a, ContextSet.t) section_universes; (** Universes local to the section *) sec_entries : section_entry list; (** Definitions introduced in the section *) - sec_data : 'a section_universes entry_map; + sec_data : ('a, unit) section_universes entry_map; + (** Additional data synchronized with the section *) + sec_custom : 'b; } (** 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; +type 'a t = { + sec_poly : ([ `poly ], 'a) section list; + sec_mono : ([ `mono ], 'a) section list; } let empty = { @@ -64,7 +66,7 @@ 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 } +type 'b on_sec = { on_sec : 'a. 'a section_kind -> ('a, 'b) section -> ('a, 'b) section } let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with | [], [] -> CErrors.user_err (Pp.str "No opened section") @@ -75,7 +77,7 @@ let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with 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 } +type ('r, 'b) with_sec = { with_sec : 'a. ('a section_kind * ('a, 'b) section) option -> 'r } let with_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with | [], [] -> f.with_sec None @@ -87,7 +89,7 @@ let push_local s = 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 + 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 -> @@ -97,35 +99,48 @@ let push_context (nas, ctx) s = in on_last_section { on_sec } s -let open_section ~poly sections = +let push_constraints uctx s = + let on_sec (type a) (kind : a section_kind) (sec : (a, _) section) : (a, _) section = match kind with + | SecMono -> + let SecMonoUniv uctx' = sec.sec_universes in + let sec_universes = SecMonoUniv (ContextSet.union uctx uctx') in + { sec with sec_universes } + | SecPoly -> + CErrors.anomaly (Pp.str "Adding monomorphic constraints to polymorphic section") + in + on_last_section { on_sec } s + +let open_section ~poly ~custom sections = if poly then let sec = { sec_context = 0; sec_universes = SecPolyUniv ([||], Univ.UContext.empty); sec_entries = []; sec_data = (Cmap.empty, Mindmap.empty); + sec_custom = custom; } 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_universes = SecMonoUniv Univ.ContextSet.empty; sec_entries = []; sec_data = (Cmap.empty, Mindmap.empty); + sec_custom = custom; } 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, _ -> + | sec :: psecs, _ -> let sections = { sections with sec_poly = psecs } in - sections - | [], _sec :: msecs -> + sections, sec.sec_entries, Univ.ContextSet.empty, sec.sec_custom + | [], sec :: msecs -> let sections = { sections with sec_mono = msecs } in - sections + let SecMonoUniv cstrs = sec.sec_universes in + sections, sec.sec_entries, cstrs, sec.sec_custom | [], [] -> CErrors.user_err (Pp.str "No opened section.") @@ -133,13 +148,17 @@ let same_poly (type a) ~poly (knd : a section_kind) = match knd with | SecPoly -> poly | SecMono -> not poly +let drop_global (type a) : (a, _) section_universes -> (a, unit) section_universes = function +| SecMonoUniv _ -> SecMonoUniv () +| SecPolyUniv _ as u -> u + 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; + sec_data = add_emap e (drop_global sec.sec_universes) sec.sec_data; } else CErrors.user_err (Pp.str "Cannot mix universe polymorphic and \ monomorphic declarations in sections.") @@ -179,13 +198,13 @@ let extract_hyps sec vars 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 + 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 -> + | SecMono, SecMonoUniv () -> Instance.empty, AUContext.empty | SecPoly, SecPolyUniv (nas, ctx) -> Univ.abstract_universes nas ctx diff --git a/kernel/section.mli b/kernel/section.mli index 4b23115ca2..c1026a2980 100644 --- a/kernel/section.mli +++ b/kernel/section.mli @@ -13,39 +13,51 @@ open Univ (** Kernel implementation of sections. *) -type t -(** Type of sections *) +type 'a t +(** Type of sections with additional data ['a] *) -val empty : t +val empty : 'a t -val is_empty : t -> bool +val is_empty : 'a t -> bool (** Checks whether there is no opened section *) -val is_polymorphic : t -> bool +val is_polymorphic : 'a t -> bool (** Checks whether last opened section is polymorphic *) (** {6 Manipulating sections} *) -val open_section : poly:bool -> t -> t +type section_entry = +| SecDefinition of Constant.t +| SecInductive of MutInd.t + +val open_section : poly:bool -> custom:'a -> 'a t -> 'a 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. *) + inside a monomorphic one. A custom data can be attached to this section, + that will be returned by {!close_section}. *) -val close_section : t -> t +val close_section : 'a t -> 'a t * section_entry list * ContextSet.t * 'a +(** Close the current section and returns the entries defined inside, the set + of global monomorphic constraints added in this section, and the custom data + provided at the opening of the section. *) (** {6 Extending sections} *) -val push_local : t -> t +val push_local : 'a t -> 'a t (** Extend the current section with a local definition (cf. push_named). *) -val push_context : Name.t array * UContext.t -> t -> t +val push_context : Name.t array * UContext.t -> 'a t -> 'a 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 +val push_constraints : ContextSet.t -> 'a t -> 'a t +(** Extend the current section with a global universe context. + Assumes that the last opened section is monomorphic. *) + +val push_constant : poly:bool -> Constant.t -> 'a t -> 'a t (** Make the constant as having been defined in this section. *) -val push_inductive : poly:bool -> MutInd.t -> t -> t +val push_inductive : poly:bool -> MutInd.t -> 'a t -> 'a t (** Make the inductive block as having been defined in this section. *) (** {6 Retrieving section data} *) @@ -64,15 +76,15 @@ type abstr_info = private { val empty_segment : abstr_info (** Nothing to abstract *) -val segment_of_constant : Environ.env -> Constant.t -> t -> abstr_info +val segment_of_constant : Environ.env -> Constant.t -> 'a t -> abstr_info (** Section segment at the time of the constant declaration *) -val segment_of_inductive : Environ.env -> MutInd.t -> t -> abstr_info +val segment_of_inductive : Environ.env -> MutInd.t -> 'a t -> abstr_info (** Section segment at the time of the inductive declaration *) -val replacement_context : Environ.env -> t -> Opaqueproof.work_list +val replacement_context : Environ.env -> 'a t -> Opaqueproof.work_list (** Section segments of all declarations from this section. *) -val is_in_section : Environ.env -> GlobRef.t -> t -> bool +val is_in_section : Environ.env -> GlobRef.t -> 'a t -> bool -val is_polymorphic_univ : Level.t -> t -> bool +val is_polymorphic_univ : Level.t -> 'a t -> bool |