1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Libnames
open Mod_subst
(** [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 '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
*)
type object_name = full_path * Names.KerName.t
type 'a object_declaration = {
object_name : string;
cache_function : object_name * 'a -> unit;
load_function : int -> object_name * 'a -> unit;
open_function : int -> object_name * 'a -> unit;
classify_function : 'a -> 'a substitutivity;
subst_function : substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
rebuild_function : 'a -> 'a }
(** 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 object_declaration
(** the identity substitution function *)
val ident_subst_function : substitution * 'a -> 'a
(** {6 ... } *)
(** Given an object declaration, the function [declare_object_full]
will hand back two functions, the "injection" and "projection"
functions for dynamically typed library-objects. *)
type obj
type algebraic_objects =
| Objs of objects
| Ref of Names.ModPath.t * Mod_subst.substitution
and t =
| ModuleObject of substitutive_objects
| ModuleTypeObject of substitutive_objects
| IncludeObject of algebraic_objects
| KeepObject of objects
| ExportObject of { mp : Names.ModPath.t }
| AtomicObject of obj
and objects = (Names.Id.t * t) list
and substitutive_objects = Names.MBId.t list * algebraic_objects
val declare_object_full :
'a object_declaration -> ('a -> obj) * (obj -> 'a)
val declare_object :
'a object_declaration -> ('a -> obj)
val object_tag : obj -> string
val cache_object : object_name * obj -> unit
val load_object : int -> object_name * obj -> unit
val open_object : int -> object_name * obj -> unit
val subst_object : substitution * obj -> obj
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
|
