package coq

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

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

type 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

type object_name = Libnames.full_path * Names.KerName.t
type open_filter
type ('a, 'b) object_declaration = {
  1. object_name : string;
  2. cache_function : 'b -> unit;
  3. load_function : int -> 'b -> unit;
  4. open_function : open_filter -> int -> 'b -> unit;
  5. classify_function : 'a -> substitutivity;
  6. subst_function : (Mod_subst.substitution * 'a) -> 'a;
  7. discharge_function : 'a -> 'a option;
  8. rebuild_function : 'a -> 'a;
}
val unfiltered : open_filter
val make_filter : finite:bool -> string CAst.t list -> open_filter

Anomaly when the list is empty.

type category
val create_category : string -> category

Anomaly if called more than once for a given string.

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

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

val filter_and : open_filter -> open_filter -> open_filter option

Returns None when the intersection is empty.

val 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

val default_object : string -> ('a, 'b) object_declaration
val 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
type obj = Dyn.t
type algebraic_objects =
  1. | Objs of t list
  2. | Ref of Names.ModPath.t * Mod_subst.substitution
and 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
and 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.
val declare_object : ('a, 'a) object_declaration -> 'a -> obj
val declare_object_full : ('a, Nametab.object_prefix * 'a) object_declaration -> 'a Dyn.tag
val declare_named_object_full : ('a, object_name * 'a) object_declaration -> (Names.Id.t * 'a) Dyn.tag
val declare_named_object : ('a, object_name * 'a) object_declaration -> Names.Id.t -> 'a -> obj
val declare_named_object_gen : ('a, Nametab.object_prefix * 'a) object_declaration -> 'a -> obj
val cache_object : (Nametab.object_prefix * obj) -> unit
val load_object : int -> (Nametab.object_prefix * obj) -> unit
val open_object : open_filter -> int -> (Nametab.object_prefix * obj) -> unit
val subst_object : (Mod_subst.substitution * obj) -> obj
val classify_object : obj -> substitutivity
val discharge_object : 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:('a -> unit) -> discharge:('a -> 'a option) -> ('a, 'a) object_declaration
val local_object_nodischarge : string -> cache:('a -> unit) -> ('a, 'a) object_declaration
val global_object : ?cat:category -> string -> cache:('a -> unit) -> subst:((Mod_subst.substitution * 'a) -> 'a) option -> discharge:('a -> 'a option) -> ('a, 'a) object_declaration
val global_object_nodischarge : ?cat:category -> string -> cache:('a -> unit) -> subst:((Mod_subst.substitution * 'a) -> 'a) option -> ('a, 'a) object_declaration
val superglobal_object : string -> cache:('a -> unit) -> subst:((Mod_subst.substitution * 'a) -> 'a) option -> discharge:('a -> 'a option) -> ('a, 'a) object_declaration
val superglobal_object_nodischarge : string -> cache:('a -> unit) -> subst:((Mod_subst.substitution * 'a) -> 'a) option -> ('a, 'a) object_declaration
Debug
val dump : unit -> (int * string) list