why3session : add copy_archive, factorize copy and mod

Makefile.in

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

src/util/util.ml

@@ -207,6 +207,17 @@ let ends_with s suf =
   let suflen = String.length suf in
   slen >= suflen && aux s suf suflen (slen - suflen) 0
 
+let padd_string c s i =
+  let sl = String.length s in
+  if sl < i then
+    let p = String.create i in
+    String.blit s 0 p 0 sl;
+    String.fill p sl (i-sl) c;
+    p
+  else if sl > i
+  then String.sub s 0 i
+  else s
+
 (** usefule function on char *)
 let is_uppercase c = 'A' <= c && c <= 'Z'
 

src/util/util.mli

@@ -145,6 +145,9 @@ val split_string_rev : string -> char -> string list
 val ends_with : string -> string -> bool
 (** test if a string ends with another *)
 
+val padd_string : char -> string -> int -> string
+(** extract or padd the given string in order to have the given length *)
+
 (* useful function on char *)
 val is_uppercase : char -> bool
 

src/why3session/why3session.ml

@@ -23,19 +23,22 @@ open Why3session_lib
 
 let cmds =
   [|
-    Why3session_mod.cmd;
-    Why3session_copy.cmd;
+    Why3session_copy.cmd_mod;
+    Why3session_copy.cmd_copy;
+    Why3session_copy.cmd_archive;
     Why3session_info.cmd;
     Why3session_rm.cmd;
   |]
 
-let usage = "why3session cmd [opts]:"
+let usage = "why3session cmd [opts]"
 
 let print_usage () =
+  let maxl = Array.fold_left
+    (fun acc e -> max acc (String.length e.cmd_name)) 0 cmds in
   eprintf "%s@.@.command:@.@[<hov>%a@]@."
     usage (Pp.print_iter1 Array.iter Pp.newline
-             (fun fmt e -> fprintf fmt "%s     @[<hov>%s@]"
-               e.cmd_name e.cmd_desc)) cmds;
+             (fun fmt e -> fprintf fmt "%s   @[<hov>%s@]"
+               (Util.padd_string ' ' e.cmd_name maxl) e.cmd_desc)) cmds;
   exit 1
 
 

src/why3session/why3session_copy.ml

@@ -23,45 +23,70 @@ open Whyconf
 open Session
 open Format
 
-type filter_prover =
-  | Prover of Whyconf.prover
-  | ProverId of string
-
 (**
    TODO add_transformation,...
+
+   TODO:
+    filter_state
+    filter_time
+    filter_?
+
 **)
 
+(** To prover *)
+
 let opt_to_prover = ref None
 
 (** Currently doesn't share the configuration of ide *)
 type replace = Interactive | Always | Not_valid | Never
 let opt_replace = ref Not_valid
 let set_replace s () = opt_replace := s
-let opt_convert_unknown = ref false
+
+
+let opt_to_known = ref false
+
+let tobe_archived = ref None
+let set_opt_archived () = tobe_archived := Some true
+let unset_opt_archived () = tobe_archived := Some false
+
+let tobe_obsolete = ref false
 
 let spec =
-  ("--to-prover",
+  ("--set-obsolete", Arg.Set tobe_obsolete,
+   " the proof is set to obsolete" ) ::
+  ("--set-archive", Arg.Unit set_opt_archived,
+   " the proof is set to archive" ) ::
+  ("--unset-archive", Arg.Unit unset_opt_archived,
+   " the proof is set to replayable" ) ::
+  ("--set-obsolete", Arg.Set tobe_obsolete,
+   " the proof is set to obsolete" ) ::
+  ("--set-archive", Arg.Unit set_opt_archived,
+   " the proof is set to archive" ) ::
+  ("--unset-archive", Arg.Unit unset_opt_archived,
+   " the proof is set to replayable" ) ::
+  ("--to-known-prover",
+   Arg.Set opt_to_known,
+   " convert the unknown provers to the most similar known prover.")::
+  ["--to-prover",
    Arg.String (fun s -> opt_to_prover := Some (read_opt_prover s)),
-   " the proof is copied to this new prover")::
-  ("--convert-unknown",
-   Arg.Set opt_convert_unknown,
-   " convert the unknown provers to the most similar known prover.
-The converted proof attempt are set to archived.
-The archived proof attempt are not converted")::
-  ("--interactive",
-   Arg.Unit (set_replace Interactive), " ask before replacing proof_attempt")::
-  ("-i",
-   Arg.Unit (set_replace Interactive), " same as --interactive")::
-  ("--force", Arg.Unit (set_replace Always),
-   " force the replacement of proof_attempt")::
-  ("-f", Arg.Unit (set_replace Always), " same as --force")::
-  ("--conservative", Arg.Unit (set_replace Not_valid),
-   " never replace proof which are not obsolete and valid (default)")::
-  ("-c", Arg.Unit (set_replace Not_valid), " same as --conservative")::
-  ("--never", Arg.Unit (set_replace Never),
-   " never replace a proof")::
-  ("-n", Arg.Unit (set_replace Never), " same as --never")::
-  (filter_spec @ env_spec)
+   " the proof is copied to this new prover";
+   "--interactive", Arg.Unit (set_replace Interactive),
+   " ask before replacing proof_attempt";
+   "-i", Arg.Unit (set_replace Interactive), " same as --interactive";
+   "--force", Arg.Unit (set_replace Always),
+   " force the replacement of proof_attempt";
+   "-f", Arg.Unit (set_replace Always), " same as --force";
+   "--conservative", Arg.Unit (set_replace Not_valid),
+   " never replace proof which are not obsolete and valid (default)";
+   "-c", Arg.Unit (set_replace Not_valid), " same as --conservative";
+   "--never", Arg.Unit (set_replace Never), " never replace a proof";
+   "-n", Arg.Unit (set_replace Never), " same as --never"]@
+    (force_obsolete_spec @ filter_spec @ env_spec)
+
+type action =
+  | Copy
+  | CopyArchive
+  | Mod
 
 let rec interactive to_remove =
   eprintf "Do you want to replace the external proof %a (y/n)@."
@@ -77,12 +102,14 @@ let keygen ?parent:_ _ = ()
 type to_prover =
   | Convert of prover Mprover.t
   | To_prover of prover
+  | SameProver
 
 let get_to_prover pk session config =
   match pk with
     | Some pk -> To_prover pk
-    | None -> (** We are in the case convert-unknown *)
-      assert (!opt_convert_unknown);
+    | None when !opt_to_known
+           -> (** We are in the case --to-known-prover *)
+      assert (!opt_to_known);
       let known_provers = get_provers config in
       let provers = get_used_provers session in
       let unknown_provers = Mprover.set_diff provers known_provers in
@@ -94,38 +121,54 @@ let get_to_prover pk session config =
           | a::_,_ -> Some a
           | _ -> None in
       Convert (Mprover.mapi_filter map unknown_provers)
+    | None -> SameProver
+
+exception NoAlt
 
-let run_one env config filters pk fname =
+let run_one ~action env config filters pk fname =
   let env_session,_ =
-    read_update_session ~allow_obsolete:false env config fname in
+    read_update_session ~allow_obsolete:!opt_force_obsolete env config fname in
   let to_prover = get_to_prover pk env_session.session config in
   let s = Stack.create () in
   session_iter_proof_attempt_by_filter filters
     (fun pr -> Stack.push pr s) env_session.session;
   Stack.iter (fun pr ->
     try
-      let prover = match to_prover with To_prover pk -> pk
-        | Convert mprover -> Mprover.find_exn Exit pr.proof_prover mprover
+      let prover = match to_prover with To_prover pk -> Some pk
+        | Convert mprover ->
+          Some (Mprover.find_exn NoAlt pr.proof_prover mprover)
+        | SameProver -> None
       in
+      let prn = match prover with
+        | None -> pr
+        | Some prover ->
       (** If such a prover already exists on the goal *)
-      let exists =
-        (PHprover.mem pr.proof_parent.goal_external_proofs prover) in
-      let replace = not exists || match !opt_replace with
-        | Always -> true | Never -> false
-        | Interactive ->
-          interactive
-            (PHprover.find pr.proof_parent.goal_external_proofs prover)
-        | Not_valid ->
-          let rm =
-            (PHprover.find pr.proof_parent.goal_external_proofs prover) in
-          not (proof_verified rm) in
-      if replace then
-        begin
-          ignore (copy_external_proof ~keygen ~prover ~env_session pr);
-          match to_prover with To_prover _ -> ()
-            | Convert _ -> set_archived pr true
-        end
-    with Exit -> () (** a known prover or no alternative has been found *)
+          let exists =
+            (PHprover.mem pr.proof_parent.goal_external_proofs prover) in
+          let replace = not exists || match !opt_replace with
+            | Always -> true | Never -> false
+            | Interactive ->
+              interactive
+                (PHprover.find pr.proof_parent.goal_external_proofs prover)
+            | Not_valid ->
+              let rm =
+                (PHprover.find pr.proof_parent.goal_external_proofs prover) in
+              not (proof_verified rm) in
+          if not replace then raise Exit;
+          copy_external_proof ~keygen ~prover ~env_session pr
+      in
+      if !tobe_obsolete then set_obsolete prn;
+      begin match !tobe_archived with
+        | None -> ()
+        | Some b -> set_archived prn b end;
+      raise Exit
+    with
+      | NoAlt -> () (** a known prover or no alternative has been found *)
+      | Exit  ->    (** normal or existing prover not replaced *)
+        match action with
+          | CopyArchive -> set_archived pr true
+          | Mod when to_prover <> SameProver -> remove_external_proof pr
+          | _ -> ()
   ) s;
   save_session env_session.session
 
@@ -141,25 +184,39 @@ let read_to_prover config =
           exit 1
 
 
-let run () =
+let run ~action () =
   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 --convert-unknown *)
-  if (!opt_to_prover <> None) = (!opt_convert_unknown) then begin
-    eprintf "The option --to-prover@ and@ --convert-unknown@ are@ exclusive@ \
+  (** sanitize --to-prover and --to-known-prover for Copy* *)
+  if action<>Mod && (!opt_to_prover <> None) = (!opt_to_known) then begin
+    eprintf "The option --to-prover@ and@ --to-known-prover@ are@ exclusive@ \
 but@ one@ is@ needed.@.";
     exit 1
   end;
   (** get the provers *)
   let pk = read_to_prover config in
-  iter_files (run_one env config filters pk)
+  iter_files (run_one ~action env config filters pk)
+
+let cmd_copy =
+  { cmd_spec     = spec;
+    cmd_desc     = "copy proof based on a filter.";
+    cmd_name     = "copy";
+    cmd_run      = run ~action:Copy;
+  }
 
 
-let cmd =
+let cmd_archive =
+  { cmd_spec     = spec;
+    cmd_desc     = "same as copy but archive the source.";
+    cmd_name     = "copy-archive";
+    cmd_run      = run ~action:CopyArchive;
+  }
+
+
+let cmd_mod =
   { cmd_spec = spec;
-    cmd_desc     = "copy proof based on a filter. \
-No filter means all the possibilities (except for --filter-archived).";
-    cmd_name     = "copy";
-    cmd_run      = run;
+    cmd_desc     = "modify proof based on filter.";
+    cmd_name     = "mod";
+    cmd_run      = run ~action:Mod;
   }

src/why3session/why3session_info.ml

@@ -69,7 +69,7 @@ let run () =
 
 let cmd =
   { cmd_spec = spec;
-    cmd_desc = "print informations about session";
+    cmd_desc = "print informations about session.";
     cmd_name = "info";
     cmd_run  = run;
   }

src/why3session/why3session_lib.ml

@@ -201,3 +201,9 @@ let session_iter_proof_attempt_by_filter filters f session =
 
 
 let set_filter_verified_goal t = opt_filter_verified_goal := t
+
+let opt_force_obsolete = ref false
+
+let force_obsolete_spec =
+  ["-F", Arg.Set opt_force_obsolete,
+   " transform obsolete session"]

src/why3session/why3session_lib.mli

@@ -80,3 +80,7 @@ val session_iter_proof_attempt_by_filter :
 (* quite ad-hoc *)
 type filter_three = | FT_Yes | FT_No | FT_All
 val set_filter_verified_goal : filter_three -> unit
+
+(** force obsolete *)
+val opt_force_obsolete : bool ref
+val force_obsolete_spec : spec_list

src/why3session/why3session_mod.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
-module S = Session
-
-(** TODO:
-    filter_state
-    filter_time
-    filter_?
-*)
-
-let tobe_archived = ref None
-let set_archived () = tobe_archived := Some true
-let unset_archived () = tobe_archived := Some false
-
-let tobe_obsolete = ref false
-
-let spec =
-  ("--set-obsolete", Arg.Set tobe_obsolete,
-   " the proof is set to obsolete" ) ::
-  ("--set-archive", Arg.Unit set_archived,
-   " the proof is set to archive" ) ::
-  ("--unset-archive", Arg.Unit unset_archived,
-   " the proof is set to replayable" ) ::
-  (filter_spec @ env_spec)
-
-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 a ->
-      if !tobe_obsolete then S.set_obsolete a;
-      begin match !tobe_archived with
-        | None -> ()
-        | Some b -> S.set_archived a b end;
-    ) env_session.S.session;
-  S.save_session env_session.S.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     = "modify proof based on filter. \
-No filter means all the possibilities (except for --filter-archived).";
-    cmd_name     = "mod";
-    cmd_run      = run;
-  }

src/why3session/why3session_rm.ml

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