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.

1 files changed, 32 insertions, 4 deletions

diff --git a/library/libobject.ml b/library/libobject.ml
index 72791661bc..27e7810e6c 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Pp
+open Names
 
 module Dyn = Dyn.Make ()
 
@@ -34,7 +35,7 @@ let default_object s = {
   open_function = (fun _ _ -> ());
   subst_function = (fun _ ->
     CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
-  classify_function = (fun obj -> Keep obj);
+  classify_function = (fun atomic_obj -> Keep atomic_obj);
   discharge_function = (fun _ -> None);
   rebuild_function = (fun x -> x)}
 
@@ -52,8 +53,35 @@ let default_object s = {
 
 let ident_subst_function (_,a) = a
 
+
 type obj = Dyn.t (* persistent dynamic objects *)
 
+(** {6 Substitutive objects}
+
+    - The list of bound identifiers is nonempty only if the objects
+      are owned by a functor
+
+    - Then comes either the object segment itself (for interactive
+      modules), or a compact way to store derived objects (path to
+      a earlier module + substitution).
+*)
+
+type algebraic_objects =
+  | Objs of objects
+  | Ref of Names.ModPath.t * Mod_subst.substitution
+
+and t =
+  | ModuleObject of substitutive_objects
+  | ModuleTypeObject of substitutive_objects
+  | IncludeObject of algebraic_objects
+  | KeepObject of objects
+  | ImportObject of { export : bool; mp : ModPath.t }
+  | AtomicObject of obj
+
+and objects = (Names.Id.t * t) list
+
+and substitutive_objects = MBId.t list * algebraic_objects
+
 type dynamic_object_declaration = {
   dyn_cache_function : object_name * obj -> unit;
   dyn_load_function : int -> object_name * obj -> unit;
@@ -77,9 +105,9 @@ let declare_object_full odecl =
   and substituter (sub,lobj) = infun (odecl.subst_function (sub,outfun lobj))
   and classifier lobj = match odecl.classify_function (outfun lobj) with
   | Dispose -> Dispose
-  | Substitute obj -> Substitute (infun obj)
-  | Keep obj -> Keep (infun obj)
-  | Anticipate (obj) -> Anticipate (infun obj)
+  | Substitute atomic_obj -> Substitute (infun atomic_obj)
+  | Keep atomic_obj -> Keep (infun atomic_obj)
+  | Anticipate (atomic_obj) -> Anticipate (infun atomic_obj)
   and discharge (oname,lobj) =
     Option.map infun (odecl.discharge_function (oname,outfun lobj))
   and rebuild lobj = infun (odecl.rebuild_function (outfun lobj))