main.ml 24.8 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
1
2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4
5
6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
8
(*    Andrei Paskevich                                                    *)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
9
10
11
12
13
14
15
16
17
18
19
20
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

21
open Format
22
open Why3
23
24
open Util
open Whyconf
25
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
26
open Task
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
27
open Driver
28

29
30
let usage_msg = sprintf
  "Usage: %s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
31
  (Filename.basename Sys.argv.(0))
32

33
34
35
let version_msg = sprintf "Why3 platform, version %s (build date: %s)"
  Config.version Config.builddate

36
let opt_queue = Queue.create ()
37

38
39
let opt_input = ref None
let opt_theory = ref None
40
let opt_trans = ref []
41
let opt_metas = ref []
42

43
44
let add_opt_file x =
  let tlist = Queue.create () in
45
  Queue.push (Some x, tlist) opt_queue;
46
  opt_input := Some tlist
47

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

let add_opt_goal x = match !opt_theory with
  | None ->
74
      eprintf "Option '-G'/'--goal' requires a theory.@.";
75
76
77
      exit 1
  | Some glist ->
      let l = Str.split (Str.regexp "\\.") x in
78
      Queue.push (x, l) glist
79
80

let add_opt_trans x = opt_trans := x::!opt_trans
81

82
let add_opt_meta meta =
83
  let meta_name, meta_arg =
84
85
86
87
88
89
90
    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
91
92
  opt_metas := (meta_name,meta_arg)::!opt_metas

93
let opt_config = ref None
94
let opt_extra = ref []
95
let opt_parser = ref None
96
let opt_prover = ref None
97
let opt_loadpath = ref []
98
99
let opt_driver = ref None
let opt_output = ref None
100
101
let opt_timelimit = ref None
let opt_memlimit = ref None
102
let opt_command = ref None
103
let opt_task = ref None
104
let opt_realize = ref false
105
let opt_extract = ref None
106
let opt_bisect = ref false
107

108
109
110
let opt_print_libdir = ref false
let opt_print_datadir = ref false

111
112
113
114
let opt_print_theory = ref false
let opt_print_namespace = ref false
let opt_list_transforms = ref false
let opt_list_printers = ref false
115
let opt_list_provers = ref false
116
let opt_list_formats = ref false
117
let opt_list_metas = ref false
118

119
let opt_token_count = ref false
120
121
let opt_parse_only = ref false
let opt_type_only = ref false
122
let opt_version = ref false
123
124
125
126

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

217
let () = try
218
219
  Arg.parse option_list add_opt_file usage_msg;

220
221
222
223
  if !opt_version then begin
    printf "%s@." version_msg;
    exit 0
  end;
224
225
226
227
228
229
230
231
  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;
232

François Bobot's avatar
François Bobot committed
233
  (** Configuration *)
234
  let config = read_config !opt_config in
235
  let config = List.fold_left merge_config config !opt_extra in
François Bobot's avatar
François Bobot committed
236
237
238
  let main = get_main config in
  Whyconf.load_plugins main;

239
240
  Debug.Opt.set_flags_selected ();

François Bobot's avatar
François Bobot committed
241
242
  (** listings*)

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

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

300
301
302
  if !opt_prover <> None && !opt_driver <> None then begin
    eprintf "Options '-P'/'--prover' and \
      '-D'/'--driver' cannot be used together.@.";
303
304
    exit 1
  end;
305

306
  if !opt_output <> None
307
  && !opt_driver = None && !opt_prover = None && !opt_extract = None then begin
308
309
310
311
312
    eprintf
      "Option '-o'/'--output' requires a prover, a driver, or option '-E'.@.";
    exit 1
  end;

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

330
  if !opt_extract <> None && !opt_output = None then begin
331
332
333
334
335
    eprintf
      "Option '-E'/'--extract' require a directory to output the result.@.";
    exit 1
  end;

336
337
338
339
340
  if !opt_bisect && !opt_output = None then begin
    eprintf "Option '--bisect' require a directory to output the result.@.";
    exit 1
  end;

341
342
343
  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);
344
  begin match !opt_prover with
345
  | Some s ->
346
347
348
349
350
    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)
351
  | None ->
352
353
      ()
  end;
354
  let add_meta task (meta,s) =
355
    let meta = lookup_meta meta in
356
357
358
359
360
    let args = match s with
      | Some s -> [MAstr s]
      | None -> []
    in
    add_meta task meta args
361
  in
362
  opt_task := List.fold_left add_meta !opt_task !opt_metas
363

364
365
366
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
367
368

let timelimit = match !opt_timelimit with
369
370
371
  | None -> 10
  | Some i when i <= 0 -> 0
  | Some i -> i
372

373
let memlimit = match !opt_memlimit with
374
375
376
377
  | None -> 0
  | Some i when i <= 0 -> 0
  | Some i -> i

378
let print_th_namespace fmt th =
379
  Pretty.print_namespace fmt th.th_name.Ident.id_string th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
380

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

383
384
385
let output_task drv fname _tname th task dir =
  let fname = Filename.basename fname in
  let fname =
386
    try Filename.chop_extension fname with _ -> fname in
387
388
389
390
391
392
393
394
395
396
397
398
399
  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 =
400
    try Filename.chop_extension fname with _ -> fname in
401
402
403
404
405
406
407
408
409
410
  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

411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
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
426

Andrei Paskevich's avatar
Andrei Paskevich committed
427
let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
428
  match !opt_output, !opt_command with
429
430
431
    | Some dir, _ when !opt_realize ->
        output_theory drv fname tname th task dir
    | None, _ when !opt_realize ->
Andrei Paskevich's avatar
Andrei Paskevich committed
432
433
        eprintf "Output directory (-o) is required.@.";
        exit 1
434
    | Some dir, Some command when !opt_bisect ->
435
        let test task =
436
          let call = Driver.prove_task
437
438
439
440
441
442
            ~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
443
        if not (test task)
444
        then printf "I can't bisect %s %s %s which is not valid@." fname tname
445
          (task_goal task).Decl.pr_name.Ident.id_string
446
        else
447
448
449
450
451
452
453
454
          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
455
          output_task_prepared drv fname tname th prepared_task dir
456
    | None, Some command ->
Andrei Paskevich's avatar
Andrei Paskevich committed
457
458
        let call = Driver.prove_task ~command ~timelimit ~memlimit drv task in
        let res = Call_provers.wait_on_call (call ()) () in
459
        printf "%s %s %s : %a@." fname tname
460
          (task_goal task).Decl.pr_name.Ident.id_string
461
462
          Call_provers.print_prover_result res
    | None, None ->
463
        Driver.print_task drv std_formatter task
464
    | Some dir, _ -> output_task drv fname tname th task dir
465

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

479
let do_theory env drv fname tname th glist =
480
481
482
483
  if !opt_print_theory then
    printf "%a@." Pretty.print_theory th
  else if !opt_print_namespace then
    printf "%a@." print_th_namespace th
484
485
486
487
488
489
490
491
492
493
494
495
  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
      let drv = Util.of_option drv in
      let task = Task.use_export None th in
      do_tasks env drv fname tname th task
    end
496
  else begin
497
    let add acc (x,l) =
498
499
500
501
      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
502
      Decl.Spr.add pr acc
503
504
    in
    let drv = Util.of_option drv in
505
506
507
508
    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
509
  end
MARCHE Claude's avatar
MARCHE Claude committed
510

511
let do_global_theory env drv (tname,p,t,glist) =
512
  let format = Util.def_option "why" !opt_parser in
Andrei Paskevich's avatar
Andrei Paskevich committed
513
  let th = try Env.read_theory ~format env p t with Env.TheoryNotFound _ ->
514
515
    eprintf "Theory '%s' not found.@." tname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
516
  in
517
  do_theory env drv "lib" tname th glist
MARCHE Claude's avatar
MARCHE Claude committed
518

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

526
527
(* program extraction *)

528
let extract_to ?fname th extract =
529
530
  let dir = Util.of_option !opt_output in
  let file = Filename.concat dir (Mlw_ocaml.extract_filename ?fname th) in
531
532
533
534
535
536
537
538
539
  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
540

541
let do_extract_theory edrv ?fname tname th =
542
543
  let extract file ?old fmt = ignore (old);
    Debug.dprintf Mlw_ocaml.debug "extract theory %s to file %s@." tname file;
544
    Mlw_ocaml.extract_theory edrv ?old ?fname fmt th
545
546
547
  in
  extract_to ?fname th extract

548
let do_extract_module edrv ?fname tname m =
549
550
  let extract file ?old fmt = ignore (old);
    Debug.dprintf Mlw_ocaml.debug "extract module %s to file %s@." tname file;
551
    Mlw_ocaml.extract_module edrv ?old ?fname fmt m
552
553
  in
  extract_to ?fname m.Mlw_module.mod_theory extract
554

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

574
let do_extract_theory_from env fname m (tname,_,t,_) =
575
576
577
578
  let th = try Mstr.find t m with Not_found ->
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
  in
579
  do_extract_theory env ~fname tname th
580

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

590
591
let do_local_extract edrv fname cin tlist =
  let lib = edrv.Mlw_driver.drv_lib in
592
593
594
  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
595
      let do_m t m thm =
596
        do_extract_module edrv ~fname t m; Mstr.remove t thm in
597
      let thm = Mstr.fold do_m mm thm in
598
      Mstr.iter (fun t th -> do_extract_theory edrv ~fname t th) thm
599
    end else
600
      Queue.iter (do_extract_module_from edrv fname mm thm) tlist
601
  end else begin
602
    let env = Env.env_of_library lib in
603
604
605
    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
606
      let do_th _ (t,th) = do_extract_theory edrv ~fname t th in
607
608
      Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
    else
609
      Queue.iter (do_extract_theory_from edrv fname m) tlist
610
611
  end

612
613
614
let total_annot_tokens = ref 0
let total_program_tokens = ref 0

615
let do_input env drv edrv = function
616
  | None, _ when !opt_parse_only || !opt_type_only ->
617
      ()
618
619
  | None, tlist when edrv <> None ->
      Queue.iter (do_global_extract (Util.of_option edrv)) tlist
620
  | None, tlist ->
MARCHE Claude's avatar
MARCHE Claude committed
621
      Queue.iter (do_global_theory env drv) tlist
622
  | Some f, tlist ->
623
624
625
626
      let fname, cin = match f with
        | "-" -> "stdin", stdin
        | f   -> f, open_in f
      in
627
      if !opt_token_count then begin
628
629
630
        let lb = Lexing.from_channel cin in
        let a,p = Lexer.token_counter lb in
        close_in cin;
631
632
633
634
635
636
637
638
639
640
        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
641
642
      end else if edrv <> None then begin
        do_local_extract (Util.of_option edrv) fname cin tlist;
643
644
        close_in cin
      end else begin
645
646
647
648
        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
649
        else
650
651
652
653
654
655
656
          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
657
      end
MARCHE Claude's avatar
MARCHE Claude committed
658

659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
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 []

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

688
(*
689
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
690
compile-command: "unset LANG; make -C .. byte"
691
End:
692
*)