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

3 files changed, 92 insertions, 9 deletions

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