main.ml 15.8 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
8 9 10 11 12 13 14 15 16 17 18 19
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

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

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

35
let opt_queue = Queue.create ()
36

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

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

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

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

let add_opt_trans x = opt_trans := x::!opt_trans
80

81 82 83
let add_opt_meta meta_name meta_arg =
  opt_metas := (meta_name,meta_arg)::!opt_metas

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

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

let opt_parse_only = ref false
let opt_type_only = ref false
let opt_debug = ref false

let option_list = Arg.align [
  "-", Arg.Unit (fun () -> add_opt_file "-"),
      " Read the input file from stdin";
110
  "-T", Arg.String add_opt_theory,
111 112
      "<theory> Select <theory> in the input file or in the library";
  "--theory", Arg.String add_opt_theory,
113 114
      " same as -T";
  "-G", Arg.String add_opt_goal,
115 116
      "<goal> Select <goal> in the last selected theory";
  "--goal", Arg.String add_opt_goal,
117
      " same as -G";
118 119 120 121 122
  "-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";
  "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
123
      "<dir> Add <dir> to the library search path";
124 125 126 127 128 129 130 131
  "--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";
132 133 134 135
  "-F", Arg.String (fun s -> opt_parser := Some s),
      "<format> Input format (default: \"why\")";
  "--format", Arg.String (fun s -> opt_parser := Some s),
      " same as -F";
136
  "-t", Arg.Int (fun i -> opt_timelimit := Some i),
137 138
      "<sec> Set the prover's time limit (default=10, no limit=0)";
  "--timelimit", Arg.Int (fun i -> opt_timelimit := Some i),
139 140
      " same as -t";
  "-m", Arg.Int (fun i -> opt_memlimit := Some i),
141 142
      "<MiB> Set the prover's memory limit (default: no limit)";
  "--memlimit", Arg.Int (fun i -> opt_timelimit := Some i),
143
      " same as -m";
144 145 146 147 148
  "-M", 
  begin let meta_opt = ref "" in 
        Arg.Tuple ([Arg.Set_string meta_opt;
                    Arg.String (fun s -> add_opt_meta !meta_opt s)]) end,
    "<meta_name>,<string> Add a meta option to each tasks";
149
  "-D", Arg.String (fun s -> opt_driver := Some s),
150
      "<file> Specify a prover's driver (conflicts with -P)";
151 152 153 154 155 156 157 158 159 160 161 162 163 164
  "--driver", Arg.String (fun s -> opt_driver := Some s),
      " 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";
  "--print-theory", Arg.Set opt_print_theory,
      " Print the selected theories";
  "--print-namespace", Arg.Set opt_print_namespace,
      " Print the namespaces of selected theories";
  "--list-transforms", Arg.Set opt_list_transforms,
      " List the registered transformations";
  "--list-printers", Arg.Set opt_list_printers,
      " List the registered printers";
165 166
  "--list-provers", Arg.Set opt_list_provers,
      " List the known provers";
167 168
  "--list-formats", Arg.Set opt_list_formats,
      " List the known input formats";
169 170
  "--list-metas", Arg.Set opt_list_metas,
    " List the known metas option (currently only with one string argument)";
171 172 173 174 175
  "--parse-only", Arg.Set opt_parse_only,
      " Stop after parsing";
  "--type-only", Arg.Set opt_type_only,
      " Stop after type checking";
  "--debug", Arg.Set opt_debug,
176 177 178 179
      " Set the debug flag";
  "-a", Arg.String add_opt_trans, 
  "<transformation> Add a transformation to apply to the task" ;
  "--apply-transform", Arg.String add_opt_trans, 
180
  " same as -a" ]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
181

182 183 184
let () =
  Arg.parse option_list add_opt_file usage_msg;

185 186
  (* TODO? : Since drivers can dynlink ml code they can add printer, 
     transformations, ... So drivers should be loaded before listing *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
187
  if !opt_list_transforms then begin
188
    printf "@[<hov 2>Transed non-splitting transformations:@\n%a@]@\n@."
189
      (Pp.print_list Pp.newline Pp.string)
190 191
      (List.sort String.compare (Trans.list_transforms ()));
    printf "@[<hov 2>Transed splitting transformations:@\n%a@]@\n@."
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
192
      (Pp.print_list Pp.newline Pp.string)
193
      (List.sort String.compare (Trans.list_transforms_l ()));
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
194
  end;
195
  if !opt_list_printers then begin
196
    printf "@[<hov 2>Transed printers:@\n%a@]@\n@."
197
      (Pp.print_list Pp.newline Pp.string)
198
      (List.sort String.compare (Printer.list_printers ()))
199 200 201 202 203 204 205 206 207 208
  end;
  if !opt_list_formats then begin
    let print1 fmt s = fprintf fmt "%S" s in
    let print fmt (p, l) = 
      fprintf fmt "%s [%a]" p (Pp.print_list Pp.comma print1) l
    in
    printf "@[<hov 2>Known input formats:@\n%a@]@." 
      (Pp.print_list Pp.newline print)
      (List.sort Pervasives.compare (Env.list_formats ()))
  end;
209 210 211 212 213 214
  if !opt_list_provers then begin
    let config = read_config !opt_config in
    let print fmt s prover = fprintf fmt "%s (%s)@\n" s prover.name in
    let print fmt m = Mstr.iter (print fmt) m in
    printf "@[<hov 2>Known provers:@\n%a@]@." print config.provers
  end;
215 216 217 218 219 220 221 222 223 224 225 226
  if !opt_list_metas then begin
    let metas = list_metas () in
    let filter (s,args) =
      match args with
        | [MTstring] -> is_meta_excl s
        | _ -> false in
    let metas = List.filter filter metas in
    let metas = List.map fst metas in
    printf "@[<hov 2>Known metas:@\n%a@]@\n@."
      (Pp.print_list Pp.newline Pp.string)
      (List.sort String.compare metas)
  end;
227
  if !opt_list_transforms || !opt_list_printers || !opt_list_provers ||
228
     !opt_list_formats || !opt_list_metas
229
  then exit 0;
230 231 232 233 234 235

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

236 237 238
  if !opt_prover <> None && !opt_driver <> None then begin
    eprintf "Options '-P'/'--prover' and \
      '-D'/'--driver' cannot be used together.@.";
239 240
    exit 1
  end;
241 242 243 244 245 246 247

  if !opt_prover = None then begin
    if !opt_driver = None && !opt_output <> None then begin
      eprintf "Option '-o'/'--output' requires a prover or a driver.@.";
      exit 1
    end;
    if !opt_timelimit <> None then begin
248
      eprintf "Option '-t'/'--timelimit' requires a prover.@.";
249 250 251
      exit 1
    end;
    if !opt_memlimit <> None then begin
252
      eprintf "Option '-m'/'--memlimit' requires a prover.@.";
253 254 255 256
      exit 1
    end;
    if !opt_driver = None && not !opt_print_namespace then
      opt_print_theory := true
257 258
  end;

259 260 261 262 263 264 265 266 267 268 269 270 271 272 273
  let config = try read_config !opt_config with Not_found ->
    option_iter (eprintf "Config file '%s' not found.@.") !opt_config;
    option_iter
      (eprintf "No config file found (required by '-P %s').@.") !opt_prover;
    if !opt_config <> None || !opt_prover <> None then exit 1;
    { conf_file = "";
      loadpath  = [];
      timelimit = None;
      memlimit  = None;
      provers   = Mstr.empty }
  in

  opt_loadpath := List.rev_append !opt_loadpath config.loadpath;
  if !opt_timelimit = None then opt_timelimit := config.timelimit;
  if !opt_memlimit  = None then opt_memlimit  := config.memlimit;
274
  begin match !opt_prover with
275 276
  | Some s ->
      let prover = try Mstr.find s config.provers with
277
        | Not_found -> eprintf "Driver %s not found.@." s; exit 1
278
      in
279
      opt_command := Some prover.command;
280 281
      opt_driver := Some prover.driver
  | None ->
282 283 284
    () end;
  let add_meta task (meta,s) = add_meta task meta [MAstr s] in
  opt_task := List.fold_left add_meta !opt_task !opt_metas
285 286

let timelimit = match !opt_timelimit with
287 288 289
  | None -> 10
  | Some i when i <= 0 -> 0
  | Some i -> i
290

291
let memlimit = match !opt_memlimit with
292 293 294 295 296
  | None -> 0
  | Some i when i <= 0 -> 0
  | Some i -> i

let debug = !opt_debug
297

298
let print_th_namespace fmt th =
299
  Pretty.print_namespace fmt th.th_name.Ident.id_string th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
300

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

303
let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
304 305
  match !opt_output, !opt_command with
    | None, Some command ->
306
        let res =
307
          Driver.prove_task ~debug ~command ~timelimit ~memlimit drv task ()
308
        in
309
        printf "%s %s %s : %a@." fname tname
310
          (task_goal task).Decl.pr_name.Ident.id_string
311 312
          Call_provers.print_prover_result res
    | None, None ->
313
        Driver.print_task ~debug drv std_formatter task
314
    | Some dir, _ ->
315 316 317 318
        let fname = Filename.basename fname in
        let fname =
          try Filename.chop_extension fname with _ -> fname
        in
319
        let tname = th.th_name.Ident.id_string in
320
        let dest = Driver.file_of_task drv fname tname task in
321 322 323 324 325
        (* 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
326
        Driver.print_task ~debug drv (formatter_of_out_channel cout) task;
327 328
        close_out cout

329
let do_tasks env drv fname tname th trans task =
330
  let lookup acc t = 
331 332
    (try t, Trans.singleton (Trans.lookup_transform t env) with
       Trans.UnknownTrans _ -> t, Trans.lookup_transform_l t env) :: acc
333
  in
334
  let transl = List.fold_left lookup [] trans in
335 336
  let apply tasks (s, tr) = 
    try
337 338
      if debug then Format.eprintf "apply transformation %s@." s;
      let l = List.fold_left 
339
        (fun acc task -> 
340
           List.rev_append (Trans.apply tr task) acc) [] tasks in
341
      List.rev l (* In order to keep the order for 1-1 transformation *)
342 343 344 345 346 347
    with e when not debug ->
      Format.eprintf "failure in transformation %s@." s;
      raise e
  in
  let tasks = List.fold_left apply [task] transl in
  List.iter (do_task drv fname tname th) tasks
348

349
let do_theory env drv fname tname th trans glist =
350 351 352 353 354
  if !opt_print_theory then
    printf "%a@." Pretty.print_theory th
  else if !opt_print_namespace then
    printf "%a@." print_th_namespace th
  else begin
355
    let add (accm,accs) (x,l,trans) =
356 357 358 359
      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
360
      let accs = Decl.Spr.add pr accs in
361
      (pr,trans)::accm,accs
362 363
    in
    let drv = Util.of_option drv in
364 365
    if Queue.is_empty glist 
    then 
366
      let tasks = List.rev (split_theory ~init:!opt_task th None) in
367
      let do_tasks = do_tasks env drv fname tname th trans in
368 369 370
      List.iter do_tasks tasks
    else 
      let prtrans,prs = Queue.fold add ([],Decl.Spr.empty) glist in
371
      let tasks = split_theory ~init:!opt_task th (Some prs) in
372 373 374 375 376 377
      let recover_pr mpr task =
        let pr = task_goal task in
        Decl.Mpr.add pr task mpr in
      let mpr = List.fold_left recover_pr Decl.Mpr.empty tasks in
      let do_tasks (pr,trans) =
        let task = Decl.Mpr.find pr mpr in
378
        do_tasks env drv fname tname th trans task in
379
      List.iter do_tasks (List.rev prtrans)
380
  end
MARCHE Claude's avatar
MARCHE Claude committed
381

382
let do_global_theory env drv (tname,p,t,glist,trans) =
383 384 385
  let th = try Env.find_theory env p t with Env.TheoryNotFound _ ->
    eprintf "Theory '%s' not found.@." tname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
386
  in
387
  do_theory env drv "lib" tname th trans glist
MARCHE Claude's avatar
MARCHE Claude committed
388

389
let do_local_theory env drv fname m (tname,_,t,glist,trans) =
390 391 392
  let th = try Mnm.find t m with Not_found ->
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
393
  in
394
  do_theory env drv fname tname th trans glist
395 396

let do_input env drv = function
397
  | None, _, _ when !opt_parse_only || !opt_type_only ->
398
      ()
399
  | None, tlist, _ ->
400
      Queue.iter (do_global_theory env drv) tlist
401
  | Some f, tlist, trans ->
402 403 404 405
      let fname, cin = match f with
        | "-" -> "stdin", stdin
        | f   -> f, open_in f
      in
406 407
      let report = Env.report ?name:!opt_parser fname in
      try
408 409 410 411 412 413 414 415 416 417 418
	let m = 
	  Env.read_channel ?name:!opt_parser ~debug:!opt_debug 
	    ~parse_only:!opt_parse_only ~type_only:!opt_type_only
	    env fname cin 
	in
        close_in cin;
        if !opt_type_only then 
	  ()
        else 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
419
          let do_th _ (t,th) = do_theory env drv fname t th trans glist in
420 421
          Ident.Mid.iter do_th (Mnm.fold add_th m Ident.Mid.empty)
        else
422
          Queue.iter (do_local_theory env drv fname m) tlist
423 424
      with 
	| Loc.Located (loc, e) ->
425
	    eprintf "@[%a%a@]@." Loc.report_position loc report e; exit 1
426
	| e ->
427
	    eprintf "@[%a@]@." report e; exit 1
MARCHE Claude's avatar
MARCHE Claude committed
428

429 430
let () =
  try
431
    let env = Env.create_env (Typing.retrieve !opt_loadpath) in
432
    let drv = Util.option_map (load_driver env) !opt_driver in
433
    Queue.iter (do_input env drv) opt_queue
434
  with e when not debug ->
435
    eprintf "%a@." Exn_printer.exn_printer e;
436
    exit 1
437

438
(*
439
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
440
compile-command: "unset LANG; make -C .. byte"
441
End:
442
*)