Merge PR #11307: Remove the hacks relying on hardwired libobject tags.

Reviewed-by: maximedenes

11 files changed, 121 insertions, 50 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 835c20a4f7..f640a33773 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -254,7 +254,9 @@ let ppenvwithcst e = pp
 
 let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
-let ppobj obj = Format.print_string (Libobject.object_tag obj)
+let ppobj obj =
+  let Libobject.Dyn.Dyn (tag, _) = obj in
+  Format.print_string (Libobject.Dyn.repr tag)
 
 let cnt = ref 0
 
diff --git a/library/libobject.ml b/library/libobject.ml
index c9ea6bcff8..28d0654444 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -82,8 +82,6 @@ and objects = (Names.Id.t * t) list
 
 and substitutive_objects = MBId.t list * algebraic_objects
 
-let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t
-
 module DynMap = Dyn.Map (struct type 'a t = 'a object_declaration end)
 
 let cache_tab = ref DynMap.empty
@@ -92,14 +90,12 @@ let declare_object_full odecl =
   let na = odecl.object_name in
   let tag = Dyn.create na in
   let () = cache_tab := DynMap.add tag odecl !cache_tab in
-  let infun v = Dyn.Dyn (tag, v) in
-  let outfun v = match Dyn.Easy.prj v tag with
-  | None -> assert false
-  | Some v -> v
-  in
-  (infun,outfun)
+  tag
 
-let declare_object odecl = fst (declare_object_full odecl)
+let declare_object odecl =
+  let tag = declare_object_full odecl in
+  let infun v = Dyn.Dyn (tag, v) in
+  infun
 
 let cache_object (sp, Dyn.Dyn (tag, v)) =
   let decl = DynMap.find tag !cache_tab in
diff --git a/library/libobject.mli b/library/libobject.mli
index 146ccc293f..c25345994a 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -101,7 +101,9 @@ val ident_subst_function : substitution * 'a -> 'a
    will hand back two functions, the "injection" and "projection"
    functions for dynamically typed library-objects. *)
 
-type obj
+module Dyn : Dyn.S
+
+type obj = Dyn.t
 
 type algebraic_objects =
   | Objs of objects
@@ -120,13 +122,11 @@ 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)
+  'a object_declaration -> 'a Dyn.tag
 
 val declare_object :
   'a object_declaration -> ('a -> obj)
 
-val object_tag : obj -> string
-
 val cache_object : object_name * obj -> unit
 val load_object : int -> object_name * obj -> unit
 val open_object : int -> object_name * obj -> unit
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 35110552ab..2dc3e8a934 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -26,19 +26,29 @@ open Common
 (*S Part I: computing Coq environment. *)
 (***************************************)
 
+(* FIXME: this is a Libobject hack that should be removed. *)
+module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> (Label.t * structure_field_body) option end)
+
+let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with
+| f -> f o
+| exception Not_found -> None
+
 let toplevel_env () =
   let get_reference = function
-    | (_,kn), Lib.Leaf Libobject.AtomicObject o ->
-      let mp,l = KerName.repr kn in
-            begin match Libobject.object_tag o with
-            | "CONSTANT" ->
+  | (_,kn), Lib.Leaf Libobject.AtomicObject o ->
+    let mp,l = KerName.repr kn in
+    let handler =
+      DynHandle.add Declare.Internal.objConstant begin fun _ ->
         let constant = Global.lookup_constant (Constant.make1 kn) in
         Some (l, SFBconst constant)
-            | "INDUCTIVE" ->
+      end @@
+      DynHandle.add DeclareInd.Internal.objInductive begin fun _ ->
         let inductive = Global.lookup_mind (MutInd.make1 kn) in
         Some (l, SFBmind inductive)
-            | _ -> None
-      end
+      end @@
+      DynHandle.empty
+    in
+    handle handler o
     | (_,kn), Lib.Leaf Libobject.ModuleObject _ ->
       let mp,l = KerName.repr kn in
       let modl = Global.lookup_module (MPdot (mp, l)) in
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 9a14f4d40f..c7581fb0e0 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -130,8 +130,8 @@ let dummy_constant cst = {
 
 let classify_constant cst = Substitute (dummy_constant cst)
 
-let (inConstant : constant_obj -> obj) =
-  declare_object { (default_object "CONSTANT") with
+let (objConstant : constant_obj Libobject.Dyn.tag) =
+  declare_object_full { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
     open_function = open_constant;
@@ -139,6 +139,8 @@ let (inConstant : constant_obj -> obj) =
     subst_function = ident_subst_function;
     discharge_function = discharge_constant }
 
+let inConstant v = Libobject.Dyn.Easy.inj v objConstant
+
 let update_tables c =
   Impargs.declare_constant_implicits c;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c)
@@ -357,10 +359,12 @@ type variable_declaration =
 
 (* This object is only for things which iterate over objects to find
    variables (only Prettyp.print_context AFAICT) *)
-let inVariable : unit -> obj =
-  declare_object { (default_object "VARIABLE") with
+let objVariable : unit Libobject.Dyn.tag =
+  declare_object_full { (default_object "VARIABLE") with
     classify_function = (fun () -> Dispose)}
 
+let inVariable v = Libobject.Dyn.Easy.inj v objVariable
+
 let declare_variable ~name ~kind d =
   (* Variables are distinguished by only short names *)
   if Decls.variable_exists name then
@@ -497,4 +501,9 @@ module Internal = struct
     ; proof_entry_type = Some typ
     }, args
 
+  type nonrec constant_obj = constant_obj
+
+  let objVariable = objVariable
+  let objConstant = objConstant
+
 end
diff --git a/tactics/declare.mli b/tactics/declare.mli
index c646d2f85b..00c1e31717 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -131,7 +131,8 @@ val check_exists : Id.t -> unit
 (* Used outside this module only in indschemes *)
 exception AlreadyDeclared of (string option * Id.t)
 
-(* For legacy support, do not use *)
+(** {6 For legacy support, do not use}  *)
+
 module Internal : sig
 
   val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry
@@ -145,4 +146,9 @@ module Internal : sig
 
   val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list
 
+  type constant_obj
+
+  val objConstant : constant_obj Libobject.Dyn.tag
+  val objVariable : unit Libobject.Dyn.tag
+
 end
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index 2375028541..7dd53564cc 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -60,9 +60,9 @@ let cache_inductive ((sp, kn), names) =
 let discharge_inductive ((sp, kn), names) =
   Some names
 
-let inInductive : inductive_obj -> Libobject.obj =
+let objInductive : inductive_obj Libobject.Dyn.tag =
   let open Libobject in
-  declare_object {(default_object "INDUCTIVE") with
+  declare_object_full {(default_object "INDUCTIVE") with
     cache_function = cache_inductive;
     load_function = load_inductive;
     open_function = open_inductive;
@@ -71,6 +71,7 @@ let inInductive : inductive_obj -> Libobject.obj =
     discharge_function = discharge_inductive;
   }
 
+let inInductive v = Libobject.Dyn.Easy.inj v objInductive
 
 let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c
 
@@ -212,3 +213,9 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p
   if mie.mind_entry_private == None
   then Indschemes.declare_default_schemes mind;
   mind
+
+module Internal =
+struct
+  type nonrec inductive_obj = inductive_obj
+  let objInductive = objInductive
+end
diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli
index df8895a999..17647d50aa 100644
--- a/vernac/declareInd.mli
+++ b/vernac/declareInd.mli
@@ -21,3 +21,12 @@ val declare_mutual_inductive_with_eliminations
   -> UnivNames.universe_binders
   -> one_inductive_impls list
   -> Names.MutInd.t
+
+(** {6 For legacy support, do not use}  *)
+module Internal :
+sig
+
+type inductive_obj
+val objInductive : inductive_obj Libobject.Dyn.tag
+
+end
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index b999ce9f3f..2cd1cf7c65 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -670,25 +670,35 @@ let gallina_print_syntactic_def env kn =
      Constrextern.without_specific_symbols
        [Notation.SynDefRule kn] (pr_glob_constr_env env) c)
 
-let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
+module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t option end)
+
+let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with
+| f -> f o
+| exception Not_found -> None
+
+(* TODO: this kind of feature should not rely on the Libobject stack. There is
+   no reason that an object in the stack corresponds to a user-facing
+   declaration. It may have been so at the time this was written, but this
+   needs to be done in a more principled way. *)
+let gallina_print_leaf_entry env sigma with_values ((sp, kn),lobj) =
   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") ->
+    let handler =
+      DynHandle.add Declare.Internal.objVariable begin fun _ ->
           (* Outside sections, VARIABLES still exist but only with universes
              constraints *)
           (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None)
-      | (_,"CONSTANT") ->
+      end @@
+      DynHandle.add Declare.Internal.objConstant begin fun _ ->
           Some (print_constant with_values sep (Constant.make1 kn) None)
-      | (_,"INDUCTIVE") ->
+      end @@
+      DynHandle.add DeclareInd.Internal.objInductive begin fun _ ->
           Some (gallina_print_inductive (MutInd.make1 kn) None)
-      | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
-            "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
-      (* To deal with forgotten cases... *)
-      | (_,s) -> None
-    end
+      end @@
+      DynHandle.empty
+    in
+    handle handler o
   | ModuleObject _ ->
     let (mp,l) = KerName.repr kn in
     Some (print_module with_values ~mod_ops:Declaremods.mod_ops (MPdot (mp,l)))
@@ -777,11 +787,18 @@ let print_full_context env sigma =
 let print_full_context_typ env sigma =
   print_context env sigma false None (Lib.contents ())
 
+module DynHandleF = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t end)
+
+let handleF h (Libobject.Dyn.Dyn (tag, o)) = match DynHandleF.find tag h with
+| f -> f o
+| exception Not_found -> mt ()
+
+(* TODO: see the comment for {!gallina_print_leaf_entry} *)
 let print_full_pure_context env sigma =
   let rec prec = function
   | ((_,kn),Lib.Leaf AtomicObject lobj)::rest ->
-      let pp = match object_tag lobj with
-      | "CONSTANT" ->
+    let handler =
+      DynHandleF.add Declare.Internal.objConstant begin fun _ ->
           let con = Global.constant_of_delta_kn kn in
           let cb = Global.lookup_constant con in
           let typ = cb.const_type in
@@ -804,12 +821,16 @@ let print_full_pure_context env sigma =
                  str "Primitive " ++
                    print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ)
           ++ str "." ++ fnl () ++ fnl ()
-      | "INDUCTIVE" ->
+      end @@
+      DynHandleF.add DeclareInd.Internal.objInductive begin fun _ ->
           let mind = Global.mind_of_delta_kn kn in
           let mib = Global.lookup_mind mind in
           pr_mutual_inductive_body (Global.env()) mind mib None ++
             str "." ++ fnl () ++ fnl ()
-      | _ -> mt () in
+      end @@
+      DynHandleF.empty
+    in
+    let pp = handleF handler lobj in
       prec rest ++ pp
   | ((_,kn),Lib.Leaf ModuleObject _)::rest ->
           (* TODO: make it reparsable *)
diff --git a/vernac/search.ml b/vernac/search.ml
index 364dae7152..b8825c3b29 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -71,6 +71,14 @@ let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) =
   let pfctxt = named_context e in
   iter_named_context_name_type iter_hyp pfctxt
 
+(* FIXME: this is a Libobject hack that should be replaced with a proper
+   registration mechanism. *)
+module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> unit end)
+
+let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with
+| f -> f o
+| exception Not_found -> ()
+
 (* General search over declarations *)
 let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
   let env = Global.env () in
@@ -78,13 +86,14 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
     (Environ.named_context env);
   let iter_obj (sp, kn) lobj = match lobj with
     | AtomicObject o ->
-      begin match object_tag o with
-        | "CONSTANT" ->
+      let handler =
+        DynHandle.add Declare.Internal.objConstant begin fun _ ->
           let cst = Global.constant_of_delta_kn kn in
           let gr = GlobRef.ConstRef cst in
           let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
           fn gr env typ
-        | "INDUCTIVE" ->
+        end @@
+        DynHandle.add DeclareInd.Internal.objInductive begin fun _ ->
           let mind = Global.mind_of_delta_kn kn in
           let mib = Global.lookup_mind mind in
           let iter_packet i mip =
@@ -97,8 +106,10 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
             iter_constructors ind u fn env len
           in
           Array.iteri iter_packet mib.mind_packets
-        | _ -> ()
-      end
+        end @@
+        DynHandle.empty
+      in
+      handle handler o
     | _ -> ()
   in
   try Declaremods.iter_all_segments iter_obj
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 7b4924eaed..6e398d87ca 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -19,11 +19,9 @@ DeclareObl
 Canonical
 RecLemmas
 Library
-Prettyp
 Lemmas
 ComCoercion
 Auto_ind_decl
-Search
 Indschemes
 Obligations
 ComDefinition
@@ -31,6 +29,8 @@ Classes
 ComPrimitive
 ComAssumption
 DeclareInd
+Search
+Prettyp
 ComInductive
 ComFixpoint
 ComProgramFixpoint