session_tools.ml 3.05 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10
(********************************************************************)
François Bobot's avatar
François Bobot committed
11

12
open Whyconf
François Bobot's avatar
François Bobot committed
13 14 15
open Session

(** convert unknown prover *)
16 17 18 19 20 21 22 23 24 25 26 27 28 29
let unknown_to_known_provers provers pu =
  Mprover.fold (fun pk _ (others,name,version) ->
    match
      pk.prover_name = pu.prover_name,
      pk.prover_version = pu.prover_version,
      pk.prover_altern = pu.prover_altern with
        | false, _, _ -> pk::others, name, version
        | _, false, _ -> others, pk::name, version
        | _           -> others, name, pk::version
  ) provers ([],[],[])

let utkp provers pu () =
  let _,name,version = unknown_to_known_provers provers pu in
  version@name
François Bobot's avatar
François Bobot committed
30

31
let convert_unknown_prover ~keygen env_session =
32 33 34
  let known_provers = get_provers env_session.whyconf in
  let provers = get_used_provers env_session.session in
  let unknown_provers = Mprover.set_diff provers known_provers in
François Bobot's avatar
François Bobot committed
35
  if not (Sprover.is_empty unknown_provers) then begin
36
    (* construct the list of compatible provers for each unknown provers *)
François Bobot's avatar
François Bobot committed
37
    let unknown_provers =
38
      Mprover.mapi (utkp known_provers) unknown_provers in
François Bobot's avatar
François Bobot committed
39
    session_iter_proof_attempt (fun pr ->
40
      let pks = Mprover.find_def [] pr.proof_prover unknown_provers in
François Bobot's avatar
François Bobot committed
41
      List.iter (fun pk ->
42
        (* If such a prover already exists we add nothing *)
François Bobot's avatar
François Bobot committed
43
        if not (PHprover.mem pr.proof_parent.goal_external_proofs pk) then
44
          ignore (copy_external_proof ~keygen ~prover:pk pr)
45 46
      ) pks;
    ) env_session.session
François Bobot's avatar
François Bobot committed
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
  end

(** filter the proof attempt *)
let filter_proof_attempt ?notify f s =
  session_iter_proof_attempt (fun pr ->
    if not (f pr) then remove_external_proof ?notify pr) s

(** get all proof_attempt *)
let all_proof_attempts s =
  let l = ref [] in
  session_iter_proof_attempt (fun pr -> l:=pr::!l) s;
  !l

(** apply a transformation on all the proof_attempt *)
let transform_proof_attempt ?notify ~keygen env_session tr_name =
  let replace pr =
    let g = pr.proof_parent in
    remove_external_proof ?notify pr;
    let tr =
      try
        PHstr.find g.goal_transformations tr_name
      with Not_found ->
69 70
        add_registered_transformation ~keygen env_session tr_name g
    in
François Bobot's avatar
François Bobot committed
71 72
    let add_pa sg =
      if not (PHprover.mem sg.goal_external_proofs pr.proof_prover) then
73
        ignore (copy_external_proof ~keygen ~goal:sg
74
                  ~attempt_status:Interrupted pr)
75
    in
François Bobot's avatar
François Bobot committed
76 77 78
    List.iter add_pa tr.transf_goals in
  let proofs = all_proof_attempts env_session.session in
  List.iter replace proofs