why3session_copy.ml 7.74 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
(*    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

(**
   TODO add_transformation,...
29 30 31 32 33 34

   TODO:
    filter_state
    filter_time
    filter_?

35 36
**)

37 38
(** To prover *)

39 40 41 42 43 44
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
45 46 47 48 49 50 51 52 53


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
54 55

let spec =
56 57 58 59 60 61 62 63 64 65 66 67
  ("--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" ) ::
68
(*
69 70 71
  ("--to-known-prover",
   Arg.Set opt_to_known,
   " convert the unknown provers to the most similar known prover.")::
72
*)
73
  ["--to-prover",
74
   Arg.String (fun s -> opt_to_prover := Some (read_opt_prover s)),
75 76 77 78 79 80 81 82 83 84 85 86
   " 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"]@
87
    (force_obsolete_spec @ filter_spec @ common_options)
88 89 90 91 92

type action =
  | Copy
  | CopyArchive
  | Mod
93 94 95 96 97 98 99 100 101 102 103 104

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:_ _ = ()

105 106 107
type to_prover =
  | Convert of prover Mprover.t
  | To_prover of prover
108
  | SameProver
109 110 111 112

let get_to_prover pk session config =
  match pk with
    | Some pk -> To_prover pk
113 114 115
    | None when !opt_to_known
           -> (** We are in the case --to-known-prover *)
      assert (!opt_to_known);
116 117 118 119 120 121 122 123 124 125 126
      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)
127 128 129
    | None -> SameProver

exception NoAlt
130

131
let run_one ~action env config filters pk fname =
132
  let env_session,_ =
133
    read_update_session ~allow_obsolete:!opt_force_obsolete env config fname in
134
  let to_prover = get_to_prover pk env_session.session config in
135 136 137 138
  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 ->
139
    try
140 141 142 143
      let prover = match to_prover with To_prover pk -> Some pk
        | Convert mprover ->
          Some (Mprover.find_exn NoAlt pr.proof_prover mprover)
        | SameProver -> None
144
      in
145 146 147
      let prn = match prover with
        | None -> pr
        | Some prover ->
148
      (** If such a prover already exists on the goal *)
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
          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
          | _ -> ()
175
  ) s;
MARCHE Claude's avatar
MARCHE Claude committed
176
  save_session config env_session.session
177

178 179 180 181 182 183 184 185 186 187 188
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

189

190
let run ~action () =
191 192 193
  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;
194 195 196
  (** 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@ \
197 198 199 200 201
but@ one@ is@ needed.@.";
    exit 1
  end;
  (** get the provers *)
  let pk = read_to_prover config in
202 203 204 205 206 207 208 209
  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;
  }
210 211


212 213 214 215 216 217 218 219 220
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 =
221
  { cmd_spec = spec;
222 223 224
    cmd_desc     = "modify proof based on filter.";
    cmd_name     = "mod";
    cmd_run      = run ~action:Mod;
225
  }