main.ml 25.5 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
9
10
(*                                                                  *)
(*  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_theory_eval = ref None
32
let opt_trans = ref []
33
let opt_metas = ref []
34

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

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

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

76
77
78
79
80
81
82
83
let add_opt_eval x = match !opt_theory_eval with
  | None ->
      eprintf "Option '--eval' requires a theory.@.";
      exit 1
  | Some elist ->
      let l = Str.split (Str.regexp "\\.") x in
      Queue.push (x, l) elist

84
let add_opt_trans x = opt_trans := x::!opt_trans
85

86
let add_opt_meta meta =
87
  let meta_name, meta_arg =
88
89
90
91
92
93
94
    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
95
96
  opt_metas := (meta_name,meta_arg)::!opt_metas

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

112
113
114
let opt_print_libdir = ref false
let opt_print_datadir = ref false

115
116
117
118
let opt_print_theory = ref false
let opt_print_namespace = ref false
let opt_list_transforms = ref false
let opt_list_printers = ref false
119
let opt_list_provers = ref false
120
let opt_list_formats = ref false
121
let opt_list_metas = ref false
122

123
let opt_token_count = ref false
124
let opt_version = ref false
125
126
127
128

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

221
let () = try
222
223
  Arg.parse option_list add_opt_file usage_msg;

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

François Bobot's avatar
François Bobot committed
237
  (** Configuration *)
238
  let config = read_config !opt_config in
239
  let config = List.fold_left merge_config config !opt_extra in
François Bobot's avatar
François Bobot committed
240
241
242
  let main = get_main config in
  Whyconf.load_plugins main;

243
  Debug.Args.set_flags_selected ();
244

François Bobot's avatar
François Bobot committed
245
246
  (** listings*)

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

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

308
309
310
  if !opt_prover <> None && !opt_driver <> None then begin
    eprintf "Options '-P'/'--prover' and \
      '-D'/'--driver' cannot be used together.@.";
311
312
    exit 1
  end;
313

314
  if !opt_output <> None
315
  && !opt_driver = None && !opt_prover = None && !opt_extract = None then begin
316
317
318
319
320
    eprintf
      "Option '-o'/'--output' requires a prover, a driver, or option '-E'.@.";
    exit 1
  end;

321
322
  if !opt_prover = None then begin
    if !opt_timelimit <> None then begin
323
      eprintf "Option '-t'/'--timelimit' requires a prover.@.";
324
325
326
      exit 1
    end;
    if !opt_memlimit <> None then begin
327
      eprintf "Option '-m'/'--memlimit' requires a prover.@.";
328
329
      exit 1
    end;
330
331
332
333
    if !opt_bisect then begin
      eprintf "Option '--bisect' requires a prover.@.";
      exit 1
    end;
334
335
    if !opt_driver = None && not !opt_print_namespace then
      opt_print_theory := true
336
337
  end;

338
  if !opt_extract <> None && !opt_output = None then begin
339
340
341
342
343
    eprintf
      "Option '-E'/'--extract' require a directory to output the result.@.";
    exit 1
  end;

344
345
346
347
348
  if !opt_bisect && !opt_output = None then begin
    eprintf "Option '--bisect' require a directory to output the result.@.";
    exit 1
  end;

349
350
351
  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);
352
  begin match !opt_prover with
353
  | Some s ->
354
355
356
357
358
    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)
359
  | None ->
360
361
      ()
  end;
362
  let add_meta task (meta,s) =
363
    let meta = lookup_meta meta in
364
365
366
367
368
    let args = match s with
      | Some s -> [MAstr s]
      | None -> []
    in
    add_meta task meta args
369
  in
370
  opt_task := List.fold_left add_meta !opt_task !opt_metas
371

372
373
374
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
375
376

let timelimit = match !opt_timelimit with
377
378
379
  | None -> 10
  | Some i when i <= 0 -> 0
  | Some i -> i
380

381
let memlimit = match !opt_memlimit with
382
383
384
385
  | None -> 0
  | Some i when i <= 0 -> 0
  | Some i -> i

386
let print_th_namespace fmt th =
387
  Pretty.print_namespace fmt th.th_name.Ident.id_string th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
388

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

391
392
393
let output_task drv fname _tname th task dir =
  let fname = Filename.basename fname in
  let fname =
394
    try Filename.chop_extension fname with _ -> fname in
395
396
397
398
399
400
401
402
403
404
405
406
407
  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 =
408
    try Filename.chop_extension fname with _ -> fname in
409
410
411
412
413
414
415
416
417
418
  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

419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
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
434

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

474
let do_tasks env drv fname tname th task =
475
  let lookup acc t =
476
477
    (try Trans.singleton (Trans.lookup_transform t env) with
       Trans.UnknownTrans _ -> Trans.lookup_transform_l t env) :: acc
478
  in
479
  let trans = List.fold_left lookup [] !opt_trans in
480
  let apply tasks tr =
481
    List.rev (List.fold_left (fun acc task ->
482
      List.rev_append (Trans.apply tr task) acc) [] tasks)
483
  in
484
  let tasks = List.fold_left apply [task] trans in
Andrei Paskevich's avatar
Andrei Paskevich committed
485
  List.iter (do_task drv fname tname th) tasks
486

487
let do_theory env drv fname tname th glist elist =
488
489
490
491
  if !opt_print_theory then
    printf "%a@." Pretty.print_theory th
  else if !opt_print_namespace then
    printf "%a@." print_th_namespace th
492
493
494
495
496
497
498
499
  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
500
      let drv = Opt.get drv in
501
      let task = Task.use_export !opt_task th in
502
503
      do_tasks env drv fname tname th task
    end
504
  else begin
505
    let add acc (x,l) =
506
507
508
509
      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
510
      Decl.Spr.add pr acc
511
    in
512
    let drv = Opt.get drv in
513
514
515
    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
516
517
518
519
520
521
522
523
524
525
526
527
528
529
    List.iter (do_tasks env drv fname tname th) tasks;
    let eval (x,l) =
      let ls = try ns_find_ls th.th_export l with Not_found ->
        eprintf "Declaration '%s' not found in theory '%s'.@." x tname;
        exit 1
      in
      match Decl.find_logic_definition th.th_known ls with
      | None -> eprintf "Symbol '%s' has no definition in theory '%s'.@." x tname;
        exit 1
      | Some d ->
        let l,t = Decl.open_ls_defn d in
        match l with
        | [] ->
          let t = Mlw_interp.eval_term Term.Mvs.empty Term.Mvs.empty t in
MARCHE Claude's avatar
MARCHE Claude committed
530
          printf "@[<hov 2>Evaluation of %s:@ %a@]@." x Pretty.print_term t
531
532
533
534
535
        | _ ->
          eprintf "Symbol '%s' is not a constant in theory '%s'.@." x tname;
          exit 1
    in
    Queue.iter eval elist
536
  end
MARCHE Claude's avatar
MARCHE Claude committed
537

538
let do_global_theory env drv (tname,p,t,glist,elist) =
539
  let format = Opt.get_def "why" !opt_parser in
Andrei Paskevich's avatar
Andrei Paskevich committed
540
  let th = try Env.read_theory ~format env p t with Env.TheoryNotFound _ ->
541
542
    eprintf "Theory '%s' not found.@." tname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
543
  in
544
  do_theory env drv "lib" tname th glist elist
MARCHE Claude's avatar
MARCHE Claude committed
545

546
let do_local_theory env drv fname m (tname,_,t,glist,elist) =
547
  let th = try Mstr.find t m with Not_found ->
548
549
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
550
  in
551
  do_theory env drv fname tname th glist elist
552

553
554
(* program extraction *)

555
let extract_to ?fname th extract =
556
  let dir = Opt.get !opt_output in
557
  let file = Filename.concat dir (Mlw_ocaml.extract_filename ?fname th) in
558
559
560
561
562
563
564
565
566
  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
567

568
let do_extract_theory edrv ?fname tname th =
569
570
  let extract file ?old fmt = ignore (old);
    Debug.dprintf Mlw_ocaml.debug "extract theory %s to file %s@." tname file;
571
    Mlw_ocaml.extract_theory edrv ?old ?fname fmt th
572
573
574
  in
  extract_to ?fname th extract

575
let do_extract_module edrv ?fname tname m =
576
577
  let extract file ?old fmt = ignore (old);
    Debug.dprintf Mlw_ocaml.debug "extract module %s to file %s@." tname file;
578
    Mlw_ocaml.extract_module edrv ?old ?fname fmt m
579
580
  in
  extract_to ?fname m.Mlw_module.mod_theory extract
581

582
let do_global_extract edrv (tname,p,t,_,_) =
583
  let lib = edrv.Mlw_driver.drv_lib in
584
585
586
587
  try
    let mm, thm = Env.read_lib_file lib p in
    try
      let m = Mstr.find t mm in
588
      do_extract_module edrv tname m
589
590
    with Not_found ->
      let th = Mstr.find t thm in
591
      do_extract_theory edrv tname th
592
  with Env.LibFileNotFound _ | Not_found -> try
593
    let format = Opt.get_def "why" !opt_parser in
594
    let env = Env.env_of_library lib in
595
    let th = Env.read_theory ~format env p t in
596
    do_extract_theory edrv tname th
597
598
599
600
  with Env.LibFileNotFound _ | Env.TheoryNotFound _ ->
    eprintf "Theory/module '%s' not found.@." tname;
    exit 1

601
let do_extract_theory_from env fname m (tname,_,t,_,_) =
602
603
604
605
  let th = try Mstr.find t m with Not_found ->
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
  in
606
  do_extract_theory env ~fname tname th
607

608
let do_extract_module_from env fname mm thm (tname,_,t,_,_) =
609
  try
610
    let m = Mstr.find t mm in do_extract_module env ~fname tname m
611
  with Not_found -> try
612
    let th = Mstr.find t thm in do_extract_theory env ~fname tname th
613
614
615
616
  with Not_found ->
    eprintf "Theory/module '%s' not found in file '%s'.@." tname fname;
    exit 1

617
618
let do_local_extract edrv fname cin tlist =
  let lib = edrv.Mlw_driver.drv_lib in
619
620
621
  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
622
      let do_m t m thm =
623
        do_extract_module edrv ~fname t m; Mstr.remove t thm in
624
      let thm = Mstr.fold do_m mm thm in
625
      Mstr.iter (fun t th -> do_extract_theory edrv ~fname t th) thm
626
    end else
627
      Queue.iter (do_extract_module_from edrv fname mm thm) tlist
628
  end else begin
629
    let env = Env.env_of_library lib in
630
631
632
    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
633
      let do_th _ (t,th) = do_extract_theory edrv ~fname t th in
634
635
      Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
    else
636
      Queue.iter (do_extract_theory_from edrv fname m) tlist
637
638
  end

639
640
641
let total_annot_tokens = ref 0
let total_program_tokens = ref 0

642
let do_input env drv edrv = function
643
644
  | None, _ when Debug.test_flag Typing.debug_type_only ||
                 Debug.test_flag Typing.debug_parse_only ->
645
      ()
646
  | None, tlist when edrv <> None ->
647
      Queue.iter (do_global_extract (Opt.get edrv)) tlist
648
  | None, tlist ->
MARCHE Claude's avatar
MARCHE Claude committed
649
      Queue.iter (do_global_theory env drv) tlist
650
  | Some f, tlist ->
651
652
653
654
      let fname, cin = match f with
        | "-" -> "stdin", stdin
        | f   -> f, open_in f
      in
655
      if !opt_token_count then begin
656
657
658
        let lb = Lexing.from_channel cin in
        let a,p = Lexer.token_counter lb in
        close_in cin;
659
660
661
662
663
664
665
666
667
668
        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
669
      end else if edrv <> None then begin
670
        do_local_extract (Opt.get edrv) fname cin tlist;
671
672
        close_in cin
      end else begin
673
674
        let m = Env.read_channel ?format:!opt_parser env fname cin in
        close_in cin;
675
        if Debug.test_flag Typing.debug_type_only then
676
          ()
MARCHE Claude's avatar
MARCHE Claude committed
677
        else
678
679
          if Queue.is_empty tlist then
            let glist = Queue.create () in
680
            let elist = Queue.create () in
681
            let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
682
            let do_th _ (t,th) = do_theory env drv fname t th glist elist in
683
684
685
            Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
          else
            Queue.iter (do_local_theory env drv fname m) tlist
686
      end
MARCHE Claude's avatar
MARCHE Claude committed
687

688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
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 []

703
704
let () =
  try
705
    let env = Env.create_env !opt_loadpath in
706
707
    let drv = Opt.map (load_driver env) !opt_driver in
    let edrv = Opt.map (load_driver_extract env) !opt_extract in
708
    Queue.iter (do_input env drv edrv) opt_queue;
709
    if !opt_token_count then
Andrei Paskevich's avatar
Andrei Paskevich committed
710
      Format.printf "Total: %d annot/%d programs, ratio = %.3f@."
711
712
        !total_annot_tokens !total_program_tokens
        ((float !total_annot_tokens) /. (float !total_program_tokens))
713
  with e when not (Debug.test_flag Debug.stack_trace) ->
714
    eprintf "%a@." Exn_printer.exn_printer e;
715
    exit 1
716

717
(*
718
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
719
compile-command: "unset LANG; make -C .. byte"
720
End:
721
*)