summaryrefslogtreecommitdiff
path: root/checker/checker.ml
blob: 1c7ace12f0628373f1b169e33659b2ea3dc1e3e7 (plain)
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
(************************************************************************)
(*  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: coqtop.ml 10153 2007-09-28 18:00:45Z glondu $ *)

open Pp
open Util
open System
open Flags
open Names
open Term
open Check

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
      [] -> invalid_arg "dirpath_of_string"
    | dir -> make_dirpath (List.map id_of_string dir)
let path_of_string s =
  match parse_dir s with
      [] -> invalid_arg "dirpath_of_string"
    | l::dir -> {dirpath=dir; basename=l}

let (/) = Filename.concat

let get_version_date () =
  try
    let ch = open_in (Coq_config.coqlib^"/revision") in
    let ver = input_line ch in
    let rev = input_line ch in
      (ver,rev)
  with _ -> (Coq_config.version,Coq_config.date)

let print_header () =
  let (ver,rev) = (get_version_date ()) in
    Printf.printf "Welcome to Chicken %s (%s)\n" ver rev;
    flush stdout

(* 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
    msg_warning (str ("Cannot open " ^ dir))

let convert_string d =
  try id_of_string d
  with _ -> 
    if_verbose warning 
      ("Directory "^d^" cannot be used as a Coq identifier (skipped)");
    flush_all ();
    failwith "caught"

let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath =
  let dirs = all_subdirs dir in
  let prefix = 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 Check.add_load_path dirs
    end
  else
    msg_warning (str ("Cannot open " ^ dir))

(* By the option -include -I or -R of the command line *)
let includes = ref []
let push_include (s, alias) = includes := (s,alias,false) :: !includes
let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes

let check_coq_overwriting p = 
  if string_of_id (list_last (repr_dirpath p)) = "Coq" then
    error "The \"Coq\" logical root directory is reserved for the Coq library"

let set_default_include d =
  push_include (d, Check.default_root_prefix)
let set_default_rec_include d =
  let p = Check.default_root_prefix in
  check_coq_overwriting p; 
  push_rec_include (d, p)

(* Initializes the LoadPath according to COQLIB and Coq_config *)
let init_load_path () =
  let coqlib =
    (* variable COQLIB overrides the default library *)
    getenv_else "COQLIB"
      (if Coq_config.local || !Flags.boot then Coq_config.coqtop
	else Coq_config.coqlib) in
  let user_contrib = coqlib/"user-contrib" in
  let contrib = coqlib/"contrib" in
  (* first user-contrib *)
  if Sys.file_exists user_contrib then 
    add_rec_path user_contrib Check.default_root_prefix;
  (* then contrib *)
  add_rec_path contrib (Names.make_dirpath [coq_root]);
  (* then standard library *)
(*  List.iter 
    (fun (s,alias) ->
      add_rec_path (coqlib/s) ([alias; coq_root])) 
    theories_dirs_map;*)
  add_rec_path (coqlib/"theories") (Names.make_dirpath[coq_root]);
  (* then current directory *)
  add_path "." Check.default_root_prefix;
  (* additional loadpath, given with -I -include -R options *)
  List.iter 
    (fun (s,alias,reci) ->
      if reci then add_rec_path s alias else add_path s alias)
    (List.rev !includes);
  includes := []


let set_debug () = Flags.debug := true

let engagement = ref None
let set_engagement c = engagement := Some c
let engage () =
  match !engagement with Some c -> Safe_typing.set_engagement c | None -> ()


let admit_list = ref ([] : section_path list)
let add_admit s =
  admit_list := path_of_string s :: !admit_list

let norec_list = ref ([] : section_path list)
let add_norec s =
  norec_list := path_of_string s :: !norec_list

let compile_list = ref ([] : section_path 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 () =
  Check.recheck_library
    ~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 (%s)\n"
    Coq_config.version Coq_config.date;
  Printf.printf "compiled on %s\n" Coq_config.compile_date;
  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 "Coq options are:\n";
  output_string co
"  -I dir                 add directory dir in the include path
  -include dir           (idem)
  -R dir coqdir          recursively map physical dir to logical coqdir 

  -admit module          load module and dependencies without checking
  -norec module          check module but admit dependencies without checking

  -where                 print Coq's standard library location and exit
  -v                     print Coq version and exit

  -h, --help             print this list of options
"

(* print the usage on standard error *)

let print_usage = print_usage_channel stderr

let print_usage_coqtop () =
  print_usage "Usage: coqchk <options>\n\n"

let usage () =
  print_usage_coqtop ();
  flush stderr;
  exit 1

let warning s = msg_warning (str s)

open Type_errors

let anomaly_string () = str "Anomaly: "
let report () = (str "." ++ spc () ++ str "Please report.")

let print_loc loc =
  if loc = dummy_loc then 
    (str"<unknown>")
  else 
    let loc = unloc loc in
    (int (fst loc) ++ str"-" ++ int (snd loc))
let guill s = "\""^s^"\""

let where s =
  if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())

let rec explain_exn = function
  | Stream.Failure -> 
      hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
  | Stream.Error txt -> 
      hov 0 (str "Syntax error: " ++ str txt)
  | Token.Error txt -> 
      hov 0 (str "Syntax error: " ++ str txt)
  | Sys_error msg -> 
      hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() )
  | UserError(s,pps) -> 
      hov 1 (str "User error: " ++ where s ++ pps)
  | Out_of_memory -> 
      hov 0 (str "Out of memory")
  | Stack_overflow -> 
      hov 0 (str "Stack overflow")
  | Anomaly (s,pps) -> 
      hov 1 (anomaly_string () ++ where s ++ pps ++ report ())
  | Match_failure(filename,pos1,pos2) ->
      hov 1 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ 
      if Sys.ocaml_version = "3.06" then
		   (str " from character " ++ int pos1 ++ 
                    str " to " ++ int pos2)
		 else
		   (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 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report ())
  | Invalid_argument s -> 
      hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
  | Sys.Break -> 
      hov 0 (fnl () ++ str "User interrupt.")
  | Univ.UniverseInconsistency (o,u,v) ->
      let msg = 
	if !Flags.debug (*!Constrextern.print_universes*) then
	  spc() ++ str "(cannot enforce" ++ spc() ++ (*Univ.pr_uni u ++*) spc() ++
          str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=")
	  ++ spc() ++ (*Univ.pr_uni v ++*) str")"
	else
	  mt() in
      hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
  | TypeError(ctx,te) -> 
(*      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx *)
      (*      te)*)
      hov 0 (str "Type error")

  | Indtypes.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)*)
  | Stdpp.Exc_located (loc,exc) ->
      hov 0 ((if loc = dummy_loc then (mt ())
               else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
               ++ explain_exn exc)
  | Assert_failure (s,b,e) ->
      hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
	       (if s <> "" then 
		 if Sys.ocaml_version = "3.06" then
		   (str ("(file \"" ^ s ^ "\", characters ") ++ 
		    int b ++ str "-" ++ int e ++ str ")")
		 else
		   (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
		    str ", characters " ++ int e ++ str "-" ++
		    int (e+6) ++ str ")")
	       else
		 (mt ())) ++
	       report ())
  | reraise ->
      hov 0 (anomaly_string () ++ str "Uncaught exception " ++ 
	       str (Printexc.to_string reraise)++report())

let parse_args() =
  let rec parse = function
    | [] -> ()
   | "-impredicative-set" :: rem -> 
       set_engagement Declarations.ImpredicativeSet; parse rem

    | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
    | ("-I"|"-include") :: []       -> usage ()

    | "-R" :: d :: p :: rem ->
        push_rec_include (d, dirpath_of_string p);parse rem
    | "-R" :: ([] | [_]) -> usage ()

    | "-debug" :: rem -> set_debug (); parse rem

    | "-where" :: _ ->
        print_endline (getenv_else "COQLIB" Coq_config.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

    | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; 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.make_silent true; parse rem

    | s :: _ when s<>"" && s.[0]='-' ->
        msgnl (str "Unknown option " ++ str s); exit 1
    | s :: rem ->  add_compile s; parse rem
  in
  try
    parse (List.tl (Array.to_list Sys.argv))
  with 
    | UserError(_,s) as e -> begin
	try
	  Stream.empty s; exit 1
	with Stream.Failure ->
	  msgnl (explain_exn e); exit 1
      end
    | e -> begin msgnl (explain_exn e); exit 1 end


(* To prevent from doing the initialization twice *)
let initialized = ref false

let init() =
  if not !initialized then begin
    initialized := true;
    Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
    try
      parse_args();
      if_verbose print_header ();
      init_load_path ();
      engage ();
    with e ->
      flush_all();
      message "Error during initialization :";
      msgnl (explain_exn e);
      exit 1
  end

let run () =
  try 
    compile_files ();
    flush_all()
  with e ->
    (Pp.ppnl(explain_exn e);
    flush_all(); 
    exit 1)

let start () = init(); run(); exit 0