main.ml 24.2 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
4
5
6
7
8
9
10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
11

12
open Format
13
open Why3
14
open Stdlib
15
open Whyconf
16
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
17
open Task
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
18
open Driver
19

20
21
let usage_msg = sprintf
  "Usage: %s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
22
  (Filename.basename Sys.argv.(0))
23

24
25
26
let version_msg = sprintf "Why3 platform, version %s (build date: %s)"
  Config.version Config.builddate

27
let opt_queue = Queue.create ()
28

29
30
let opt_input = ref None
let opt_theory = ref None
31
let opt_trans = ref []
32
let opt_metas = ref []
33

34
35
let add_opt_file x =
  let tlist = Queue.create () in
36
  Queue.push (Some x, tlist) opt_queue;
37
  opt_input := Some tlist
38

39
40
41
let add_opt_theory =
  let rdot = (Str.regexp "\\.") in fun x ->
  let l = Str.split rdot x in
42
43
44
45
46
47
  let p, t = match List.rev l with
    | t::p -> List.rev p, t
    | _ -> assert false
  in
  match !opt_input, p with
  | None, [] ->
48
      eprintf "Option '-T'/'--theory' with a non-qualified \
49
50
51
52
        argument requires an input file.@.";
      exit 1
  | Some tlist, [] ->
      let glist = Queue.create () in
53
      Queue.push (x, p, t, glist) tlist;
54
55
56
      opt_theory := Some glist
  | _ ->
      let tlist = Queue.create () in
57
      Queue.push (None, tlist) opt_queue;
58
59
      opt_input := None;
      let glist = Queue.create () in
60
      Queue.push (x, p, t, glist) tlist;
61
62
63
64
      opt_theory := Some glist

let add_opt_goal x = match !opt_theory with
  | None ->
65
      eprintf "Option '-G'/'--goal' requires a theory.@.";
66
67
68
      exit 1
  | Some glist ->
      let l = Str.split (Str.regexp "\\.") x in
69
      Queue.push (x, l) glist
70
71

let add_opt_trans x = opt_trans := x::!opt_trans
72

73
let add_opt_meta meta =
74
  let meta_name, meta_arg =
75
76
77
78
79
80
81
    try
      let index = String.index meta '=' in
      (String.sub meta 0 index),
      Some (String.sub meta (index+1) (String.length meta - (index + 1)))
    with Not_found ->
      meta, None
  in
82
83
  opt_metas := (meta_name,meta_arg)::!opt_metas

84
let opt_config = ref None
85
let opt_extra = ref []
86
let opt_parser = ref None
87
let opt_prover = ref None
88
let opt_loadpath = ref []
89
90
let opt_driver = ref None
let opt_output = ref None
91
92
let opt_timelimit = ref None
let opt_memlimit = ref None
93
let opt_command = ref None
94
let opt_task = ref None
95
let opt_realize = ref false
96
let opt_extract = ref None
97
let opt_bisect = ref false
98

99
100
101
let opt_print_libdir = ref false
let opt_print_datadir = ref false

102
103
104
105
let opt_print_theory = ref false
let opt_print_namespace = ref false
let opt_list_transforms = ref false
let opt_list_printers = ref false
106
let opt_list_provers = ref false
107
let opt_list_formats = ref false
108
let opt_list_metas = ref false
109

110
let opt_token_count = ref false
111
112
let opt_parse_only = ref false
let opt_type_only = ref false
113
let opt_version = ref false
114
115
116
117

let option_list = Arg.align [
  "-", Arg.Unit (fun () -> add_opt_file "-"),
      " Read the input file from stdin";
118
  "-T", Arg.String add_opt_theory,
119
120
      "<theory> Select <theory> in the input file or in the library";
  "--theory", Arg.String add_opt_theory,
121
122
      " same as -T";
  "-G", Arg.String add_opt_goal,
123
124
      "<goal> Select <goal> in the last selected theory";
  "--goal", Arg.String add_opt_goal,
125
      " same as -G";
126
127
128
129
  "-C", Arg.String (fun s -> opt_config := Some s),
      "<file> Read configuration from <file>";
  "--config", Arg.String (fun s -> opt_config := Some s),
      " same as -C";
130
131
  "--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]),
      "<file> Read additional configuration from <file>";
132
  "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
133
      "<dir> Add <dir> to the library search path";
134
135
136
137
138
139
140
141
  "--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
      " same as -L";
  "-I", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
      " same as -L (obsolete)";
  "-P", Arg.String (fun s -> opt_prover := Some s),
      "<prover> Prove or print (with -o) the selected goals";
  "--prover", Arg.String (fun s -> opt_prover := Some s),
      " same as -P";
142
  "-F", Arg.String (fun s -> opt_parser := Some s),
143
      "<format> Select input format (default: \"why\")";
144
145
  "--format", Arg.String (fun s -> opt_parser := Some s),
      " same as -F";
146
  "-t", Arg.Int (fun i -> opt_timelimit := Some i),
147
148
      "<sec> Set the prover's time limit (default=10, no limit=0)";
  "--timelimit", Arg.Int (fun i -> opt_timelimit := Some i),
149
150
      " same as -t";
  "-m", Arg.Int (fun i -> opt_memlimit := Some i),
151
152
      "<MiB> Set the prover's memory limit (default: no limit)";
  "--memlimit", Arg.Int (fun i -> opt_timelimit := Some i),
153
      " same as -m";
154
155
156
157
  "-a", Arg.String add_opt_trans,
      "<transformation> Apply a transformation to every task";
  "--apply-transform", Arg.String add_opt_trans,
      " same as -a";
158
  "-M", Arg.String add_opt_meta,
159
      "<meta_name>[=<string>] Add a meta to every task";
160
161
  "--meta", Arg.String add_opt_meta,
      " same as -M";
162
  "-D", Arg.String (fun s -> opt_driver := Some (s, [])),
163
      "<file> Specify a prover's driver (conflicts with -P)";
164
  "--driver", Arg.String (fun s -> opt_driver := Some (s, [])),
165
166
167
168
169
      " same as -D";
  "-o", Arg.String (fun s -> opt_output := Some s),
      "<dir> Print the selected goals to separate files in <dir>";
  "--output", Arg.String (fun s -> opt_output := Some s),
      " same as -o";
170
171
  "--realize", Arg.Set opt_realize,
      " Realize selected theories from the library";
172
173
174
  "-E", Arg.String (fun s -> opt_extract := Some s),
      "<driver> Generate code for selected theories/modules";
  "--extract", Arg.String (fun s -> opt_extract := Some s),
175
      " same as -E";
176
  "--bisect", Arg.Set opt_bisect,
177
178
      " Reduce the set of needed axioms which prove a goal, \
        and output the resulting task";
179
  "--print-theory", Arg.Set opt_print_theory,
180
      " Print selected theories";
181
  "--print-namespace", Arg.Set opt_print_namespace,
182
      " Print namespaces of selected theories";
183
  "--list-transforms", Arg.Set opt_list_transforms,
184
      " List known transformations";
185
  "--list-printers", Arg.Set opt_list_printers,
186
      " List known printers";
187
  "--list-provers", Arg.Set opt_list_provers,
188
      " List known provers";
189
  "--list-formats", Arg.Set opt_list_formats,
190
      " List known input formats";
191
  "--list-metas", Arg.Set opt_list_metas,
192
      " List known metas";
193
  Debug.Args.desc_debug_list;
194
195
  "--token-count", Arg.Set opt_token_count,
      " Only lexing, and give numbers of tokens in spec vs in program";
196
197
  Debug.Args.desc_shortcut "parse_only" "--parse-only" " Stop after parsing";
  Debug.Args.desc_shortcut
198
    "type_only" "--type-only" " Stop after type checking";
199
200
  Debug.Args.desc_debug_all;
  Debug.Args.desc_debug;
201
202
203
204
  "--print-libdir", Arg.Set opt_print_libdir,
      " Print location of binary components (plugins, etc)";
  "--print-datadir", Arg.Set opt_print_datadir,
      " Print location of non-binary data (theories, modules, etc)";
205
206
  "--version", Arg.Set opt_version,
      " Print version information" ]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
207

208
let () = try
209
210
  Arg.parse option_list add_opt_file usage_msg;

211
212
213
214
  if !opt_version then begin
    printf "%s@." version_msg;
    exit 0
  end;
215
216
217
218
219
220
221
222
  if !opt_print_libdir then begin
    printf "%s@." Config.libdir;
    exit 0
  end;
  if !opt_print_datadir then begin
    printf "%s@." Config.datadir;
    exit 0
  end;
223

François Bobot's avatar
François Bobot committed
224
  (** Configuration *)
225
  let config = read_config !opt_config in
226
  let config = List.fold_left merge_config config !opt_extra in
François Bobot's avatar
François Bobot committed
227
228
229
  let main = get_main config in
  Whyconf.load_plugins main;

230
  Debug.Args.set_flags_selected ();
231

François Bobot's avatar
François Bobot committed
232
233
  (** listings*)

234
  let sort_pair (x,_) (y,_) = String.compare x y in
235
  let opt_list = ref false in
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
236
  if !opt_list_transforms then begin
237
    opt_list := true;
238
239
    let print_trans_desc fmt (x,r) =
      fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" x Pp.formatted r in
240
    printf "@[<hov 2>Known non-splitting transformations:@\n%a@]@\n@."
241
      (Pp.print_list Pp.newline2 print_trans_desc)
242
      (List.sort sort_pair (Trans.list_transforms ()));
243
    printf "@[<hov 2>Known splitting transformations:@\n%a@]@\n@."
244
      (Pp.print_list Pp.newline2 print_trans_desc)
245
      (List.sort sort_pair (Trans.list_transforms_l ()))
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
246
  end;
247
  if !opt_list_printers then begin
248
    opt_list := true;
249
250
    let print_printer_desc fmt (s,f) =
      fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" s Pp.formatted f in
251
    printf "@[<hov 2>Known printers:@\n%a@]@\n@."
252
      (Pp.print_list Pp.newline2 print_printer_desc)
253
      (List.sort sort_pair (Printer.list_printers ()))
254
255
  end;
  if !opt_list_formats then begin
256
    opt_list := true;
257
    let print1 fmt s = fprintf fmt "%S" s in
258
259
260
261
    let print fmt (p, l, f) =
      fprintf fmt "@[%s [%a]@\n  @[%a@]@]"
        p (Pp.print_list Pp.comma print1) l
        Pp.formatted f
262
    in
263
264
    printf "@[Known input formats:@\n  @[%a@]@]@."
      (Pp.print_list Pp.newline2 print)
265
266
      (List.sort Pervasives.compare (Env.list_formats ()))
  end;
267
  if !opt_list_provers then begin
268
    opt_list := true;
269
270
    let print = Pp.print_iter2 Mprover.iter Pp.newline Pp.nothing
      print_prover Pp.nothing in
271
272
    let provers = get_provers config in
    printf "@[<hov 2>Known provers:@\n%a@]@." print provers
273
  end;
274
  if !opt_list_metas then begin
275
    opt_list := true;
276
    let print fmt m = fprintf fmt "@[<h 2>%s %s%a@\n@[<hov>%a@]@]"
277
278
      (let s = m.meta_name in
        if String.contains s ' ' then "\"" ^ s ^ "\"" else s)
François Bobot's avatar
François Bobot committed
279
      (if m.meta_excl then "(flag) " else "")
280
      (Pp.print_list Pp.space Pretty.print_meta_arg_type) m.meta_type
281
      Pp.formatted m.meta_desc
282
    in
283
284
    let cmp m1 m2 = Pervasives.compare m1.meta_name m2.meta_name in
    printf "@[<hov 2>Known metas:@\n%a@]@\n@."
285
      (Pp.print_list Pp.newline2 print) (List.sort cmp (Theory.list_metas ()))
286
  end;
287
  opt_list :=  Debug.Args.option_list () || !opt_list;
288
  if !opt_list then exit 0;
289
290
291
292
293
294

  if Queue.is_empty opt_queue then begin
    Arg.usage option_list usage_msg;
    exit 1
  end;

295
296
297
  if !opt_prover <> None && !opt_driver <> None then begin
    eprintf "Options '-P'/'--prover' and \
      '-D'/'--driver' cannot be used together.@.";
298
299
    exit 1
  end;
300

301
  if !opt_output <> None
302
  && !opt_driver = None && !opt_prover = None && !opt_extract = None then begin
303
304
305
306
307
    eprintf
      "Option '-o'/'--output' requires a prover, a driver, or option '-E'.@.";
    exit 1
  end;

308
309
  if !opt_prover = None then begin
    if !opt_timelimit <> None then begin
310
      eprintf "Option '-t'/'--timelimit' requires a prover.@.";
311
312
313
      exit 1
    end;
    if !opt_memlimit <> None then begin
314
      eprintf "Option '-m'/'--memlimit' requires a prover.@.";
315
316
      exit 1
    end;
317
318
319
320
    if !opt_bisect then begin
      eprintf "Option '--bisect' requires a prover.@.";
      exit 1
    end;
321
322
    if !opt_driver = None && not !opt_print_namespace then
      opt_print_theory := true
323
324
  end;

325
  if !opt_extract <> None && !opt_output = None then begin
326
327
328
329
330
    eprintf
      "Option '-E'/'--extract' require a directory to output the result.@.";
    exit 1
  end;

331
332
333
334
335
  if !opt_bisect && !opt_output = None then begin
    eprintf "Option '--bisect' require a directory to output the result.@.";
    exit 1
  end;

336
337
338
  opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main);
  if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main);
  if !opt_memlimit  = None then opt_memlimit  := Some (Whyconf.memlimit main);
339
  begin match !opt_prover with
340
  | Some s ->
341
342
343
344
345
    let filter_prover = Whyconf.parse_filter_prover s in
    let prover = Whyconf.filter_one_prover config filter_prover in
    opt_command :=
      Some (String.concat " " (prover.command :: prover.extra_options));
    opt_driver := Some (prover.driver, prover.extra_drivers)
346
  | None ->
347
348
      ()
  end;
349
  let add_meta task (meta,s) =
350
    let meta = lookup_meta meta in
351
352
353
354
355
    let args = match s with
      | Some s -> [MAstr s]
      | None -> []
    in
    add_meta task meta args
356
  in
357
  opt_task := List.fold_left add_meta !opt_task !opt_metas
358

359
360
361
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
362
363

let timelimit = match !opt_timelimit with
364
365
366
  | None -> 10
  | Some i when i <= 0 -> 0
  | Some i -> i
367

368
let memlimit = match !opt_memlimit with
369
370
371
372
  | None -> 0
  | Some i when i <= 0 -> 0
  | Some i -> i

373
let print_th_namespace fmt th =
374
  Pretty.print_namespace fmt th.th_name.Ident.id_string th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
375

376
let fname_printer = ref (Ident.create_ident_printer [])
MARCHE Claude's avatar
MARCHE Claude committed
377

378
379
380
let output_task drv fname _tname th task dir =
  let fname = Filename.basename fname in
  let fname =
381
    try Filename.chop_extension fname with _ -> fname in
382
383
384
385
386
387
388
389
390
391
392
393
394
  let tname = th.th_name.Ident.id_string in
  let dest = Driver.file_of_task drv fname tname task in
  (* Uniquify the filename before the extension if it exists*)
  let i = try String.rindex dest '.' with _ -> String.length dest in
  let name = Ident.string_unique !fname_printer (String.sub dest 0 i) in
  let ext = String.sub dest i (String.length dest - i) in
  let cout = open_out (Filename.concat dir (name ^ ext)) in
  Driver.print_task drv (formatter_of_out_channel cout) task;
  close_out cout

let output_task_prepared drv fname _tname th task dir =
  let fname = Filename.basename fname in
  let fname =
395
    try Filename.chop_extension fname with _ -> fname in
396
397
398
399
400
401
402
403
404
405
  let tname = th.th_name.Ident.id_string in
  let dest = Driver.file_of_task drv fname tname task in
  (* Uniquify the filename before the extension if it exists*)
  let i = try String.rindex dest '.' with _ -> String.length dest in
  let name = Ident.string_unique !fname_printer (String.sub dest 0 i) in
  let ext = String.sub dest i (String.length dest - i) in
  let cout = open_out (Filename.concat dir (name ^ ext)) in
  Driver.print_task_prepared drv (formatter_of_out_channel cout) task;
  close_out cout

406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
let output_theory drv fname _tname th task dir =
  let fname = Filename.basename fname in
  let fname =
    try Filename.chop_extension fname with _ -> fname in
  let dest = Driver.file_of_theory drv fname th in
  let file = Filename.concat dir dest in
  let old =
    if Sys.file_exists file then begin
      let backup = file ^ ".bak" in
      Sys.rename file backup;
      Some (open_in backup)
    end else None in
  let cout = open_out file in
  Driver.print_task ?old drv (formatter_of_out_channel cout) task;
  close_out cout
421

Andrei Paskevich's avatar
Andrei Paskevich committed
422
let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
423
  match !opt_output, !opt_command with
424
425
426
    | Some dir, _ when !opt_realize ->
        output_theory drv fname tname th task dir
    | None, _ when !opt_realize ->
Andrei Paskevich's avatar
Andrei Paskevich committed
427
428
        eprintf "Output directory (-o) is required.@.";
        exit 1
429
    | Some dir, Some command when !opt_bisect ->
430
        let test task =
431
          let call = Driver.prove_task
432
433
434
435
436
437
            ~command ~timelimit ~memlimit drv task in
          let res = Call_provers.wait_on_call (call ()) () in
          printf "%s %s %s : %a@." fname tname
            (task_goal task).Decl.pr_name.Ident.id_string
            Call_provers.print_prover_result res;
          res.Call_provers.pr_answer = Call_provers.Valid in
438
        if not (test task)
439
        then printf "I can't bisect %s %s %s which is not valid@." fname tname
440
          (task_goal task).Decl.pr_name.Ident.id_string
441
        else
442
443
444
445
446
447
448
449
          let rem = Eliminate_definition.bisect test task in
          let goal,task = Task.task_separate_goal task in
          let task = List.fold_left
            (fun task (m,ml) -> Task.add_meta task m ml) task rem in
          let task = add_tdecl task goal in
          (** We suppose here that the first transformation in the driver
              is remove_builtin *)
          let prepared_task = Driver.prepare_task drv task in
450
          output_task_prepared drv fname tname th prepared_task dir
451
    | None, Some command ->
Andrei Paskevich's avatar
Andrei Paskevich committed
452
453
        let call = Driver.prove_task ~command ~timelimit ~memlimit drv task in
        let res = Call_provers.wait_on_call (call ()) () in
454
        printf "%s %s %s : %a@." fname tname
455
          (task_goal task).Decl.pr_name.Ident.id_string
456
457
          Call_provers.print_prover_result res
    | None, None ->
458
        Driver.print_task drv std_formatter task
459
    | Some dir, _ -> output_task drv fname tname th task dir
460

461
let do_tasks env drv fname tname th task =
462
  let lookup acc t =
463
464
    (try Trans.singleton (Trans.lookup_transform t env) with
       Trans.UnknownTrans _ -> Trans.lookup_transform_l t env) :: acc
465
  in
466
  let trans = List.fold_left lookup [] !opt_trans in
467
  let apply tasks tr =
468
    List.rev (List.fold_left (fun acc task ->
469
      List.rev_append (Trans.apply tr task) acc) [] tasks)
470
  in
471
  let tasks = List.fold_left apply [task] trans in
Andrei Paskevich's avatar
Andrei Paskevich committed
472
  List.iter (do_task drv fname tname th) tasks
473

474
let do_theory env drv fname tname th glist =
475
476
477
478
  if !opt_print_theory then
    printf "%a@." Pretty.print_theory th
  else if !opt_print_namespace then
    printf "%a@." print_th_namespace th
479
480
481
482
483
484
485
486
  else if !opt_realize then
    if th.th_path = [] then begin
      eprintf "Theory %s is not from the library.@." tname;
      exit 1
    end else if not (Queue.is_empty glist) then begin
      eprintf "Cannot realize individual goals.@.";
      exit 1
    end else begin
487
      let drv = Opt.get drv in
488
489
490
      let task = Task.use_export None th in
      do_tasks env drv fname tname th task
    end
491
  else begin
492
    let add acc (x,l) =
493
494
495
496
      let pr = try ns_find_pr th.th_export l with Not_found ->
        eprintf "Goal '%s' not found in theory '%s'.@." x tname;
        exit 1
      in
497
      Decl.Spr.add pr acc
498
    in
499
    let drv = Opt.get drv in
500
501
502
503
    let prs = Queue.fold add Decl.Spr.empty glist in
    let sel = if Decl.Spr.is_empty prs then None else Some prs in
    let tasks = List.rev (split_theory th sel !opt_task) in
    List.iter (do_tasks env drv fname tname th) tasks
504
  end
MARCHE Claude's avatar
MARCHE Claude committed
505

506
let do_global_theory env drv (tname,p,t,glist) =
507
  let format = Opt.get_def "why" !opt_parser in
Andrei Paskevich's avatar
Andrei Paskevich committed
508
  let th = try Env.read_theory ~format env p t with Env.TheoryNotFound _ ->
509
510
    eprintf "Theory '%s' not found.@." tname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
511
  in
512
  do_theory env drv "lib" tname th glist
MARCHE Claude's avatar
MARCHE Claude committed
513

514
let do_local_theory env drv fname m (tname,_,t,glist) =
515
  let th = try Mstr.find t m with Not_found ->
516
517
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
518
  in
519
  do_theory env drv fname tname th glist
520

521
522
(* program extraction *)

523
let extract_to ?fname th extract =
524
  let dir = Opt.get !opt_output in
525
  let file = Filename.concat dir (Mlw_ocaml.extract_filename ?fname th) in
526
527
528
529
530
531
532
533
534
  let old =
    if Sys.file_exists file then begin
      let backup = file ^ ".bak" in
      Sys.rename file backup;
      Some (open_in backup)
    end else None in
  let cout = open_out file in
  extract file ?old (formatter_of_out_channel cout);
  close_out cout
535

536
let do_extract_theory edrv ?fname tname th =
537
538
  let extract file ?old fmt = ignore (old);
    Debug.dprintf Mlw_ocaml.debug "extract theory %s to file %s@." tname file;
539
    Mlw_ocaml.extract_theory edrv ?old ?fname fmt th
540
541
542
  in
  extract_to ?fname th extract

543
let do_extract_module edrv ?fname tname m =
544
545
  let extract file ?old fmt = ignore (old);
    Debug.dprintf Mlw_ocaml.debug "extract module %s to file %s@." tname file;
546
    Mlw_ocaml.extract_module edrv ?old ?fname fmt m
547
548
  in
  extract_to ?fname m.Mlw_module.mod_theory extract
549

550
551
let do_global_extract edrv (tname,p,t,_) =
  let lib = edrv.Mlw_driver.drv_lib in
552
553
554
555
  try
    let mm, thm = Env.read_lib_file lib p in
    try
      let m = Mstr.find t mm in
556
      do_extract_module edrv tname m
557
558
    with Not_found ->
      let th = Mstr.find t thm in
559
      do_extract_theory edrv tname th
560
  with Env.LibFileNotFound _ | Not_found -> try
561
    let format = Opt.get_def "why" !opt_parser in
562
    let env = Env.env_of_library lib in
563
    let th = Env.read_theory ~format env p t in
564
    do_extract_theory edrv tname th
565
566
567
568
  with Env.LibFileNotFound _ | Env.TheoryNotFound _ ->
    eprintf "Theory/module '%s' not found.@." tname;
    exit 1

569
let do_extract_theory_from env fname m (tname,_,t,_) =
570
571
572
573
  let th = try Mstr.find t m with Not_found ->
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
  in
574
  do_extract_theory env ~fname tname th
575

576
let do_extract_module_from env fname mm thm (tname,_,t,_) =
577
  try
578
    let m = Mstr.find t mm in do_extract_module env ~fname tname m
579
  with Not_found -> try
580
    let th = Mstr.find t thm in do_extract_theory env ~fname tname th
581
582
583
584
  with Not_found ->
    eprintf "Theory/module '%s' not found in file '%s'.@." tname fname;
    exit 1

585
586
let do_local_extract edrv fname cin tlist =
  let lib = edrv.Mlw_driver.drv_lib in
587
588
589
  if !opt_parser = Some "whyml" || Filename.check_suffix fname ".mlw" then begin
    let mm, thm = Mlw_main.read_channel lib [] fname cin in
    if Queue.is_empty tlist then begin
590
      let do_m t m thm =
591
        do_extract_module edrv ~fname t m; Mstr.remove t thm in
592
      let thm = Mstr.fold do_m mm thm in
593
      Mstr.iter (fun t th -> do_extract_theory edrv ~fname t th) thm
594
    end else
595
      Queue.iter (do_extract_module_from edrv fname mm thm) tlist
596
  end else begin
597
    let env = Env.env_of_library lib in
598
599
600
    let m = Env.read_channel ?format:!opt_parser env fname cin in
    if Queue.is_empty tlist then
      let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
601
      let do_th _ (t,th) = do_extract_theory edrv ~fname t th in
602
603
      Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
    else
604
      Queue.iter (do_extract_theory_from edrv fname m) tlist
605
606
  end

607
608
609
let total_annot_tokens = ref 0
let total_program_tokens = ref 0

610
let do_input env drv edrv = function
611
  | None, _ when !opt_parse_only || !opt_type_only ->
612
      ()
613
  | None, tlist when edrv <> None ->
614
      Queue.iter (do_global_extract (Opt.get edrv)) tlist
615
  | None, tlist ->
MARCHE Claude's avatar
MARCHE Claude committed
616
      Queue.iter (do_global_theory env drv) tlist
617
  | Some f, tlist ->
618
619
620
621
      let fname, cin = match f with
        | "-" -> "stdin", stdin
        | f   -> f, open_in f
      in
622
      if !opt_token_count then begin
623
624
625
        let lb = Lexing.from_channel cin in
        let a,p = Lexer.token_counter lb in
        close_in cin;
626
627
628
629
630
631
632
633
634
635
        if a = 0 then begin
          (* hack: we assume it is a why file and not a mlw *)
          total_annot_tokens := !total_annot_tokens + p;
          Format.printf "File %s: %d tokens@." f p;
        end else begin
          total_program_tokens := !total_program_tokens + p;
          total_annot_tokens := !total_annot_tokens + a;
          Format.printf "File %s: %d tokens in annotations@." f a;
          Format.printf "File %s: %d tokens in programs@." f p
        end
636
      end else if edrv <> None then begin
637
        do_local_extract (Opt.get edrv) fname cin tlist;
638
639
        close_in cin
      end else begin
640
641
642
643
        let m = Env.read_channel ?format:!opt_parser env fname cin in
        close_in cin;
        if !opt_type_only then
          ()
MARCHE Claude's avatar
MARCHE Claude committed
644
        else
645
646
647
648
649
650
651
          if Queue.is_empty tlist then
            let glist = Queue.create () in
            let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
            let do_th _ (t,th) = do_theory env drv fname t th glist in
            Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
          else
            Queue.iter (do_local_theory env drv fname m) tlist
652
      end
MARCHE Claude's avatar
MARCHE Claude committed
653

654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
let driver_file s =
  if Sys.file_exists s || String.contains s '/' || String.contains s '.' then
    s
  else
    Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv"))

let load_driver env (s,ef) =
  let file = driver_file s in
  load_driver env file ef

let load_driver_extract env s =
  let file = driver_file s in
  let lib = Mlw_main.library_of_env env in
  Mlw_driver.load_driver lib file []

669
670
let () =
  try
671
    let env = Env.create_env !opt_loadpath in
672
673
    let drv = Opt.map (load_driver env) !opt_driver in
    let edrv = Opt.map (load_driver_extract env) !opt_extract in
674
    Queue.iter (do_input env drv edrv) opt_queue;
675
    if !opt_token_count then
Andrei Paskevich's avatar
Andrei Paskevich committed
676
      Format.printf "Total: %d annot/%d programs, ratio = %.3f@."
677
678
        !total_annot_tokens !total_program_tokens
        ((float !total_annot_tokens) /. (float !total_program_tokens))
679
  with e when not (Debug.test_flag Debug.stack_trace) ->
680
    eprintf "%a@." Exn_printer.exn_printer e;
681
    exit 1
682

683
(*
684
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
685
compile-command: "unset LANG; make -C .. byte"
686
End:
687
*)