why3session_lib.ml 8.93 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11 12

open Why3
13

14 15 16
module S = Session
module C = Whyconf

17 18 19
let verbose = Debug.register_info_flag "verbose"
    ~desc:"Increase verbosity."

20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
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 read_simple_spec () =
35 36
  Debug.Args.set_flags_selected ();
  Debug.Args.option_list ()
37 38 39

let opt_config = ref None
let opt_loadpath = ref []
40
let opt_extra = ref []
41

42
let common_options = [
43
  "-C", Arg.String (fun s -> opt_config := Some s),
44
      "<file> read configuration from <file>";
45
  "--config", Arg.String (fun s -> opt_config := Some s),
MARCHE Claude's avatar
MARCHE Claude committed
46
      "<file> same as -C";
47
  "--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]),
48
      "<file> read additional configuration from <file>";
49
  "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
50
      "<dir> add <dir> to the library search path";
51
  "--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
MARCHE Claude's avatar
MARCHE Claude committed
52
      "<dir> same as -L";
53
  Debug.Args.desc_shortcut "verbose" "--verbose" "increase verbosity";
54 55 56
  Debug.Args.desc_debug_list;
  Debug.Args.desc_debug_all;
  Debug.Args.desc_debug;
57 58
]

59
(* dead code
Andrei Paskevich's avatar
Andrei Paskevich committed
60
let env_spec = common_options
61
*)
62 63

let read_env_spec () =
64
  (* Configuration *)
65
  let config = Whyconf.read_config !opt_config in
66
  let config = List.fold_left Whyconf.merge_config config !opt_extra in
67 68 69
  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
70
    @ List.rev !opt_loadpath in
71 72 73 74
  let env = Env.create_env loadpath in
  env,config,read_simple_spec ()

let read_update_session ~allow_obsolete env config fname =
75
  let project_dir = S.get_project_dir fname in
76
  let session,use_shapes = S.read_session project_dir in
77 78 79 80
  let ctxt = S.mk_update_context
    ~allow_obsolete_goals:allow_obsolete
    ~use_shapes_for_pairing_sub_goals:use_shapes
    (fun ?parent:_ () -> ())
81
  in
82
  S.update_session ~ctxt session env config
83 84 85

(** filter *)
type filter_prover =
86 87
| Prover of Whyconf.prover
| FilterProver of Whyconf.filter_prover
88 89 90 91

let filter_prover = Stack.create ()

let read_opt_prover s =
92
  try
93
    let l = Strings.rev_split ',' s in
94
    match l with
95
    (* A prover specified uniquely *)
96 97
    | [altern;version;name]
      when List.for_all (fun s -> s = "" || s.[0] <> '^') l ->
98 99 100 101 102 103 104 105
      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 ^")
106 107 108 109


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

110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
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)

125 126
let opt_status = ref []

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
   " 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)";
139 140 141 142 143 144 145 146 147 148
   "--filter-highfailure",
   Arg.Unit (fun () -> opt_status := Call_provers.HighFailure::!opt_status),
   " filter the call that fail in an unexpeted way";
   "--filter-valid",
   Arg.Unit (fun () -> opt_status := Call_provers.Valid::!opt_status),
   " filter the valid goals (can be obsolete)";
   "--filter-invalid",
   Arg.Unit (fun () -> opt_status := Call_provers.Invalid::!opt_status),
   " filter the invalid goals";
   "--filter-unknown",
149
   Arg.String (fun s -> opt_status := Call_provers.Unknown (s, None)::!opt_status),
150 151 152 153
   " filter when the prover reports it can't determine if the task is valid";
   "--filter-failure",
   Arg.String (fun s -> opt_status := Call_provers.Failure s::!opt_status),
   " filter when the prover reports a failure";
154
]
155

156 157 158 159 160 161
type filters =
    { provers : C.Sprover.t; (* if empty : every provers *)
      obsolete : filter_three;
      archived : filter_three;
      verified : filter_three;
      verified_goal : filter_three;
162
      status : Call_provers.prover_answer list; (* if empty : any answer *)
163
    }
164

165 166 167 168 169
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)

170
let prover_of_filter_prover whyconf = function
171 172 173 174
  | Prover p        -> p
  | FilterProver fp ->
    (C.filter_one_prover whyconf fp).C.prover

175 176 177 178 179 180

let read_filter_spec whyconf : filters * bool =
  let should_exit = ref false in
  let s = ref C.Sprover.empty in
  let iter p =
    try
181 182
      s := C.Sprover.union (provers_of_filter_prover whyconf p) !s
    with C.ProverNotFound (_,fp) ->
183
      Format.eprintf
184 185 186
        "The prover %a is not found in the configuration file %s@."
        Whyconf.print_filter_prover fp
        (Whyconf.get_conf_file whyconf);
187 188
      should_exit := true in
  Stack.iter iter filter_prover;
189 190 191 192 193
  {provers = !s;
   obsolete = !opt_filter_obsolete;
   archived = !opt_filter_archived;
   verified = !opt_filter_verified;
   verified_goal = !opt_filter_verified_goal;
194
   status = !opt_status;
195 196
  },!should_exit

197
let iter_proof_attempt_by_filter iter filters f session =
198
  (* provers *)
199 200 201
  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
202
  (* three value *)
203 204
  let three_value f v p =
    let iter_obsolete a =
205 206 207
      match v, p a with
        | FT_No, false -> f a
        | FT_Yes, true -> f a
208
        | _ -> () (* FT_All treated after *) in
209
    if v = FT_All then f else iter_obsolete in
210
  (* obsolete *)
211
  let f = three_value f filters.obsolete (fun a -> a.S.proof_obsolete) in
212
  (* archived *)
213
  let f = three_value f filters.archived (fun a -> a.S.proof_archived) in
214
  (* verified_goal *)
215
  let f = three_value f filters.verified_goal
216
    (fun a -> Opt.inhabited (S.goal_verified a.S.proof_parent)) in
217
  (* verified *)
218
  let f = three_value f filters.verified
219
    (fun p -> Opt.inhabited (S.proof_verified p)) in
220
  (* status *)
221 222 223 224 225 226 227 228 229 230
  let f = if filters.status = [] then f else
      (fun a -> match a.S.proof_state with
      | S.Done pr when List.mem pr.Call_provers.pr_answer filters.status -> f a
      | _ -> ()) in
  iter f session

let theory_iter_proof_attempt_by_filter filters f th =
  iter_proof_attempt_by_filter S.theory_iter_proof_attempt filters f th
let session_iter_proof_attempt_by_filter filters f s =
  iter_proof_attempt_by_filter S.session_iter_proof_attempt filters f s
231 232

let set_filter_verified_goal t = opt_filter_verified_goal := t
233 234 235 236 237 238

let opt_force_obsolete = ref false

let force_obsolete_spec =
  ["-F", Arg.Set opt_force_obsolete,
   " transform obsolete session"]
239 240 241 242 243 244 245 246 247 248 249



let rec ask_yn () =
  Format.printf "(y/n)@.";
  let answer = read_line () in
  match answer with
    | "y" -> true
    | "n" -> false
    | _ -> ask_yn ()

250
let ask_yn_nonblock ~callback =
251
  let b = Buffer.create 3 in
252
  let s = Strings.create 1 in
253 254 255 256 257 258
  Format.printf "(y/n)@.";
  fun () ->
    match Unix.select [Unix.stdin] [] [] 0. with
    | [],_,_ -> true
    | _ ->
      if Unix.read Unix.stdin s 1 0 = 0 then
259
        begin (* EndOfFile *) callback false; false end
260 261 262 263 264 265 266 267 268 269 270 271
      else begin
        if s.[0] <> '\n'
        then (Buffer.add_char b s.[0]; true)
        else
          match Buffer.contents b with
          | "y" -> callback true; false
          | "n" | "" -> callback false; false
          | _ ->
            Format.printf "(y/N)@.";
            Buffer.clear b;
            true
      end