controller_itp.ml 29.8 KB
Newer Older
1
open Format
Clément Fumex's avatar
Clément Fumex committed
2 3
open Session_itp

4 5
exception Noprogress

6 7 8
let () = Exn_printer.register
    (fun fmt e ->
      match e with
Sylvain Dailler's avatar
Sylvain Dailler committed
9 10
      | Noprogress ->
          Format.fprintf fmt "The transformation made no progress.\n"
11 12
      | _ -> raise e)

Clément Fumex's avatar
Clément Fumex committed
13 14 15 16 17 18 19 20 21
(** 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 *)
22
    | Uninstalled of Whyconf.prover (** prover is uninstalled *)
Clément Fumex's avatar
Clément Fumex committed
23

MARCHE Claude's avatar
MARCHE Claude committed
24 25
let print_status fmt st =
  match st with
Sylvain Dailler's avatar
Sylvain Dailler committed
26 27 28 29 30 31 32 33 34 35 36
  | 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
  | Uninstalled pr    ->
      fprintf fmt "Prover %a is uninstalled" Whyconf.print_prover pr
MARCHE Claude's avatar
MARCHE Claude committed
37 38

type transformation_status =
39
  | TSscheduled | TSdone of transID | TSfailed of (proofNodeID * exn)
40 41 42 43

let print_trans_status fmt st =
  match st with
  | TSscheduled -> fprintf fmt "TScheduled"
44
  | TSdone _tid -> fprintf fmt "TSdone" (* TODO print tid *)
45
  | TSfailed _e -> fprintf fmt "TSfailed"
Clément Fumex's avatar
Clément Fumex committed
46

47 48 49 50
type strategy_status = STSgoto of proofNodeID * int | STShalt

let print_strategy_status fmt st =
  match st with
Sylvain Dailler's avatar
Sylvain Dailler committed
51 52
  | STSgoto(id,n) ->
      fprintf fmt "goto step %d in proofNode %a" n print_proofNodeID id
53 54 55
  | STShalt -> fprintf fmt "halt"


56 57 58 59 60 61 62 63
open Ident

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

64
let init_proof_state () =
65 66 67 68
  {th_state = Hid.create 7;
   tn_state = Htn.create 42;
   pn_state = Hpn.create 42}

69
type controller =
Sylvain Dailler's avatar
Sylvain Dailler committed
70 71 72 73 74
  { mutable controller_session: Session_itp.session;
    proof_state: proof_state;
    controller_env: Env.env;
    controller_provers:
      (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
75 76
  }

77 78 79 80 81
let clear_proof_state c =
  Hid.clear c.proof_state.th_state;
  Htn.clear c.proof_state.tn_state;
  Hpn.clear c.proof_state.pn_state

82 83
let create_controller env =
  {
84 85
    controller_session = Session_itp.dummy_session;
    proof_state = init_proof_state ();
86
    controller_env = env;
87
    controller_provers = Whyconf.Hprover.create 7;
88
  }
89

90
let init_controller s c =
91
  clear_proof_state (c);
92 93
  c.controller_session <- s

Clément Fumex's avatar
Clément Fumex committed
94 95
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
96 97 98 99 100
let th_proved c th  =
  if (theory_goals th = []) then
    Hid.find_def c.proof_state.th_state true (theory_name th)
  else
    Hid.find_def c.proof_state.th_state false (theory_name th)
101 102 103 104 105
let file_proved c f =
  if f.file_theories = [] then
    true
  else
    List.for_all (fun th -> th_proved c th) f.file_theories
106

107 108 109 110 111 112 113 114 115
let any_proved cont any : bool =
  match any with
  | AFile file -> file_proved cont file
  | ATh th -> th_proved cont th
  | ATn tn -> tn_proved cont tn
  | APn pn -> pn_proved cont pn
  | APa pa ->
      begin
        let pa = get_proof_attempt_node cont.controller_session pa in
Sylvain Dailler's avatar
Sylvain Dailler committed
116
        match pa.Session_itp.proof_state with
117 118 119 120 121 122 123 124 125
        | None -> false
        | Some pa ->
          begin
            match pa.Call_provers.pr_answer with
            | Call_provers.Valid -> true
            | _ -> false
          end
      end

126 127 128 129 130 131 132 133
let remove_any_proof_state cont any : unit =
  match any with
  | AFile _file -> ()
  | ATh th     -> Hid.remove cont.proof_state.th_state (theory_name th)
  | APn pn     -> Hpn.remove cont.proof_state.pn_state pn
  | ATn tn     -> Htn.remove cont.proof_state.tn_state tn
  | APa _pa     -> ()

134
(* Update the result of the theory according to its children *)
135
let update_theory_proof_state notification ps th =
136
  let goals = theory_goals th in
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
  if Hid.mem ps.th_state (theory_name th) then
  begin
    let old_state = Hid.find_def ps.th_state false (theory_name th) in
    let new_state =
      List.for_all (fun id -> Hpn.find_def ps.pn_state false id) goals in
    if new_state != old_state then
      begin
        Hid.replace ps.th_state (theory_name th) new_state;
        notification (ATh th) new_state
      end
  end
  else
  begin
    let new_state =
      List.for_all (fun id -> Hpn.find_def ps.pn_state false id) goals in
    Hid.replace ps.th_state (theory_name th) new_state;
    notification (ATh th) new_state
  end
155

156
let rec propagate_proof notification c (id: Session_itp.proofNodeID) =
157
  let tr_list = get_transformations c.controller_session id in
Clément Fumex's avatar
Clément Fumex committed
158 159
  let new_state = List.exists (fun id -> tn_proved c id) tr_list in
  if new_state != pn_proved c id then
160 161
    begin
      Hpn.replace c.proof_state.pn_state id new_state;
162 163
      notification (APn id) new_state;
      update_proof notification c id
164 165
    end

166
and propagate_trans notification c (tid: Session_itp.transID) =
167
  let proof_list = get_sub_tasks c.controller_session tid in
Clément Fumex's avatar
Clément Fumex committed
168 169
  let cur_state = tn_proved c tid in
  let new_state = List.for_all (fun id -> pn_proved c id) proof_list in
170 171 172
  if cur_state != new_state then
    begin
      Htn.replace c.proof_state.tn_state tid new_state;
173 174
      notification (ATn tid) new_state;
      propagate_proof notification c (get_trans_parent c.controller_session tid)
175 176
    end

177
and update_proof notification c id =
178
  match get_proof_parent c.controller_session id with
179 180
  | Theory th -> update_theory_proof_state notification c.proof_state th
  | Trans tid -> propagate_trans notification c tid
181 182 183

(* [update_proof_node c id b] Update the whole proof_state
   of c according to the result (id, b) *)
184
let update_proof_node notification c id b =
185
  if Hpn.mem c.proof_state.pn_state id then
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
  begin
    let b' = Hpn.find_def c.proof_state.pn_state false id in
    if b != b' then
    begin
      Hpn.replace c.proof_state.pn_state id b;
      notification (APn id) b;
      update_proof notification c id
    end
  end
  else
  begin
    Hpn.replace c.proof_state.pn_state id b;
    notification (APn id) b;
    update_proof notification c id
  end

(* [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 notification c id b =
205
  if Htn.mem c.proof_state.tn_state id then
206 207 208 209 210 211 212 213 214 215 216 217
  begin
    let b' = Htn.find_def c.proof_state.tn_state false id in
    if b != b' then
    begin
      Htn.replace c.proof_state.tn_state id b;
      notification (ATn id) b
    end
  end
  else
    (Htn.replace c.proof_state.tn_state id b;
     notification (ATn id) b);
  propagate_proof notification c (get_trans_parent c.controller_session id)
218

219 220 221 222 223 224 225 226 227 228 229
(** TODO make the whole reloading of proof_state more efficient and natural *)

(* Note that f has side effect on the elements of l. We want this effect to
   happen. That's why we cannot use List.for_all (respectively List.exists)
   directly (List.for_all stops on first element that evaluates to false) *)
let for_all_se f l =
  List.for_all (fun b -> b) (List.map f l)

let exists_se f l =
  List.exists (fun b -> b) (List.map f l)

230
(* init proof state after reload *)
231
let rec reload_goal_proof_state c g =
232 233 234
  let ses = c.controller_session in
  let tr_list = get_transformations ses g in
  let pa_list = get_proof_attempts ses g in
235
  let proved = exists_se (reload_trans_proof_state c) tr_list in
236
  let proved = exists_se reload_pa_proof_state pa_list || proved in
237 238 239
  Hpn.replace c.proof_state.pn_state g proved;
  proved

240
and reload_trans_proof_state c tr =
241
  let proof_list = get_sub_tasks c.controller_session tr in
242
  let proved = for_all_se (reload_goal_proof_state c) proof_list in
243 244 245 246 247 248 249 250 251 252 253 254
  Htn.replace c.proof_state.tn_state tr proved;
  proved

and reload_pa_proof_state pa =
  match pa.proof_obsolete, pa.Session_itp.proof_state with
  | false, Some pr when pr.Call_provers.pr_answer = Call_provers.Valid -> true
  | _ -> false

(* to be called after reload *)
let reload_theory_proof_state c th =
  let ps = c.proof_state in
  let goals = theory_goals th in
255
  let proved = for_all_se (reload_goal_proof_state c) goals in
256 257 258 259 260 261 262 263 264 265 266
  Hid.replace ps.th_state (theory_name th) proved

(* to be called after reload *)
let reload_file_proof_state c f =
  List.iter (reload_theory_proof_state c) f.file_theories

(* to be called after reload *)
let reload_session_proof_state c =
  Stdlib.Hstr.iter
    (fun _ f -> reload_file_proof_state c f)
    (get_files c.controller_session)
267

268 269 270 271 272 273 274
(* Get children of any without proofattempts *)
let get_undetached_children_no_pa s any : any list =
  match any with
  | AFile f -> List.map (fun th -> ATh th) f.file_theories
  | ATh th  -> List.map (fun g -> APn g) (theory_goals th)
  | ATn tn  -> List.map (fun pn -> APn pn) (get_sub_tasks s tn)
  | APn pn  -> List.map (fun tn -> ATn tn) (get_transformations s pn)
Sylvain Dailler's avatar
Sylvain Dailler committed
275
  | APa _ -> []
276

277 278 279 280 281 282 283 284 285 286 287 288
(* printing *)

module PSession = struct

  open Stdlib

  type any =
    | Session
    | File of file
    | Theory of theory
    | Goal of proofNodeID
    | Transf of transID
289
    | ProofAttempt of proof_attempt_node
290 291 292 293 294 295 296 297 298 299 300

  type 'a t = { tcont : controller;
                tkind : any }

  let decomp x =
    let s = x.tcont.controller_session in
    let n y acc = { x with tkind = y } :: acc in
    match x.tkind with
    | Session -> "", Hstr.fold (fun _ f -> n (File f)) (get_files s) []
    | File f ->
       f.file_name,
Sylvain Dailler's avatar
Sylvain Dailler committed
301 302 303 304
       List.fold_right
          (fun th -> n (Theory th))
          f.file_detached_theories
          (List.fold_right (fun th -> n (Theory th)) f.file_theories [])
305 306 307
    | Theory th ->
       let id = theory_name th in
       let name = id.Ident.id_string in
308
       let name = if th_proved x.tcont th then name^"!" else name^"?" in
309
       name,
Sylvain Dailler's avatar
Sylvain Dailler committed
310 311 312 313
       List.fold_right
         (fun g -> n (Goal g))
         (theory_goals th)
         (List.fold_right (fun g -> n (Goal g)) (theory_detached_goals th) [])
314 315 316
    | Goal id ->
       let gid = get_proof_name s id in
       let name = gid.Ident.id_string in
317
       let name = if pn_proved x.tcont id then name^"!" else name^"?" in
318 319 320 321 322 323 324
       let pas = get_proof_attempts s id in
       let trs = get_transformations s id in
       name,
       List.fold_right (fun g -> n (Transf g)) trs
                       (List.fold_right (fun g -> n (ProofAttempt g)) pas [])
    | ProofAttempt pa ->
       Pp.sprintf_wnl "%a%s%s"
Sylvain Dailler's avatar
Sylvain Dailler committed
325 326 327 328 329
          Whyconf.print_prover pa.prover
          (match pa.Session_itp.proof_state with
          | Some { Call_provers.pr_answer = Call_provers.Valid} -> ""
          | _ -> "?")
          (if pa.proof_obsolete then "O" else ""), []
330 331
    | Transf id ->
       let name = get_transf_name s id in
332
       let name = if tn_proved x.tcont id then name^"!" else name^"?" in
333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349
       let sts = get_sub_tasks s id in
       let dsts = get_detached_sub_tasks s id in
       name,
       List.fold_right (fun g -> n (Goal g)) sts
                       (List.fold_right (fun g -> n (Goal g)) dsts [])

end

module P = Print_tree.PMake(PSession)

let print_session fmt c =
  P.print fmt { PSession.tcont = c; PSession.tkind = PSession.Session }

(*********)



350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374
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


(** 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 *)

375
let merge_file (old_ses : session) (c : controller) ~use_shapes _ file =
376 377 378 379 380 381
  let format = file.file_format in
  let old_theories = file.file_theories in
  let file_name = Filename.concat (get_dir old_ses) file.file_name in
  let new_theories =
    try
      read_file c.controller_env file_name ?format
382 383
    with e -> (* TODO: filter only syntax error and typing errors *)
      raise e
384
  in
385
  merge_file_section
386 387
    c.controller_session ~use_shapes ~old_ses ~old_theories
    ~env:c.controller_env file_name new_theories format;
388
  reload_session_proof_state c
389

390
let reload_files (c : controller) ~use_shapes =
391
  let old_ses = c.controller_session in
Sylvain Dailler's avatar
Sylvain Dailler committed
392 393
  c.controller_session <-
    empty_session ~shape_version:(get_shape_version old_ses) (get_dir old_ses);
394 395 396 397 398 399 400
  try
    Stdlib.Hstr.iter
      (fun f -> merge_file old_ses c ~use_shapes f)
      (get_files old_ses)
  with e ->
    c.controller_session <- old_ses;
    raise e
401 402 403 404

let add_file c ?format fname =
  let theories = read_file c.controller_env ?format fname in
  add_file_section ~use_shapes:false c.controller_session fname theories format
405

406 407 408 409 410
(* Update the proof_state according to new false state and then remove
   the subtree *)
let remove_subtree c (n: any) ~removed ~node_change =
  let removed = (fun x -> removed x; remove_any_proof_state c x) in
  let parent = get_any_parent c.controller_session n in
411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433
  (* Note that this line can raise RemoveError when called on inappropriate
     node (attached theory / goals) *)
  Session_itp.remove_subtree c.controller_session n ~notification:removed;
  (match parent with
  | Some (APn parent) ->
      (* If proof_state of the parent is actually changed update the branch
         otherwise do nothing *)
      let tr_list = get_transformations c.controller_session parent in
      let pa_list = get_proof_attempts c.controller_session parent in
      let proved = List.exists (tn_proved c) tr_list in
      let proved = List.exists reload_pa_proof_state pa_list || proved in
      if proved then
        ()
      else
        update_proof_node node_change c parent false
  | Some _ ->
      (* This case corresponds to removal of detached node. We don't need to
         update the proof_state *)
      ()
  | None ->
      (* Cannot remove root. Note that this should already have failed in call
         to Session_itp.remove_subtree *)
      raise RemoveError)
434 435 436 437 438 439

module type Scheduler = sig
  val timeout: ms:int -> (unit -> bool) -> unit
  val idle: prio:int -> (unit -> bool) -> unit
end

440 441
module Make(S : Scheduler) = struct

MARCHE Claude's avatar
MARCHE Claude committed
442 443 444 445 446 447 448 449
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

450 451 452 453 454
let set_max_tasks n =
  max_number_of_running_provers := n;
  Prove_client.set_max_running_provers n


MARCHE Claude's avatar
MARCHE Claude committed
455
let number_of_running_provers = ref 0
456

457 458 459 460
let observer = ref (fun _ _ _ -> ())

let register_observer = (:=) observer

461
module Hprover = Whyconf.Hprover
MARCHE Claude's avatar
MARCHE Claude committed
462

463 464 465
let build_prover_call c id pr limit callback =
  let (config_pr,driver) = Hprover.find c.controller_provers pr in
  let command =
Sylvain Dailler's avatar
Sylvain Dailler committed
466 467 468
    Whyconf.get_complete_command
      config_pr
      ~with_steps:Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
469
  let task = Session_itp.get_task c.controller_session id in
470
  let table = Session_itp.get_table c.controller_session id in
471
  let call =
MARCHE Claude's avatar
itp  
MARCHE Claude committed
472
    Driver.prove_task ?old:None ~cntexample:true ~inplace:false ~command
473
                      ~limit ?name_table:table driver task
474
  in
475
  let pa = (c.controller_session,id,pr,callback,false,call) in
MARCHE Claude's avatar
MARCHE Claude committed
476 477 478 479 480 481
  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
Sylvain Dailler's avatar
Sylvain Dailler committed
482 483
    let (ses,id,pr,callback,started,call) as c =
      Queue.pop prover_tasks_in_progress in
484
    match Call_provers.query_call call with
MARCHE Claude's avatar
MARCHE Claude committed
485 486 487 488 489
    | Call_provers.NoUpdates -> Queue.add c q
    | Call_provers.ProverStarted ->
       assert (not started);
       callback Running;
       incr number_of_running_provers;
490
       Queue.add (ses,id,pr,callback,true,call) q
MARCHE Claude's avatar
MARCHE Claude committed
491 492
    | Call_provers.ProverFinished res ->
       if started then decr number_of_running_provers;
493 494 495
       (* update the session *)
       update_proof_attempt ses id pr res;
       (* inform the callback *)
MARCHE Claude's avatar
MARCHE Claude committed
496
       callback (Done res)
497 498 499 500 501 502 503 504
    | Call_provers.ProverInterrupted ->
       if started then decr number_of_running_provers;
       (* inform the callback *)
       callback (Interrupted)
    | Call_provers.InternalFailure exn ->
       if started then decr number_of_running_provers;
       (* inform the callback *)
       callback (InternalFailure (exn))
MARCHE Claude's avatar
MARCHE Claude committed
505 506
  done;
  Queue.transfer q prover_tasks_in_progress;
507
  (* if the number of prover tasks is less than 3 times the maximum
MARCHE Claude's avatar
MARCHE Claude committed
508 509
     number of running provers, then we heuristically decide to add
     more tasks *)
510 511 512 513 514 515 516 517
  begin
    try
      for _i = Queue.length prover_tasks_in_progress
          to 3 * !max_number_of_running_provers do
        let (c,id,pr,limit,callback) = Queue.pop scheduled_proof_attempts in
        try
          build_prover_call c id pr limit callback
        with e when not (Debug.test_flag Debug.stack_trace) ->
518
          (*Format.eprintf
519
            "@[Exception raised in Controller_itp.build_prover_call:@ %a@.@]"
520
            Exn_printer.exn_printer e;*)
521 522 523 524 525 526 527 528 529
          callback (InternalFailure e)
      done
  with Queue.Empty -> ()
  end;
  let scheduled = Queue.length scheduled_proof_attempts in
  let waiting_or_running = Queue.length prover_tasks_in_progress in
  let running = !number_of_running_provers in
  !observer scheduled (waiting_or_running - running) running;
  true
MARCHE Claude's avatar
MARCHE Claude committed
530

531 532 533 534 535 536 537 538 539 540 541 542 543 544
let interrupt () =
  while not (Queue.is_empty prover_tasks_in_progress) do
    let (_ses,_id,_pr,callback,_started,_call) =
      Queue.pop prover_tasks_in_progress in
    (* TODO: apply some Call_provers.interrupt_call call *)
    callback Interrupted
  done;
  number_of_running_provers := 0;
  while not (Queue.is_empty scheduled_proof_attempts) do
    let (_c,_id,_pr,_limit,callback) = Queue.pop scheduled_proof_attempts in
    callback Interrupted
  done;
  !observer 0 0 0

MARCHE Claude's avatar
MARCHE Claude committed
545 546 547 548 549 550 551
let run_timeout_handler () =
  if not !timeout_handler_running then
    begin
      timeout_handler_running := true;
      S.timeout ~ms:125 timeout_handler;
    end

552
let schedule_proof_attempt_r c id pr ~limit ~callback =
553
  let panid =
554
    graft_proof_attempt c.controller_session id pr ~limit
555 556 557
  in
  Queue.add (c,id,pr,limit,callback panid) scheduled_proof_attempts;
  callback panid Scheduled;
MARCHE Claude's avatar
MARCHE Claude committed
558
  run_timeout_handler ()
Clément Fumex's avatar
Clément Fumex committed
559

560
let schedule_proof_attempt c id pr ~limit ~callback ~notification =
Sylvain Dailler's avatar
Sylvain Dailler committed
561
  let callback panid s = callback panid s;
Sylvain Dailler's avatar
Sylvain Dailler committed
562
    (match s with
Sylvain Dailler's avatar
Sylvain Dailler committed
563 564 565 566
    | Done pr -> update_proof_node notification c id
          (pr.Call_provers.pr_answer == Call_provers.Valid)
    | Interrupted | InternalFailure _ ->
        update_proof_node notification c id false
Sylvain Dailler's avatar
Sylvain Dailler committed
567
    | _ -> ())
568
  in
569
  schedule_proof_attempt_r c id pr ~limit ~callback
570 571

let schedule_transformation_r c id name args ~callback =
572 573
  let apply_trans () =
    let task = get_task c.controller_session id in
574 575 576
    let table = match get_table c.controller_session id with
    | None -> raise (Task.Bad_name_table "Controller_itp.schedule_transformation_r")
    | Some table -> table in
577 578
    begin
      try
Sylvain Dailler's avatar
Sylvain Dailler committed
579
        let subtasks =
580
          Trans.apply_transform_args name c.controller_env args table task in
581 582 583 584
        (* if result is same as input task, consider it as a failure *)
        begin
          match subtasks with
          | [t'] when Task.task_equal t' task ->
585
             callback (TSfailed (id, Noprogress))
586 587 588 589 590
          | _ ->
             let tid = graft_transf c.controller_session id name args subtasks in
             callback (TSdone tid)
        end
      with e when not (Debug.test_flag Debug.stack_trace) ->
591
        (* Format.eprintf
592
          "@[Exception raised in Trans.apply_transform %s:@ %a@.@]"
593
          name Exn_printer.exn_printer e; TODO *)
594
        callback (TSfailed (id, e))
595 596
    end;
    false
597 598 599
  in
  S.idle ~prio:0 apply_trans;
  callback TSscheduled
Clément Fumex's avatar
Clément Fumex committed
600

601
let schedule_transformation c id name args ~callback ~notification =
602
  let callback s = callback s; (match s with
603 604 605 606 607 608
      | TSdone tid ->
        let has_subtasks =
          match get_sub_tasks c.controller_session tid with
          | [] -> true
          | _ -> false
        in
609
        update_trans_node notification c tid has_subtasks
610
      | TSfailed _e -> ()
611
      | _ -> ()) in
612 613 614 615
  schedule_transformation_r c id name args ~callback

open Strategy

Sylvain Dailler's avatar
Sylvain Dailler committed
616 617
let run_strategy_on_goal
    c id strat ~callback_pa ~callback_tr ~callback ~notification =
618 619 620 621 622 623
  let rec exec_strategy pc strat g =
    if pc < 0 || pc >= Array.length strat then
      callback STShalt
    else
      match Array.get strat pc with
      | Icall_prover(p,timelimit,memlimit) ->
MARCHE Claude's avatar
MARCHE Claude committed
624 625
         let callback panid res =
           callback_pa panid res;
626 627 628 629 630
           match res with
           | Scheduled | Running -> (* nothing to do yet *) ()
           | Done { Call_provers.pr_answer = Call_provers.Valid } ->
              (* proof succeeded, nothing more to do *)
              callback STShalt
631 632
           | Interrupted | InternalFailure _ ->
              callback STShalt
633 634 635 636 637
           | Done _ ->
              (* proof did not succeed, goto to next step *)
              callback (STSgoto (g,pc+1));
              let run_next () = exec_strategy (pc+1) strat g; false in
              S.idle ~prio:0 run_next
638
           | Unedited | JustEdited | Uninstalled _ ->
639 640 641 642 643 644
                         (* should not happen *)
                         assert false
         in
         let limit = { Call_provers.empty_limit with
                       Call_provers.limit_time = timelimit;
                       limit_mem  = memlimit} in
645
         schedule_proof_attempt c g p ~limit ~callback ~notification
646 647
      | Itransform(trname,pcsuccess) ->
         let callback ntr =
MARCHE Claude's avatar
MARCHE Claude committed
648
           callback_tr ntr;
649
           match ntr with
650
           | TSfailed _e -> (* transformation failed *)
651 652 653 654 655 656 657 658 659 660 661 662
              callback (STSgoto (g,pc+1));
              let run_next () = exec_strategy (pc+1) strat g; false in
              S.idle ~prio:0 run_next
           | TSscheduled -> ()
           | TSdone tid ->
              List.iter
                (fun g ->
                 callback (STSgoto (g,pcsuccess));
                 let run_next () =
                   exec_strategy pcsuccess strat g; false
                 in
                 S.idle ~prio:0 run_next)
MARCHE Claude's avatar
MARCHE Claude committed
663
                (get_sub_tasks c.controller_session tid)
664
         in
665
         schedule_transformation c g trname [] ~callback ~notification
666 667 668 669 670 671
      | Igoto pc ->
         callback (STSgoto (g,pc));
         exec_strategy pc strat g
  in
  exec_strategy 0 strat id

Sylvain Dailler's avatar
Sylvain Dailler committed
672 673
let schedule_pa_with_same_arguments
    c (pa: proof_attempt_node) (pn: proofNodeID) ~callback ~notification =
Sylvain Dailler's avatar
Sylvain Dailler committed
674 675 676 677
  let prover = pa.prover in
  let limit = pa.limit in
  schedule_proof_attempt c pn prover ~limit ~callback ~notification

Sylvain Dailler's avatar
Sylvain Dailler committed
678 679
let schedule_tr_with_same_arguments
    c (tr: transID) (pn: proofNodeID) ~callback ~notification =
Sylvain Dailler's avatar
Sylvain Dailler committed
680 681 682 683 684
  let s = c.controller_session in
  let args = get_transf_args s tr in
  let name = get_transf_name s tr in
  schedule_transformation c pn name args ~callback ~notification

685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704
let clean_session c ~remove ~node_change =
  let is_valid (pa: proof_attempt_node) : bool =
    match pa.Session_itp.proof_state with
    | None -> false
    | Some pr ->
      begin
        match pr.Call_provers.pr_answer with
        | Call_provers.Valid -> true
        | _ -> false
      end
  in
  let s = c.controller_session in
  Session_itp.session_iter_proof_attempt
    (fun _ pa ->
      let pnid = pa.parent in
      Hprover.iter (fun _ paid ->
        if (not (is_valid (get_proof_attempt_node s paid))) then
          remove_subtree c ~removed:remove ~node_change (APa paid))
        (get_proof_attempt_ids s pnid)) s

705 706 707 708 709 710 711 712 713 714 715 716 717
let mark_as_obsolete ~node_change ~node_obsolete c any =
  let s = c.controller_session in
  match any with
  | APa n ->
    let parent = get_proof_attempt_parent s n in
    Session_itp.mark_obsolete s n;
    node_obsolete any true;
    let b = reload_goal_proof_state c parent in
    node_change (APn parent) b;
    update_proof_node node_change c parent b
  | _ -> ()


Sylvain Dailler's avatar
Sylvain Dailler committed
718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736
exception BadCopyPaste

(* Reproduce the transformation made on node on an other one *)
let rec copy_paste ~notification ~callback_pa ~callback_tr c from_any to_any =
  let s = c.controller_session in
  if (not (is_below s from_any to_any) &&
      not (is_below s to_any from_any)) then
    match from_any, to_any with
    | AFile _, AFile _ ->
        raise BadCopyPaste
    | ATh _from_th, ATh _to_th ->
        raise BadCopyPaste
    | APn from_pn, APn to_pn ->
      let from_pa_list = get_proof_attempts s from_pn in
      List.iter (fun x -> schedule_pa_with_same_arguments c x to_pn
          ~callback:callback_pa ~notification) from_pa_list;
      let from_tr_list = get_transformations s from_pn in
      let callback x st = callback_tr st;
        match st with
Sylvain Dailler's avatar
Sylvain Dailler committed
737 738
        | TSdone tid ->
          copy_paste c (ATn x) (ATn tid) ~notification ~callback_pa ~callback_tr
Sylvain Dailler's avatar
Sylvain Dailler committed
739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758
        | _ -> ()
      in
      List.iter (fun x -> schedule_tr_with_same_arguments c x to_pn
          ~callback:(callback x) ~notification) from_tr_list
    | ATn from_tn, ATn to_tn ->
        let from_tn_list = get_sub_tasks s from_tn in
        let to_tn_list = get_sub_tasks s to_tn in
        if (List.length from_tn_list = List.length to_tn_list) then
          List.iter2 (fun x y -> copy_paste c (APn x) (APn y)
              ~notification ~callback_pa ~callback_tr) from_tn_list to_tn_list
    | _ -> raise BadCopyPaste


let copy_detached ~copy c from_any =
  match from_any with
  | APn from_pn ->
    begin
      let pn_id = copy_proof_node_as_detached c.controller_session from_pn in
      let parent = get_any_parent c.controller_session from_any in
      match parent with
759
      | None -> raise (BadCopyDetached "copy_detached no parent")
Sylvain Dailler's avatar
Sylvain Dailler committed
760 761
      | Some parent ->
          copy ~parent (APn pn_id);
Sylvain Dailler's avatar
Sylvain Dailler committed
762 763
          copy_structure
            ~notification:copy c.controller_session (APn from_pn) (APn pn_id)
Sylvain Dailler's avatar
Sylvain Dailler committed
764
    end
765 766
  (* Only goal can be detached *)
  | _ -> raise (BadCopyDetached "copy_detached. Can only copy goal")
Sylvain Dailler's avatar
Sylvain Dailler committed
767 768


769
let replay_proof_attempt c pr limit (parid: proofNodeID) id ~callback ~notification =
770 771 772
  (* The replay can be done on a different machine so we need
     to check more things before giving the attempt to the scheduler *)
  if not (Hprover.mem c.controller_provers pr) then
773
    callback id (Uninstalled pr)
774
  else
775
    schedule_proof_attempt c parid pr ~limit ~callback ~notification
776 777 778 779 780

type report =
  | Result of Call_provers.prover_result * Call_provers.prover_result
  (** Result(new_result,old_result) *)
  | CallFailed of exn
781
  | Replay_interrupted
782 783 784 785 786 787 788 789 790 791 792
  | Prover_not_installed
  | Edited_file_absent of string
  | No_former_result of Call_provers.prover_result

(* TODO find a better way to print it *)
let print_report fmt (r: report) =
  match r with
  | Result (new_r, old_r) ->
    Format.fprintf fmt "new_result = %a, old_result = %a@."
      Call_provers.print_prover_result new_r
      Call_provers.print_prover_result old_r
793 794 795 796
  | CallFailed e ->
    Format.fprintf fmt "Callfailed %a@." Exn_printer.exn_printer e
  | Replay_interrupted ->
    Format.fprintf fmt "Interrupted@."
797 798 799 800 801 802 803 804 805
  | Prover_not_installed ->
    Format.fprintf fmt "Prover not installed@."
  | Edited_file_absent _ ->
    Format.fprintf fmt "No edited file@."
  | No_former_result new_r ->
    Format.fprintf fmt "new_result = %a, no former result@."
      Call_provers.print_prover_result new_r

(* TODO to be removed when we have a better way to print *)
806
let replay_print fmt (lr: (proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list) =
807 808
  let pp_elem fmt (id, pr, rl, report) =
    fprintf fmt "ProofNodeID: %d, Prover: %a, Timelimit?: %d, Result: %a@."
Sylvain Dailler's avatar
Sylvain Dailler committed
809 810
      (Obj.magic id) Whyconf.print_prover pr
      rl.Call_provers.limit_time print_report report
811
  in
812
  Format.fprintf fmt "%a@." (Pp.print_list Pp.newline pp_elem) lr
813

814 815
let replay ?(obsolete_only=true) ?(use_steps=false)
           c ~callback ~notification ~final_callback =
816

817
  let craft_report count s r id pr limits pa =
818
    match s with
819 820 821
    | Scheduled | Running -> ()
    | Unedited | JustEdited -> assert false
    | Interrupted ->
822
       decr count;
823
       r := (id, pr, limits, Replay_interrupted ) :: !r
824
    | Done new_r ->
825
       decr count;
826 827 828 829
        (match pa.Session_itp.proof_state with
        | None -> (r := (id, pr, limits, No_former_result new_r) :: !r)
        | Some old_r -> r := (id, pr, limits, Result (new_r, old_r)) :: !r)
    | InternalFailure e ->
830
       decr count;
831
        r := (id, pr, limits, CallFailed (e)) :: !r
832 833 834
    | Uninstalled _ ->
       decr count;
       r := (id, pr, limits, Prover_not_installed) :: !r;
835
  in
836 837 838 839 840 841 842 843 844

  (* === replay === *)
  let session = c.controller_session in
  let count = ref 0 in
  let report = ref [] in

  (* TODO count the number of node in a more efficient way *)
  (* Counting the number of proof_attempt to print report only once *)
  Session_itp.session_iter_proof_attempt
845
    (fun _ pa -> if pa.proof_obsolete || not obsolete_only then incr count) session;
846 847

  (* Replaying function *)
848
  let replay_pa id pa =
849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866
    if pa.proof_obsolete || not obsolete_only then
      begin
        let parid = pa.parent in
        let pr = pa.prover in
        (* If use_steps, we give only steps as a limit *)
        let limit =
          if use_steps then
            Call_provers.{empty_limit with limit_steps = pa.limit.limit_steps}
          else
            Call_provers.{ pa.limit with limit_steps = empty_limit.limit_steps }
        in
        replay_proof_attempt c pr limit parid id
                             ~callback:(fun id s ->
                                        craft_report count s report parid pr limit pa;
                                        callback id s;
                                        if !count = 0 then final_callback !report)
                             ~notification
      end in
867 868

  (* Calling replay on all the proof_attempts of the session *)
869
  Session_itp.session_iter_proof_attempt replay_pa session
870

871
end