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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <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 Names
(** {6 Modules } *)
(** Rigid / flexible module signature *)
type 'a module_signature =
| Enforce of 'a (** ... : T *)
| Check of 'a list (** ... <: T1 <: T2, possibly empty *)
(** Which module inline annotations should we honor,
either None or the ones whose level is less or equal
to the given integer *)
type inline =
| NoInline
| DefaultInline
| InlineAt of int
(** Kinds of modules *)
type module_kind = Module | ModType | ModAny
type 'modast module_interpretor =
Environ.env -> module_kind -> 'modast ->
Entries.module_struct_entry * module_kind * Univ.ContextSet.t
type 'modast module_params =
(lident list * ('modast * inline)) list
(** [declare_module interp_modast id fargs typ exprs]
declares module [id], with structure constructed by [interp_modast]
from functor arguments [fargs], with final type [typ].
[exprs] is usually of length 1 (Module definition with a concrete
body), but it could also be empty ("Declare Module", with non-empty [typ]),
or multiple (body of the shape M <+ N <+ ...). *)
val declare_module :
'modast module_interpretor ->
Id.t ->
'modast module_params ->
('modast * inline) module_signature ->
('modast * inline) list -> ModPath.t
val start_module :
'modast module_interpretor ->
bool option -> Id.t ->
'modast module_params ->
('modast * inline) module_signature -> ModPath.t
val end_module : unit -> ModPath.t
(** {6 Module types } *)
(** [declare_modtype interp_modast id fargs typs exprs]
Similar to [declare_module], except that the types could be multiple *)
val declare_modtype :
'modast module_interpretor ->
Id.t ->
'modast module_params ->
('modast * inline) list ->
('modast * inline) list ->
ModPath.t
val start_modtype :
'modast module_interpretor ->
Id.t ->
'modast module_params ->
('modast * inline) list -> ModPath.t
val end_modtype : unit -> ModPath.t
(** {6 Libraries i.e. modules on disk } *)
type library_name = DirPath.t
type library_objects
val register_library :
library_name ->
Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest ->
Univ.ContextSet.t -> unit
val get_library_native_symbols : library_name -> Nativecode.symbols
val start_library : library_name -> unit
val end_library :
?except:Future.UUIDSet.t -> library_name ->
Safe_typing.compiled_library * library_objects * Safe_typing.native_library
(** append a function to be executed at end_library *)
val append_end_library_hook : (unit -> unit) -> unit
(** [really_import_module mp] opens the module [mp] (in a Caml sense).
It modifies Nametab and performs the [open_object] function for
every object of the module. Raises [Not_found] when [mp] is unknown
or when [mp] corresponds to a functor. *)
val really_import_module : ModPath.t -> unit
(** [import_module export mp] is a synchronous version of
[really_import_module]. If [export] is [true], the module is also
opened every time the module containing it is. *)
val import_module : bool -> ModPath.t -> unit
(** Include *)
val declare_include :
'modast module_interpretor -> ('modast * inline) list -> unit
(** {6 ... } *)
(** [iter_all_segments] iterate over all segments, the modules'
segments first and then the current segment. Modules are presented
in an arbitrary order. The given function is applied to all leaves
(together with their section path). *)
val iter_all_segments :
(Libnames.object_name -> Libobject.obj -> unit) -> unit
val debug_print_modtab : unit -> Pp.t
(** For printing modules, [process_module_binding] adds names of
bound module (and its components) to Nametab. It also loads
objects associated to it. It may raise a [Failure] when the
bound module hasn't an atomic type. *)
val process_module_binding :
MBId.t -> Declarations.module_alg_expr -> unit
|
