Merge PR #8096: Higher-level libobject API for objects with fixed scopes

14 files changed, 172 insertions, 128 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index c0f15f02a5..e7d4b605c7 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -52,6 +52,26 @@ Macros:
   where `atts : Vernacexpr.vernac_flags` was bound in the expression
   and had to be manually parsed.
 
+Libobject
+
+- A Higher-level API for objects with fixed scope was introduced. It supports the following kinds of objects:
+
+  * Local objects, meaning that objects cannot be imported from outside.
+  * Global objects, meaning that they can be imported (by importing the module that contains the object).
+  * Superglobal objects, meaning that objects survive to closing a module, and
+    are imported when the file which contains them is Required (even without
+    Import).
+  * Objects that survive section closing or don't (see `nodischarge` variants,
+    however we discourage defining such objects)
+
+  This API is made of the following functions:
+  * `Libobject.local_object`
+  * `Libobject.local_object_nodischarge`
+  * `Libobject.global_object`
+  * `Libobject.global_object_nodischarge`
+  * `Libobject.superglobal_object`
+  * `Libobject.superglobal_object_nodischarge`
+
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
diff --git a/interp/declare.ml b/interp/declare.ml
index a0ebc3775e..6778fa1e7a 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -445,11 +445,9 @@ let assumption_message id =
 (** Monomorphic universes need to survive sections. *)
 
 let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
-  declare_object
-    { (default_object "Monomorphic section universes") with
-      cache_function = (fun (na, uctx) -> Global.push_context_set false uctx);
-      discharge_function = (fun (_, x) -> Some x);
-      classify_function = (fun a -> Dispose) }
+  declare_object @@ local_object "Monomorphic section universes"
+    ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
+    ~discharge:(fun (_, x) -> Some x)
 
 let declare_universe_context poly ctx =
   if poly then
diff --git a/library/keys.ml b/library/keys.ml
index 53447a679a..58883ccc88 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -100,18 +100,13 @@ let discharge_keys (_,(k,k')) =
   | Some x, Some y -> Some (x, y)
   | _ -> None
 
-let rebuild_keys (ref,ref') = (ref, ref')
-
 type key_obj = key * key
 
 let inKeys : key_obj -> obj =
-  declare_object {(default_object "KEYS") with
-    cache_function = cache_keys;
-    load_function = load_keys;
-    subst_function = subst_keys;
-    classify_function = (fun x -> Substitute x);
-    discharge_function = discharge_keys;
-    rebuild_function = rebuild_keys }
+  declare_object @@ superglobal_object "KEYS"
+    ~cache:cache_keys
+    ~subst:(Some subst_keys)
+    ~discharge:discharge_keys
 
 let declare_equiv_keys ref ref' =
   Lib.add_anonymous_leaf (inKeys (ref,ref'))
diff --git a/library/libobject.ml b/library/libobject.ml
index c153e9a09a..3d17b4a605 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -129,3 +129,46 @@ let rebuild_object lobj =
   apply_dyn_fun (fun d -> d.dyn_rebuild_function lobj) lobj
 
 let dump = Dyn.dump
+
+let local_object_nodischarge s ~cache =
+  { (default_object s) with
+    cache_function = cache;
+    classify_function = (fun _ -> Dispose);
+  }
+
+let local_object s ~cache ~discharge =
+  { (local_object_nodischarge s ~cache) with
+    discharge_function = discharge }
+
+let global_object_nodischarge s ~cache ~subst =
+  let import i o = if Int.equal i 1 then cache o in
+  { (default_object s) with
+    cache_function = cache;
+    open_function = import;
+    subst_function = (match subst with
+        | None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")
+        | Some subst -> subst;
+      );
+    classify_function =
+      if Option.has_some subst then (fun o -> Substitute o) else (fun o -> Keep o);
+  }
+
+let global_object s ~cache ~subst ~discharge =
+  { (global_object_nodischarge s ~cache ~subst) with
+    discharge_function = discharge }
+
+let superglobal_object_nodischarge s ~cache ~subst =
+  { (default_object s) with
+    load_function = (fun _ x -> cache x);
+    cache_function = cache;
+    subst_function = (match subst with
+        | None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")
+        | Some subst -> subst;
+      );
+    classify_function =
+      if Option.has_some subst then (fun o -> Substitute o) else (fun o -> Keep o);
+  }
+
+let superglobal_object s ~cache ~subst ~discharge =
+  { (superglobal_object_nodischarge s ~cache ~subst) with
+    discharge_function = discharge }
diff --git a/library/libobject.mli b/library/libobject.mli
index 32ffc5b79e..00515bd273 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -119,6 +119,51 @@ val classify_object : obj -> obj substitutivity
 val discharge_object : object_name * obj -> obj option
 val rebuild_object : obj -> obj
 
+(** Higher-level API for objects with fixed scope.
+
+- Local means that the object cannot be imported from outside.
+- Global means that it can be imported (by importing the module that contains the
+object).
+- Superglobal means that the object survives to closing a module, and is imported
+when the file which contains it is Required (even without Import).
+- With the nodischarge variants, the object does not survive section closing.
+  With the normal variants, it does.
+
+We recommend to avoid declaring superglobal objects and using the nodischarge
+variants.
+*)
+
+val local_object : string ->
+  cache:(object_name * 'a -> unit) ->
+  discharge:(object_name * 'a -> 'a option) ->
+  'a object_declaration
+
+val local_object_nodischarge : string ->
+  cache:(object_name * 'a -> unit) ->
+  'a object_declaration
+
+val global_object : string ->
+  cache:(object_name * 'a -> unit) ->
+  subst:(Mod_subst.substitution * 'a -> 'a) option ->
+  discharge:(object_name * 'a -> 'a option) ->
+  'a object_declaration
+
+val global_object_nodischarge : string ->
+  cache:(object_name * 'a -> unit) ->
+  subst:(Mod_subst.substitution * 'a -> 'a) option ->
+  'a object_declaration
+
+val superglobal_object : string ->
+  cache:(object_name * 'a -> unit) ->
+  subst:(Mod_subst.substitution * 'a -> 'a) option ->
+  discharge:(object_name * 'a -> 'a option) ->
+  'a object_declaration
+
+val superglobal_object_nodischarge : string ->
+  cache:(object_name * 'a -> unit) ->
+  subst:(Mod_subst.substitution * 'a -> 'a) option ->
+  'a object_declaration
+
 (** {6 Debug} *)
 
 val dump : unit -> (int * string) list
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 16890ea260..2058837b8e 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -621,10 +621,9 @@ let lang_ref = Summary.ref Ocaml ~name:"ExtrLang"
 let lang () = !lang_ref
 
 let extr_lang : lang -> obj =
-  declare_object
-    {(default_object "Extraction Lang") with
-       cache_function = (fun (_,l) -> lang_ref := l);
-       load_function = (fun _ (_,l) -> lang_ref := l)}
+  declare_object @@ superglobal_object_nodischarge "Extraction Lang"
+    ~cache:(fun (_,l) -> lang_ref := l)
+    ~subst:None
 
 let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
@@ -648,15 +647,10 @@ let add_inline_entries b l =
 (* Registration of operations for rollback. *)
 
 let inline_extraction : bool * GlobRef.t list -> obj =
-  declare_object
-    {(default_object "Extraction Inline") with
-       cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
-       load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
-       classify_function = (fun o -> Substitute o);
-       discharge_function = (fun (_,x) -> Some x);
-       subst_function =
-        (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
-    }
+  declare_object @@ superglobal_object "Extraction Inline"
+    ~cache:(fun (_,(b,l)) -> add_inline_entries b l)
+    ~subst:(Some (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))))
+    ~discharge:(fun (_,x) -> Some x)
 
 (* Grammar entries. *)
 
@@ -685,10 +679,9 @@ let print_extraction_inline () =
 (* Reset part *)
 
 let reset_inline : unit -> obj =
-  declare_object
-    {(default_object "Reset Extraction Inline") with
-       cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
-       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table)}
+  declare_object @@ superglobal_object_nodischarge "Reset Extraction Inline"
+    ~cache:(fun (_,_)-> inline_table :=  empty_inline_table)
+    ~subst:None
 
 let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
@@ -731,13 +724,9 @@ let add_implicits r l =
 (* Registration of operations for rollback. *)
 
 let implicit_extraction : GlobRef.t * int_or_id list -> obj =
-  declare_object
-    {(default_object "Extraction Implicit") with
-       cache_function = (fun (_,(r,l)) -> add_implicits r l);
-       load_function = (fun _ (_,(r,l)) -> add_implicits r l);
-       classify_function = (fun o -> Substitute o);
-       subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l))
-    }
+  declare_object @@ superglobal_object_nodischarge "Extraction Implicit"
+    ~cache:(fun (_,(r,l)) -> add_implicits r l)
+    ~subst:(Some (fun (s,(r,l)) -> (fst (subst_global s r), l)))
 
 (* Grammar entries. *)
 
@@ -784,12 +773,9 @@ let add_blacklist_entries l =
 (* Registration of operations for rollback. *)
 
 let blacklist_extraction : string list -> obj =
-  declare_object
-    {(default_object "Extraction Blacklist") with
-       cache_function = (fun (_,l) -> add_blacklist_entries l);
-       load_function = (fun _ (_,l) -> add_blacklist_entries l);
-       subst_function = (fun (_,x) -> x)
-    }
+  declare_object @@ superglobal_object_nodischarge "Extraction Blacklist"
+    ~cache:(fun (_,l) -> add_blacklist_entries l)
+    ~subst:None
 
 (* Grammar entries. *)
 
@@ -805,10 +791,9 @@ let print_extraction_blacklist () =
 (* Reset part *)
 
 let reset_blacklist : unit -> obj =
-  declare_object
-    {(default_object "Reset Extraction Blacklist") with
-       cache_function = (fun (_,_)-> blacklist_table := Id.Set.empty);
-       load_function = (fun _ (_,_)-> blacklist_table := Id.Set.empty)}
+  declare_object @@ superglobal_object_nodischarge "Reset Extraction Blacklist"
+    ~cache:(fun (_,_)-> blacklist_table := Id.Set.empty)
+    ~subst:None
 
 let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 
@@ -852,23 +837,14 @@ let find_custom_match pv =
 (* Registration of operations for rollback. *)
 
 let in_customs : GlobRef.t * string list * string -> obj =
-  declare_object
-    {(default_object "ML extractions") with
-       cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
-       load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
-       classify_function = (fun o -> Substitute o);
-       subst_function =
-        (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
-    }
+  declare_object @@ superglobal_object_nodischarge "ML extractions"
+    ~cache:(fun (_,(r,ids,s)) -> add_custom r ids s)
+    ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)))
 
 let in_custom_matchs : GlobRef.t * string -> obj =
-  declare_object
-    {(default_object "ML extractions custom matchs") with
-       cache_function = (fun (_,(r,s)) -> add_custom_match r s);
-       load_function = (fun _ (_,(r,s)) -> add_custom_match r s);
-       classify_function = (fun o -> Substitute o);
-       subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s))
-    }
+  declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs"
+    ~cache:(fun (_,(r,s)) -> add_custom_match r s)
+    ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s)))
 
 (* Grammar entries. *)
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 19f954c10d..5d0d17ee6b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -237,7 +237,6 @@ let cache_Function (_,finfos) =
   from_graph := Indmap.add finfos.graph_ind finfos !from_graph
 
 
-let load_Function _  = cache_Function
 let subst_Function (subst,finfos) =
   let do_subst_con c = Mod_subst.subst_constant subst c
   and do_subst_ind i = Mod_subst.subst_ind subst i
@@ -271,9 +270,6 @@ let subst_Function (subst,finfos) =
       is_general = finfos.is_general
     }
 
-let classify_Function infos = Libobject.Substitute infos
-
-
 let discharge_Function (_,finfos) = Some finfos
 
 let pr_ocst c =
@@ -302,15 +298,11 @@ let pr_table tb =
   Pp.prlist_with_sep fnl pr_info l
 
 let in_Function : function_info -> Libobject.obj =
-  Libobject.declare_object
-    {(Libobject.default_object "FUNCTIONS_DB") with
-       Libobject.cache_function = cache_Function;
-       Libobject.load_function  = load_Function;
-       Libobject.classify_function  = classify_Function;
-       Libobject.subst_function = subst_Function;
-       Libobject.discharge_function = discharge_Function
-(*        Libobject.open_function = open_Function; *)
-    }
+  let open Libobject in
+  declare_object @@ superglobal_object "FUNCTIONS_DB"
+    ~cache:cache_Function
+    ~subst:(Some subst_Function)
+    ~discharge:discharge_Function
 
 
 let find_or_none id =
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index ec2adf065a..47f593ff3e 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -531,11 +531,9 @@ let cache_transitivity_lemma (_,(left,lem)) =
 let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
 
 let inTransitivity : bool * Constr.t -> obj =
-  declare_object {(default_object "TRANSITIVITY-STEPS") with
-    cache_function = cache_transitivity_lemma;
-    open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o);
-    subst_function = subst_transitivity_lemma;
-    classify_function = (fun o -> Substitute o) }
+  declare_object @@ global_object_nodischarge "TRANSITIVITY-STEPS"
+    ~cache:cache_transitivity_lemma
+    ~subst:(Some subst_transitivity_lemma)
 
 (* Main entry points *)
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9fea3ddcda..65201d922f 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -394,13 +394,9 @@ let subst_th (subst,th) =
 
 let theory_to_obj : ring_info -> obj =
   let cache_th (name,th) = add_entry name th in
-  declare_object
-    {(default_object "tactic-new-ring-theory") with
-      open_function = (fun i o -> if Int.equal i 1 then cache_th o);
-      cache_function = cache_th;
-      subst_function = subst_th;
-      classify_function = (fun x -> Substitute x)}
-
+  declare_object @@ global_object_nodischarge "tactic-new-ring-theory"
+    ~cache:cache_th
+    ~subst:(Some subst_th)
 
 let setoid_of_relation env evd a r =
   try
@@ -891,12 +887,9 @@ let subst_th (subst,th) =
 
 let ftheory_to_obj : field_info -> obj =
   let cache_th (name,th) = add_field_entry name th in
-  declare_object
-    {(default_object "tactic-new-field-theory") with
-      open_function = (fun i o -> if Int.equal i 1 then cache_th o);
-      cache_function = cache_th;
-      subst_function = subst_th;
-      classify_function = (fun x -> Substitute x) }
+  declare_object @@ global_object_nodischarge "tactic-new-field-theory"
+    ~cache:cache_th
+    ~subst:(Some subst_th)
 
 let field_equality evd r inv req =
   match EConstr.kind !evd req with
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 3f974ea063..1aa64d7141 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -45,16 +45,11 @@ module AdaptorDb = struct
     let t' = Detyping.subst_glob_constr subst t in
     if t' == t then a else k, t'
 
-  let classify_adaptor x = Libobject.Substitute x
-
   let in_db =
-    Libobject.declare_object {
-       (Libobject.default_object "VIEW_ADAPTOR_DB")
-    with
-       Libobject.open_function = (fun i o -> if i = 1 then cache_adaptor o);
-       Libobject.cache_function = cache_adaptor;
-       Libobject.subst_function = subst_adaptor;
-       Libobject.classify_function = classify_adaptor }
+    let open Libobject in
+    declare_object @@ global_object_nodischarge "VIEW_ADAPTOR_DB"
+      ~cache:cache_adaptor
+      ~subst:(Some subst_adaptor)
 
   let declare kind terms =
     List.iter (fun term -> Lib.add_anonymous_leaf (in_db (kind,term)))
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f8e8fa9eb9..9c9877fd23 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -69,11 +69,9 @@ let subst_reduction_effect (subst,(con,funkey)) =
   (subst_constant subst con,funkey)
 
 let inReductionEffect : Constant.t * string -> obj =
-  declare_object {(default_object "REDUCTION-EFFECT") with
-    cache_function = cache_reduction_effect;
-    open_function = (fun i o -> if Int.equal i 1 then cache_reduction_effect o);
-    subst_function = subst_reduction_effect;
-    classify_function = (fun o -> Substitute o) }
+  declare_object @@ global_object_nodischarge "REDUCTION-EFFECT"
+    ~cache:cache_reduction_effect
+    ~subst:(Some subst_reduction_effect)
 
 let declare_reduction_effect funkey f =
   if String.Map.mem funkey !effect_table then
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 76cbdee0d5..f824552705 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -196,17 +196,12 @@ let subst_hintrewrite (subst,(rbase,list as node)) =
     if list' == list then node else
       (rbase,list')
 
-let classify_hintrewrite x = Libobject.Substitute x
-
-
 (* Declaration of the Hint Rewrite library object *)
 let inHintRewrite : string * HintDN.t -> Libobject.obj =
-  Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
-    Libobject.cache_function = cache_hintrewrite;
-    Libobject.load_function = (fun _ -> cache_hintrewrite);
-    Libobject.subst_function = subst_hintrewrite;
-    Libobject.classify_function = classify_hintrewrite }
-
+  let open Libobject in
+  declare_object @@ superglobal_object_nodischarge "HINT_REWRITE"
+    ~cache:cache_hintrewrite
+    ~subst:(Some subst_hintrewrite)
 
 open Clenv
 
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index a53e3bf20d..a67f5f6d6e 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -59,12 +59,10 @@ let discharge_scheme (_,(kind,l)) =
   Some (kind, l)
 
 let inScheme : string * (inductive * Constant.t) array -> obj =
-  declare_object {(default_object "SCHEME") with
-                    cache_function = cache_scheme;
-                    load_function = (fun _ -> cache_scheme);
-                    subst_function = subst_scheme;
-		    classify_function = (fun obj -> Substitute obj);
-		    discharge_function = discharge_scheme}
+  declare_object @@ superglobal_object "SCHEME"
+    ~cache:cache_scheme
+    ~subst:(Some subst_scheme)
+    ~discharge:discharge_scheme
 
 (**********************************************************************)
 (* The table of scheme building functions *)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index dccd776fa8..790b62c9d0 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -33,11 +33,9 @@ open Nameops
 let cache_token (_,s) = CLexer.add_keyword s
 
 let inToken : string -> obj =
-  declare_object {(default_object "TOKEN") with
-       open_function = (fun i o -> if Int.equal i 1 then cache_token o);
-       cache_function = cache_token;
-       subst_function = Libobject.ident_subst_function;
-       classify_function = (fun o -> Substitute o)}
+  declare_object @@ global_object_nodischarge "TOKEN"
+    ~cache:cache_token
+    ~subst:(Some Libobject.ident_subst_function)
 
 let add_token_obj s = Lib.add_anonymous_leaf (inToken s)