Module `Libobject`Source

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 'a substitutivity =

| Dispose
| Substitute of 'a
| Keep of 'a
| Anticipate of 'a

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

Sourcetype object_name = Libnames.full_path * Names.KerName.t

Sourcetype open_filter

Sourcetype 'a object_declaration = {

object_name : string;
cache_function : (object_name * 'a) -> unit;
load_function : int -> (object_name * 'a) -> unit;
open_function : open_filter -> int -> (object_name * 'a) -> unit;
classify_function : 'a -> 'a substitutivity;
subst_function : (Mod_subst.substitution * 'a) -> 'a;
discharge_function : (object_name * 'a) -> 'a option;
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.

Source

val simple_open : 
  ?cat:category ->
  (int -> (object_name * 'a) -> unit) ->
  open_filter ->
  int ->
  (object_name * '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_and : open_filter -> open_filter -> open_filter option

Returns None when the intersection is empty.

Sourceval filter_or : open_filter -> open_filter -> open_filter

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 : string -> 'a 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.

Sourcemodule Dyn : Dyn.S

Sourcetype obj = Dyn.t

Sourcetype algebraic_objects =

| Objs of objects
| Ref of Names.ModPath.t * Mod_subst.substitution

Sourceand t =

| ModuleObject of substitutive_objects
| ModuleTypeObject of substitutive_objects
| IncludeObject of algebraic_objects
| KeepObject of objects
| ExportObject of {
1. mpl : (open_filter * Names.ModPath.t) list;
}
| AtomicObject of obj

Sourceand objects = (Names.Id.t * t) list

Sourceand substitutive_objects = Names.MBId.t list * algebraic_objects

Sourceval declare_object_full : 'a object_declaration -> 'a Dyn.tag

Sourceval declare_object : 'a object_declaration -> 'a -> obj

Sourceval cache_object : (object_name * obj) -> unit

Sourceval load_object : int -> (object_name * obj) -> unit

Sourceval open_object : open_filter -> int -> (object_name * obj) -> unit

Sourceval subst_object : (Mod_subst.substitution * obj) -> obj

Sourceval classify_object : obj -> obj substitutivity

Sourceval discharge_object : (object_name * obj) -> obj option

Sourceval 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.

Source

val local_object : 
  string ->
  cache:((object_name * 'a) -> unit) ->
  discharge:((object_name * 'a) -> 'a option) ->
  'a object_declaration

Source

val local_object_nodischarge : 
  string ->
  cache:((object_name * 'a) -> unit) ->
  'a object_declaration

Source

val global_object : 
  ?cat:category ->
  string ->
  cache:((object_name * 'a) -> unit) ->
  subst:((Mod_subst.substitution * 'a) -> 'a) option ->
  discharge:((object_name * 'a) -> 'a option) ->
  'a object_declaration

Source

val global_object_nodischarge : 
  ?cat:category ->
  string ->
  cache:((object_name * 'a) -> unit) ->
  subst:((Mod_subst.substitution * 'a) -> 'a) option ->
  'a object_declaration

Source

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

Source

val superglobal_object_nodischarge : 
  string ->
  cache:((object_name * 'a) -> unit) ->
  subst:((Mod_subst.substitution * 'a) -> 'a) option ->
  'a object_declaration

Debug

Sourceval dump : unit -> (int * string) list

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Libobject/index.html

Module `Libobject`Source

...

Debug

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Libobject/index.html

Module LibobjectSource

...

Debug

Module `Libobject`Source