diff options
| author | Maxime Dénès | 2019-06-11 10:49:25 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-06-28 13:28:03 +0200 |
| commit | 19ea68ecafcee5199dde1b044fd4be9edc211673 (patch) | |
| tree | f6a6fec1e8825371cbdab78931d0dd5c831dd15b /library/lib.mli | |
| parent | a4f6189978b15df8ce4cc8c8fcb8acb6f069ee8e (diff) | |
Reify libobject containers
We make a few libobject constructions (Module, Module Type,
Include,...) first-class and rephrase their handling in direct style (removing
the inversion of control). This makes it easier to define iterators over
objects without hacks like inspecting the tags of dynamic objects.
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/library/lib.mli b/library/lib.mli index 2cd43b66b3..01366ddfd0 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -20,22 +20,24 @@ type is_type = bool (* Module Type or just Module *) type export = bool option (* None for a Module Type *) val make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name +val make_foname : Names.Id.t -> Libnames.full_path * Names.KerName.t type node = - | Leaf of Libobject.obj + | Leaf of Libobject.t | CompilingLibrary of Nametab.object_prefix | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen | OpenedSection of Nametab.object_prefix * Summary.frozen type library_segment = (Libobject.object_name * node) list -type lib_objects = (Id.t * Libobject.obj) list +type lib_atomic_objects = (Id.t * Libobject.obj) list +type lib_objects = (Id.t * Libobject.t) list (** {6 Object iteration functions. } *) -val open_objects : int -> Nametab.object_prefix -> lib_objects -> unit -val load_objects : int -> Nametab.object_prefix -> lib_objects -> unit -val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects +val open_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit +val load_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit +val subst_atomic_objects : Mod_subst.substitution -> lib_atomic_objects -> lib_atomic_objects (*val load_and_subst_objects : int -> Libnames.Nametab.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*) (** [classify_segment seg] verifies that there are no OpenedThings, @@ -44,12 +46,17 @@ val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects [Substitute], [Keep], [Anticipate] respectively. The order of each returned list is the same as in the input list. *) val classify_segment : - library_segment -> lib_objects * lib_objects * Libobject.obj list + library_segment -> lib_objects * lib_objects * Libobject.t list (** [segment_of_objects prefix objs] forms a list of Leafs *) val segment_of_objects : Nametab.object_prefix -> lib_objects -> library_segment +(** {6 ... } *) +(** Low-level adding operations *) + +val add_entry : Libobject.object_name -> node -> unit +val add_anonymous_entry : node -> unit (** {6 ... } *) (** Adding operations (which call the [cache] method, and getting the |