[libobject] Common metadata for declared objects

This is a first implementation of CEP coq/rfcs#65

We add a common metadata object to atomic libobjects, so we can store
documentation, location, names, and other interesting attributes that
are needed by clients to implement functionality.

As we allow storing names of the objects, we can index them by name to
provide efficient reverse lookup.

We export an experimental API for clients to consume this metadata.

PR coq#16261 is implemented on top of this one.

checker/values.ml

@@ -379,6 +379,10 @@ let v_compiled_lib =
 
 let v_obj = Dyn
 
+let v_source = Sum("source",0, [| [| Opt String |]; [| String |] |])
+let v_loc = Tuple("loc", [| v_source ; Int; Int; Int; Int; Int; Int |])
+let v_obj_data = Tuple("obj_data", [| Opt v_loc; Opt String; Opt v_id |])
+
 let v_open_filter = Sum ("open_filter",1,[|[|v_pred String|]|])
 
 let rec v_aobjs = Sum("algebraic_objects", 0,
@@ -393,7 +397,7 @@ and v_libobjt = Sum("Libobject.t",0,
      [| v_aobjs |];
      [| v_id; v_libobjs |];
      [| List (v_pair v_open_filter v_mp)|];
-     [| v_obj |]
+     [| v_obj_data; v_obj |]
   |])
 
 and v_libobjs = List v_libobjt

interp/abbreviation.ml

@@ -113,7 +113,8 @@ let declare_abbreviation ~local ?(also_in_cases_pattern=true) deprecation id ~on
       abbrev_activated = true;
     }
   in
-  add_leaf (inAbbreviation id (local,abbrev))
+  let data = Data.make ~name:id () in
+  add_leaf ~data (inAbbreviation id (local,abbrev))
 
 let pr_abbreviation kn = pr_qualid (Nametab.shortest_qualid_of_abbreviation Id.Set.empty kn)
 

library/lib.ml

@@ -63,7 +63,7 @@ let classify_segment seg =
           clean (substl, o::keepl, anticipl) stk
         | ExportObject _ ->
           clean (o::substl, keepl, anticipl) stk
-        | AtomicObject obj as o ->
+        | AtomicObject { obj ; _ } as o ->
           begin match classify_object obj with
             | Dispose -> clean acc stk
             | Keep ->
@@ -168,14 +168,15 @@ let add_leaf_entry leaf =
   in
   lib_state := { !lib_state with lib_stk }
 
-let add_discharged_leaf obj =
+let add_discharged_leaf (data, obj) =
   let newobj = Libobject.rebuild_object obj in
-  Libobject.cache_object (prefix(),newobj);
-  add_leaf_entry (AtomicObject newobj)
+  Libobject.cache_object (prefix(), newobj);
+  add_leaf_entry (AtomicObject { data; obj = newobj })
 
-let add_leaf obj =
-  Libobject.cache_object (prefix(),obj);
-  add_leaf_entry (AtomicObject obj)
+let add_leaf ?data obj =
+  let data = Option.default (Libobject.Data.empty) data in
+  Libobject.cache_object (prefix(), obj);
+  add_leaf_entry (AtomicObject { data; obj })
 
 (* Modules. *)
 
@@ -387,7 +388,9 @@ let open_section id =
 let discharge_item = Libobject.(function
   | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | KeepObject _
   | ExportObject _ -> None
-  | AtomicObject obj -> discharge_object obj)
+  | AtomicObject { obj; data } ->
+    let oobj = discharge_object obj in
+    Option.map (fun obj -> (data, obj)) oobj)
 
 let close_section () =
   let (secdecls,mark,before) = split_lib_at_opening () in

library/lib.mli

@@ -52,7 +52,7 @@ val add_leaf_entry : Libobject.t -> unit
 (** Adding operations (which call the [cache] method, and getting the
   current list of operations (most recent ones coming first). *)
 
-val add_leaf : Libobject.obj -> unit
+val add_leaf : ?data:Libobject.Data.t -> Libobject.obj -> unit
 
 (** {6 ... } *)
 

library/libobject.ml

@@ -102,6 +102,27 @@ let ident_subst_function (_,a) = a
 
 type obj = Dyn.t (* persistent dynamic objects *)
 
+module Data : sig
+
+  type t
+
+  val empty : t
+  val make : ?loc:Loc.t -> ?doc:string -> ?name:Names.Id.t -> unit -> t
+  val name : t -> Names.Id.t option
+
+end = struct
+
+  type t =
+    { loc : Loc.t option
+    ; doc : string option
+    ; name : Names.Id.t option
+    }
+
+  let make ?loc ?doc ?name () = { loc; doc; name }
+  let empty = make ()
+  let name { name } = name
+end
+
 (** {6 Substitutive objects}
 
     - The list of bound identifiers is nonempty only if the objects
@@ -122,7 +143,7 @@ and t =
   | IncludeObject of algebraic_objects
   | KeepObject of Names.Id.t * t list
   | ExportObject of { mpl : (open_filter * Names.ModPath.t) list }
-  | AtomicObject of obj
+  | AtomicObject of { data : Data.t ; obj : obj }
 
 and substitutive_objects = Names.MBId.t list * algebraic_objects
 

library/libobject.mli

@@ -132,21 +132,43 @@ val ident_subst_function : substitution * 'a -> 'a
    will hand back two functions, the "injection" and "projection"
    functions for dynamically typed library-objects. *)
 
+(** Common metadata for objects that are stored in modules / .vo files *)
+module Data : sig
+
+  type t
+
+  val empty : t
+  val make : ?loc:Loc.t -> ?doc:string -> ?name:Id.t -> unit -> t
+  val name : t -> Id.t option
+
+end
+
 module Dyn : Dyn.S
 
 type obj = Dyn.t
 
+(** EJGA: Should we attach info to all objects? *)
 type algebraic_objects =
   | Objs of t list
   | Ref of ModPath.t * Mod_subst.substitution
 
 and t =
   | ModuleObject of Id.t * substitutive_objects
+  (** Information and contents for a Coq Module *)
   | ModuleTypeObject of Id.t * substitutive_objects
+  (** Similar but for module types *)
   | IncludeObject of algebraic_objects
+  (** Similar but for include *)
   | KeepObject of Id.t * t list
+  (** A Keep Object is stored at module closing time after the
+     [ModuleObject] proper, and with the goal to register the objects
+     that survive the module with the [Declaremods] registration
+     table. Some other checks are also done. *)
   | ExportObject of { mpl : (open_filter * ModPath.t) list }
-  | AtomicObject of obj
+  (** [ExportObject] stores a list of objects that must be opened in
+     the local context *)
+  | AtomicObject of { data : Data.t; obj : obj }
+  (** Regular  *)
 
 and substitutive_objects = MBId.t list * algebraic_objects
 

plugins/ltac/tacenv.ml

@@ -205,7 +205,8 @@ let inMD : tacdef -> obj =
      classify_function = classify_md}
 
 let register_ltac for_ml local ?deprecation id tac =
-  Lib.add_leaf (inMD {local; replace=NoReplace id; for_ml; expr=tac; depr=deprecation})
+  let data = Libobject.Data.make ~name:id () in
+  Lib.add_leaf ~data (inMD {local; replace=NoReplace id; for_ml; expr=tac; depr=deprecation})
 
 let redefine_ltac local ?deprecation kn tac =
   Lib.add_leaf (inMD {local; replace=Replace kn; for_ml=false; expr=tac; depr=deprecation})

plugins/ltac2/tac2entries.ml

@@ -369,7 +369,8 @@ let register_ltac ?deprecation ?(local = false) ?(mut = false) isrec tactics =
       tacdef_type = t;
       tacdef_deprecation = deprecation;
     } in
-    Lib.add_leaf (inTacDef id def)
+    let data = Libobject.Data.make ~name:id () in
+    Lib.add_leaf ~data (inTacDef id def)
   in
   List.iter iter defs
 
@@ -460,7 +461,9 @@ let register_typedef ?(local = false) isrec types =
     (id, typdef)
   in
   let types = List.map map types in
-  let iter (id, def) = Lib.add_leaf (inTypDef id def) in
+  let iter (id, def) =
+    let data = Libobject.Data.make ~name:id () in
+    Lib.add_leaf ~data (inTypDef id def) in
   List.iter iter types
 
 let register_primitive ?deprecation ?(local = false) {loc;v=id} t ml =
@@ -489,7 +492,8 @@ let register_primitive ?deprecation ?(local = false) {loc;v=id} t ml =
     tacdef_type = t;
     tacdef_deprecation = deprecation;
   } in
-  Lib.add_leaf (inTacDef id def)
+  let data = Libobject.Data.make ~name:id () in
+  Lib.add_leaf ~data (inTacDef id def)
 
 let register_open ?(local = false) qid (params, def) =
   let kn =
@@ -752,7 +756,8 @@ let register_notation ?deprecation ?(local = false) tkn lev body = match tkn, le
   let () = check_lowercase CAst.(make ?loc id) in
   let body = Tac2intern.globalize Id.Set.empty body in
   let abbr = { abbr_body = body; abbr_depr = deprecation } in
-  Lib.add_leaf (inTac2Abbreviation id abbr)
+  let data = Libobject.Data.make ~name:id () in
+  Lib.add_leaf ~data (inTac2Abbreviation id abbr)
 | _ ->
   (* Check that the tokens make sense *)
   let entries = List.map ParseToken.parse_token tkn in

vernac/declare.ml

@@ -221,8 +221,9 @@ let update_tables c =
 
 let register_constant kn kind local =
   let id = Label.to_id (Constant.label kn) in
+  let data = Libobject.Data.make ~name:id () in
   let o = inConstant (id, { cst_kind = kind; cst_locl = local; }) in
-  let () = Lib.add_leaf o in
+  let () = Lib.add_leaf ~data o in
   update_tables kn
 
 let register_side_effect (c, body, role) =
@@ -520,7 +521,8 @@ let declare_variable_core ~name ~kind d =
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
   Decls.(add_variable_data name {opaque;kind});
-  Lib.add_leaf (inVariable name);
+  let data = Libobject.Data.make ~name () in
+  Lib.add_leaf ~data (inVariable name);
   Impargs.declare_var_implicits ~impl name;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
 

vernac/declare.mli

@@ -562,7 +562,7 @@ val is_local_constant : Constant.t -> bool
 
 module Internal : sig
 
-  (* Liboject exports *)
+  (* Libobject exports *)
   module Constant : sig
     type t
     val tag : (Id.t * t) Libobject.Dyn.tag

vernac/declareInd.ml

@@ -108,7 +108,8 @@ let declare_mind ?typing_flags mie =
       Declare.check_exists typ;
       List.iter Declare.check_exists cons) names;
   let mind = Global.add_mind ?typing_flags id mie in
-  let () = Lib.add_leaf (inInductive (id, { ind_names = names })) in
+  let data = Libobject.Data.make ~name:id () in
+  let () = Lib.add_leaf ~data (inInductive (id, { ind_names = names })) in
   if is_unsafe_typing_flags() then feedback_axiom ();
   let isprim = Inductive.is_primitive_record (Inductive.lookup_mind_specif (Global.env()) (mind,0)) in
   Impargs.declare_mib_implicits mind;

vernac/declaremods.ml

@@ -101,9 +101,9 @@ and subst_sobjs sub (mbids,aobjs as sobjs) =
 and subst_objects subst seg =
   let subst_one node =
     match node with
-    | AtomicObject obj ->
+    | AtomicObject { data; obj } ->
       let obj' = Libobject.subst_object (subst,obj) in
-      if obj' == obj then node else AtomicObject obj'
+      if obj' == obj then node else AtomicObject { data; obj=obj' }
     | ModuleObject (id, sobjs) ->
       let sobjs' = subst_sobjs subst sobjs in
       if sobjs' == sobjs then node else ModuleObject (id, sobjs')
@@ -155,9 +155,11 @@ let expand_sobjs (_,aobjs) = expand_aobjs aobjs
 *)
 
 type module_objects =
-  { module_prefix : Nametab.object_prefix;
-    module_substituted_objects : Libobject.t list;
-    module_keep_objects : Libobject.t list;
+  { module_prefix : Nametab.object_prefix
+  ; module_substituted_objects : Libobject.t list
+  ; module_substituted_objects_by_name : Libobject.t Id.Map.t
+  ; module_keep_objects : Libobject.t list
+  ; module_keep_objects_by_name : Libobject.t Id.Map.t
   }
 
 module ModObjs :
@@ -175,6 +177,7 @@ module ModObjs :
    let all () = !table
  end
 
+let modmap () = ModObjs.all ()
 
 (** {6 Name management}
 
@@ -212,6 +215,17 @@ let consistency_checks exists dir =
 
 (** Iterate some function [iter_objects] on all components of a module *)
 
+let get_libobject_name (o : Libobject.t) = match o with
+  | Libobject.AtomicObject { data; _ } ->
+    Libobject.Data.name data
+  | _ -> None
+
+let build_obj_map objs : Libobject.t Id.Map.t =
+  List.fold_left (fun om obj ->
+      let name = get_libobject_name obj in
+      Option.cata (fun name -> Id.Map.add name obj om) om name
+    ) Id.Map.empty objs
+
 let do_module iter_objects i obj_dir obj_mp sobjs kobjs =
   let prefix = Nametab.{ obj_dir ; obj_mp; } in
   consistency_checks false obj_dir;
@@ -220,10 +234,15 @@ let do_module iter_objects i obj_dir obj_mp sobjs kobjs =
   (* If we're not a functor, let's iter on the internal components *)
   if sobjs_no_functor sobjs then begin
     let objs = expand_sobjs sobjs in
+    (* Format.eprintf "do_module: subst: %d | keep %d@\n%!" (List.length objs) (List.length kobjs); *)
+    let module_substituted_objects_by_name = build_obj_map objs in
+    let module_keep_objects_by_name = build_obj_map kobjs in
     let module_objects =
-      { module_prefix = prefix;
-        module_substituted_objects = objs;
-        module_keep_objects = kobjs;
+      { module_prefix = prefix
+      ; module_substituted_objects = objs
+      ; module_substituted_objects_by_name
+      ; module_keep_objects = kobjs
+      ; module_keep_objects_by_name
       }
     in
     ModObjs.set obj_mp module_objects;
@@ -252,7 +271,8 @@ let load_modtype i sp mp sobjs =
 
 let rec load_object i (prefix, obj) =
   match obj with
-  | AtomicObject o -> Libobject.load_object i (prefix, o)
+  | AtomicObject { obj; data } ->
+    Libobject.load_object i (prefix, obj)
   | ModuleObject (id,sobjs) ->
     let name = Lib.make_oname prefix id in
     do_module' load_objects i (name, sobjs)
@@ -350,7 +370,8 @@ let open_modtype i ((sp,kn),_) =
 
 let rec open_object f i (prefix, obj) =
   match obj with
-  | AtomicObject o -> Libobject.open_object f i (prefix, o)
+  | AtomicObject { obj; data } ->
+    Libobject.open_object f i (prefix, obj)
   | ModuleObject (id,sobjs) ->
     let name = Lib.make_oname prefix id in
     let dir = dir_of_sp (fst name) in
@@ -401,7 +422,8 @@ and cache_keep ((sp,kn),kobjs) =
 
 let cache_object (prefix, obj) =
   match obj with
-  | AtomicObject o -> Libobject.cache_object (prefix, o)
+  | AtomicObject { obj; _ } ->
+    Libobject.cache_object (prefix, obj)
   | ModuleObject (id,sobjs) ->
     let name = Lib.make_oname prefix id in
     do_module' load_objects 1 (name, sobjs)
@@ -759,7 +781,6 @@ let end_module_core id m_info objects fs =
     | [], _ | _, _ :: _ -> special@[node]
     | _ -> special@[node;KeepObject (id,keep)]
   in
-
   mp, objects
 
 let end_module () =

vernac/declaremods.mli

@@ -118,3 +118,14 @@ val debug_print_modtab : unit -> Pp.t
 
 val process_module_binding :
   MBId.t -> (Constr.t * Univ.AbstractContext.t option) Declarations.module_alg_expr -> unit
+
+(** Experimental API *)
+type module_objects = private
+  { module_prefix : Nametab.object_prefix
+  ; module_substituted_objects : Libobject.t list
+  ; module_substituted_objects_by_name : Libobject.t Id.Map.t
+  ; module_keep_objects : Libobject.t list
+  ; module_keep_objects_by_name : Libobject.t Id.Map.t
+  }
+
+val modmap : unit -> module_objects Names.MPmap.t

vernac/mltop.ml

@@ -388,7 +388,7 @@ let () =
     ; Summary.unfreeze_function = unfreeze_ml_modules
     ; Summary.init_function = reset_loaded_modules }
 
-(* Liboject entries of declared ML Modules *)
+(* Libobject entries of declared ML Modules *)
 type ml_module_object =
   { mlocal : Vernacexpr.locality_flag
   ; mnames : PluginSpec.t list