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

21
open Whyconf
François Bobot's avatar
François Bobot committed
22 23 24
open Session

(** convert unknown prover *)
25 26 27 28 29 30 31 32 33 34 35 36 37 38
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
39

40
let convert_unknown_prover ~keygen env_session =
41 42 43
  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
44 45 46
  if not (Sprover.is_empty unknown_provers) then begin
    (** construct the list of compatible provers for each unknown provers *)
    let unknown_provers =
47
      Mprover.mapi (utkp known_provers) unknown_provers in
François Bobot's avatar
François Bobot committed
48
    session_iter_proof_attempt (fun pr ->
49
      let pks = Mprover.find_def [] pr.proof_prover unknown_provers in
François Bobot's avatar
François Bobot committed
50 51 52
      List.iter (fun pk ->
        (** If such a prover already exists we add nothing *)
        if not (PHprover.mem pr.proof_parent.goal_external_proofs pk) then
53
          ignore (copy_external_proof ~keygen ~prover:pk pr)
54 55
      ) pks;
    ) env_session.session
François Bobot's avatar
François Bobot committed
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77
  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 ->
78 79
        add_registered_transformation ~keygen env_session tr_name g
    in
François Bobot's avatar
François Bobot committed
80 81
    let add_pa sg =
      if not (PHprover.mem sg.goal_external_proofs pr.proof_prover) then
82
        ignore (copy_external_proof ~keygen ~goal:sg
83
                  ~attempt_status:Interrupted pr)
84
    in
François Bobot's avatar
François Bobot committed
85 86 87
    List.iter add_pa tr.transf_goals in
  let proofs = all_proof_attempts env_session.session in
  List.iter replace proofs