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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(*i*)
open Names
open Libnames
open Mod_subst
(*i*)
(* [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 sufixes.
* 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 sufixes no shorter then 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 sufix of the length the "int" argument
* a classification function, specyfying 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
Substitue - 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 which have to be explicitely
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 obove)
* an export function, to enable optional writing of its contents
to disk (.vo). This function is also the oportunity to remove
redundant information in order to keep .vo size small
The export function is a little obsolete and will be removed
in the near future...
*)
type 'a substitutivity =
Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
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 : object_name * 'a -> 'a substitutivity;
subst_function : object_name * substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
export_function : 'a -> 'a option }
(* 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 : object_name * substitution * 'a -> 'a
(*s Given an object declaration, the function [declare_object]
will hand back two functions, the "injection" and "projection"
functions for dynamically typed library-objects. *)
type obj
val declare_object :
'a object_declaration -> ('a -> obj) * (obj -> 'a)
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 : object_name * substitution * obj -> obj
val classify_object : object_name * obj -> obj substitutivity
val export_object : obj -> obj option
val discharge_object : object_name * obj -> obj option
val relax : bool -> unit
|
