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
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(* $Id$ *)
(* 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 multi_dump () = !glob_output = MultFiles
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 previous_state = ref MultFiles
let pause () = previous_state := !glob_output; glob_output := NoGlob
let continue () = glob_output := !previous_state
let token_number = ref 0
let last_pos = ref 0
type coqdoc_state = Lexer.location_table * int * int
let coqdoc_freeze () =
let lt = Lexer.location_table() in
let state = (lt,!token_number,!last_pos) in
token_number := 0;
last_pos := 0;
state
let coqdoc_unfreeze (lt,tn,lp) =
Lexer.restore_location_table lt;
token_number := tn;
last_pos := lp
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.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
else
(* Theorem/Lemma outside its outer section of definition *)
dir
let dump_ref loc filepath modpath ident ty =
dump_string (Printf.sprintf "R%d %s %s %s %s\n"
(fst (Util.unloc loc)) 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 <> Util.dummy_loc then
let sp = Nametab.sp_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 <> Util.dummy_loc then
let sp = Nametab.sp_of_syntactic_definition kn in
let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
add_glob_gen loc sp lib_dp "syndef"
let add_local loc id = ()
(* let mod_dp,id = repr_path sp in *)
(* let mod_dp = remove_sections mod_dp in *)
(* let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *)
(* let filepath = string_of_dirpath lib_dp in *)
(* let modpath = string_of_dirpath mod_dp_trunc in *)
(* let ident = string_of_id id in *)
(* dump_string (Printf.sprintf "R%d %s %s %s %s\n" *)
(* (fst (unloc loc)) filepath modpath ident ty) *)
let dump_binding loc id = ()
let dump_definition (loc, id) sec s =
dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc))
(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
let dump_reference loc modpath ident ty =
dump_string (Printf.sprintf "R%d %s %s %s %s\n"
(fst (Util.unloc loc)) (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_name (loc, n) sec ty =
match n with
| Names.Name id -> dump_definition (loc, id) sec ty
| Names.Anonymous -> ()
let dump_local_binder b sec ty =
if dump () then
match b with
| Topconstr.LocalRawAssum (nl, _, _) ->
List.iter (fun x -> dump_name x sec ty) nl
| Topconstr.LocalRawDef _ -> ()
let dump_modref loc mp ty =
if dump () then
let (dp, l) = Lib.split_modpath mp in
let fp = Names.string_of_dirpath dp in
let mp = Names.string_of_dirpath (Names.make_dirpath (Util.list_drop_last l)) in
dump_string (Printf.sprintf "R%d %s %s %s %s\n"
(fst (Util.unloc loc)) fp mp "<>" ty)
let dump_moddef loc mp ty =
if dump () then
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 %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
let dump_libref loc dp ty =
dump_string (Printf.sprintf "R%d %s <> <> %s\n"
(fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
let dump_notation_location pos ((path,df),sc) =
if dump () then
let rec next growing =
let loc = Lexer.location_function !token_number in
let (bp,_) = Util.unloc loc in
if growing then if bp >= pos then loc else (incr token_number; next true)
else if bp = pos then loc
else if bp > pos then (decr token_number;next false)
else (incr token_number;next true) in
let loc = next (pos >= !last_pos) in
last_pos := pos;
let path = Names.string_of_dirpath path in
let _sc = match sc with Some sc -> " "^sc | _ -> "" in
dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df)
|
