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.
---
 checker/values.ml                 |  22 ++-
 library/declaremods.ml            | 320 ++++++++++++++++++++------------------
 library/declaremods.mli           |   2 +-
 library/lib.ml                    |  59 ++++---
 library/lib.mli                   |  19 ++-
 library/libobject.ml              |  36 ++++-
 library/libobject.mli             |  16 ++
 library/library.ml                |   4 +-
 plugins/extraction/extract_env.ml |  39 ++---
 printing/prettyp.ml               |  41 ++---
 vernac/search.ml                  |  50 +++---
 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 31dcfdd168..69e5c4231f 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
-- 
cgit v1.2.3