Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

why3session_lib.ml 6.8 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39

open Why3
module S = Session
module C = Whyconf

type spec_list = (Arg.key * Arg.spec * Arg.doc) list

type cmd =
    {
      cmd_spec : spec_list;
      cmd_desc : string;
      cmd_name : string;
      cmd_run  : unit -> unit;
    }

let files = Queue.create ()
let iter_files f = Queue.iter f files
let anon_fun (f:string) = Queue.add f files

let opt_version = ref false

let print_version () =
  Format.printf "Why3 session, version %s (build date: %s)@."
    Config.version Config.builddate

let read_simple_spec () =
  if !opt_version then begin
    print_version (); exit 0
  end;
40 41
  Debug.Args.set_flags_selected ();
  Debug.Args.option_list ()
42 43 44 45 46



let opt_config = ref None
let opt_loadpath = ref []
47
let opt_extra = ref []
48

49
let common_options = [
50
  "-C", Arg.String (fun s -> opt_config := Some s),
MARCHE Claude's avatar
MARCHE Claude committed
51
      "<file> reads configuration from <file>";
52
  "--config", Arg.String (fun s -> opt_config := Some s),
MARCHE Claude's avatar
MARCHE Claude committed
53
      "<file> same as -C";
54
  "--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]),
MARCHE Claude's avatar
MARCHE Claude committed
55
      "<file> reads additional configuration from <file>";
56
  "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
MARCHE Claude's avatar
MARCHE Claude committed
57
      "<dir> adds <dir> to the library search path";
58
  "--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
MARCHE Claude's avatar
MARCHE Claude committed
59 60
      "<dir> same as -L";
  "-v", Arg.Set opt_version, " prints version information" ;
61 62 63
  Debug.Args.desc_debug_list;
  Debug.Args.desc_debug_all;
  Debug.Args.desc_debug;
64 65
]

66
(* dead code
Andrei Paskevich's avatar
Andrei Paskevich committed
67
let env_spec = common_options
68
*)
69 70 71 72

let read_env_spec () =
  (** Configuration *)
  let config = Whyconf.read_config !opt_config in
73
  let config = List.fold_left Whyconf.merge_config config !opt_extra in
74 75 76
  let main = Whyconf.get_main config in
  Whyconf.load_plugins main;
  let loadpath = (Whyconf.loadpath (Whyconf.get_main config))
MARCHE Claude's avatar
MARCHE Claude committed
77
    @ List.rev !opt_loadpath in
78 79 80 81 82 83 84 85 86 87 88 89
  let env = Env.create_env loadpath in
  env,config,read_simple_spec ()


let read_update_session ~allow_obsolete env config fname =
  let project_dir = Session.get_project_dir fname in
  let session = Session.read_session project_dir in
  Session.update_session ~keygen:(fun ?parent:_ _ -> ())
    ~allow_obsolete session env config

(** filter *)
type filter_prover =
90 91
| Prover of Whyconf.prover
| FilterProver of Whyconf.filter_prover
92 93 94 95

let filter_prover = Stack.create ()

let read_opt_prover s =
96
  try
97
    let l = Strings.rev_split s ',' in
98 99 100 101 102 103 104 105 106 107
    match l with
    | [altern;version;name] when List.for_all (fun s -> s.[0] <> '^') l ->
      Prover {Whyconf.prover_name = name;
              prover_version = version;
              prover_altern = altern}
    | _ -> FilterProver (Whyconf.parse_filter_prover s)
  with Whyconf.ParseFilterProver _ ->
    raise (Arg.Bad
             "--filter-prover name[,version[,alternative]|,,alternative] \
                regexp must start with ^")
108 109 110 111


let add_filter_prover s = Stack.push (read_opt_prover s) filter_prover

112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
type filter_three = | FT_Yes | FT_No | FT_All

let opt_filter_archived = ref FT_No
let opt_filter_obsolete = ref FT_All
let opt_filter_verified_goal = ref FT_All
let opt_filter_verified = ref FT_All

let add_filter_three r = function
  | "no" -> r := FT_No
  | "yes" -> r := FT_Yes
  | "all" -> r := FT_All
  | _ -> assert false

let opt_three r = Arg.Symbol (["yes";"no";"all"], add_filter_three r)

127 128 129
let filter_spec =
  ["--filter-prover", Arg.String add_filter_prover,
   " [name,version[,alternative]|id] \
130
the proof containing this prover are selected";
François Bobot's avatar
François Bobot committed
131
   "--filter-obsolete", opt_three opt_filter_obsolete,
132 133 134 135 136 137 138 139
   " no: only non-obsolete, yes: only obsolete (default all)";
   "--filter-archived", opt_three opt_filter_archived,
   " no: only unarchived, yes: only archived (default no)";
   "--filter-verified-goal", opt_three opt_filter_verified_goal,
   " no: only parent goal not verified, yes: only verified (default all)";
   "--filter-verified", opt_three opt_filter_verified,
   " no: only not verified, yes: only verified (default all)";
]
140

141 142 143 144 145 146 147
type filters =
    { provers : C.Sprover.t; (* if empty : every provers *)
      obsolete : filter_three;
      archived : filter_three;
      verified : filter_three;
      verified_goal : filter_three;
    }
148

149 150 151 152 153
let provers_of_filter_prover whyconf = function
  | Prover p        -> C.Sprover.singleton p
  | FilterProver fp ->
    C.Mprover.map (Util.const ()) (C.filter_provers whyconf fp)

154
let prover_of_filter_prover whyconf = function
155 156 157 158
  | Prover p        -> p
  | FilterProver fp ->
    (C.filter_one_prover whyconf fp).C.prover

159 160 161 162 163 164

let read_filter_spec whyconf : filters * bool =
  let should_exit = ref false in
  let s = ref C.Sprover.empty in
  let iter p =
    try
165 166
      s := C.Sprover.union (provers_of_filter_prover whyconf p) !s
    with C.ProverNotFound (_,fp) ->
167
      Format.eprintf
168 169 170
        "The prover %a is not found in the configuration file %s@."
        Whyconf.print_filter_prover fp
        (Whyconf.get_conf_file whyconf);
171 172
      should_exit := true in
  Stack.iter iter filter_prover;
173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
  {provers = !s;
   obsolete = !opt_filter_obsolete;
   archived = !opt_filter_archived;
   verified = !opt_filter_verified;
   verified_goal = !opt_filter_verified_goal;
  },!should_exit

let session_iter_proof_attempt_by_filter filters f session =
  (** provers *)
  let iter_provers a =
    if C.Sprover.mem a.S.proof_prover filters.provers then f a in
  let f = if C.Sprover.is_empty filters.provers then f else iter_provers in
  (** three value *)
  let three_value f v p =
    let iter_obsolete a =
      match v with
        | FT_No  when not (p a) -> f a
        | FT_Yes when     (p a) -> f a
        | _ -> () (** FT_All treated after *) in
    if v = FT_All then f else iter_obsolete in
  (** obsolete *)
  let f = three_value f filters.obsolete (fun a -> a.S.proof_obsolete) in
  (** archived *)
  let f = three_value f filters.archived (fun a -> a.S.proof_archived) in
  (** verified_goal *)
  let f = three_value f filters.verified_goal
    (fun a -> a.S.proof_parent.S.goal_verified) in
  (** verified *)
  let f = three_value f filters.verified S.proof_verified in
  S.session_iter_proof_attempt f session


let set_filter_verified_goal t = opt_filter_verified_goal := t
206 207 208 209 210 211

let opt_force_obsolete = ref false

let force_obsolete_spec =
  ["-F", Arg.Set opt_force_obsolete,
   " transform obsolete session"]