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

Reviewed-by: maximedenes

5 files changed, 72 insertions, 24 deletions

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