From 19ea68ecafcee5199dde1b044fd4be9edc211673 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 11 Jun 2019 10:49:25 +0200
Subject: 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.
---
 library/lib.mli | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

(limited to 'library/lib.mli')

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
-- 
cgit v1.2.3