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
186
187
188
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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
(** Lib: record of operations, backtrack, low-level sections *)
(** This module provides a general mechanism to keep a trace of all operations
and to backtrack (undo) those operations. It provides also the section
mechanism (at a low level; discharge is not known at this step). *)
type is_type = bool (* Module Type or just Module *)
type export_flag = Export | Import
type export = (export_flag * Libobject.open_filter) option (* None for a Module Type *)
val make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name
val make_foname : Names.Id.t -> Libobject.object_name
val oname_prefix : Libobject.object_name -> Nametab.object_prefix
type 'summary node =
| CompilingLibrary of Nametab.object_prefix
| OpenedModule of is_type * export * Nametab.object_prefix * 'summary
| OpenedSection of Nametab.object_prefix * 'summary
(** Extract the [object_prefix] component. Note that it is the prefix
of the objects *inside* this node, eg in [Module M.] we have
[OpenedModule] with prefix containing [M]. *)
val node_prefix : 'summary node -> Nametab.object_prefix
type 'summary library_segment = ('summary node * Libobject.t list) list
(** {6 ... } *)
(** Adding operations (which call the [cache] method, and getting the
current list of operations (most recent ones coming first). *)
val add_leaf : Libobject.obj -> unit
(** {6 ... } *)
(** The function [contents] gives access to the current entire segment *)
val contents : unit -> Summary.Interp.frozen library_segment
(** {6 Functions relative to current path } *)
(** User-side names
[cwd()] is [(prefix()).obj_dir]
[current_mp()] is [(prefix()).obj_mp]
Inside a library A.B module M section S, we have
- library_dp = A.B
- cwd = A.B.M.S
- cwd_except_section = A.B.M
- current_dirpath true = M.S
- current_dirpath false = S
- current_mp = MPdot(MPfile A.B, M)
make_path (resp make_path_except_section) uses cwd (resp cwd_except_section)
make_kn uses current_mp
*)
val prefix : unit -> Nametab.object_prefix
val cwd : unit -> DirPath.t
val cwd_except_section : unit -> DirPath.t
val current_dirpath : bool -> DirPath.t (* false = except sections *)
val make_path : Id.t -> Libnames.full_path
val make_path_except_section : Id.t -> Libnames.full_path
(** Kernel-side names *)
val current_mp : unit -> ModPath.t
val make_kn : Id.t -> KerName.t
(** Are we inside an opened section *)
val sections_are_opened : unit -> bool
val sections_depth : unit -> int
(** Are we inside an opened module type *)
val is_module_or_modtype : unit -> bool
val is_modtype : unit -> bool
(* [is_modtype_strict] checks not only if we are in a module type, but
if the latest module started is a module type. *)
val is_modtype_strict : unit -> bool
val is_module : unit -> bool
(** The [StagedLibS] abstraction describes operations and traversal for Lib at a
given stage. *)
module type StagedLibS = sig
type summary
type classified_objects = {
substobjs : Libobject.t list;
keepobjs : Libobject.t list;
anticipateobjs : Libobject.t list;
}
val classify_segment : Libobject.t list -> classified_objects
(** Returns the opening node of a given name *)
val find_opening_node : Id.t -> summary node
val add_entry : summary node -> unit
val add_leaf_entry : Libobject.t -> unit
(** {6 Sections } *)
val open_section : Id.t -> unit
val close_section : unit -> unit
(** {6 Modules and module types } *)
val start_module :
export -> module_ident -> ModPath.t ->
summary -> Nametab.object_prefix
val start_modtype :
module_ident -> ModPath.t ->
summary -> Nametab.object_prefix
val end_module :
unit ->
Nametab.object_prefix * summary * classified_objects
val end_modtype :
unit ->
Nametab.object_prefix * summary * classified_objects
type frozen
val freeze : unit -> frozen
val unfreeze : frozen -> unit
val init : unit -> unit
(** Keep only the libobject structure, not the objects themselves *)
val drop_objects : frozen -> frozen
val declare_info : Library_info.t -> unit
end
(** We provide two instances of [StagedLibS], corresponding to the Synterp and
Interp stages. *)
module Synterp : StagedLibS with type summary = Summary.Synterp.frozen
module Interp : StagedLibS with type summary = Summary.Interp.frozen
(** {6 Compilation units } *)
val start_compilation : DirPath.t -> ModPath.t -> unit
(** Finalize the compilation of a library and return respectively the library
prefix, the regular objects, and the syntax-related objects. *)
val end_compilation : DirPath.t -> Nametab.object_prefix * Library_info.t * Interp.classified_objects * Synterp.classified_objects
(** The function [library_dp] returns the [DirPath.t] of the current
compiling library (or [default_library]) *)
val library_dp : unit -> DirPath.t
(** Extract the library part of a name even if in a section *)
val split_modpath : ModPath.t -> DirPath.t * Id.t list
val library_part : GlobRef.t -> DirPath.t
(** {6 Section management for discharge } *)
val section_segment_of_constant : Constant.t -> Cooking.cooking_info
val section_segment_of_inductive: MutInd.t -> Cooking.cooking_info
val section_segment_of_reference : GlobRef.t -> Cooking.cooking_info
val section_instance : GlobRef.t -> Constr.t array
val is_in_section : GlobRef.t -> bool
(** {6 Discharge: decrease the section level if in the current section } *)
(** [discharge_proj_repr p] discharges projection [p] if the associated record
was defined in the current section. If that is not the case, it returns [p]
unchanged. *)
val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t
(** Compatibility layer *)
val init : unit -> unit
val open_section : Id.t -> unit
val close_section : unit -> unit
|
