package coq-core

  1. Overview
  2. Docs
On This Page
  1. ...
  2. Debug
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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.

  • declare_object_full and declare_named_object_gen pass the raw prefix which you can manipulate as you wish.
  • declare_named_object_full and declare_named_object provide the convenience of packaging it with the provided Id.t into a object_name.
  • declare_object ignores the prefix for 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.

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

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct