-
Notifications
You must be signed in to change notification settings - Fork 631
/
checker.ml
417 lines (360 loc) · 15 KB
/
checker.ml
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
(************************************************************************)
(* * 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 Pp
open CErrors
open Util
open System
open Names
open Check
open Environ
let () = at_exit flush_all
let fatal_error info anomaly =
flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]@\n%!" Pp.pp_with info; flush_all ();
exit (if anomaly then 129 else 1)
let coq_root = Id.of_string "Coq"
let parse_dir s =
let len = String.length s in
let rec decoupe_dirs dirs n =
if n>=len then dirs else
let pos =
try
String.index_from s n '.'
with Not_found -> len
in
let dir = String.sub s n (pos-n) in
decoupe_dirs (dir::dirs) (pos+1)
in
decoupe_dirs [] 0
let dirpath_of_string s =
match parse_dir s with
[] -> Check.default_root_prefix
| dir -> DirPath.make (List.map Id.of_string dir)
let path_of_string s =
if Filename.check_suffix s ".vo" then PhysicalFile s
else match parse_dir s with
[] -> invalid_arg "path_of_string"
| l::dir -> LogicalFile {dirpath=dir; basename=l}
let get_version () =
try
let env = Boot.Env.init () in
let revision = Boot.Env.(Path.to_string (revision env)) in
let ch = open_in revision in
let ver = input_line ch in
let rev = input_line ch in
let () = close_in ch in
Printf.sprintf "%s (%s)" ver rev
with _ -> Coq_config.version
let print_header () =
Printf.printf "Welcome to Chicken %s\n%!" (get_version ())
(* Adding files to Coq loadpath *)
let add_path ~unix_path:dir ~coq_root:coq_dirpath =
if exists_dir dir then
begin
Check.add_load_path (dir,coq_dirpath)
end
else
Feedback.msg_warning (str "Cannot open " ++ str dir)
let convert_string d =
try Id.of_string d
with CErrors.UserError _ ->
Flags.if_verbose Feedback.msg_warning
(str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
raise_notrace Exit
let add_rec_path ~unix_path ~coq_root =
if exists_dir unix_path then
let dirs = all_subdirs ~unix_path in
let prefix = DirPath.repr coq_root in
let convert_dirs (lp, cp) =
try
let path = List.rev_map convert_string cp @ prefix in
Some (lp, Names.DirPath.make path)
with Exit -> None
in
let dirs = List.map_filter convert_dirs dirs in
List.iter Check.add_load_path dirs;
Check.add_load_path (unix_path, coq_root)
else
Feedback.msg_warning (str "Cannot open " ++ str unix_path)
(* By the option -R/-Q of the command line *)
let includes = ref []
let push_include (s, alias) = includes := (s,alias) :: !includes
let set_include d p =
let p = dirpath_of_string p in
push_include (d,p)
(* Initializes the LoadPath *)
let init_load_path () =
let coqenv = Boot.Env.init () in
(* the to_string casting won't be necessary once Boot handles
include paths *)
let plugins = Boot.Env.plugins coqenv |> Boot.Path.to_string in
let theories = Boot.Env.stdlib coqenv |> Boot.Path.to_string in
let user_contrib = Boot.Env.user_contrib coqenv |> Boot.Path.to_string in
let xdg_dirs = Envars.xdg_dirs in
let coqpath = Envars.coqpath in
(* NOTE: These directories are searched from last to first *)
(* first standard library *)
add_rec_path ~unix_path:theories ~coq_root:(Names.DirPath.make[coq_root]);
(* then plugins *)
add_rec_path ~unix_path:plugins ~coq_root:(Names.DirPath.make [coq_root]);
(* then user-contrib *)
if Sys.file_exists user_contrib then
add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
(* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix)
(xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)));
(* then directories in COQPATH *)
List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
(* then current directory *)
add_path ~unix_path:"." ~coq_root:Check.default_root_prefix
let impredicative_set = ref false
let set_impredicative_set () = impredicative_set := true
let boot = ref false
let set_boot () = boot := true
let indices_matter = ref false
let enable_vm = ref false
let make_senv () =
let senv = Safe_typing.empty_environment in
let senv = Safe_typing.set_impredicative_set !impredicative_set senv in
let senv = Safe_typing.set_indices_matter !indices_matter senv in
let senv = Safe_typing.set_VM !enable_vm senv in
let senv = Safe_typing.set_allow_sprop true senv in (* be smarter later *)
Safe_typing.set_native_compiler false senv
let admit_list = ref ([] : object_file list)
let add_admit s =
admit_list := path_of_string s :: !admit_list
let norec_list = ref ([] : object_file list)
let add_norec s =
norec_list := path_of_string s :: !norec_list
let compile_list = ref ([] : object_file list)
let add_compile s =
compile_list := path_of_string s :: !compile_list
(*s Parsing of the command line.
We no longer use [Arg.parse], in order to use share [Usage.print_usage]
between coqtop and coqc. *)
let compile_files senv =
Check.recheck_library senv
~norec:(List.rev !norec_list)
~admit:(List.rev !admit_list)
~check:(List.rev !compile_list)
let version () =
Printf.printf "The Coq Proof Checker, version %s\n" Coq_config.version;
exit 0
(* print the usage of coqtop (or coqc) on channel co *)
let print_usage_channel co command =
output_string co command;
output_string co "coqchk options are:\n";
output_string co
"\
\n -Q dir coqdir map physical dir to logical coqdir\
\n -R dir coqdir synonymous for -Q\
\n -coqlib dir set coqchk's standard library location\
\n -boot don't initialize the library paths automatically\
\n\
\n -admit module load module and dependencies without checking\
\n -norec module check module but admit dependencies without checking\
\n\
\n -debug enable debugging info\
\n -where print coqchk's standard library location and exit\
\n -v, --version print coqchk version and exit\
\n -o, --output-context print the list of assumptions\
\n -m, --memory print the maximum heap size\
\n -silent disable trace of constants being checked\
\n\
\n -impredicative-set set sort Set impredicative\
\n -indices-matter levels of indices (and nonuniform parameters)\
\n contribute to the level of inductives\
\n -bytecode-compiler (yes|no) enable the vm_compute reduction machine (default is no)\
\n\
\n -h, --help print this list of options\
\n"
(* print the usage on standard error *)
let print_usage = print_usage_channel stderr
let print_usage_coqtop () =
print_usage "Usage: coqchk <options> modules\n\n"
let usage () =
print_usage_coqtop ();
flush stderr;
exit 1
open Type_errors
let anomaly_string () = str "Anomaly: "
let report () = strbrk (". Please report at " ^ Coq_config.wwwbugtracker ^ ".")
let guill s = str "\"" ++ str s ++ str "\""
let explain_exn = function
| Sys_error msg ->
hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ guill msg ++ report() )
| UserError pps ->
hov 1 (str "User error: " ++ pps)
| Out_of_memory ->
hov 0 (str "Out of memory")
| Stack_overflow ->
hov 0 (str "Stack overflow")
| Match_failure(filename,pos1,pos2) ->
hov 1 (anomaly_string () ++ str "Match failure in file " ++
guill filename ++ str " at line " ++ int pos1 ++
str " character " ++ int pos2 ++ report ())
| Not_found ->
hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
| Failure s ->
hov 0 (str "Failure: " ++ str s ++ report ())
| Invalid_argument s ->
hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ())
| Sys.Break ->
hov 0 (fnl () ++ str "User interrupt.")
| UGraph.UniverseInconsistency i ->
let msg =
if CDebug.(get_flag misc) then
str "." ++ spc() ++
UGraph.explain_universe_inconsistency Sorts.QVar.raw_pr Univ.Level.raw_pr i
else
mt() in
hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
| TypeError(ctx,te) ->
hov 0 (str "Type error: " ++
(match te with
| UnboundRel i -> str"UnboundRel " ++ int i
| UnboundVar v -> str"UnboundVar" ++ str(Names.Id.to_string v)
| NotAType _ -> str"NotAType"
| BadAssumption _ -> str"BadAssumption"
| ReferenceVariables _ -> str"ReferenceVariables"
| ElimArity _ -> str"ElimArity"
| CaseNotInductive _ -> str"CaseNotInductive"
| CaseOnPrivateInd _ -> str"CaseOnPrivateInd"
| WrongCaseInfo _ -> str"WrongCaseInfo"
| NumberBranches _ -> str"NumberBranches"
| IllFormedBranch _ -> str"IllFormedBranch"
| IllFormedCaseParams -> str "IllFormedCaseParams"
| Generalization _ -> str"Generalization"
| ActualType _ -> str"ActualType"
| IncorrectPrimitive _ -> str"IncorrectPrimitive"
| CantApplyBadType ((n,a,b),{uj_val = hd; uj_type = hdty},args) ->
let pp_arg i judge =
hv 1 (str"arg " ++ int (i+1) ++ str"= " ++
Constr.debug_print judge.uj_val ++
str ",type= " ++ Constr.debug_print judge.uj_type) ++ fnl ()
in
Feedback.msg_notice (str"====== ill-typed term ====" ++ fnl () ++
hov 2 (str"application head= " ++ Constr.debug_print hd) ++ fnl () ++
hov 2 (str"head type= " ++ Constr.debug_print hdty) ++ fnl () ++
str"arguments:" ++ fnl () ++ hv 1 (prvecti pp_arg args));
Feedback.msg_notice (str"====== type error ====@" ++ fnl () ++
Constr.debug_print b ++ fnl () ++
str"is not convertible with" ++ fnl () ++
Constr.debug_print a ++ fnl ());
Feedback.msg_notice (str"====== universes ====" ++ fnl () ++
(UGraph.pr_universes Univ.Level.raw_pr
(UGraph.repr (ctx.Environ.env_universes))));
str "CantApplyBadType at argument " ++ int n
| CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
| IllFormedRecBody _ -> str"IllFormedRecBody"
| IllTypedRecBody _ -> str"IllTypedRecBody"
| UnsatisfiedQConstraints _ -> str"UnsatisfiedQConstraints"
| UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
| DisallowedSProp -> str"DisallowedSProp"
| BadBinderRelevance _ -> str"BadBinderRelevance"
| BadCaseRelevance _ -> str"BadCaseRelevance"
| BadInvert -> str"BadInvert"
| UndeclaredQualities _ -> str"UndeclaredQualities"
| UndeclaredUniverse _ -> str"UndeclaredUniverse"
| BadVariance _ -> str "BadVariance"
| UndeclaredUsedVariables _ -> str "UndeclaredUsedVariables"
))
| InductiveError e ->
hov 0 (str "Error related to inductive types")
(* let ctx = Check.get_env() in
hov 0
(str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
| CheckInductive.InductiveMismatch (mind,field) ->
hov 0 (MutInd.print mind ++ str ": field " ++ str field ++ str " is incorrect.")
| Mod_checking.BadConstant (cst, why) ->
hov 0 (Constant.print cst ++ spc() ++ why)
| Assert_failure (s,b,e) ->
hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
(if s = "" then mt ()
else
(str "(file \"" ++ str s ++ str "\", line " ++ int b ++
str ", characters " ++ int e ++ str "-" ++
int (e+6) ++ str ")")) ++
report ())
| e -> CErrors.print e (* for anomalies and other uncaught exceptions *)
let parse_args argv =
let rec parse = function
| [] -> ()
| "-impredicative-set" :: rem ->
set_impredicative_set (); parse rem
| "-indices-matter" :: rem ->
indices_matter:=true; parse rem
| "-bytecode-compiler" :: "yes" :: rem ->
enable_vm := true; parse rem
| "-bytecode-compiler" :: "no" :: rem ->
enable_vm := false; parse rem
| "-coqlib" :: s :: rem ->
if not (exists_dir s) then
fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
Boot.Env.set_coqlib s;
parse rem
| "-boot" :: rem ->
set_boot ();
parse rem
| ("-Q"|"-R") :: d :: p :: rem -> set_include d p;parse rem
| ("-Q"|"-R") :: ([] | [_]) -> usage ()
| "-debug" :: rem -> CDebug.set_debug_all true; parse rem
| "-where" :: _ ->
let env = Boot.Env.init () in
let coqlib = Boot.Env.coqlib env |> Boot.Path.to_string in
print_endline coqlib;
exit 0
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
| ("-v"|"--version") :: _ -> version ()
| ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem
| ("-o" | "--output-context") :: rem ->
Check_stat.output_context := true; parse rem
| "-admit" :: s :: rem -> add_admit s; parse rem
| "-admit" :: [] -> usage ()
| "-norec" :: s :: rem -> add_norec s; parse rem
| "-norec" :: [] -> usage ()
| "-silent" :: rem ->
Flags.quiet := true; parse rem
| s :: _ when s<>"" && s.[0]='-' ->
fatal_error (str "Unknown option " ++ str s) false
| s :: rem -> add_compile s; parse rem
in
parse (List.tl (Array.to_list argv))
(* XXX: At some point we need to either port the checker to use the
feedback system or to remove its use completely. *)
let init_with_argv argv =
Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
try
parse_args argv;
CWarnings.set_flags ("+"^Typeops.warn_bad_relevance_name);
if CDebug.(get_flag misc) then Printexc.record_backtrace true;
Flags.if_verbose print_header ();
if not !boot then init_load_path ();
(* additional loadpath, given with -R/-Q options *)
List.iter
(fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root)
(List.rev !includes);
includes := [];
make_senv ()
with e ->
fatal_error (str "Error during initialization :" ++ (explain_exn e)) (is_anomaly e)
let init() = init_with_argv Sys.argv
let run senv =
try
let senv = compile_files senv in
flush_all(); senv
with e ->
if CDebug.(get_flag misc) then Printexc.print_backtrace stderr;
fatal_error (explain_exn e) (is_anomaly e)
let start () =
let senv = init() in
let senv, opac = run senv in
Check_stat.stats (Safe_typing.env_of_safe_env senv) opac;
exit 0