Merge PR #10442: Reify libobject containers

Reviewed-by: ejgallego
Reviewed-by: ppedrot

11 files changed, 359 insertions, 249 deletions

diff --git a/checker/values.ml b/checker/values.ml
index cde2db2721..8dc09aed87 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -345,8 +345,26 @@ let v_compiled_lib =
 (** Library objects *)
 
 let v_obj = Dyn
-let v_libobj = Tuple ("libobj", [|v_id;v_obj|])
-let v_libobjs = List v_libobj
+
+let rec v_aobjs = Sum("algebraic_objects", 0,
+  [| [|v_libobjs|];
+     [|v_mp;v_subst|]
+  |])
+and v_substobjs =
+  Tuple("*", [|List v_uid;v_aobjs|])
+and v_libobjt = Sum("Libobject.t",0,
+  [| [| v_substobjs |];
+     [| v_substobjs |];
+     [| v_aobjs |];
+     [| v_libobjs |];
+     [| v_bool; v_mp |];
+     [| v_obj |]
+  |])
+
+and v_libobj = Tuple ("libobj", [|v_id;v_libobjt|])
+
+and v_libobjs = List v_libobj
+
 let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|])
 
 (** STM objects *)
diff --git a/library/declaremods.ml b/library/declaremods.ml
index fc3e667c20..f3922125fe 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -44,22 +44,6 @@ let inl2intopt = function
   | InlineAt i -> Some i
   | DefaultInline -> default_inline ()
 
-(** {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 Lib.lib_objects
-  | Ref of ModPath.t * substitution
-
-type substitutive_objects = MBId.t list * algebraic_objects
-
 (** ModSubstObjs : a cache of module substitutive objects
 
    This table is common to modules and module types.
@@ -99,17 +83,45 @@ module ModSubstObjs :
 
 let sobjs_no_functor (mbids,_) = List.is_empty mbids
 
-let subst_aobjs sub = function
-  | Objs o -> Objs (Lib.subst_objects sub o)
-  | Ref (mp, sub0) -> Ref (mp, join sub0 sub)
-
-let subst_sobjs sub (mbids,aobjs) = (mbids, subst_aobjs sub aobjs)
+let rec subst_aobjs sub = function
+  | Objs o as objs ->
+    let o' = subst_objects sub o in
+    if o == o' then objs else Objs o'
+  | Ref (mp, sub0) as r ->
+    let sub0' = join sub0 sub in
+    if sub0' == sub0 then r else Ref (mp, sub0')
+
+and subst_sobjs sub (mbids,aobjs as sobjs) =
+  let aobjs' = subst_aobjs sub aobjs in
+  if aobjs' == aobjs then sobjs else (mbids, aobjs')
+
+and subst_objects subst seg =
+  let subst_one (id,obj as node) =
+    match obj with
+    | AtomicObject obj ->
+      let obj' = Libobject.subst_object (subst,obj) in
+      if obj' == obj then node else (id, AtomicObject obj')
+    | ModuleObject sobjs ->
+      let sobjs' = subst_sobjs subst sobjs in
+      if sobjs' == sobjs then node else (id, ModuleObject sobjs')
+    | ModuleTypeObject sobjs ->
+      let sobjs' = subst_sobjs subst sobjs in
+      if sobjs' == sobjs then node else (id, ModuleTypeObject sobjs')
+    | IncludeObject aobjs ->
+      let aobjs' = subst_aobjs subst aobjs in
+      if aobjs' == aobjs then node else (id, IncludeObject aobjs')
+    | ImportObject { export; mp } ->
+      let mp' = subst_mp subst mp in
+      if mp'==mp then node else (id, ImportObject { export; mp = mp' })
+    | KeepObject _ -> assert false
+  in
+  List.Smart.map subst_one seg
 
 let expand_aobjs = function
   | Objs o -> o
   | Ref (mp, sub) ->
     match ModSubstObjs.get mp with
-      | (_,Objs o) -> Lib.subst_objects sub o
+      | (_,Objs o) -> subst_objects sub o
       | _ -> assert false (* Invariant : any alias points to concrete objs *)
 
 let expand_sobjs (_,aobjs) = expand_aobjs aobjs
@@ -216,27 +228,41 @@ let do_module' exists iter_objects i ((sp,kn),sobjs) =
 (** Nota: Interactive modules and module types cannot be recached!
     This used to be checked here via a flag along the substobjs. *)
 
-let cache_module = do_module' false Lib.load_objects 1
-let load_module = do_module' false Lib.load_objects
-let open_module = do_module' true Lib.open_objects
-let subst_module (subst,sobjs) = subst_sobjs subst sobjs
-let classify_module sobjs = Substitute sobjs
+(** {6 Declaration of module type substitutive objects} *)
 
-let (in_module : substitutive_objects -> obj),
-    (out_module : obj -> substitutive_objects) =
-  declare_object_full {(default_object "MODULE") with
-    cache_function = cache_module;
-    load_function = load_module;
-    open_function = open_module;
-    subst_function = subst_module;
-    classify_function = classify_module }
+(** Nota: Interactive modules and module types cannot be recached!
+    This used to be checked more properly here. *)
 
+let do_modtype i sp mp sobjs =
+  if Nametab.exists_modtype sp then
+    anomaly (pr_path sp ++ str " already exists.");
+  Nametab.push_modtype (Nametab.Until i) sp mp;
+  ModSubstObjs.set mp sobjs
 
-(** {6 Declaration of module keep objects} *)
+(** {6 Declaration of substitutive objects for Include} *)
 
-let cache_keep _ = anomaly (Pp.str "This module should not be cached!")
+let rec load_object i (name, obj) =
+  match obj with
+  | AtomicObject o -> Libobject.load_object i (name, o)
+  | ModuleObject sobjs -> do_module' false load_objects i (name, sobjs)
+  | ModuleTypeObject sobjs ->
+    let (sp,kn) = name in
+    do_modtype i sp (mp_of_kn kn) sobjs
+  | IncludeObject aobjs -> load_include i (name, aobjs)
+  | ImportObject _ -> ()
+  | KeepObject objs -> load_keep i (name, objs)
+
+and load_objects i prefix objs =
+  List.iter (fun (id, obj) -> load_object i (Lib.make_oname prefix id, obj)) objs
+
+and load_include i ((sp,kn), aobjs) =
+  let obj_dir = Libnames.dirpath sp in
+  let obj_mp = KerName.modpath kn in
+  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  let o = expand_aobjs aobjs in
+  load_objects i prefix o
 
-let load_keep i ((sp,kn),kobjs) =
+and load_keep i ((sp,kn),kobjs) =
   (* Invariant : seg isn't empty *)
   let obj_dir = dir_of_sp sp and obj_mp  = mp_of_kn kn in
   let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
@@ -247,37 +273,29 @@ let load_keep i ((sp,kn),kobjs) =
   assert Nametab.(eq_op prefix' prefix);
   assert (List.is_empty kobjs0);
   ModObjs.set obj_mp (prefix,sobjs,kobjs);
-  Lib.load_objects i prefix kobjs
-
-let open_keep i ((sp,kn),kobjs) =
-  let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
-  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
-  Lib.open_objects i prefix kobjs
-
-let in_modkeep : Lib.lib_objects -> obj =
-  declare_object {(default_object "MODULE KEEP") with
-    cache_function = cache_keep;
-    load_function = load_keep;
-    open_function = open_keep }
-
+  load_objects i prefix kobjs
 
-(** {6 Declaration of module type substitutive objects} *)
-
-(** Nota: Interactive modules and module types cannot be recached!
-    This used to be checked more properly here. *)
-
-let do_modtype i sp mp sobjs =
-  if Nametab.exists_modtype sp then
-    anomaly (pr_path sp ++ str " already exists.");
-  Nametab.push_modtype (Nametab.Until i) sp mp;
-  ModSubstObjs.set mp sobjs
-
-let cache_modtype ((sp,kn),sobjs) = do_modtype 1 sp (mp_of_kn kn) sobjs
-let load_modtype i ((sp,kn),sobjs) = do_modtype i sp (mp_of_kn kn) sobjs
-let subst_modtype (subst,sobjs) = subst_sobjs subst sobjs
-let classify_modtype sobjs = Substitute sobjs
+(** {6 Implementation of Import and Export commands} *)
 
-let open_modtype i ((sp,kn),_) =
+let rec really_import_module mp =
+  (* May raise Not_found for unknown module and for functors *)
+  let prefix,sobjs,keepobjs = ModObjs.get mp in
+  open_objects 1 prefix sobjs;
+  open_objects 1 prefix keepobjs
+
+and open_object i (name, obj) =
+  match obj with
+  | AtomicObject o -> Libobject.open_object i (name, o)
+  | ModuleObject sobjs -> do_module' true open_objects i (name, sobjs)
+  | ModuleTypeObject sobjs -> open_modtype i (name, sobjs)
+  | IncludeObject aobjs -> open_include i (name, aobjs)
+  | ImportObject { mp; _ } -> open_import i mp
+  | KeepObject objs -> open_keep i (name, objs)
+
+and open_objects i prefix objs =
+  List.iter (fun (id, obj) -> open_object i (Lib.make_oname prefix id, obj)) objs
+
+and open_modtype i ((sp,kn),_) =
   let mp = mp_of_kn kn in
   let mp' =
     try Nametab.locate_modtype (qualid_of_path sp)
@@ -287,41 +305,61 @@ let open_modtype i ((sp,kn),_) =
   assert (ModPath.equal mp mp');
   Nametab.push_modtype (Nametab.Exactly i) sp mp
 
-let (in_modtype : substitutive_objects -> obj),
-    (out_modtype : obj -> substitutive_objects) =
-  declare_object_full {(default_object "MODULE TYPE") with
-      cache_function = cache_modtype;
-      open_function = open_modtype;
-      load_function = load_modtype;
-      subst_function = subst_modtype;
-      classify_function = classify_modtype }
-
-
-(** {6 Declaration of substitutive objects for Include} *)
-
-let do_include do_load do_open i ((sp,kn),aobjs) =
+and open_include i ((sp,kn), aobjs) =
   let obj_dir = Libnames.dirpath sp in
   let obj_mp = KerName.modpath kn in
   let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
   let o = expand_aobjs aobjs in
-  if do_load then Lib.load_objects i prefix o;
-  if do_open then Lib.open_objects i prefix o
-
-let cache_include = do_include true true 1
-let load_include = do_include true false
-let open_include = do_include false true
-let subst_include (subst,aobjs) = subst_aobjs subst aobjs
-let classify_include aobjs = Substitute aobjs
+  open_objects i prefix o
 
-let (in_include : algebraic_objects -> obj),
-    (out_include : obj -> algebraic_objects) =
-  declare_object_full {(default_object "INCLUDE") with
-    cache_function = cache_include;
-    load_function = load_include;
-    open_function = open_include;
-    subst_function = subst_include;
-    classify_function = classify_include }
+and open_import i mp =
+  if Int.equal i 1 then really_import_module mp
 
+and open_keep i ((sp,kn),kobjs) =
+  let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
+  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  open_objects i prefix kobjs
+
+let rec cache_object (name, obj) =
+  match obj with
+  | AtomicObject o -> Libobject.cache_object (name, o)
+  | ModuleObject sobjs -> do_module' false load_objects 1 (name, sobjs)
+  | ModuleTypeObject sobjs ->
+    let (sp,kn) = name in
+    do_modtype 1 sp (mp_of_kn kn) sobjs
+  | IncludeObject aobjs -> cache_include (name, aobjs)
+  | ImportObject { mp } -> really_import_module mp
+  | KeepObject objs -> cache_keep (name, objs)
+
+and cache_include ((sp,kn), aobjs) =
+  let obj_dir = Libnames.dirpath sp in
+  let obj_mp = KerName.modpath kn in
+  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  let o = expand_aobjs aobjs in
+  load_objects 1 prefix o;
+  open_objects 1 prefix o
+
+and cache_keep ((sp,kn),kobjs) =
+  anomaly (Pp.str "This module should not be cached!")
+
+(* Adding operations with containers *)
+
+let add_leaf id obj =
+  if ModPath.equal (Lib.current_mp ()) ModPath.initial then
+    user_err Pp.(str "No session module started (use -top dir)");
+  let oname = Lib.make_foname id in
+  cache_object (oname,obj);
+  Lib.add_entry oname (Lib.Leaf obj);
+  oname
+
+let add_leaves id objs =
+  let oname = Lib.make_foname id in
+  let add_obj obj =
+    Lib.add_entry oname (Lib.Leaf obj);
+    load_object 1 (oname,obj)
+  in
+  List.iter add_obj objs;
+  oname
 
 (** {6 Handler for missing entries in ModSubstObjs} *)
 
@@ -331,11 +369,11 @@ let (in_include : algebraic_objects -> obj),
 
 let mp_id mp id = MPdot (mp, Label.of_id id)
 
-let rec register_mod_objs mp (id,obj) = match object_tag obj with
-  | "MODULE" -> ModSubstObjs.set (mp_id mp id) (out_module obj)
-  | "MODULE TYPE" -> ModSubstObjs.set (mp_id mp id) (out_modtype obj)
-  | "INCLUDE" ->
-    List.iter (register_mod_objs mp) (expand_aobjs (out_include obj))
+let rec register_mod_objs mp (id,obj) = match obj with
+  | ModuleObject sobjs -> ModSubstObjs.set (mp_id mp id) sobjs
+  | ModuleTypeObject sobjs -> ModSubstObjs.set (mp_id mp id) sobjs
+  | IncludeObject aobjs ->
+    List.iter (register_mod_objs mp) (expand_aobjs aobjs)
   | _ -> ()
 
 let handle_missing_substobjs mp = match mp with
@@ -387,15 +425,18 @@ let rec replace_module_object idl mp0 objs0 mp1 objs1 =
   match idl, objs0 with
   | _,[] -> []
   | id::idl,(id',obj)::tail when Id.equal id id' ->
-    assert (String.equal (object_tag obj) "MODULE");
-    let mp_id = MPdot(mp0, Label.of_id id) in
-    let objs = match idl with
-      | [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1
-      | _ ->
-        let objs_id = expand_sobjs (out_module obj) in
-        replace_module_object idl mp_id objs_id mp1 objs1
-    in
-    (id, in_module ([], Objs objs))::tail
+    begin match obj with
+    | ModuleObject sobjs ->
+      let mp_id = MPdot(mp0, Label.of_id id) in
+      let objs = match idl with
+        | [] -> subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1
+        | _ ->
+          let objs_id = expand_sobjs sobjs in
+          replace_module_object idl mp_id objs_id mp1 objs1
+      in
+      (id, ModuleObject ([], Objs objs))::tail
+    | _ -> assert false
+    end
   | idl,lobj::tail -> lobj::replace_module_object idl mp0 tail mp1 objs1
 
 let type_of_mod mp env = function
@@ -450,7 +491,7 @@ let process_module_binding mbid me =
   let sobjs = get_module_sobjs false (Global.env()) (default_inline ()) me in
   let subst = map_mp (get_module_path me) mp empty_delta_resolver in
   let sobjs = subst_sobjs subst sobjs in
-  do_module false Lib.load_objects 1 dir mp sobjs []
+  do_module false load_objects 1 dir mp sobjs []
 
 (** Process a declaration of functor parameter(s) (Id1 .. Idn : Typ)
     i.e. possibly multiple names with the same module type.
@@ -473,7 +514,7 @@ let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) =
     let mp = MPbound mbid in
     let resolver = Global.add_module_parameter mbid mty inl in
     let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
-    do_module false Lib.load_objects 1 dir mp sobjs [];
+    do_module false load_objects 1 dir mp sobjs [];
     (mbid,mty,inl)::acc
   in
   let acc = List.fold_left fold acc idl in
@@ -632,13 +673,13 @@ let end_module () =
       | Some (mty, _) ->
         subst_sobjs (map_mp (get_module_path mty) mp resolver) sobjs
   in
-  let node = in_module sobjs in
+  let node = ModuleObject sobjs in
   (* We add the keep objects, if any, and if this isn't a functor *)
   let objects = match keep, mbids with
     | [], _ | _, _ :: _ -> special@[node]
-    | _ -> special@[node;in_modkeep keep]
+    | _ -> special@[node;KeepObject keep]
   in
-  let newoname = Lib.add_leaves id objects in
+  let newoname = add_leaves id objects in
 
   (* Name consistency check : start_ vs. end_module, kernel vs. library *)
   assert (eq_full_path (fst newoname) (fst oldoname));
@@ -705,7 +746,7 @@ let declare_module interp_modast id args res mexpr_o fs =
   check_subtypes mp subs;
 
   let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
-  ignore (Lib.add_leaf id (in_module sobjs));
+  ignore (add_leaf id (ModuleObject sobjs));
   mp
 
 end
@@ -734,7 +775,7 @@ let end_modtype () =
   let mp, mbids = Global.end_modtype fs id in
   let modtypeobjs = (mbids, Objs substitute) in
   check_subtypes_mt mp sub_mty_l;
-  let oname = Lib.add_leaves id (special@[in_modtype modtypeobjs])
+  let oname = add_leaves id (special@[ModuleTypeObject modtypeobjs])
   in
   (* Check name consistence : start_ vs. end_modtype, kernel vs. library *)
   assert (eq_full_path (fst oname) (fst oldoname));
@@ -779,7 +820,7 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs =
   (* Subtyping checks *)
   check_subtypes_mt mp sub_mty_l;
 
-  ignore (Lib.add_leaf id (in_modtype sobjs));
+  ignore (add_leaf id (ModuleTypeObject sobjs));
   mp
 
 end
@@ -834,7 +875,7 @@ let declare_one_include interp_modast (me_ast,annot) =
   let resolver = Global.add_include me is_mod inl in
   let subst = join subst_self (map_mp base_mp cur_mp resolver) in
   let aobjs = subst_aobjs subst aobjs in
-  ignore (Lib.add_leaf (Lib.current_mod_id ()) (in_include aobjs))
+  ignore (add_leaf (Lib.current_mod_id ()) (IncludeObject aobjs))
 
 let declare_include interp me_asts =
   List.iter (declare_one_include interp) me_asts
@@ -913,7 +954,7 @@ let register_library dir cenv (objs:library_objects) digest univ =
         anomaly (Pp.str "Unexpected disk module name.");
   in
   let sobjs,keepobjs = objs in
-  do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs
+  do_module false load_objects 1 dir mp ([],Objs sobjs) keepobjs
 
 let get_library_native_symbols dir =
   Safe_typing.get_library_native_symbols (Global.safe_env ()) dir
@@ -937,45 +978,16 @@ let end_library ?except ~output_native_objects dir =
   let substitute, keep, _ = Lib.classify_segment lib_stack in
   cenv,(substitute,keep),ast
 
-
-
-(** {6 Implementation of Import and Export commands} *)
-
-let really_import_module mp =
-  (* May raise Not_found for unknown module and for functors *)
-  let prefix,sobjs,keepobjs = ModObjs.get mp in
-  Lib.open_objects 1 prefix sobjs;
-  Lib.open_objects 1 prefix keepobjs
-
-let cache_import (_,(_,mp)) = really_import_module mp
-
-let open_import i obj =
-  if Int.equal i 1 then cache_import obj
-
-let classify_import (export,_ as obj) =
-  if export then Substitute obj else Dispose
-
-let subst_import (subst,(export,mp as obj)) =
-  let mp' = subst_mp subst mp in
-  if mp'==mp then obj else (export,mp')
-
-let in_import : bool * ModPath.t -> obj =
-  declare_object {(default_object "IMPORT MODULE") with
-    cache_function = cache_import;
-    open_function = open_import;
-    subst_function = subst_import;
-    classify_function = classify_import }
-
 let import_module export mp =
-  Lib.add_anonymous_leaf (in_import (export,mp))
-
+  really_import_module mp;
+  Lib.add_anonymous_entry (Lib.Leaf (ImportObject { export; mp }))
 
 (** {6 Iterators} *)
 
 let iter_all_segments f =
-  let rec apply_obj prefix (id,obj) = match object_tag obj with
-    | "INCLUDE" ->
-      let objs = expand_aobjs (out_include obj) in
+  let rec apply_obj prefix (id,obj) = match obj with
+    | IncludeObject aobjs ->
+      let objs = expand_aobjs aobjs in
       List.iter (apply_obj prefix) objs
     | _ -> f (Lib.make_oname prefix id) obj
   in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 93aadd25de..9c0baf0a4c 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -130,7 +130,7 @@ val declare_include :
     (together with their section path). *)
 
 val iter_all_segments :
-  (Libobject.object_name -> Libobject.obj -> unit) -> unit
+  (Libobject.object_name -> Libobject.t -> unit) -> unit
 
 
 val debug_print_modtab : unit -> Pp.t
diff --git a/library/lib.ml b/library/lib.ml
index 3eb74808e4..576e23c4f5 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -28,7 +28,7 @@ let make_oname Nametab.{ obj_dir; obj_mp } id =
 
 (* let make_oname (dirpath,(mp,dir)) id = *)
 type node =
-  | Leaf of 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
@@ -37,7 +37,8 @@ type library_entry = object_name * node
 
 type library_segment = library_entry list
 
-type lib_objects =  (Names.Id.t * obj) list
+type lib_atomic_objects = (Id.t * Libobject.obj) list
+type lib_objects =  (Names.Id.t * Libobject.t) list
 
 let module_kind is_type =
   if is_type then "module type" else "module"
@@ -45,10 +46,10 @@ let module_kind is_type =
 let iter_objects f i prefix =
   List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
 
-let load_objects i pr = iter_objects load_object i pr
-let open_objects i pr = iter_objects open_object i pr
+let load_atomic_objects i pr = iter_objects load_object i pr
+let open_atomic_objects i pr = iter_objects open_object i pr
 
-let subst_objects subst seg = 
+let subst_atomic_objects subst seg =
   let subst_one = fun (id,obj as node) ->
     let obj' = subst_object (subst,obj) in
       if obj' == obj then node else
@@ -67,15 +68,28 @@ let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
     | ((sp,kn),Leaf o) :: stk ->
-	let id = Names.Label.to_id (Names.KerName.label kn) in
-	  (match classify_object o with
-	     | Dispose -> clean acc stk
-	     | Keep o' ->
-		 clean (substl, (id,o')::keepl, anticipl) stk
-	     | Substitute o' ->
-		 clean ((id,o')::substl, keepl, anticipl) stk
-	     | Anticipate o' ->
-		 clean (substl, keepl, o'::anticipl) stk)
+          let id = Names.Label.to_id (Names.KerName.label kn) in
+    begin match o with
+    | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ ->
+      clean ((id,o)::substl, keepl, anticipl) stk
+    | KeepObject _ ->
+      clean (substl, (id,o)::keepl, anticipl) stk
+    | ImportObject { export } ->
+      if export then
+        clean ((id,o)::substl, keepl, anticipl) stk
+      else
+        clean acc stk
+    | AtomicObject obj ->
+      begin match classify_object obj with
+        | Dispose -> clean acc stk
+        | Keep o' ->
+          clean (substl, (id,AtomicObject o')::keepl, anticipl) stk
+        | Substitute o' ->
+          clean ((id,AtomicObject o')::substl, keepl, anticipl) stk
+        | Anticipate o' ->
+          clean (substl, keepl, AtomicObject o'::anticipl) stk
+      end
+    end
     | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections")
     | (_,OpenedModule (ty,_,_,_)) :: _ ->
       user_err ~hdr:"Lib.classify_segment"
@@ -223,19 +237,19 @@ let add_leaf id obj =
     user_err Pp.(str "No session module started (use -top dir)");
   let oname = make_foname id in
   cache_object (oname,obj);
-  add_entry oname (Leaf obj);
+  add_entry oname (Leaf (AtomicObject obj));
   oname
 
 let add_discharged_leaf id obj =
   let oname = make_foname id in
   let newobj = rebuild_object obj in
   cache_object (oname,newobj);
-  add_entry oname (Leaf newobj)
+  add_entry oname (Leaf (AtomicObject newobj))
 
 let add_leaves id objs =
   let oname = make_foname id in
   let add_obj obj =
-    add_entry oname (Leaf obj);
+    add_entry oname (Leaf (AtomicObject obj));
     load_object 1 (oname,obj)
   in
   List.iter add_obj objs;
@@ -246,9 +260,9 @@ let add_anonymous_leaf ?(cache_first = true) obj =
   let oname = make_foname id in
   if cache_first then begin
     cache_object (oname,obj);
-    add_entry oname (Leaf obj)
+    add_entry oname (Leaf (AtomicObject obj))
   end else begin
-    add_entry oname (Leaf obj);
+    add_entry oname (Leaf (AtomicObject obj));
     cache_object (oname,obj)
   end
 
@@ -583,7 +597,12 @@ let open_section id =
 let discharge_item ((sp,_ as oname),e) =
   match e with
   | Leaf lobj ->
-      Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
+    begin match lobj with
+    | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | KeepObject _
+    | ImportObject _ -> None
+    | AtomicObject obj ->
+      Option.map (fun o -> (basename sp,o)) (discharge_object (oname,obj))
+    end
   | OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
       anomaly (Pp.str "discharge_item.")
 
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
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))
diff --git a/library/libobject.mli b/library/libobject.mli
index a7151d3bf2..3b37db4a6f 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -103,6 +103,22 @@ val ident_subst_function : substitution * 'a -> 'a
 
 type obj
 
+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 : Names.ModPath.t }
+  | AtomicObject of obj
+
+and objects = (Names.Id.t * t) list
+
+and substitutive_objects = Names.MBId.t list * algebraic_objects
+
 val declare_object_full :
   'a object_declaration -> ('a -> obj) * (obj -> 'a)
 
diff --git a/library/library.ml b/library/library.ml
index 0d4148d7e4..b72dd9dd67 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -488,7 +488,7 @@ let require_library_from_dirpath ~lib_resolver modrefl export =
 let safe_locate_module qid =
   try Nametab.locate_module qid
   with Not_found ->
-    user_err ?loc:qid.CAst.loc ~hdr:"import_library"
+    user_err ?loc:qid.CAst.loc ~hdr:"safe_locate_module"
       (pr_qualid qid ++ str " is not a module")
 
 let import_module export modl =
@@ -513,7 +513,7 @@ let import_module export modl =
             flush acc;
             try Declaremods.import_module export mp; aux [] l
             with Not_found ->
-              user_err ?loc:qid.CAst.loc ~hdr:"import_library"
+              user_err ?loc:qid.CAst.loc ~hdr:"import_module"
                 (pr_qualid qid ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7ee8d7f342..ca1520594d 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -29,24 +29,27 @@ open Common
 
 let toplevel_env () =
   let get_reference = function
-    | (_,kn), Lib.Leaf o ->
-        let mp,l = KerName.repr kn in
-	begin match Libobject.object_tag o with
-	  | "CONSTANT" ->
-            let constant = Global.lookup_constant (Constant.make1 kn) in
-            Some (l, SFBconst constant)
-	  | "INDUCTIVE" ->
-            let inductive = Global.lookup_mind (MutInd.make1 kn) in
-            Some (l, SFBmind inductive)
-	  | "MODULE" ->
-            let modl = Global.lookup_module (MPdot (mp, l)) in
-            Some (l, SFBmodule modl)
-	  | "MODULE TYPE" ->
-            let modtype = Global.lookup_modtype (MPdot (mp, l)) in
-            Some (l, SFBmodtype modtype)
-          | "INCLUDE" -> user_err Pp.(str "No extraction of toplevel Include yet.")
-	  | _ -> None
-        end
+    | (_,kn), Lib.Leaf Libobject.AtomicObject o ->
+      let mp,l = KerName.repr kn in
+            begin match Libobject.object_tag o with
+            | "CONSTANT" ->
+        let constant = Global.lookup_constant (Constant.make1 kn) in
+        Some (l, SFBconst constant)
+            | "INDUCTIVE" ->
+        let inductive = Global.lookup_mind (MutInd.make1 kn) in
+        Some (l, SFBmind inductive)
+            | _ -> None
+      end
+    | (_,kn), Lib.Leaf Libobject.ModuleObject _ ->
+      let mp,l = KerName.repr kn in
+      let modl = Global.lookup_module (MPdot (mp, l)) in
+      Some (l, SFBmodule modl)
+    | (_,kn), Lib.Leaf Libobject.ModuleTypeObject _ ->
+      let mp,l = KerName.repr kn in
+      let modtype = Global.lookup_modtype (MPdot (mp, l)) in
+      Some (l, SFBmodtype modtype)
+    | (_,kn), Lib.Leaf Libobject.IncludeObject _ ->
+      user_err Pp.(str "No extraction of toplevel Include yet.")
     | _ -> None
   in
   List.rev (List.map_filter get_reference (Lib.contents ()))
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index a2bdb30773..9b1acddef1 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -611,9 +611,11 @@ let gallina_print_syntactic_def env kn =
        [Notation.SynDefRule kn] (pr_glob_constr_env env) c)
 
 let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
-  let sep = if with_values then " = " else " : "
-  and tag = object_tag lobj in
-    match (oname,tag) with
+  let sep = if with_values then " = " else " : " in
+  match lobj with
+  | AtomicObject o ->
+    let tag = object_tag o in
+    begin match (oname,tag) with
       | (_,"VARIABLE") ->
 	  (* Outside sections, VARIABLES still exist but only with universes
              constraints *)
@@ -622,16 +624,18 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
           Some (print_constant with_values sep (Constant.make1 kn) None)
       | (_,"INDUCTIVE") ->
           Some (gallina_print_inductive (MutInd.make1 kn) None)
-      | (_,"MODULE") ->
-          let (mp,l) = KerName.repr kn in
-	    Some (print_module with_values (MPdot (mp,l)))
-      | (_,"MODULE TYPE") ->
-          let (mp,l) = KerName.repr kn in
-	  Some (print_modtype (MPdot (mp,l)))
       | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
 	    "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
       (* To deal with forgotten cases... *)
       | (_,s) -> None
+    end
+  | ModuleObject _ ->
+    let (mp,l) = KerName.repr kn in
+    Some (print_module with_values (MPdot (mp,l)))
+  | ModuleTypeObject _ ->
+    let (mp,l) = KerName.repr kn in
+          Some (print_modtype (MPdot (mp,l)))
+  | _ -> None
 
 let gallina_print_library_entry env sigma with_values ent =
   let pr_name (sp,_) = Id.print (basename sp) in
@@ -713,7 +717,7 @@ let print_full_context_typ env sigma = print_context env sigma false None (Lib.c
 
 let print_full_pure_context env sigma =
   let rec prec = function
-  | ((_,kn),Lib.Leaf lobj)::rest ->
+  | ((_,kn),Lib.Leaf AtomicObject lobj)::rest ->
       let pp = match object_tag lobj with
       | "CONSTANT" ->
 	  let con = Global.constant_of_delta_kn kn in
@@ -741,17 +745,16 @@ let print_full_pure_context env sigma =
 	  let mib = Global.lookup_mind mind in
           pr_mutual_inductive_body (Global.env()) mind mib None ++
 	    str "." ++ fnl () ++ fnl ()
-      | "MODULE" ->
-	  (* TODO: make it reparsable *)
-          let (mp,l) = KerName.repr kn in
-	  print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
-      | "MODULE TYPE" ->
-	  (* TODO: make it reparsable *)
-	  (* TODO: make it reparsable *)
-          let (mp,l) = KerName.repr kn in
-	  print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
       | _ -> mt () in
       prec rest ++ pp
+  | ((_,kn),Lib.Leaf ModuleObject _)::rest ->
+          (* TODO: make it reparsable *)
+    let (mp,l) = KerName.repr kn in
+          prec rest ++ print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
+  | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest ->
+          (* TODO: make it reparsable *)
+    let (mp,l) = KerName.repr kn in
+          prec rest ++ print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
   | _::rest -> prec rest
   | _ -> mt () in
   prec (Lib.contents ())
diff --git a/vernac/search.ml b/vernac/search.ml
index a7f1dd33c2..4af14e895d 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -75,30 +75,34 @@ let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) =
 (* General search over declarations *)
 let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
   let env = Global.env () in
-  let iter_obj (sp, kn) lobj = match object_tag lobj with
-  | "VARIABLE" ->
-    begin try
-      let decl = Global.lookup_named (basename sp) in
-      fn (VarRef (NamedDecl.get_id decl)) env (NamedDecl.get_type decl)
-    with Not_found -> (* we are in a section *) () end
-  | "CONSTANT" ->
-    let cst = Global.constant_of_delta_kn kn in
-    let gr = ConstRef cst in
-    let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
+  let iter_obj (sp, kn) lobj = match lobj with
+  | AtomicObject o ->
+    begin match object_tag o with
+    | "VARIABLE" ->
+      begin try
+        let decl = Global.lookup_named (basename sp) in
+        fn (VarRef (NamedDecl.get_id decl)) env (NamedDecl.get_type decl)
+      with Not_found -> (* we are in a section *) () end
+    | "CONSTANT" ->
+      let cst = Global.constant_of_delta_kn kn in
+      let gr = ConstRef cst in
+      let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
       fn gr env typ
-  | "INDUCTIVE" ->
-    let mind = Global.mind_of_delta_kn kn in
-    let mib = Global.lookup_mind mind in
-    let iter_packet i mip =
-      let ind = (mind, i) in
-      let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
-      let i = (ind, u) in
-      let typ = Inductiveops.type_of_inductive env i in
-      let () = fn (IndRef ind) env typ in
-      let len = Array.length mip.mind_user_lc in
-      iter_constructors ind u fn env len
-    in
-    Array.iteri iter_packet mib.mind_packets
+    | "INDUCTIVE" ->
+      let mind = Global.mind_of_delta_kn kn in
+      let mib = Global.lookup_mind mind in
+      let iter_packet i mip =
+        let ind = (mind, i) in
+        let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
+        let i = (ind, u) in
+        let typ = Inductiveops.type_of_inductive env i in
+        let () = fn (IndRef ind) env typ in
+        let len = Array.length mip.mind_user_lc in
+        iter_constructors ind u fn env len
+      in
+      Array.iteri iter_packet mib.mind_packets
+    | _ -> ()
+    end
   | _ -> ()
   in
   try Declaremods.iter_all_segments iter_obj