main.ml 28.4 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_exec = Queue.create ()
33
let opt_trans = ref []
34
let opt_metas = ref []
35

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

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

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

77
78
79
80
81
82
83
84
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

85
86
let add_opt_exec x = Queue.push x opt_exec

87
let add_opt_trans x = opt_trans := x::!opt_trans
88

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

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

115
116
117
let opt_print_libdir = ref false
let opt_print_datadir = ref false

118
119
120
121
let opt_print_theory = ref false
let opt_print_namespace = ref false
let opt_list_transforms = ref false
let opt_list_printers = ref false
122
let opt_list_provers = ref false
123
let opt_list_formats = ref false
124
let opt_list_metas = ref false
125

126
let opt_token_count = ref false
127
let opt_version = ref false
128
129
130
131

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

226
let () = try
227
228
  Arg.parse option_list add_opt_file usage_msg;

229
230
231
232
  if !opt_version then begin
    printf "%s@." version_msg;
    exit 0
  end;
233
234
235
236
237
238
239
240
  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;
241

François Bobot's avatar
François Bobot committed
242
  (** Configuration *)
243
  let config = read_config !opt_config in
244
  let config = List.fold_left merge_config config !opt_extra in
François Bobot's avatar
François Bobot committed
245
246
247
  let main = get_main config in
  Whyconf.load_plugins main;

248
  Debug.Args.set_flags_selected ();
249

François Bobot's avatar
François Bobot committed
250
251
  (** listings*)

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

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

313
314
315
  if !opt_prover <> None && !opt_driver <> None then begin
    eprintf "Options '-P'/'--prover' and \
      '-D'/'--driver' cannot be used together.@.";
316
317
    exit 1
  end;
318

319
  if !opt_output <> None
320
  && !opt_driver = None && !opt_prover = None && !opt_extract = None then begin
321
322
323
324
325
    eprintf
      "Option '-o'/'--output' requires a prover, a driver, or option '-E'.@.";
    exit 1
  end;

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

343
  if !opt_extract <> None && !opt_output = None then begin
344
345
346
347
348
    eprintf
      "Option '-E'/'--extract' require a directory to output the result.@.";
    exit 1
  end;

349
350
351
352
353
  if !opt_bisect && !opt_output = None then begin
    eprintf "Option '--bisect' require a directory to output the result.@.";
    exit 1
  end;

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

377
378
379
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
380
381

let timelimit = match !opt_timelimit with
382
383
384
  | None -> 10
  | Some i when i <= 0 -> 0
  | Some i -> i
385

386
let memlimit = match !opt_memlimit with
387
388
389
390
  | None -> 0
  | Some i when i <= 0 -> 0
  | Some i -> i

391
let print_th_namespace fmt th =
392
  Pretty.print_namespace fmt th.th_name.Ident.id_string th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
393

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

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

424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
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
439

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

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

492
let do_theory env drv fname tname th glist elist =
493
494
495
496
  if !opt_print_theory then
    printf "%a@." Pretty.print_theory th
  else if !opt_print_namespace then
    printf "%a@." print_th_namespace th
497
498
499
500
501
502
503
504
  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
505
      let drv = Opt.get drv in
506
      let task = Task.use_export !opt_task th in
507
508
      do_tasks env drv fname tname th task
    end
509
  else begin
510
    let add acc (x,l) =
511
512
513
514
      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
515
      Decl.Spr.add pr acc
516
    in
517
    let drv = Opt.get drv in
518
519
520
    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
521
522
523
524
525
526
527
528
529
530
531
532
533
    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
        | [] ->
534
          let t = Mlw_interp.eval_global_term env th.th_known t in
MARCHE Claude's avatar
MARCHE Claude committed
535
          printf "@[<hov 2>Evaluation of %s:@ %a@]@." x Pretty.print_term t
536
537
538
539
540
        | _ ->
          eprintf "Symbol '%s' is not a constant in theory '%s'.@." x tname;
          exit 1
    in
    Queue.iter eval elist
541
  end
MARCHE Claude's avatar
MARCHE Claude committed
542

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

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

558
559
560
(* program execution *)

let do_exec env fname cin exec =
561
  if !opt_parser = Some "whyml" || Filename.check_suffix fname ".mlw" then
562
563
564
    let lib = Mlw_main.library_of_env env in
    let mm, _thm = Mlw_main.read_channel lib [] fname cin in
    let do_exec x =
565
      let mid,name =
566
567
568
        match Str.split (Str.regexp "\\.") x with
          | [m;i] -> m,i
          | _ ->
569
            Format.eprintf
570
571
572
573
574
575
576
              "'--exec argument must be of the form 'module.ident'@.";
            exit 2
      in
      let m = try Mstr.find mid mm with Not_found ->
        eprintf "Module '%s' not found.@." mid;
        exit 1
      in
577
      let ps = try Mlw_module.ns_find_ps m.Mlw_module.mod_export [name]
578
579
580
581
        with Not_found ->
          eprintf "Function '%s' not found in module '%s'.@." name mid;
          exit 1
      in
582
583
584
585
586
587
588
589
590
591
592
593
      match Mlw_decl.find_definition m.Mlw_module.mod_known ps with
        | None ->
          eprintf "Function %s.%s has no definition.@." mid name;
          exit 1
        | Some d ->
          let lam = d.Mlw_expr.fun_lambda in
          match lam.Mlw_expr.l_args with
            | [pvs] when Mlw_ty.ity_equal pvs.Mlw_ty.pv_ity Mlw_ty.ity_unit ->
              printf "@[<hov 2>Execution of %s ():@\n" x;
              let body = lam.Mlw_expr.l_expr in
              printf "type  : @[%a@]@\n"
                Mlw_pretty.print_vty body.Mlw_expr.e_vty;
594
595
            (* printf "effect: %a@\n" *)
            (*   Mlw_pretty.print_effect body.Mlw_expr.e_effect; *)
596
597
598
599
600
601
602
603
604
605
606
              let res, st =
                Mlw_interp.eval_global_expr env
                  m.Mlw_module.mod_known m.Mlw_module.mod_theory.Theory.th_known
                  lam.Mlw_expr.l_expr
              in
              printf "result: %a@\nstate: %a@]@." 
                Mlw_interp.print_result res
                Mlw_interp.print_state st
            | _ ->
              eprintf "Only functions with one unit argument can be executed.@.";
              exit 1
607
608
609
610
611
612
613
614
615
616
617
    in
    Queue.iter do_exec exec
(*
    if Queue.is_empty tlist then begin
      let do_m t m thm =
        do_extract_module edrv ~fname t m; Mstr.remove t thm in
      let thm = Mstr.fold do_m mm thm in
      Mstr.iter (fun t th -> do_extract_theory edrv ~fname t th) thm
    end else
      Queue.iter (do_extract_module_from edrv fname mm thm) tlist
*)
618
 else
619
620
621
622
623
  begin
    Format.eprintf "'--exec is available only for mlw files@.";
    exit 2
  end

624
625
(* program extraction *)

626
let extract_to ?fname th extract =
627
  let dir = Opt.get !opt_output in
628
  let file = Filename.concat dir (Mlw_ocaml.extract_filename ?fname th) in
629
630
631
632
633
634
635
636
637
  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
638

639
let do_extract_theory edrv ?fname tname th =
640
641
  let extract file ?old fmt = ignore (old);
    Debug.dprintf Mlw_ocaml.debug "extract theory %s to file %s@." tname file;
642
    Mlw_ocaml.extract_theory edrv ?old ?fname fmt th
643
644
645
  in
  extract_to ?fname th extract

646
let do_extract_module edrv ?fname tname m =
647
648
  let extract file ?old fmt = ignore (old);
    Debug.dprintf Mlw_ocaml.debug "extract module %s to file %s@." tname file;
649
    Mlw_ocaml.extract_module edrv ?old ?fname fmt m
650
651
  in
  extract_to ?fname m.Mlw_module.mod_theory extract
652

653
let do_global_extract edrv (tname,p,t,_,_) =
654
  let lib = edrv.Mlw_driver.drv_lib in
655
656
657
658
  try
    let mm, thm = Env.read_lib_file lib p in
    try
      let m = Mstr.find t mm in
659
      do_extract_module edrv tname m
660
661
    with Not_found ->
      let th = Mstr.find t thm in
662
      do_extract_theory edrv tname th
663
  with Env.LibFileNotFound _ | Not_found -> try
664
    let format = Opt.get_def "why" !opt_parser in
665
    let env = Env.env_of_library lib in
666
    let th = Env.read_theory ~format env p t in
667
    do_extract_theory edrv tname th
668
669
670
671
  with Env.LibFileNotFound _ | Env.TheoryNotFound _ ->
    eprintf "Theory/module '%s' not found.@." tname;
    exit 1

672
let do_extract_theory_from env fname m (tname,_,t,_,_) =
673
674
675
676
  let th = try Mstr.find t m with Not_found ->
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
  in
677
  do_extract_theory env ~fname tname th
678

679
let do_extract_module_from env fname mm thm (tname,_,t,_,_) =
680
  try
681
    let m = Mstr.find t mm in do_extract_module env ~fname tname m
682
  with Not_found -> try
683
    let th = Mstr.find t thm in do_extract_theory env ~fname tname th
684
685
686
687
  with Not_found ->
    eprintf "Theory/module '%s' not found in file '%s'.@." tname fname;
    exit 1

688
689
let do_local_extract edrv fname cin tlist =
  let lib = edrv.Mlw_driver.drv_lib in
690
691
692
  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
693
      let do_m t m thm =
694
        do_extract_module edrv ~fname t m; Mstr.remove t thm in
695
      let thm = Mstr.fold do_m mm thm in
696
      Mstr.iter (fun t th -> do_extract_theory edrv ~fname t th) thm
697
    end else
698
      Queue.iter (do_extract_module_from edrv fname mm thm) tlist
699
  end else begin
700
    let env = Env.env_of_library lib in
701
702
703
    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
704
      let do_th _ (t,th) = do_extract_theory edrv ~fname t th in
705
706
      Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
    else
707
      Queue.iter (do_extract_theory_from edrv fname m) tlist
708
709
  end

710
711
712
let total_annot_tokens = ref 0
let total_program_tokens = ref 0

713
let do_input env drv edrv = function
714
715
  | None, _ when Debug.test_flag Typing.debug_type_only ||
                 Debug.test_flag Typing.debug_parse_only ->
716
      ()
717
  | None, tlist when edrv <> None ->
718
      Queue.iter (do_global_extract (Opt.get edrv)) tlist
719
  | None, tlist ->
MARCHE Claude's avatar
MARCHE Claude committed
720
      Queue.iter (do_global_theory env drv) tlist
721
  | Some f, tlist ->
722
723
724
725
      let fname, cin = match f with
        | "-" -> "stdin", stdin
        | f   -> f, open_in f
      in
726
      if !opt_token_count then
727
728
729
730
        begin
          let lb = Lexing.from_channel cin in
          let a,p = Lexer.token_counter lb in
          close_in cin;
731
          if a = 0 then
732
733
734
735
            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;
736
737
            end
          else
738
739
740
741
742
743
            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
744
745
746
        end
      else
        if edrv <> None then
747
748
749
          begin
            do_local_extract (Opt.get edrv) fname cin tlist;
            close_in cin
750
751
          end
        else
752
753
          if not (Queue.is_empty opt_exec) then
            do_exec env fname cin opt_exec
754
          else
755
756
757
758
759
760
761
762
763
764
            begin
              let m = Env.read_channel ?format:!opt_parser env fname cin in
              close_in cin;
              if Debug.test_flag Typing.debug_type_only then
                ()
              else
                if Queue.is_empty tlist then
                  let glist = Queue.create () in
                  let elist = Queue.create () in
                  let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
765
766
                  let do_th _ (t,th) =
                    do_theory env drv fname t th glist elist
767
768
769
770
771
                  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
            end
MARCHE Claude's avatar
MARCHE Claude committed
772

773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
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 []

788
789
let () =
  try
790
    let env = Env.create_env !opt_loadpath in
791
792
    let drv = Opt.map (load_driver env) !opt_driver in
    let edrv = Opt.map (load_driver_extract env) !opt_extract in
793
    Queue.iter (do_input env drv edrv) opt_queue;
794
    if !opt_token_count then
Andrei Paskevich's avatar
Andrei Paskevich committed
795
      Format.printf "Total: %d annot/%d programs, ratio = %.3f@."
796
797
        !total_annot_tokens !total_program_tokens
        ((float !total_annot_tokens) /. (float !total_program_tokens))
798
  with e when not (Debug.test_flag Debug.stack_trace) ->
799
    eprintf "%a@." Exn_printer.exn_printer e;
800
    exit 1
801

802
(*
803
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
804
compile-command: "unset LANG; make -C .. byte"
805
End:
806
*)