diff options
| -rw-r--r-- | kernel/safe_typing.ml | 44 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 6 | ||||
| -rw-r--r-- | library/global.ml | 7 | ||||
| -rw-r--r-- | library/global.mli | 5 | ||||
| -rw-r--r-- | library/lib.ml | 3 |
5 files changed, 63 insertions, 2 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6970a11e72..783ce63b8c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -113,8 +113,16 @@ type library_info = DirPath.t * vodigest (** Functor and funsig parameters, most recent first *) type module_parameters = (MBId.t * module_type_body) list +(** Sections can be nested with the proviso that no monomorphic section can be + opened inside a polymorphic one. The reverse is allowed. *) +type sections = { + sec_poly : int; + sec_mono : int; +} + type safe_environment = { env : Environ.env; + sections : sections; modpath : ModPath.t; modvariant : modvariant; modresolver : Mod_subst.delta_resolver; @@ -142,6 +150,11 @@ let rec library_dp_of_senv senv = | SIG(_,senv) -> library_dp_of_senv senv | STRUCT(_,senv) -> library_dp_of_senv senv +let empty_sections = { + sec_poly = 0; + sec_mono = 0; +} + let empty_environment = { env = Environ.empty_env; modpath = ModPath.initial; @@ -151,6 +164,7 @@ let empty_environment = revstruct = []; modlabels = Label.Set.empty; objlabels = Label.Set.empty; + sections = empty_sections; future_cst = []; univ = Univ.ContextSet.empty; engagement = None; @@ -385,8 +399,11 @@ let check_current_library dir senv = match senv.modvariant with (** When operating on modules, we're normally outside sections *) +let is_empty_sections s = + Int.equal s.sec_poly 0 && Int.equal s.sec_mono 0 + let check_empty_context senv = - assert (Environ.empty_context senv.env) + assert (Environ.empty_context senv.env && is_empty_sections senv.sections) (** When adding a parameter to the current module/modtype, it must have been freshly started *) @@ -435,12 +452,14 @@ let safe_push_named d env = let push_named_def (id,de) senv = + let () = assert (not @@ is_empty_sections 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'' } let push_named_assum (x,t) senv = + let () = assert (not @@ is_empty_sections 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 @@ -902,6 +921,29 @@ let add_module l me inl senv = in (mp,mb.mod_delta),senv'' +(** {6 Interactive sections *) + +let open_section ~poly senv = + let sections = senv.sections in + if poly then + let sections = { sections with sec_poly = sections.sec_poly + 1 } in + { senv with sections } + else if Int.equal sections.sec_poly 0 then + let sections = { sections with sec_mono = sections.sec_mono + 1 } in + { senv with sections } + else + CErrors.anomaly (Pp.str "Cannot open a monomorphic section inside a polymorphic one") + +let close_section senv = + let sections = senv.sections in + if not (Int.equal sections.sec_poly 0) then + let sections = { sections with sec_poly = sections.sec_poly - 1 } in + { senv with sections } + else if not (Int.equal sections.sec_mono 0) then + let sections = { sections with sec_mono = sections.sec_mono - 1 } in + { senv with sections } + else + CErrors.anomaly (Pp.str "No open section") (** {6 Starting / ending interactive modules and module types } *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index fa53fa33fa..4eef43b193 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -140,6 +140,12 @@ 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 + (** {6 Interactive module functions } *) val start_module : Label.t -> ModPath.t safe_transformer diff --git a/library/global.ml b/library/global.ml index 6bb4614aa4..e51c147f6e 100644 --- a/library/global.ml +++ b/library/global.ml @@ -104,6 +104,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..9ac6b1f53c 100644 --- a/library/global.mli +++ b/library/global.mli @@ -71,6 +71,11 @@ val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver +(** Sections *) + +val open_section : poly:bool -> unit +val close_section : Summary.frozen -> unit + (** Interactive modules and module types *) val start_module : Id.t -> ModPath.t diff --git a/library/lib.ml b/library/lib.ml index 1f97424590..367a84409b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -572,6 +572,7 @@ let is_in_section ref = (*************) (* 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 @@ -612,7 +613,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. *) |