why3session add output command same than --output of why3 command but

can be used with the task in a session

Makefile.in

@@ -609,9 +609,9 @@ install_local: bin/why3replayer
 # Session
 ###############
 
-SESSION_FILES = why3session_lib why3session_copy why3session_info \
-		why3session_latex why3session_html why3session_rm \
-		why3session
+SESSION_FILES = why3session_lib why3session_copy why3session_info	\
+		why3session_latex why3session_html why3session_rm	\
+		why3session_output why3session
 
 SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
 

src/session/session.ml

@@ -292,6 +292,10 @@ let iter_transf f t =
 
 let iter_metas f t = f t.metas_goal
 
+let iter_file f fi = List.iter f fi.file_theories
+
+let iter_session f s = PHstr.iter (fun _ th -> f th) s.session_files
+
 let goal_iter f g =
   PHprover.iter
     (fun _ a -> f (Proof_attempt a)) g.goal_external_proofs;

src/session/session.mli

@@ -473,6 +473,10 @@ val iter_transf :
   ('key goal -> unit) -> 'key transf -> unit
 val iter_metas :
   ('key goal -> unit) -> 'key metas -> unit
+val iter_file :
+  ('key theory -> unit) -> 'key file -> unit
+val iter_session :
+  ('key file -> unit) -> 'key session -> unit
 
 
 val goal_iter : ('key any -> unit) -> 'key goal -> unit

src/why3session/why3session.ml

@@ -22,6 +22,7 @@ let cmds =
     Why3session_copy.cmd_copy;
     Why3session_copy.cmd_archive;
     Why3session_rm.cmd;
+    Why3session_output.cmd;
   |]
 
 let exec_name = Sys.argv.(0)

src/why3session/why3session_lib.ml

@@ -124,6 +124,8 @@ let add_filter_three r = function
 
 let opt_three r = Arg.Symbol (["yes";"no";"all"], add_filter_three r)
 
+let opt_status = ref []
+
 let filter_spec =
   ["--filter-prover", Arg.String add_filter_prover,
    " [name,version[,alternative]|id] \
@@ -136,6 +138,21 @@ the proof containing this prover are selected";
    " no: only parent goal not verified, yes: only verified (default all)";
    "--filter-verified", opt_three opt_filter_verified,
    " no: only not verified, yes: only verified (default all)";
+   "--filter-highfailure",
+   Arg.Unit (fun () -> opt_status := Call_provers.HighFailure::!opt_status),
+   " filter the call that fail in an unexpeted way";
+   "--filter-valid",
+   Arg.Unit (fun () -> opt_status := Call_provers.Valid::!opt_status),
+   " filter the valid goals (can be obsolete)";
+   "--filter-invalid",
+   Arg.Unit (fun () -> opt_status := Call_provers.Invalid::!opt_status),
+   " filter the invalid goals";
+   "--filter-unknown",
+   Arg.String (fun s -> opt_status := Call_provers.Unknown s::!opt_status),
+   " filter when the prover reports it can't determine if the task is valid";
+   "--filter-failure",
+   Arg.String (fun s -> opt_status := Call_provers.Failure s::!opt_status),
+   " filter when the prover reports a failure";
 ]
 
 type filters =
@@ -144,6 +161,7 @@ type filters =
       archived : filter_three;
       verified : filter_three;
       verified_goal : filter_three;
+      status : Call_provers.prover_answer list; (* if empty : any answer *)
     }
 
 let provers_of_filter_prover whyconf = function
@@ -175,9 +193,10 @@ let read_filter_spec whyconf : filters * bool =
    archived = !opt_filter_archived;
    verified = !opt_filter_verified;
    verified_goal = !opt_filter_verified_goal;
+   status = !opt_status;
   },!should_exit
 
-let session_iter_proof_attempt_by_filter filters f session =
+let iter_proof_attempt_by_filter iter filters f session =
   (** provers *)
   let iter_provers a =
     if C.Sprover.mem a.S.proof_prover filters.provers then f a in
@@ -199,8 +218,17 @@ let session_iter_proof_attempt_by_filter filters f session =
     (fun a -> a.S.proof_parent.S.goal_verified) in
   (** verified *)
   let f = three_value f filters.verified S.proof_verified in
-  S.session_iter_proof_attempt f session
-
+  (** status *)
+  let f = if filters.status = [] then f else
+      (fun a -> match a.S.proof_state with
+      | S.Done pr when List.mem pr.Call_provers.pr_answer filters.status -> f a
+      | _ -> ()) in
+  iter f session
+
+let theory_iter_proof_attempt_by_filter filters f th =
+  iter_proof_attempt_by_filter S.theory_iter_proof_attempt filters f th
+let session_iter_proof_attempt_by_filter filters f s =
+  iter_proof_attempt_by_filter S.session_iter_proof_attempt filters f s
 
 let set_filter_verified_goal t = opt_filter_verified_goal := t
 

src/why3session/why3session_lib.mli

@@ -64,6 +64,9 @@ val filter_spec : spec_list
 
 val read_filter_spec : Whyconf.config -> filters * bool
 
+val theory_iter_proof_attempt_by_filter :
+  filters ->
+  ('key Session.proof_attempt -> unit) -> 'key Session.theory -> unit
 val session_iter_proof_attempt_by_filter :
   filters ->
   ('key Session.proof_attempt -> unit) -> 'key Session.session -> unit

src/why3session/why3session_output.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  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.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+open Why3
+open Why3session_lib
+open Whyconf
+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),
+   " Set the directory where to output the files";
+   "-o", Arg.String (fun s -> opt_output_dir := Some s),
+   " Same as --output"
+  ]@
+    (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 =
+  let env_session,_ =
+    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 ->
+            (** In fact That is a bad reason we can always output know? *)
+            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
+            (** Uniquify the filename before the extension if it exists*)
+            let i = try String.rindex dest '.' with _ -> String.length dest in
+            (** Before extension *)
+            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;
+  (** sanitize --to-prover and --to-known-prover for Copy* *)
+  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;
+    cmd_desc     = "output file send to the prover.";
+    cmd_name     = "output";
+    cmd_run      = run;
+  }