controller_itp.ml 9.56 KB
Newer Older
1 2 3 4



open Format
Clément Fumex's avatar
Clément Fumex committed
5 6 7 8 9 10 11 12 13 14 15 16
open Session_itp

(** State of a proof *)
type proof_attempt_status =
    | Unedited (** editor not yet run for interactive proof *)
    | JustEdited (** edited but not run yet *)
    | Interrupted (** external proof has never completed *)
    | Scheduled (** external proof attempt is scheduled *)
    | Running (** external proof attempt is in progress *)
    | Done of Call_provers.prover_result (** external proof done *)
    | InternalFailure of exn (** external proof aborted by internal error *)

MARCHE Claude's avatar
MARCHE Claude committed
17 18 19 20 21 22 23 24 25 26 27
let print_status fmt st =
  match st with
  | Unedited -> fprintf fmt "Unedited"
  | JustEdited -> fprintf fmt "JustEdited"
  | Interrupted -> fprintf fmt "Interrupted"
  | Scheduled -> fprintf fmt "Scheduled"
  | Running -> fprintf fmt "Running"
  | Done r -> fprintf fmt "Done(%a)" Call_provers.print_prover_result r
  | InternalFailure e -> fprintf fmt "InternalFailure(%a)" Exn_printer.exn_printer e

type transformation_status =
28
  | TSscheduled | TSdone of transID | TSfailed
29 30 31 32

let print_trans_status fmt st =
  match st with
  | TSscheduled -> fprintf fmt "TScheduled"
33
  | TSdone tid -> fprintf fmt "TSdone" (* TODO print tid *)
34
  | TSfailed -> fprintf fmt "TSfailed"
Clément Fumex's avatar
Clément Fumex committed
35

36 37 38 39 40 41 42 43
open Ident

type proof_state = {
    th_state: bool Hid.t;
    tn_state: bool Htn.t;
    pn_state : bool Hpn.t;
  }

Clément Fumex's avatar
Clément Fumex committed
44
let init_proof_state ses =
45 46 47 48
  {th_state = Hid.create 7;
   tn_state = Htn.create 42;
   pn_state = Hpn.create 42}

49
type controller =
50
  { mutable controller_session : Session_itp.session;
51
    proof_state : proof_state;
52
    controller_env : Env.env;
53 54 55
    controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
  }

56
let create_controller env s = {
57
    controller_session = s;
Clément Fumex's avatar
Clément Fumex committed
58
    proof_state = init_proof_state s;
59
    controller_env = env;
60 61 62
    controller_provers = Whyconf.Hprover.create 7;
}

Clément Fumex's avatar
Clément Fumex committed
63 64 65
let tn_proved c tid = Htn.find_def c.proof_state.tn_state false tid
let pn_proved c pid = Hpn.find_def c.proof_state.pn_state false pid
let th_proved c th  = Hid.find_def c.proof_state.th_state false th
66 67 68 69 70

(* Update the result of the theory according to its children *)
let update_theory th ps =
  let goals = theory_goals th in
  Hid.replace ps.th_state (theory_name th)
71
    (List.for_all (fun id -> Hpn.find_def ps.pn_state false id) goals)
72 73 74

let rec propagate_proof c (id: Session_itp.proofNodeID) =
  let tr_list = get_transformations c.controller_session id in
Clément Fumex's avatar
Clément Fumex committed
75 76
  let new_state = List.exists (fun id -> tn_proved c id) tr_list in
  if new_state != pn_proved c id then
77 78 79 80 81 82 83
    begin
      Hpn.replace c.proof_state.pn_state id new_state;
      update_proof c id
    end

and propagate_trans c (tid: Session_itp.transID) =
  let proof_list = get_sub_tasks c.controller_session tid in
Clément Fumex's avatar
Clément Fumex committed
84 85
  let cur_state = tn_proved c tid in
  let new_state = List.for_all (fun id -> pn_proved c id) proof_list in
86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107
  if cur_state != new_state then
    begin
      Htn.replace c.proof_state.tn_state tid new_state;
      propagate_proof c (get_trans_parent c.controller_session tid)
    end

and update_proof c id =
  match get_proof_parent c.controller_session id with
  | Theory th -> update_theory th c.proof_state
  | Trans tid -> propagate_trans c tid

(* [update_proof_node c id b] Update the whole proof_state
   of c according to the result (id, b) *)
let update_proof_node c id b =
  Hpn.replace c.proof_state.pn_state id b;
  update_proof c id

(* [update_trans_node c id b] Update the proof_state of c to take the result of (id,b). Then
   propagates it to its parents *)
let update_trans_node c id b =
  Htn.replace c.proof_state.tn_state id b;
  propagate_proof c (get_trans_parent c.controller_session id)
108

109

110 111
module type Scheduler = sig
  val timeout: ms:int -> (unit -> bool) -> unit
MARCHE Claude's avatar
MARCHE Claude committed
112
  val idle: prio:int -> (unit -> bool) -> unit
113 114 115 116 117
end


module Make(S : Scheduler) = struct

MARCHE Claude's avatar
MARCHE Claude committed
118 119 120 121 122 123 124 125 126
let scheduled_proof_attempts = Queue.create ()

let prover_tasks_in_progress = Queue.create ()

let timeout_handler_running = ref false

let max_number_of_running_provers = ref 1

let number_of_running_provers = ref 0
127
module Hprover = Whyconf.Hprover
MARCHE Claude's avatar
MARCHE Claude committed
128

129
(*
MARCHE Claude's avatar
MARCHE Claude committed
130 131 132 133 134 135 136 137 138
let dummy_result =
  {
    pr_answer = Call_provers.Unknown ("I'm dumb", None);
    pr_status = Unix.WEXITED 0;
    pr_output = "";
    pr_time   = 3.14;
    pr_steps  = 42;
    pr_model  = Model_parser.default_model;
}
139
 *)
MARCHE Claude's avatar
MARCHE Claude committed
140

141 142 143 144
let build_prover_call c id pr limit callback =
  let (config_pr,driver) = Hprover.find c.controller_provers pr in
  let command =
    Whyconf.get_complete_command config_pr
MARCHE Claude's avatar
MARCHE Claude committed
145
          ~with_steps:Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
146 147
  let task = Session_itp.get_task c.controller_session id in
  let call =
MARCHE Claude's avatar
itp  
MARCHE Claude committed
148
    Driver.prove_task ?old:None ~cntexample:true ~inplace:false ~command
149 150
                      ~limit driver task
  in
151
  let pa = (c.controller_session,id,pr,callback,false,call) in
MARCHE Claude's avatar
MARCHE Claude committed
152 153 154 155 156 157
  Queue.push pa prover_tasks_in_progress

let timeout_handler () =
  (* examine all the prover tasks in progress *)
  let q = Queue.create () in
  while not (Queue.is_empty prover_tasks_in_progress) do
158
    let (ses,id,pr,callback,started,call) as c = Queue.pop prover_tasks_in_progress in
159
    match Call_provers.query_call call with
MARCHE Claude's avatar
MARCHE Claude committed
160 161 162 163 164
    | Call_provers.NoUpdates -> Queue.add c q
    | Call_provers.ProverStarted ->
       assert (not started);
       callback Running;
       incr number_of_running_provers;
165
       Queue.add (ses,id,pr,callback,true,call) q
MARCHE Claude's avatar
MARCHE Claude committed
166 167
    | Call_provers.ProverFinished res ->
       if started then decr number_of_running_provers;
168 169 170
       (* update the session *)
       update_proof_attempt ses id pr res;
       (* inform the callback *)
MARCHE Claude's avatar
MARCHE Claude committed
171 172 173
       callback (Done res)
  done;
  Queue.transfer q prover_tasks_in_progress;
174
  (* if the number of prover tasks is less than 3 times the maximum
MARCHE Claude's avatar
MARCHE Claude committed
175 176 177
     number of running provers, then we heuristically decide to add
     more tasks *)
  try
178
    for _i = Queue.length prover_tasks_in_progress
MARCHE Claude's avatar
MARCHE Claude committed
179
        to 3 * !max_number_of_running_provers do
180
      let (c,id,pr,timelimit,callback) = Queue.pop scheduled_proof_attempts in
MARCHE Claude's avatar
MARCHE Claude committed
181
      try
182
        build_prover_call c id pr timelimit callback
MARCHE Claude's avatar
MARCHE Claude committed
183 184
      with e when not (Debug.test_flag Debug.stack_trace) ->
        Format.eprintf
185
          "@[Exception raised in Controller_itp.build_prover_call:@ %a@.@]"
MARCHE Claude's avatar
MARCHE Claude committed
186 187 188 189 190 191 192 193 194 195 196 197 198
          Exn_printer.exn_printer e;
        callback (InternalFailure e)
    done;
    true
  with Queue.Empty -> true

let run_timeout_handler () =
  if not !timeout_handler_running then
    begin
      timeout_handler_running := true;
      S.timeout ~ms:125 timeout_handler;
    end

199
let schedule_proof_attempt_r c id pr ~limit ~callback =
200
  graft_proof_attempt c.controller_session id pr ~timelimit:limit.Call_provers.limit_time;
201
  Queue.add (c,id,pr,limit,callback) scheduled_proof_attempts;
MARCHE Claude's avatar
MARCHE Claude committed
202 203
  callback Scheduled;
  run_timeout_handler ()
Clément Fumex's avatar
Clément Fumex committed
204

205 206
let schedule_proof_attempt c id pr ~limit ~callback =
  let callback s = (match s with
Clément Fumex's avatar
Clément Fumex committed
207
  | Done pr -> update_proof_node c id (pr.Call_provers.pr_answer == Call_provers.Valid)
208 209 210 211 212 213 214
  | Interrupted | InternalFailure _ -> update_proof_node c id false
  | _ -> ());
  callback s
  in
  schedule_proof_attempt_r c id pr ~limit:limit ~callback:callback

let schedule_transformation_r c id name args ~callback =
215 216 217
  let apply_trans () =
    let task = get_task c.controller_session id in
    try
218
      let subtasks = Trans.apply_transform_args name c.controller_env args task in
219 220
      let tid = graft_transf c.controller_session id name args subtasks in
      callback (TSdone tid);
221 222 223 224 225 226 227 228 229 230
      false
    with e when not (Debug.test_flag Debug.stack_trace) ->
      Format.eprintf
        "@[Exception raised in Trans.apply_transform %s:@ %a@.@]"
          name Exn_printer.exn_printer e;
        callback TSfailed;
        false
  in
  S.idle ~prio:0 apply_trans;
  callback TSscheduled
Clément Fumex's avatar
Clément Fumex committed
231

232 233 234 235 236 237 238
let schedule_transformation c id name args ~callback =
  let callback s = (match s with
  | TSdone tid -> update_trans_node c tid false (*(get_sub_tasks c.controller_session tid = [])*) (* TODO need to change schedule transformation to get the id ? *)
  | TSfailed -> ()
  | _ -> ()); callback s in
  schedule_transformation_r c id name args ~callback:callback

Clément Fumex's avatar
Clément Fumex committed
239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257
let read_file env ?format fn =
  let theories = Env.read_file Env.base_language env ?format fn in
  let ltheories =
    Stdlib.Mstr.fold
      (fun name th acc ->
        (* Hack : with WP [name] and [th.Theory.th_name.Ident.id_string] *)
        let th_name =
          Ident.id_register (Ident.id_derive name th.Theory.th_name) in
         match th.Theory.th_name.Ident.id_loc with
           | Some l -> (l,th_name,th)::acc
           | None   -> (Loc.dummy_position,th_name,th)::acc)
      theories []
  in
  let th =  List.sort
      (fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
      ltheories
  in
  List.map (fun (_,_,a) -> a) th

258 259
let add_file c ?format fname =
  let theories = read_file c.controller_env ?format fname in
MARCHE Claude's avatar
MARCHE Claude committed
260
  add_file_section c.controller_session fname theories format (empty_session ()) []
MARCHE Claude's avatar
MARCHE Claude committed
261

262 263 264 265 266
(** reload files, associating old proof attempts and transformations
    to the new goals.  old theories and old goals for which we cannot
    find a corresponding new theory resp. old goal are kept, with
    tasks associated to them *)

MARCHE Claude's avatar
MARCHE Claude committed
267 268 269 270 271 272 273 274 275 276 277 278
let merge_file (old_ses : session) (c : controller) _ file =
  let format = file.file_format in
  let old_theories = file.file_theories in
  let new_theories =
    try
      read_file c.controller_env file.file_name ?format
    with _ -> (* TODO: filter only syntax error and typing errors *)
      []
  in
  add_file_section
    c.controller_session file.file_name new_theories format old_ses old_theories

279 280 281 282

let reload_files (c : controller)  =
  let old_ses = c.controller_session in
  c.controller_session <- empty_session ();
283 284
  Stdlib.Hstr.iter (fun _ f -> add_file c f.file_name) (get_files old_ses)
  (* Stdlib.Hstr.iter (merge_file old_ses c) (get_files old_ses) *)
285 286

end