blob: c22ecf83d1d3e956475e7de94a7701c48fd20190 (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Util
open Names
open Entries
open Environ
open Libnames
open Libobject
open Lib
(** This modules provides official functions to declare modules and
module types *)
(** Rigid / flexible signature *)
type 'a module_signature =
| Enforce of 'a (** ... : T *)
| Check of 'a list (** ... <: T1 <: T2, possibly empty *)
(** Should we adapt a few scopes during functor application ? *)
type scope_subst = (string * string) list
val subst_scope : string -> string
(** Which 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
(** The type of annotations for functor applications *)
type funct_app_annot =
{ ann_inline : inline;
ann_scope_subst : scope_subst }
type 'a annotated = ('a * funct_app_annot)
(** {6 Modules } *)
(** [declare_module interp_modtype interp_modexpr id fargs typ expr]
declares module [id], with type constructed by [interp_modtype]
from functor arguments [fargs] and [typ] and with module body
constructed by [interp_modtype] from functor arguments [fargs] and
by [interp_modexpr] from [expr]. At least one of [typ], [expr] must
be non-empty.
The [bool] in [typ] tells if the module must be abstracted [true]
with respect to the module type or merely matched without any
restriction [false].
*)
val declare_module :
(env -> 'modast -> module_struct_entry) ->
(env -> 'modast -> module_struct_entry) ->
(env -> 'modast -> module_struct_entry * bool) ->
identifier ->
(identifier located list * ('modast annotated)) list ->
('modast annotated) module_signature ->
('modast annotated) list -> module_path
val start_module : (env -> 'modast -> module_struct_entry) ->
bool option -> identifier ->
(identifier located list * ('modast annotated)) list ->
('modast annotated) module_signature -> module_path
val end_module : unit -> module_path
(** {6 Module types } *)
val declare_modtype : (env -> 'modast -> module_struct_entry) ->
(env -> 'modast -> module_struct_entry * bool) ->
identifier ->
(identifier located list * ('modast annotated)) list ->
('modast annotated) list ->
('modast annotated) list ->
module_path
val start_modtype : (env -> 'modast -> module_struct_entry) ->
identifier -> (identifier located list * ('modast annotated)) list ->
('modast annotated) list -> module_path
val end_modtype : unit -> module_path
(** {6 ... } *)
(** Objects of a module. They come in two lists: the substitutive ones
and the other *)
val module_objects : module_path -> library_segment
(** {6 Libraries i.e. modules on disk } *)
type library_name = dir_path
type library_objects
val register_library :
library_name ->
Safe_typing.compiled_library -> library_objects -> Digest.t -> unit
val start_library : library_name -> unit
val end_library :
library_name -> Safe_typing.compiled_library * library_objects
(** set a function to be executed at end_library *)
val set_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. *)
val really_import_module : module_path -> 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 -> module_path -> unit
(** Include *)
val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) ->
('struct_expr annotated) 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 : (object_name -> obj -> unit) -> unit
val debug_print_modtab : unit -> Pp.std_ppcmds
(*i val debug_print_modtypetab : unit -> Pp.std_ppcmds i*)
(** For translator *)
val process_module_bindings : module_ident list ->
(mod_bound_id * (module_struct_entry annotated)) list -> unit
(** For Printer *)
val process_module_seb_binding :
mod_bound_id -> Declarations.struct_expr_body -> unit
|
