why3session_output.ml 3.68 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
(********************************************************************)

open Why3
open Why3session_lib
open Session
open Format

(**
   TODO add_transformation,...

   TODO:
    filter_state
    filter_time
    filter_?

**)

let opt_output_dir = ref None

let spec =
  ["--output", Arg.String (fun s -> opt_output_dir := Some s),
31
   " set the directory where to output the files";
32
   "-o", Arg.String (fun s -> opt_output_dir := Some s),
33
   " same as --output"
34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
  ]@
    (force_obsolete_spec @ filter_spec @ common_options)

type action =
  | Copy
  | CopyArchive
  | Mod

let rec interactive to_remove =
  eprintf "Do you want to replace the external proof %a (y/n)@."
    print_external_proof to_remove;
  let answer = read_line () in
  match answer with
    | "y" -> true
    | "n" -> false
    | _ -> interactive to_remove

let keygen ?parent:_ _ = ()

let fname_printer = Ident.create_ident_printer []

let run_one env config filters dir fname =
56
  let env_session,_,_ =
57 58 59 60 61 62 63 64 65 66 67 68
    read_update_session ~allow_obsolete:!opt_force_obsolete env config fname in
  iter_session (fun file ->
    let fname = Filename.basename file.file_name in
    let fname = try Filename.chop_extension fname with _ -> fname in
    iter_file (fun th ->
      let tname = th.theory_name.Ident.id_string in
      theory_iter_proof_attempt_by_filter filters
        (fun pr ->
          let task =
            Opt.get (goal_task_option pr.proof_parent) in
          match load_prover env_session pr.proof_prover with
          | None ->
69
            (* In fact That is a bad reason we can always output know? *)
70 71 72 73
            eprintf "Can't@ output@ task@ for@ prover@ %a@ not@ installed@."
              Whyconf.print_prover pr.proof_prover
          | Some lp ->
            let dest = Driver.file_of_task lp.prover_driver fname tname task in
74
            (* Uniquify the filename before the extension if it exists*)
75
            let i = try String.rindex dest '.' with _ -> String.length dest in
76
            (* Before extension *)
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
            let name = (String.sub dest 0 i) in
            let name = Ident.string_unique fname_printer name 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 lp.prover_driver
              (formatter_of_out_channel cout) task;
            close_out cout
        ) th
    ) file
  ) env_session.session

let run () =
  let env,config,should_exit1 = read_env_spec () in
  let filters,should_exit2 = read_filter_spec config in
  if should_exit1 || should_exit2 then exit 1;
92
  (* sanitize --to-prover and --to-known-prover for Copy* *)
93 94 95 96 97 98 99 100 101 102 103 104 105 106
  match !opt_output_dir with
  | None ->
    eprintf "The@ option@ --output-dir/-o@ must@ be@ set@.";
    exit 1
  | Some dir ->
    try
      iter_files (run_one env config filters dir)
    with OutdatedSession as e ->
      eprintf "@.%a@ You@ can@ allow@ it@ with@ the@ option@ -F.@."
        Exn_printer.exn_printer e


let cmd =
  { cmd_spec     = spec;
107
    cmd_desc     = "output file send to the prover";
108 109 110
    cmd_name     = "output";
    cmd_run      = run;
  }