why3session copy : add option --convert-unknown

src/util/stdlib.ml

@@ -64,6 +64,7 @@ module type S =
     val set_disjoint : 'a t -> 'b t -> bool
     val find_default : key -> 'a -> 'a t -> 'a
     val find_option : key -> 'a t -> 'a option
+    val find_exn : exn -> key -> 'a t -> 'a
     val map_filter: ('a -> 'b option) -> 'a t -> 'b t
     val mapi_filter: (key -> 'a -> 'b option) -> 'a t -> 'b t
     val mapi_fold:
@@ -517,6 +518,13 @@ module Make(Ord: OrderedType) = struct
           if c = 0 then Some d
           else find_option x (if c < 0 then l else r)
 
+    let rec find_exn exn x = function
+        Empty -> raise exn
+      | Node(l, v, d, r, _) ->
+          let c = Ord.compare x v in
+          if c = 0 then d
+          else find_exn exn x (if c < 0 then l else r)
+
     let rec map_filter f = function
         Empty -> Empty
       | Node(l, v, d, r, _h) ->

src/util/stdlib.mli

@@ -232,6 +232,10 @@ module type S =
     (** [find_default x d m] returns the [Some] of the current binding
         of [x] in [m], or return [None] if no such binding exists. *)
 
+    val find_exn : exn -> key -> 'a t -> 'a
+    (** [find_exn exn x d m] returns the current binding
+        of [x] in [m], or raise [exn] if no such binding exists. *)
+
     val map_filter: ('a -> 'b option) -> 'a t -> 'b t
     (** Same as {!Map.S.map}, but may remove bindings. *)
 

src/why3session/why3session_copy.ml

@@ -37,11 +37,17 @@ let opt_to_prover = ref None
 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 spec =
   ("--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",
@@ -68,46 +74,87 @@ let rec interactive to_remove =
 
 let keygen ?parent:_ _ = ()
 
-let run_one env config filters fname =
-  let pk = match !opt_to_prover with
-    | None ->
-      eprintf "You should specify one prover with --to_prover";
-      exit 1
-    | Some fpr ->
-      try prover_of_filter_prover config fpr
-      with ProverNotFound (_,id) ->
-        eprintf
-          "The prover %s is not found in the configuration file %s@."
-          id (get_conf_file config);
-        exit 1 in
+type to_prover =
+  | Convert of prover Mprover.t
+  | To_prover of prover
+
+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);
+      let known_provers = get_provers config in
+      let provers = get_used_provers session in
+      let unknown_provers = Mprover.set_diff provers known_provers in
+      let map pu () =
+        let _,name,version =
+          Session_tools.unknown_to_known_provers known_provers pu in
+        match name,version with
+          | _,a::_ -> Some a
+          | a::_,_ -> Some a
+          | _ -> None in
+      Convert (Mprover.mapi_filter map unknown_provers)
+
+let run_one env config filters pk fname =
   let env_session,_ =
     read_update_session ~allow_obsolete:false 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 ->
-    (** If such a prover already exists on the goal *)
-    let exists =
-      (PHprover.mem pr.proof_parent.goal_external_proofs pk) in
-    let replace = not exists || match !opt_replace with
-      | Always -> true | Never -> false
-      | Interactive ->
-        interactive
-          (PHprover.find pr.proof_parent.goal_external_proofs pk)
-      | Not_valid ->
-        let rm = (PHprover.find pr.proof_parent.goal_external_proofs pk) in
-        not (proof_verified rm) in
-    if replace then
-      ignore (copy_external_proof ~keygen ~prover:pk ~env_session 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
+      (** 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 *)
   ) s;
   save_session env_session.session
 
+let read_to_prover config =
+  match !opt_to_prover with
+    | None -> None
+    | Some fpr ->
+      try Some (prover_of_filter_prover config fpr)
+      with ProverNotFound (_,id) ->
+        eprintf
+          "The prover %s is not found in the configuration file %s@."
+          id (get_conf_file config);
+          exit 1
+
 
 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)
+  (** 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@ \
+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)
 
 
 let cmd =