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
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Dump of globalization (to be used by coqdoc) *)
let glob_file = ref Pervasives.stdout
let open_glob_file f =
glob_file := Pervasives.open_out f
let close_glob_file () =
Pervasives.close_out !glob_file
type glob_output_t =
| NoGlob
| StdOut
| MultFiles
| File of string
let glob_output = ref NoGlob
let dump () = !glob_output != NoGlob
let noglob () = glob_output := NoGlob
let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout
let dump_to_dotglob f = glob_output := MultFiles
let dump_into_file f = glob_output := File f; open_glob_file f
let dump_string s =
if dump () then Pervasives.output_string !glob_file s
let start_dump_glob vfile =
match !glob_output with
| MultFiles ->
open_glob_file (Filename.chop_extension vfile ^ ".glob");
output_string !glob_file "DIGEST ";
output_string !glob_file (Digest.to_hex (Digest.file vfile));
output_char !glob_file '\n'
| File f ->
open_glob_file f;
output_string !glob_file "DIGEST NO\n"
| NoGlob | StdOut ->
()
let end_dump_glob () =
match !glob_output with
| MultFiles | File _ -> close_glob_file ()
| NoGlob | StdOut -> ()
let previous_state = ref MultFiles
let pause () = previous_state := !glob_output; glob_output := NoGlob
let continue () = glob_output := !previous_state
type coqdoc_state = Lexer.location_table
let coqdoc_freeze = Lexer.location_table
let coqdoc_unfreeze = Lexer.restore_location_table
open Decl_kinds
let type_of_logical_kind = function
| IsDefinition def ->
(match def with
| Definition -> "def"
| Coercion -> "coe"
| SubClass -> "subclass"
| CanonicalStructure -> "canonstruc"
| Example -> "ex"
| Fixpoint -> "def"
| CoFixpoint -> "def"
| Scheme -> "scheme"
| StructureComponent -> "proj"
| IdentityCoercion -> "coe"
| Instance -> "inst"
| Method -> "meth")
| IsAssumption a ->
(match a with
| Definitional -> "defax"
| Logical -> "prfax"
| Conjectural -> "prfax")
| IsProof th ->
(match th with
| Theorem
| Lemma
| Fact
| Remark
| Property
| Proposition
| Corollary -> "thm")
let type_of_global_ref gr =
if Typeclasses.is_class gr then
"class"
else
match gr with
| Libnames.ConstRef cst ->
type_of_logical_kind (Decls.constant_kind cst)
| Libnames.VarRef v ->
"var" ^ type_of_logical_kind (Decls.variable_kind v)
| Libnames.IndRef ind ->
let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
if mib.Declarations.mind_record then
if mib.Declarations.mind_finite then "rec"
else "corec"
else if mib.Declarations.mind_finite then "ind"
else "coind"
| Libnames.ConstructRef _ -> "constr"
let remove_sections dir =
if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
(* Not yet (fully) discharged *)
Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
else
(* Theorem/Lemma outside its outer section of definition *)
dir
let interval loc =
let loc1,loc2 = Pp.unloc loc in
loc1, loc2-1
let dump_ref loc filepath modpath ident ty =
let bl,el = interval loc in
dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
bl el filepath modpath ident ty)
let add_glob_gen loc sp lib_dp ty =
if dump () then
let mod_dp,id = Libnames.repr_path sp in
let mod_dp = remove_sections mod_dp in
let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
let filepath = Names.string_of_dirpath lib_dp in
let modpath = Names.string_of_dirpath mod_dp_trunc in
let ident = Names.string_of_id id in
dump_ref loc filepath modpath ident ty
let add_glob loc ref =
if dump () && loc <> Pp.dummy_loc then
let sp = Nametab.path_of_global ref in
let lib_dp = Lib.library_part ref in
let ty = type_of_global_ref ref in
add_glob_gen loc sp lib_dp ty
let mp_of_kn kn =
let mp,sec,l = Names.repr_kn kn in
Names.MPdot (mp,l)
let add_glob_kn loc kn =
if dump () && loc <> Pp.dummy_loc then
let sp = Nametab.path_of_syndef kn in
let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
add_glob_gen loc sp lib_dp "syndef"
let dump_binding loc id = ()
let dump_definition (loc, id) sec s =
let bl,el = interval loc in
dump_string (Printf.sprintf "%s %d:%d %s %s\n" s bl el
(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
let dump_reference loc modpath ident ty =
let bl,el = interval loc in
dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
bl el (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
let dump_constraint ((loc, n), _, _) sec ty =
match n with
| Names.Name id -> dump_definition (loc, id) sec ty
| Names.Anonymous -> ()
let dump_modref loc mp ty =
if dump () then
let (dp, l) = Lib.split_modpath mp in
let l = if l = [] then l else Util.list_drop_last l in
let fp = Names.string_of_dirpath dp in
let mp = Names.string_of_dirpath (Names.make_dirpath l) in
let bl,el = interval loc in
dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
bl el fp mp "<>" ty)
let dump_moddef loc mp ty =
if dump () then
let bl,el = interval loc in
let (dp, l) = Lib.split_modpath mp in
let mp = Names.string_of_dirpath (Names.make_dirpath l) in
dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el "<>" mp)
let dump_libref loc dp ty =
let bl,el = interval loc in
dump_string (Printf.sprintf "R%d:%d %s <> <> %s\n"
bl el (Names.string_of_dirpath dp) ty)
let cook_notation df sc =
(* We encode notations so that they are space-free and still human-readable *)
(* - all spaces are replaced by _ *)
(* - all _ denoting a non-terminal symbol are replaced by x *)
(* - all terminal tokens are surrounded by single quotes, including '_' *)
(* which already denotes terminal _ *)
(* - all single quotes in terminal tokens are doubled *)
(* - characters < 32 are represented by '^A, '^B, '^C, etc *)
(* The output is decoded in function Index.prepare_entry of coqdoc *)
let ntn = String.make (String.length df * 3) '_' in
let j = ref 0 in
let l = String.length df - 1 in
let i = ref 0 in
while !i <= l do
assert (df.[!i] <> ' ');
if df.[!i] = '_' && (!i = l || df.[!i+1] = ' ') then
(* Next token is a non-terminal *)
(ntn.[!j] <- 'x'; incr j; incr i)
else begin
(* Next token is a terminal *)
ntn.[!j] <- '\''; incr j;
while !i <= l && df.[!i] <> ' ' do
if df.[!i] < ' ' then
let c = char_of_int (int_of_char 'A' + int_of_char df.[!i] - 1) in
(String.blit ("'^" ^ String.make 1 c) 0 ntn !j 3; j := !j+3; incr i)
else begin
if df.[!i] = '\'' then (ntn.[!j] <- '\''; incr j);
ntn.[!j] <- df.[!i]; incr j; incr i
end
done;
ntn.[!j] <- '\''; incr j
end;
if !i <= l then (ntn.[!j] <- '_'; incr j; incr i)
done;
let df = String.sub ntn 0 !j in
match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
let dump_notation (loc,(df,_)) sc sec =
(* We dump the location of the opening '"' *)
dump_string (Printf.sprintf "not %d %s %s\n" (fst (Pp.unloc loc))
(Names.string_of_dirpath (Lib.current_dirpath sec)) (cook_notation df sc))
let dump_notation_location posl df (((path,secpath),_),sc) =
if dump () then
let path = Names.string_of_dirpath path in
let secpath = Names.string_of_dirpath secpath in
let df = cook_notation df sc in
List.iter (fun (bl,el) ->
dump_string(Printf.sprintf "R%d:%d %s %s %s not\n" bl el path secpath df))
posl
|
