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
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
|
open Util;;
open System;;
open Ctast;;
open Pp;;
open Library;;
open Ascent;;
open Vtp;;
open Xlate;;
open Line_parser;;
open Pcoq;;
type parsed_tree =
| P_cl of ct_COMMAND_LIST
| P_c of ct_COMMAND
| P_t of ct_TACTIC_COM
| P_f of ct_FORMULA
| P_id of ct_ID
| P_s of ct_STRING
| P_i of ct_INT;;
let print_parse_results n msg =
print_string "message\nparsed\n";
print_int n;
print_string "\n";
(match msg with
| P_cl x -> fCOMMAND_LIST x
| P_c x -> fCOMMAND x
| P_t x -> fTACTIC_COM x
| P_f x -> fFORMULA x
| P_id x -> fID x
| P_s x -> fSTRING x
| P_i x -> fINT x);
print_string "e\nblabla\n";
flush stdout;;
let ctf_SyntaxErrorMessage reqid pps =
fnl () ++ str "message" ++ fnl () ++ str "syntax_error" ++ fnl () ++
int reqid ++ fnl () ++
pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
let ctf_SyntaxWarningMessage reqid pps =
fnl () ++ str "message" ++ fnl () ++ str "syntax_warning" ++ fnl () ++
int reqid ++ fnl () ++ pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl();;
let ctf_FileErrorMessage reqid pps =
fnl () ++ str "message" ++ fnl () ++ str "file_error" ++ fnl () ++
int reqid ++ fnl () ++ pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++
fnl ();;
(*In the code for CoqV6.2, the require_module call is encapsulated in
a function "without_mes_ambig". Here I have supposed that this
function has no effect on parsing *)
let try_require_module import specif name fname =
try Library.require_module
(if specif = "UNSPECIFIED" then None
else Some (specif = "SPECIFICATION"))
(Nametab.make_short_qualid (Names.id_of_string name))
fname (import = "IMPORT")
with
| e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");;
let execute_when_necessary ast =
(match ast with
| Node (_, "GRAMMAR", ((Nvar (_, s)) :: ((Node (_, "ASTLIST", al)) :: []))) ->
Metasyntax.add_grammar_obj s (List.map Ctast.ct_to_ast al)
| Node (_, "TOKEN", ((Str (_, s)) :: [])) -> Metasyntax.add_token_obj s
| Node (_, "Require",
((Str (_, import)) ::
((Str (_, specif)) :: ((Nvar (_, mname)) :: [])))) ->
try_require_module import specif mname None
| Node (_, "RequireFrom",
((Str (_, import)) ::
((Str (_, specif)) ::
((Nvar (_, mname)) :: ((Str (_, file_name)) :: []))))) ->
try_require_module import specif mname (Some file_name)
| _ -> ()); ast;;
let parse_to_dot =
let rec dot st = match Stream.next st with
| ("", ".") -> ()
| ("EOI", "") -> raise End_of_file
| _ -> dot st in
Gram.Entry.of_parser "Coqtoplevel.dot" dot;;
let rec discard_to_dot stream =
try Gram.Entry.parse parse_to_dot (Gram.parsable stream) with
| Stdpp.Exc_located(_, Token.Error _) -> discard_to_dot stream;;
let rec decompose_string_aux s n =
try let index = String.index_from s n '\n' in
(Ctast.str (String.sub s n (index - n)))::
(decompose_string_aux s (index + 1))
with Not_found -> [Ctast.str(String.sub s n ((String.length s) - n))];;
let decompose_string s n =
match decompose_string_aux s n with
(Ctast.Str(_,""))::tl -> tl
| a -> a;;
let make_string_list file_chan fst_pos snd_pos =
let len = (snd_pos - fst_pos) in
let s = String.create len in
begin
seek_in file_chan fst_pos;
really_input file_chan s 0 len;
decompose_string s 0;
end;;
let rec get_sub_aux string_list snd_pos =
match string_list with
[] -> []
| s::l ->
let len = String.length s in
if len >= snd_pos then
if snd_pos < 0 then
[]
else
[String.sub s 0 snd_pos]
else
s::(get_sub_aux l (snd_pos - len - 1));;
let rec get_substring_list string_list fst_pos snd_pos =
match string_list with
[] -> []
| s::l ->
let len = String.length s in
if fst_pos > len then
get_substring_list l (fst_pos - len - 1) (snd_pos - len - 1)
else
(* take into account the fact that carriage returns are not in the *)
(* strings. *)
let fst_pos2 = if fst_pos = 0 then 1 else fst_pos in
if snd_pos > len then
String.sub s (fst_pos2 - 1) (len + 1 - fst_pos2)::
(get_sub_aux l (snd_pos - len - 2))
else
let gap = (snd_pos - fst_pos2) in
if gap < 0 then
[]
else
[String.sub s (fst_pos2 - 1) gap];;
(* When parsing a list of commands, we try to recover error messages for
each individual command. *)
let parse_command_list reqid stream string_list =
let rec parse_whole_stream () =
let this_pos = Stream.count stream in
let first_ast =
try option_app
Ctast.ast_to_ct (Gram.Entry.parse
Pcoq.main_entry (Gram.parsable stream))
with
| (Stdpp.Exc_located(l, Stream.Error txt)) as e ->
begin
msgnl (ctf_SyntaxWarningMessage reqid (Errors.explain_exn e));
try
discard_to_dot stream;
msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++
int (Stream.count stream));
Some( Node(l, "PARSING_ERROR",
List.map Ctast.str
(get_substring_list string_list this_pos
(Stream.count stream))))
with End_of_file -> None
end
| e->
begin
discard_to_dot stream;
Some(Node((0,0), "PARSING_ERROR2",
List.map Ctast.str
(get_substring_list string_list this_pos
(Stream.count stream))))
end in
match first_ast with
| Some ast ->
let ast0 = (execute_when_necessary ast) in
(try xlate_vernac ast
with e ->
xlate_vernac
(Node((0,0), "PARSING_ERROR2",
List.map Ctast.str
(get_substring_list string_list this_pos
(Stream.count stream)))))::parse_whole_stream()
| None -> [] in
match parse_whole_stream () with
| first_one::tail -> (P_cl (CT_command_list(first_one, tail)))
| [] -> raise (UserError ("parse_string", (str "empty text.")));;
(*When parsing a string using a phylum, the string is first transformed
into a Coq Ast using the regular Coq parser, then it is transformed into
the right ascent term using xlate functions, then it is transformed into
a stream, using the right vtp function. There is a special case for commands,
since some of these must be executed!*)
let parse_string_action reqid phylum char_stream string_list =
try let msg =
match phylum with
| "COMMAND_LIST" ->
parse_command_list reqid char_stream string_list
| "COMMAND" ->
P_c
(xlate_vernac
(execute_when_necessary
(Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream)))))
| "TACTIC_COM" ->
P_t
(xlate_tactic (Ctast.ast_to_ct(Gram.Entry.parse Pcoq.Tactic.tactic_eoi
(Gram.parsable char_stream))))
| "FORMULA" ->
P_f
(xlate_formula
(Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Constr.constr_eoi (Gram.parsable char_stream))))
| "ID" -> P_id (xlate_id
(Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Prim.ident
(Gram.parsable char_stream))))
| "STRING" ->
P_s
(xlate_string (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Prim.string
(Gram.parsable char_stream))))
| "INT" ->
P_i (xlate_int (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Prim.number
(Gram.parsable char_stream))))
| _ -> error "parse_string_action : bad phylum" in
print_parse_results reqid msg
with
| Stdpp.Exc_located(l,Match_failure(_,_,_)) ->
flush_until_end_of_stream char_stream;
msgnl (ctf_SyntaxErrorMessage reqid
(Errors.explain_exn
(Stdpp.Exc_located(l,Stream.Error "match failure"))))
| e ->
flush_until_end_of_stream char_stream;
msgnl (ctf_SyntaxErrorMessage reqid (Errors.explain_exn e));;
let quiet_parse_string_action char_stream =
try let _ =
Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream) in
()
with
| _ -> flush_until_end_of_stream char_stream; ();;
let parse_file_action reqid file_name =
try let file_chan = open_in file_name in
(* file_chan_err, stream_err are the channel and stream used to
get the text when a syntax error occurs *)
let file_chan_err = open_in file_name in
let stream = Stream.of_channel file_chan in
let stream_err = Stream.of_channel file_chan_err in
let rec discard_to_dot () =
try Gram.Entry.parse parse_to_dot (Gram.parsable stream)
with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot() in
match let rec parse_whole_file () =
let this_pos = Stream.count stream in
match
try
let this_ast =
option_app Ctast.ast_to_ct
(Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)) in
this_ast
with
| Stdpp.Exc_located(l,Stream.Error txt) ->
msgnl (ctf_SyntaxWarningMessage reqid
(str "Error with file" ++ spc () ++
str file_name ++ fnl () ++
Errors.explain_exn
(Stdpp.Exc_located(l,Stream.Error txt))));
(try
begin
discard_to_dot ();
Some( Node(l, "PARSING_ERROR",
(make_string_list file_chan_err this_pos
(Stream.count stream))))
end
with End_of_file -> None)
| e ->
begin
Gram.Entry.parse parse_to_dot (Gram.parsable stream);
Some(Node((0,0), "PARSING_ERROR2",
(make_string_list file_chan this_pos
(Stream.count stream))))
end
with
| Some ast ->
let ast0=(execute_when_necessary ast) in
let term =
(try xlate_vernac ast
with e ->
print_string ("translation error between " ^
(string_of_int this_pos) ^
" " ^
(string_of_int (Stream.count stream)) ^
"\n");
xlate_vernac
(Node((0,0), "PARSING_ERROR2",
(make_string_list file_chan_err this_pos
(Stream.count stream))))) in
term::parse_whole_file ()
| None -> [] in
parse_whole_file () with
| first_one :: tail ->
print_parse_results reqid
(P_cl (CT_command_list (first_one, tail)))
| [] -> raise (UserError ("parse_file_action", str "empty file."))
with
| Stdpp.Exc_located(l,Match_failure(_,_,_)) ->
msgnl
(ctf_SyntaxErrorMessage reqid
(str "Error with file" ++ spc () ++ str file_name ++
fnl () ++
Errors.explain_exn
(Stdpp.Exc_located(l,Stream.Error "match failure"))))
| e ->
msgnl
(ctf_SyntaxErrorMessage reqid
(str "Error with file" ++ spc () ++ str file_name ++
fnl () ++ Errors.explain_exn e));;
(* This function is taken from Mltop.add_path *)
let add_path dir coq_dirpath =
if exists_dir dir then
begin
Library.add_load_path_entry (dir,coq_dirpath)
end
else
msg_warning (str ("Cannot open " ^ dir))
let convert_string d =
try Names.id_of_string d
with _ -> failwith ("could not convert " ^ d)
let add_rec_path dir coq_dirpath =
let dirs = all_subdirs dir in
let prefix = Names.repr_dirpath coq_dirpath in
if dirs <> [] then
let convert_dirs (lp,cp) =
(lp,
Names.make_dirpath ((List.map convert_string (List.rev cp))@prefix)) in
let dirs = map_succeed convert_dirs dirs in
begin
List.iter Library.add_load_path_entry dirs
end
else
msg_warning (str ("Cannot open " ^ dir));;
let add_path_action reqid string_arg =
let directory_name = glob string_arg in
let alias = Filename.basename directory_name in
begin
add_path directory_name (Names.make_dirpath [Names.id_of_string alias])
end;;
let print_version_action () =
msgnl (mt ());
msgnl (str "$Id$");;
let load_syntax_action reqid module_name =
msg (str "loading " ++ str module_name ++ str "... ");
try
(let qid = Nametab.make_short_qualid (Names.id_of_string module_name) in
read_module qid;
msg (str "opening... ");
let fullname = Nametab.locate_loaded_library qid in
import_module fullname;
msgnl (str "done" ++ fnl ());
())
with
| UserError (label, pp_stream) ->
(*This one may be necessary to make sure that the message won't be indented *)
msgnl (mt ());
msgnl
(fnl () ++ str "error while loading syntax module " ++ str module_name ++
str ": " ++ str label ++ fnl () ++ pp_stream)
| e ->
msgnl (mt ());
msgnl
(fnl () ++ str "message" ++ fnl () ++ str "load_error" ++ fnl () ++
int reqid ++ fnl ());
();;
let coqparser_loop inchan =
(parser_loop : (unit -> unit) *
(int -> string -> char Stream.t -> string list -> unit) *
(char Stream.t -> unit) * (int -> string -> unit) *
(int -> string -> unit) * (int -> string -> unit) ->
in_channel -> unit)
(print_version_action, parse_string_action, quiet_parse_string_action, parse_file_action,
add_path_action, load_syntax_action) inchan;;
if !Sys.interactive then ()
else
Libobject.relax true;
(let coqdir =
try Sys.getenv "COQDIR"
with Not_found ->
let coqdir = Coq_config.coqlib in
if Sys.file_exists coqdir then
coqdir
else
(msgnl (str "could not find the value of COQDIR"); exit 1) in
begin
add_rec_path (Filename.concat coqdir "theories")
(Names.make_dirpath [Nameops.coq_root]);
add_path (Filename.concat coqdir "tactics")
(Names.make_dirpath [Nameops.coq_root]);
add_rec_path (Filename.concat coqdir "contrib")
(Names.make_dirpath [Nameops.coq_root]);
List.iter (fun a -> msgnl (str a)) (get_load_path())
end;
(let vernacrc =
try
Sys.getenv "VERNACRC"
with
Not_found ->
List.fold_left
(fun s1 s2 -> (Filename.concat s1 s2))
coqdir [ "contrib"; "interface"; "vernacrc"] in
try
(Gramext.warning_verbose := false;
Esyntax.warning_verbose := false;
coqparser_loop (open_in vernacrc))
with
| End_of_file -> ()
| e ->
(msgnl (Errors.explain_exn e);
msgnl (str "could not load the VERNACRC file"));
try
msgnl (str vernacrc)
with
e -> ());
(try let user_vernacrc =
try Some(Sys.getenv "USERVERNACRC")
with
| Not_found as e ->
msgnl (str "no .vernacrc file"); None in
(match user_vernacrc with
Some f -> coqparser_loop (open_in f)
| None -> ())
with
| End_of_file -> ()
| e ->
msgnl (Errors.explain_exn e);
msgnl (str "error in your .vernacrc file"));
msgnl (str "Starting Centaur Specialized Parser Loop");
try
coqparser_loop stdin
with
| End_of_file -> ()
| e -> msgnl(Errors.explain_exn e))
|