Module LibobjectSource

Libobject declares persistent objects, given with methods:

* a caching function specifying how to add the object in the current scope; If the object wishes to register its visibility in the Nametab, it should do so for all possible suffixes.

* a loading function, specifying what to do when the module containing the object is loaded; If the object wishes to register its visibility in the Nametab, it should do so for all suffixes no shorter than the "int" argument

* an opening function, specifying what to do when the module containing the object is opened (imported); If the object wishes to register its visibility in the Nametab, it should do so for the suffix of the length the "int" argument

* a classification function, specifying what to do with the object, when the current module (containing the object) is ended; The possibilities are: Dispose - the object dies at the end of the module Substitute - meaning the object is substitutive and the module name must be updated Keep - the object is not substitutive, but survives module closing Anticipate - this is for objects that have to be explicitly managed by the end_module function (like Require and Read markers)

The classification function is also an occasion for a cleanup (if this function returns Keep or Substitute of some object, the cache method is never called for it)

* a substitution function, performing the substitution; this function should be declared for substitutive objects only (see above). NB: the substitution might now be delayed instead of happening at module creation, so this function should _not_ depend on the current environment

* a discharge function, that is applied at section closing time to collect the data necessary to rebuild the discharged form of the non volatile objects

* a rebuild function, that is applied after section closing to rebuild the non volatile content of a section from the data collected by the discharge function

Any type defined as a persistent object must be pure (e.g. no references) and marshallable by the OCaml Marshal module (e.g. no closures).

Sourcetype substitutivity =
  1. | Dispose
  2. | Substitute
  3. | Keep
  4. | Anticipate

Both names are passed to objects: a "semantic" kernel_name, which can be substituted and a "syntactic" full_path which can be printed

Sourcetype open_filter
Sourcetype ('a, 'b) object_declaration = {
  1. object_name : string;
  2. object_stage : Summary.Stage.t;
  3. cache_function : 'b -> unit;
  4. load_function : int -> 'b -> unit;
  5. open_function : open_filter -> int -> 'b -> unit;
  6. classify_function : 'a -> substitutivity;
  7. subst_function : (Mod_subst.substitution * 'a) -> 'a;
  8. discharge_function : 'a -> 'a option;
  9. rebuild_function : 'a -> 'a;
}
Sourceval unfiltered : open_filter
Sourceval make_filter : finite:bool -> string CAst.t list -> open_filter

Anomaly when the list is empty.

Sourcetype category
Sourceval create_category : string -> category

Anomaly if called more than once for a given string.

Sourceval in_filter : cat:category option -> open_filter -> bool

On cat:None, returns whether the filter allows opening uncategorized objects.

On cat:(Some category), returns whether the filter allows opening objects in the given category.

Sourceval simple_open : ?cat:category -> ('i -> 'a -> unit) -> open_filter -> 'i -> 'a -> unit

Combinator for making objects with simple category-based open behaviour. When cat:None, can be opened by Unfiltered, but also by Filtered with a negative set.

Sourceval filter_eq : open_filter -> open_filter -> bool
Sourceval filter_and : open_filter -> open_filter -> open_filter option

Returns None when the intersection is empty.

The default object is a "Keep" object with empty methods. Object creators are advised to use the construction {(default_object "MY_OBJECT") with cache_function = ... } and specify only these functions which are not empty/meaningless

Sourceval default_object : ?stage:Summary.Stage.t -> string -> ('a, 'b) object_declaration
Sourceval ident_subst_function : (Mod_subst.substitution * 'a) -> 'a

the identity substitution function

...

Given an object declaration, the function declare_object_full will hand back two functions, the "injection" and "projection" functions for dynamically typed library-objects.

module Dyn : Dyn.S
Sourcetype obj = Dyn.t
Sourcetype algebraic_objects =
  1. | Objs of t list
  2. | Ref of Names.ModPath.t * Mod_subst.substitution
Sourceand t =
  1. | ModuleObject of Names.Id.t * substitutive_objects
  2. | ModuleTypeObject of Names.Id.t * substitutive_objects
  3. | IncludeObject of algebraic_objects
  4. | KeepObject of Names.Id.t * t list
  5. | ExportObject of {
    1. mpl : (open_filter * Names.ModPath.t) list;
    }
  6. | AtomicObject of obj
Sourceand substitutive_objects = Names.MBId.t list * algebraic_objects

Object declaration and names: if you need the current prefix (typically to interact with the nametab), you need to have it passed to you.

Sourceval declare_object : ('a, 'a) object_declaration -> 'a -> obj
Sourceval declare_object_full : ('a, Nametab.object_prefix * 'a) object_declaration -> 'a Dyn.tag
Sourceval declare_named_object_full : ('a, object_name * 'a) object_declaration -> (Names.Id.t * 'a) Dyn.tag
Sourceval declare_named_object : ('a, object_name * 'a) object_declaration -> Names.Id.t -> 'a -> obj
Sourceval declare_named_object_gen : ('a, Nametab.object_prefix * 'a) object_declaration -> 'a -> obj
Sourceval cache_object : (Nametab.object_prefix * obj) -> unit
Sourceval load_object : int -> (Nametab.object_prefix * obj) -> unit
Sourceval open_object : open_filter -> int -> (Nametab.object_prefix * obj) -> unit
Sourceval subst_object : (Mod_subst.substitution * obj) -> obj
Sourceval classify_object : obj -> substitutivity
Sourceval discharge_object : obj -> obj option
Sourceval rebuild_object : obj -> obj
Sourceval object_stage : obj -> Summary.Stage.t

Higher-level API for objects with fixed scope.

We recommend to avoid declaring superglobal objects and using the nodischarge variants.

Sourceval local_object : ?stage:Summary.Stage.t -> string -> cache:('a -> unit) -> discharge:('a -> 'a option) -> ('a, 'a) object_declaration
Sourceval local_object_nodischarge : ?stage:Summary.Stage.t -> string -> cache:('a -> unit) -> ('a, 'a) object_declaration
Sourceval global_object : ?cat:category -> ?stage:Summary.Stage.t -> string -> cache:('a -> unit) -> subst:((Mod_subst.substitution * 'a) -> 'a) option -> discharge:('a -> 'a option) -> ('a, 'a) object_declaration
Sourceval global_object_nodischarge : ?cat:category -> ?stage:Summary.Stage.t -> string -> cache:('a -> unit) -> subst:((Mod_subst.substitution * 'a) -> 'a) option -> ('a, 'a) object_declaration
Sourceval superglobal_object : ?stage:Summary.Stage.t -> string -> cache:('a -> unit) -> subst:((Mod_subst.substitution * 'a) -> 'a) option -> discharge:('a -> 'a option) -> ('a, 'a) object_declaration
Sourceval superglobal_object_nodischarge : ?stage:Summary.Stage.t -> string -> cache:('a -> unit) -> subst:((Mod_subst.substitution * 'a) -> 'a) option -> ('a, 'a) object_declaration
Debug
Sourceval dump : unit -> (int * string) list