why3session rm : remove selected proof attempts

Makefile.in

@@ -677,7 +677,7 @@ install_local: bin/why3replayer
 ###############
 
 SESSION_FILES = why3session_lib why3session_mod why3session_copy \
-		why3session_info why3session
+		why3session_info why3session_rm why3session
 
 SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
 

src/why3session/why3session.ml

@@ -26,6 +26,7 @@ let cmds =
     Why3session_mod.cmd;
     Why3session_copy.cmd;
     Why3session_info.cmd;
+    Why3session_rm.cmd;
   |]
 
 let usage = "why3session cmd [opts]:"

src/why3session/why3session_copy.ml

@@ -104,7 +104,6 @@ let run_one env config filters pk fname =
     (fun pr -> Stack.push pr s) env_session.session;
   Stack.iter (fun pr ->
     try
-      if pr.proof_archived then raise Exit;
       let prover = match to_prover with To_prover pk -> pk
         | Convert mprover -> Mprover.find_exn Exit pr.proof_prover mprover
       in
@@ -160,7 +159,7 @@ but@ one@ is@ needed.@.";
 let cmd =
   { cmd_spec = spec;
     cmd_desc     = "copy proof based on a filter. \
-No filter means all the possibilities.";
+No filter means all the possibilities (except for --filter-archived).";
     cmd_name     = "copy";
     cmd_run      = run;
   }

src/why3session/why3session_lib.ml

@@ -115,13 +115,42 @@ let read_opt_prover s =
 
 let add_filter_prover s = Stack.push (read_opt_prover s) filter_prover
 
+type filter_three = | FT_Yes | FT_No | FT_All
+
+let opt_filter_archived = ref FT_No
+let opt_filter_obsolete = ref FT_All
+let opt_filter_verified_goal = ref FT_All
+let opt_filter_verified = ref FT_All
+
+let add_filter_three r = function
+  | "no" -> r := FT_No
+  | "yes" -> r := FT_Yes
+  | "all" -> r := FT_All
+  | _ -> assert false
+
+let opt_three r = Arg.Symbol (["yes";"no";"all"], add_filter_three r)
+
 let filter_spec =
   ["--filter-prover", Arg.String add_filter_prover,
    " [name,version[,alternative]|id] \
-the proof containing this prover will be transformed"]
+the proof containing this prover are selected";
+   "--filter-archived", opt_three opt_filter_obsolete,
+   " no: only non-obsolete, yes: only obsolete (default all)";
+   "--filter-archived", opt_three opt_filter_archived,
+   " no: only unarchived, yes: only archived (default no)";
+   "--filter-verified-goal", opt_three opt_filter_verified_goal,
+   " 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)";
+]
 
-type filters = C.Sprover.t (* if empty : every provers *)
-    (* * ... *)
+type filters =
+    { provers : C.Sprover.t; (* if empty : every provers *)
+      obsolete : filter_three;
+      archived : filter_three;
+      verified : filter_three;
+      verified_goal : filter_three;
+    }
 
 let prover_of_filter_prover whyconf = function
   | Prover p -> p
@@ -139,11 +168,36 @@ let read_filter_spec whyconf : filters * bool =
         id (Whyconf.get_conf_file whyconf);
       should_exit := true in
   Stack.iter iter filter_prover;
-  !s,!should_exit
-
-let session_iter_proof_attempt_by_filter provers f session =
-  let iter a = if C.Sprover.mem a.S.proof_prover provers then f a in
-  if C.Sprover.is_empty provers
-  (** if no prover is filtered then they are all taken *)
-  then S.session_iter_proof_attempt f session
-  else S.session_iter_proof_attempt iter session
+  {provers = !s;
+   obsolete = !opt_filter_obsolete;
+   archived = !opt_filter_archived;
+   verified = !opt_filter_verified;
+   verified_goal = !opt_filter_verified_goal;
+  },!should_exit
+
+let session_iter_proof_attempt_by_filter filters f session =
+  (** provers *)
+  let iter_provers a =
+    if C.Sprover.mem a.S.proof_prover filters.provers then f a in
+  let f = if C.Sprover.is_empty filters.provers then f else iter_provers in
+  (** three value *)
+  let three_value f v p =
+    let iter_obsolete a =
+      match v with
+        | FT_No  when not (p a) -> f a
+        | FT_Yes when     (p a) -> f a
+        | _ -> () (** FT_All treated after *) in
+    if v = FT_All then f else iter_obsolete in
+  (** obsolete *)
+  let f = three_value f filters.obsolete (fun a -> a.S.proof_obsolete) in
+  (** archived *)
+  let f = three_value f filters.archived (fun a -> a.S.proof_archived) in
+  (** verified_goal *)
+  let f = three_value f filters.verified_goal
+    (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
+
+
+let set_filter_verified_goal t = opt_filter_verified_goal := t

src/why3session/why3session_lib.mli

@@ -66,8 +66,7 @@ type filter_prover =
 val read_opt_prover : string -> filter_prover
 val prover_of_filter_prover : config -> filter_prover -> prover
 
-type filters = Sprover.t (* if empty : every provers *)
-    (* * ... *)
+type filters
 
 val filter_spec : spec_list
 
@@ -76,3 +75,8 @@ val read_filter_spec : Whyconf.config -> filters * bool
 val session_iter_proof_attempt_by_filter :
   filters ->
   ('key Session.proof_attempt -> unit) -> 'key Session.session -> unit
+
+
+(* quite ad-hoc *)
+type filter_three = | FT_Yes | FT_No | FT_All
+val set_filter_verified_goal : filter_three -> unit

src/why3session/why3session_mod.ml

@@ -66,7 +66,7 @@ let run () =
 let cmd =
   { cmd_spec = spec;
     cmd_desc     = "modify proof based on filter. \
-No filter means all the possibilities.";
+No filter means all the possibilities (except for --filter-archived).";
     cmd_name     = "mod";
     cmd_run      = run;
   }

src/why3session/why3session_rm.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2011                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Why3
+open Why3session_lib
+open Whyconf
+open Session
+open Format
+
+type filter_prover =
+  | Prover of Whyconf.prover
+  | ProverId of string
+
+(**
+   TODO remove_transformation,...
+**)
+
+(** Currently doesn't share the configuration of ide *)
+type replace = Interactive | Always | Not_valid (*| Never*)
+let opt_remove = ref Always
+let set_remove s () = opt_remove := s
+
+let spec =
+  ("--clean",
+   Arg.Unit (fun () -> set_remove Not_valid ();
+     set_filter_verified_goal FT_Yes),
+   " Remove unsuccessful proof attempts \
+associated to proved goals (same as --filter-verified-goal --conservative)")::
+  ("--interactive",
+   Arg.Unit (set_remove Interactive), " ask before replacing proof_attempt")::
+  ("-i",
+   Arg.Unit (set_remove Interactive), " same as --interactive")::
+  ("--force", Arg.Unit (set_remove Always),
+   " remove all selected proof_attempt (default)")::
+  ("-f", Arg.Unit (set_remove Always), " same as --force")::
+  ("--conservative", Arg.Unit (set_remove Not_valid),
+   " don't remove proof_attempt which are not obsolete and valid")::
+  ("-c", Arg.Unit (set_remove Not_valid), " same as --conservative")::
+(*  ("--never", Arg.Unit (set_remove Never),
+   " never remove a proof")::
+  ("-n", Arg.Unit (set_remove Never), " same as --never")::*)
+  (filter_spec @ env_spec)
+
+let rec interactive to_remove =
+  eprintf "Do you want to remove 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 run_one env config filters fname =
+  let env_session,_ =
+    read_update_session ~allow_obsolete:false env config fname in
+  session_iter_proof_attempt_by_filter filters
+    (fun pr ->
+      let remove = match !opt_remove with
+        | Always -> true (*| Never -> false*)
+        | Interactive -> interactive pr
+        | Not_valid -> not (proof_verified pr) in
+      if remove then remove_external_proof pr) env_session.session;
+  save_session 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;
+  iter_files (run_one env config filters)
+
+
+let cmd =
+  { cmd_spec = spec;
+    cmd_desc     = "remove proof based on a filter. \
+No filter means all the possibilities (except for --filter-archived).";
+    cmd_name     = "rm";
+    cmd_run      = run;
+  }