diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/opaqueproof.ml | 5 | ||||
| -rw-r--r-- | kernel/opaqueproof.mli | 1 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 126 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 7 | ||||
| -rw-r--r-- | kernel/section.ml | 63 | ||||
| -rw-r--r-- | kernel/section.mli | 46 |
6 files changed, 172 insertions, 76 deletions
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index e256466112..f0ffd2e073 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -142,11 +142,6 @@ let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = funct get_mono (Future.force cu) else Univ.ContextSet.empty -let get_direct_constraints = function -| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") -| Direct (_, cu) -> - Future.chain cu get_mono - module FMap = Future.UUIDMap let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } = diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 7c53656c3c..758a9f5107 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -63,7 +63,6 @@ type indirect_accessor = { indirect opaque accessor given as an argument. *) val force_proof : indirect_accessor -> opaquetab -> opaque -> constr * unit delayed_universes val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t -val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation val subst_opaque : substitution -> opaque -> opaque diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8d34f3a34f..db16bd1e79 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 @@ -578,15 +591,6 @@ type exported_private_constant = Constant.t let add_constant_aux ~in_section senv (kn, cb) = let l = Constant.label kn in - let delayed_cst = match cb.const_body with - | OpaqueDef o when not (Declareops.constant_is_polymorphic cb) -> - let fc = Opaqueproof.get_direct_constraints o in - begin match Future.peek_val fc with - | None -> [Later fc] - | Some c -> [Now c] - end - | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> [] - in (* This is the only place where we hashcons the contents of a constant body *) let cb = if in_section then cb else Declareops.hcons_const_body cb in let cb, otab = match cb.const_body with @@ -601,7 +605,6 @@ let add_constant_aux ~in_section senv (kn, cb) = in let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in let senv' = add_field (l,SFBconst cb) (C kn) senv in - let senv' = add_constraints_list delayed_cst senv' in let senv'' = match cb.const_body with | Undef (Some lev) -> update_resolver @@ -816,15 +819,10 @@ let export_private_constants ~in_section ce senv = let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in let bodies = List.map map exported in let exported = List.map (fun (kn, _) -> kn) exported in + (* No delayed constants to declare *) 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 cb = Term_typing.translate_recipe senv.env kn r in - let senv = add_constant_aux ~in_section senv (kn, cb) in - kn, 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 let cb = @@ -840,8 +838,24 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen Term_typing.translate_constant Term_typing.Pure senv.env kn ce in let senv = + let delayed_cst = match cb.const_body with + | OpaqueDef fc when not (Declareops.constant_is_polymorphic cb) -> + let map (_, u) = match u with + | Opaqueproof.PrivateMonomorphic ctx -> ctx + | Opaqueproof.PrivatePolymorphic _ -> assert false + in + let fc = Future.chain fc map in + begin match Future.peek_val fc with + | None -> [Later fc] + | Some c -> [Now c] + end + | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> [] + in let cb = map_constant (fun c -> Opaqueproof.create c) cb in - add_constant_aux ~in_section senv (kn, cb) in + let senv = add_constant_aux ~in_section senv (kn, cb) in + add_constraints_list delayed_cst senv + in + let senv = match decl with | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) -> @@ -934,13 +948,71 @@ 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. Those that are not forced are not readded + by {!add_constant_aux}. *) + 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 + let cb = Term_typing.translate_recipe senv.env kn r in + (* Delayed constants are already in the global environment *) + add_constant_aux ~in_section senv (kn, cb) + | `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 |