diff options
| author | Pierre-Marie Pédrot | 2019-05-17 15:58:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-25 22:14:34 +0200 |
| commit | 24eccfc6dfec012da081a0891c397f013cc590e5 (patch) | |
| tree | 2149f64a0aac6694977bfbb35b0f79c61c00dd7e /library | |
| parent | 4838fd47542018ba61cd096c93edf45b7ef68529 (diff) | |
Stub code for handling sections in kernel.
For now we only keep a count of the number of open sections, discriminating
between polymorphic and monomorphic ones.
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 7 | ||||
| -rw-r--r-- | library/global.mli | 5 | ||||
| -rw-r--r-- | library/lib.ml | 3 |
3 files changed, 14 insertions, 1 deletions
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. *) |