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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
(* Parsing of vernacular. *)
open Pp
open Lexer
open Util
open Options
open System
open Coqast
open Vernacexpr
open Vernacinterp
open Ppvernacnew
(* The functions in this module may raise (unexplainable!) exceptions.
Use the module Coqtoplevel, which catches these exceptions
(the exceptions are explained only at the toplevel). *)
exception DuringCommandInterp of Util.loc * exn
(* Like Exc_located, but specifies the outermost file read, the filename
associated to the location of the error, and the error itself. *)
exception Error_in_file of string * (string * Util.loc) * exn
(* Specifies which file is read. The intermediate file names are
discarded here. The Drop exception becomes an error. We forget
if the error ocurred during interpretation or not *)
let raise_with_file file exc =
let (cmdloc,re) =
match exc with
| DuringCommandInterp(loc,e) -> (loc,e)
| e -> (dummy_loc,e)
in
let (inner,inex) =
match re with
| Error_in_file (_, (f,loc), e) when loc <> dummy_loc ->
((f, loc), e)
| Stdpp.Exc_located (loc, e) when loc <> dummy_loc ->
((file, loc), e)
| _ -> ((file,cmdloc), re)
in
raise (Error_in_file (file, inner, disable_drop inex))
let real_error = function
| Stdpp.Exc_located (_, e) -> e
| Error_in_file (_, _, e) -> e
| e -> e
(* Opening and closing a channel. Open it twice when verbose: the first
channel is used to read the commands, and the second one to print them.
Note: we could use only one thanks to seek_in, but seeking on and on in
the file we parse seems a bit risky to me. B.B. *)
let open_file_twice_if verbosely fname =
let _,longfname = find_file_in_path (Library.get_load_path ()) fname in
let in_chan = open_in longfname in
let verb_ch = if verbosely then Some (open_in longfname) else None in
let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
(in_chan, longfname, (po, verb_ch))
let close_input in_chan (_,verb) =
try
close_in in_chan;
match verb with
| Some verb_ch -> close_in verb_ch
| _ -> ()
with _ -> ()
let verbose_phrase verbch loc =
match verbch with
| Some ch ->
let len = snd loc - fst loc in
let s = String.create len in
seek_in ch (fst loc);
really_input ch s 0 len;
message s;
pp_flush()
| _ -> ()
exception End_of_input
let parse_phrase (po, verbch) =
match Pcoq.Gram.Entry.parse Pcoq.main_entry po with
| Some (loc,_ as com) -> verbose_phrase verbch loc; com
| None -> raise End_of_input
(* vernac parses the given stream, executes interpfun on the syntax tree it
* parses, and is verbose on "primitives" commands if verbosely is true *)
let just_parsing = ref false
let chan_translate = ref stdout
let pr_comments = function
| None -> mt()
| Some l -> h 0 (List.fold_left (++) (mt ()) (List.rev l))
let rec vernac_com interpfun (loc,com) =
let rec interp = function
| VernacLoad (verbosely, fname) ->
read_vernac_file verbosely (make_suffix fname ".v")
| VernacList l -> List.iter (fun (_,v) -> interp v) l
| VernacTime v ->
let tstart = System.get_time() in
if not !just_parsing then interpfun v;
let tend = System.get_time() in
msgnl (str"Finished transaction in " ++
System.fmt_time_difference tstart tend)
(* To be interpreted in v7 or translator input only *)
| VernacV7only v -> if !Options.v7 then interp v
(* To be interpreted in translator output only *)
| VernacV8only v -> if true (* !translate *) then interp v
| v -> if not !just_parsing then interpfun v
in
try
if do_translate () then
let _ = Format.set_formatter_out_channel stdout in
let _ = interp com in
let _ = Format.set_formatter_out_channel !chan_translate in
if !translate_file then
msgnl (pr_comments !comments ++ pr_vernac com ++ sep_end)
else
msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++ pr_vernac com ++ sep_end)); comments := None
else interp com
with e ->
Format.set_formatter_out_channel stdout;
raise (DuringCommandInterp (loc, e))
and vernac interpfun input =
vernac_com interpfun (parse_phrase input)
and read_vernac_file verbosely s =
let interpfun =
if verbosely then
Vernacentries.interp
else
Options.silently Vernacentries.interp
in
let (in_chan, fname, input) = open_file_twice_if verbosely s in
try
(* we go out of the following infinite loop when a End_of_input is
* raised, which means that we raised the end of the file being loaded *)
while true do vernac interpfun input; pp_flush () done
with e -> (* whatever the exception *)
Format.set_formatter_out_channel stdout;
close_input in_chan input; (* we must close the file first *)
match real_error e with
| End_of_input -> ()
| _ -> raise_with_file fname e
(* raw_do_vernac : char Stream.t -> unit
* parses and executes one command of the vernacular char stream.
* Marks the end of the command in the lib_stk to make vernac undoing
* easier. *)
let raw_do_vernac po =
vernac (States.with_heavy_rollback Vernacentries.interp) (po,None);
Lib.mark_end_of_command()
(* Load a vernac file. Errors are annotated with file and location *)
let load_vernac verb file =
try
read_vernac_file verb file
with e ->
raise_with_file file e
(* Compile a vernac file (f is assumed without .v suffix) *)
let compile verbosely f =
(*
let s = Filename.basename f in
let m = Names.id_of_string s in
let _,longf = find_file_in_path (Library.get_load_path ()) (f^".v") in
let ldir0 = Library.find_logical_path (Filename.dirname longf) in
let ldir = Libnames.extend_dirpath ldir0 m in
Termops.set_module ldir; (* Just for universe naming *)
Lib.start_module ldir;
if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
let _ = load_vernac verbosely longf in
let mid = Lib.end_module m in
assert (mid = ldir);
Library.save_module_to ldir (longf^"o")
*)
let ldir,long_f_dot_v = Library.start_library f in
if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
chan_translate := if Options.do_translate () then open_out (f^".v8") else stdout;
let _ = Format.set_formatter_out_channel !chan_translate in
let _ = load_vernac verbosely long_f_dot_v in
let _ = close_out !chan_translate in
if Pfedit.get_all_proof_names () <> [] then
(message "Error: There are pending proofs"; exit 1);
Library.save_library_to ldir (long_f_dot_v ^ "o")
|
