session.ml 40.7 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)


open Why
22 23
open Format

24 25 26 27
(***************************)
(*     provers             *)
(***************************)

MARCHE Claude's avatar
MARCHE Claude committed
28
type prover_data =
29 30 31 32 33 34 35 36
    { prover_id : string;
      prover_name : string;
      prover_version : string;
      command : string;
      driver_name : string;
      driver : Driver.driver;
      mutable editor : string;
    }
37

38 39 40 41 42 43 44 45 46 47 48 49 50
let get_prover_data env id pr acc =
  try
    let dr = Driver.load_driver env pr.Whyconf.driver in
    Util.Mstr.add id
      { prover_id = id ;
      prover_name = pr.Whyconf.name;
      prover_version = pr.Whyconf.version;
      command = pr.Whyconf.command;
      driver_name = pr.Whyconf.driver;
      driver = dr;
      editor = pr.Whyconf.editor;
    }
      acc
MARCHE Claude's avatar
MARCHE Claude committed
51 52
  with e ->
    eprintf "Failed to load driver %s for prover %s (%a). prover disabled@."
MARCHE Claude's avatar
MARCHE Claude committed
53
      pr.Whyconf.driver
MARCHE Claude's avatar
MARCHE Claude committed
54 55 56
      pr.Whyconf.name
      Exn_printer.exn_printer e
      ;
57 58
    acc

59 60 61
(***************************)
(*      transformations    *)
(***************************)
62

63 64 65 66
type trans =
  | Trans_one of Task.task Trans.trans
  | Trans_list of Task.task Trans.tlist

MARCHE Claude's avatar
MARCHE Claude committed
67
type transformation_data =
68 69 70 71 72 73
    { transformation_name : string;
      transformation : trans;
    }

let transformation_id t = t.transformation_name

74 75 76 77 78 79 80 81 82 83 84
let lookup_trans env name =
  try
    let t = Trans.lookup_transform name env in
    Trans_one t
  with Trans.UnknownTrans _ ->
    let t = Trans.lookup_transform_l name env in
    Trans_list t

let lookup_transformation env =
  let h = Hashtbl.create 13 in
  fun name ->
MARCHE Claude's avatar
MARCHE Claude committed
85
    try
86 87 88 89 90 91
      Hashtbl.find h name
    with Not_found ->
      let t = {transformation_name = name;
	       transformation = lookup_trans env name }
      in Hashtbl.add h name t; t

92 93 94 95
(***************************)
(*     proof status        *)
(***************************)

96 97 98 99 100 101
type proof_attempt_status =
  | Undone
  | 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 *)
102 103


104 105 106 107
(***************************)
(*     main functor        *)
(***************************)

108 109 110 111
module type OBSERVER = sig
  type key
  val create: ?parent:key -> unit -> key
  val remove: key -> unit
MARCHE Claude's avatar
MARCHE Claude committed
112
  val reset: unit -> unit
113 114 115

  val timeout: ms:int -> (unit -> bool) -> unit
  val idle: (unit -> bool) -> unit
116 117 118 119
end

module Make(O : OBSERVER) = struct

120 121 122 123
(***************************)
(*     session state       *)
(***************************)

124
type proof_attempt =
125
    { prover : prover_data;
126 127 128 129 130 131 132 133
      proof_goal : goal;
      proof_key : O.key;
      mutable proof_state : proof_attempt_status;
      mutable proof_obsolete : bool;
      mutable edited_as : string;
    }

and goal_parent =
134 135
  | Parent_theory of theory
  | Parent_transf of transf
136 137 138 139 140

and goal =
    { goal_name : string;
      goal_expl : string option;
      parent : goal_parent;
141
      mutable task: Task.task option;
MARCHE Claude's avatar
MARCHE Claude committed
142
      mutable checksum : string;
143 144
      goal_key : O.key;
      mutable proved : bool;
145
      mutable goal_expanded : bool;
146 147 148 149 150
      external_proofs: (string, proof_attempt) Hashtbl.t;
      transformations : (string, transf) Hashtbl.t;
    }

and transf =
151 152
    { transf : transformation_data;
      parent_goal : goal;
153 154 155
      mutable transf_proved : bool;
      transf_key : O.key;
      mutable subgoals : goal list;
156
      mutable transf_expanded : bool;
157 158 159
    }

and theory =
160
    { theory_name : string;
MARCHE Claude's avatar
MARCHE Claude committed
161
      mutable theory : Theory.theory option;
162 163 164 165
      theory_key : O.key;
      theory_parent : file;
      mutable goals : goal list;
      mutable verified : bool;
166
      mutable theory_expanded : bool;
167 168 169 170 171 172 173
    }

and file =
    { file_name : string;
      file_key : O.key;
      mutable theories: theory list;
      mutable file_verified : bool;
174
      mutable file_expanded : bool;
175 176
    }

177 178 179 180 181 182 183
type any =
  | File of file
  | Theory of theory
  | Goal of goal
  | Proof_attempt of proof_attempt
  | Transformation of transf

MARCHE Claude's avatar
MARCHE Claude committed
184 185 186 187
let theory_name t = t.theory_name
let theory_key t = t.theory_key
let verified t = t.verified
let goals t = t.goals
188 189
let theory_expanded t = t.theory_expanded

MARCHE Claude's avatar
MARCHE Claude committed
190

MARCHE Claude's avatar
MARCHE Claude committed
191 192 193
let get_theory t =
  match t.theory with
    | None ->
MARCHE Claude's avatar
MARCHE Claude committed
194 195
	eprintf "Session: theory not yet reimported, this should not happen@.";
	assert false
196 197
    | Some t -> t

MARCHE Claude's avatar
MARCHE Claude committed
198
let goal_name g = g.goal_name
MARCHE Claude's avatar
MARCHE Claude committed
199 200
let goal_expl g =
  match g.goal_expl with
MARCHE Claude's avatar
MARCHE Claude committed
201 202 203 204 205
    | None -> g.goal_name
    | Some s -> s
let goal_key g = g.goal_key
let goal_proved g = g.proved
let transformations g = g.transformations
206 207
let external_proofs g = g.external_proofs
let goal_expanded g = g.goal_expanded
MARCHE Claude's avatar
MARCHE Claude committed
208

MARCHE Claude's avatar
MARCHE Claude committed
209 210 211
let get_task g =
  match g.task with
    | None ->
212 213 214 215 216 217 218 219
	begin
	  match g.parent with
	    | Parent_theory _th ->
		assert false (* should not happen *)
	    | Parent_transf _tr ->
		(* TODO: recompute the task from the parent transformation *)
		assert false
	end
220 221
    | Some t -> t

222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241

let rec set_goal_expanded g b = 
  g.goal_expanded <- b;
  if not b then
    Hashtbl.iter (fun _ tr -> set_transf_expanded tr b) g.transformations

and set_transf_expanded tr b = 
  tr.transf_expanded <- b;
  if not b then
    List.iter (fun g -> set_goal_expanded g b) tr.subgoals

let set_theory_expanded t b = 
  t.theory_expanded <- b;
  if not b then
    List.iter (fun th -> set_goal_expanded th b) t.goals

let set_file_expanded f b =
  f.file_expanded <- b;
  if not b then
    List.iter (fun th -> set_theory_expanded th b) f.theories
242

243 244
let all_files : file list ref = ref []

245
let get_all_files () = !all_files
MARCHE Claude's avatar
MARCHE Claude committed
246

247 248 249 250
(************************)
(* saving state on disk *)
(************************)

MARCHE Claude's avatar
MARCHE Claude committed
251
let save_result fmt r =
MARCHE Claude's avatar
MARCHE Claude committed
252
  fprintf fmt "@\n<result status=\"%s\" time=\"%.2f\"/>"
MARCHE Claude's avatar
MARCHE Claude committed
253 254 255 256 257 258 259 260 261 262 263
    (match r.Call_provers.pr_answer with
       | Call_provers.Valid -> "valid"
       | Call_provers.Failure _ -> "failure"
       | Call_provers.Unknown _ -> "unknown"
       | Call_provers.HighFailure -> "highfailure"
       | Call_provers.Timeout -> "timeout"
       | Call_provers.Invalid -> "invalid")
    r.Call_provers.pr_time

let save_status fmt s =
  match s with
MARCHE Claude's avatar
MARCHE Claude committed
264
    | Undone | Scheduled | Running ->
MARCHE Claude's avatar
MARCHE Claude committed
265 266 267
        fprintf fmt "<undone/>@\n"
    | InternalFailure msg ->
        fprintf fmt "<internalfailure reason=\"%s\"/>@\n"
MARCHE Claude's avatar
MARCHE Claude committed
268
          (Printexc.to_string msg)
MARCHE Claude's avatar
MARCHE Claude committed
269 270 271
    | Done r -> save_result fmt r

let save_proof_attempt fmt _key a =
272 273
  fprintf fmt "@\n@[<v 1><proof prover=\"%s\" edited=\"%s\" obsolete=\"%b\">"
    a.prover.prover_id a.edited_as a.proof_obsolete;
MARCHE Claude's avatar
MARCHE Claude committed
274
  save_status fmt a.proof_state;
MARCHE Claude's avatar
MARCHE Claude committed
275
  fprintf fmt "@]@\n</proof>"
276 277 278 279 280 281

let opt lab fmt = function
  | None -> ()
  | Some s -> fprintf fmt "%s=\"%s\" " lab s

let rec save_goal fmt g =
282 283
  fprintf fmt "@\n@[<v 1><goal name=\"%s\" %asum=\"%s\" proved=\"%b\" expanded=\"%b\">"
    g.goal_name (opt "expl") g.goal_expl g.checksum g.proved  g.goal_expanded;
284
  Hashtbl.iter (save_proof_attempt fmt) g.external_proofs;
MARCHE Claude's avatar
MARCHE Claude committed
285
  Hashtbl.iter (save_trans fmt) g.transformations;
MARCHE Claude's avatar
MARCHE Claude committed
286
  fprintf fmt "@]@\n</goal>"
287

MARCHE Claude's avatar
MARCHE Claude committed
288
and save_trans fmt _ t =
289 290
  fprintf fmt "@\n@[<v 1><transf name=\"%s\" proved=\"%b\" expanded=\"%b\">"
    t.transf.transformation_name t.transf_proved t.transf_expanded;
MARCHE Claude's avatar
MARCHE Claude committed
291
  List.iter (save_goal fmt) t.subgoals;
MARCHE Claude's avatar
MARCHE Claude committed
292
  fprintf fmt "@]@\n</transf>"
293 294

let save_theory fmt t =
295 296
  fprintf fmt "@\n@[<v 1><theory name=\"%s\" verified=\"%b\" expanded=\"%b\">"
    t.theory_name t.verified t.theory_expanded;
297
  List.iter (save_goal fmt) t.goals;
MARCHE Claude's avatar
MARCHE Claude committed
298
  fprintf fmt "@]@\n</theory>"
299 300

let save_file fmt f =
301
  fprintf fmt "@\n@[<v 1><file name=\"%s\" verified=\"%b\" expanded=\"%b\">" f.file_name f.file_verified f.file_expanded;
302
  List.iter (save_theory fmt) f.theories;
MARCHE Claude's avatar
MARCHE Claude committed
303
  fprintf fmt "@]@\n</file>"
MARCHE Claude's avatar
MARCHE Claude committed
304

305 306 307 308
let save fname =
  let ch = open_out fname in
  let fmt = formatter_of_out_channel ch in
  fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
MARCHE Claude's avatar
MARCHE Claude committed
309 310
  fprintf fmt "<!DOCTYPE why3session SYSTEM \"why3session.dtd\">@\n";
  fprintf fmt "@[<v 1><why3session name=\"%s\">" fname;
311
  List.iter (save_file fmt) (get_all_files());
MARCHE Claude's avatar
MARCHE Claude committed
312 313
  fprintf fmt "@]@\n</why3session>";
  fprintf fmt "@.";
314 315 316 317 318 319
  close_out ch

(************************)
(*     actions          *)
(************************)

320 321 322 323
let init_fun = ref (fun (_:O.key) (_:any) -> ())

let notify_fun = ref (fun (_:any) -> ())

324 325
let check_file_verified f =
  let b = List.for_all (fun t -> t.verified) f.theories in
326 327
  f.file_verified <- b;
  !notify_fun (File f)
328 329 330

let check_theory_proved t =
  let b = List.for_all (fun g -> g.proved) t.goals in
331 332 333
  t.verified <- b;
  !notify_fun (Theory t);
  check_file_verified t.theory_parent
334 335 336 337 338 339 340 341 342 343 344

let rec check_goal_proved g =
  let b1 = Hashtbl.fold
    (fun _ a acc -> acc ||
       match a.proof_state with
	 | Done { Call_provers.pr_answer = Call_provers.Valid} -> true
	 | _ -> false) g.external_proofs false
  in
  let b = Hashtbl.fold
    (fun _ t acc -> acc || t.transf_proved) g.transformations b1
  in
345 346 347 348 349
  g.proved <- b;
  !notify_fun (Goal g);
  match g.parent with
    | Parent_theory t -> check_theory_proved t
    | Parent_transf t -> check_transf_proved t
350 351 352

and check_transf_proved t =
  let b = List.for_all (fun g -> g.proved) t.subgoals in
353 354 355
  t.transf_proved <- b;
  !notify_fun (Transformation t);
  check_goal_proved t.parent_goal
356 357 358 359

let set_proof_state ~obsolete a res =
  a.proof_state <- res;
  a.proof_obsolete <- obsolete;
MARCHE Claude's avatar
MARCHE Claude committed
360
  !notify_fun (Proof_attempt a);
361
  check_goal_proved a.proof_goal
362

363 364
(*************************)
(*         Scheduler     *)
MARCHE Claude's avatar
MARCHE Claude committed
365
(*************************)
366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495


(* timeout handler *)

let maximum_running_proofs = ref 2
let running_proofs = ref []

let proof_attempts_queue = Queue.create ()

let timeout_handler_activated = ref false
let timeout_handler_running = ref false

let timeout_handler () =
  assert (not !timeout_handler_running);
  timeout_handler_running := true;
  let l = List.fold_left
    (fun acc ((callback,call) as c) ->
       match Call_provers.query_call call with
	 | None -> c::acc
	 | Some post ->
	     let res = post () in callback (Done res);
	     acc)
    [] !running_proofs
  in
  let l =
    if List.length l < !maximum_running_proofs then
      begin try
	let (callback,pre_call) = Queue.pop proof_attempts_queue in
	callback Running;
	let call = pre_call () in
	(callback,call)::l
      with Queue.Empty -> l
      end
    else l
  in
  running_proofs := l;
  let continue =
    match l with
      | [] ->
(*
          eprintf "Info: timeout_handler stopped@.";
*)
          false
      | _ -> true
  in
  timeout_handler_activated := continue;
  timeout_handler_running := false;
  continue


let run_timeout_handler () =
  if !timeout_handler_activated then () else
    begin
      timeout_handler_activated := true;
(*
      eprintf "Info: timeout_handler started@.";
*)
      O.timeout ~ms:100 timeout_handler
    end

(* idle handler *)


type action =
  | Action_proof_attempt of bool * int * int * in_channel option * string * Driver.driver *
    (proof_attempt_status -> unit) * Task.task
  | Action_delayed of (unit -> unit)

let actions_queue = Queue.create ()

let idle_handler_activated = ref false

let idle_handler () =
  try
    begin
      match Queue.pop actions_queue with
	| Action_proof_attempt(debug,timelimit,memlimit,old,command,driver,
			       callback,goal) ->
	    callback Scheduled;
	    if debug then
	      Format.eprintf "Task for prover: %a@."
		(Driver.print_task driver) goal;
	    let pre_call =
	      Driver.prove_task ?old ~command ~timelimit ~memlimit driver goal
	    in
	    Queue.push (callback,pre_call) proof_attempts_queue;
	    run_timeout_handler ()
        | Action_delayed callback -> callback ()
    end;
    true
  with Queue.Empty ->
    idle_handler_activated := false;
(*
    eprintf "Info: idle_handler stopped@.";
*)
    false

let run_idle_handler () =
  if !idle_handler_activated then () else
    begin
      idle_handler_activated := true;
(*
      eprintf "Info: idle_handler started@.";
*)
      O.idle idle_handler
    end

(* main scheduling functions *)

let schedule_proof_attempt ~debug ~timelimit ~memlimit ?old
    ~command ~driver ~callback goal =
  Queue.push
    (Action_proof_attempt(debug,timelimit,memlimit,old,command,driver,
			callback,goal))
    actions_queue;
  run_idle_handler ()

let schedule_edition command callback =
  let precall =
    Call_provers.call_on_buffer ~command ~regexps:[] ~timeregexps:[]
      ~exitcodes:[(0,Call_provers.Unknown "")] ~filename:"" (Buffer.create 1)
  in
  callback Running;
  running_proofs := (callback, precall ()) :: !running_proofs;
  run_timeout_handler ()

let schedule_delayed_action callback =
  Queue.push (Action_delayed callback) actions_queue;
  run_idle_handler ()

496 497 498 499 500 501
let apply_transformation ~callback t task =
   match t.transformation with
    | Trans_one t ->
	callback [Trans.apply t task]
    | Trans_list t ->
	callback (Trans.apply t task)
502

503
let schedule_edit_proof ~debug:_ ~editor ~file ~driver ~callback goal =
504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521
  let old =
    if Sys.file_exists file
    then
      begin
	let backup = file ^ ".bak" in
        Sys.rename file backup;
        Some(open_in backup)
      end
    else None
  in
  let ch = open_out file in
  let fmt = formatter_of_out_channel ch in
  Driver.print_task ?old driver fmt goal;
  Util.option_iter close_in old;
  close_out ch;
  let command = editor ^ " " ^ file in
  schedule_edition command callback

522 523 524 525 526 527 528 529 530

(*******************************)
(* explanations *)
(****************)


  let expl_regexp = Str.regexp "expl:\\(.*\\)"

  let rec get_labels f =
531
    (match f.Term.t_node with
532 533 534
      | Term.Fbinop(Term.Fimplies,_,f) -> get_labels f
      | Term.Fquant(Term.Fforall,fq) ->
	  let (_,_,f) = Term.f_open_quant fq in get_labels f
535 536 537 538
      | Term.Tlet(_,fb) ->
	  let (_,f) = Term.t_open_bound fb in get_labels f
      | Term.Tcase(_,[fb]) ->
	  let (_,f) = Term.t_open_branch fb in get_labels f
539
      | _ -> [])
540
    @ f.Term.t_label
541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562

  let get_explanation id fmla =
    let r = ref None in
(*
    let fl = Debug.lookup_flag "print_labels" in
    Debug.set_flag fl;
    Format.eprintf "searching expl in formula '%a'@." Pretty.print_fmla fmla;
*)
    List.iter
      (fun s ->
         if Str.string_match expl_regexp s 0 then
           begin
	     let e = Str.matched_group 1 s in
(*
	     Format.eprintf "found explanation: '%s'" e;
*)
	     r := Some e
	   end)
      (id.Ident.id_label @ get_labels fmla);
    !r


563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582
(**********************)
(*     check sum      *)
(**********************)

let task_checksum t =
  fprintf str_formatter "%a@." Pretty.print_task t;
  let s = flush_str_formatter () in
(*
  let tmp = Filename.temp_file "task" "out" in
  let c = open_out tmp in
  output_string c s;
  close_out c;
*)
  let sum = Digest.to_hex (Digest.string s) in
(*
  eprintf "task %s, sum = %s@." tmp sum;
*)
  sum


583 584 585 586 587

(******************************)
(* raw additions to the model *)
(******************************)

588
let raw_add_external_proof ~obsolete ~edit (g:goal) p result =
589
  let key = O.create ~parent:g.goal_key () in
590
  let a = { prover = p;
591 592 593 594 595 596 597
            proof_goal = g;
            proof_key = key;
            proof_obsolete = obsolete;
	    proof_state = result;
            edited_as = edit;
          }
  in
MARCHE Claude's avatar
MARCHE Claude committed
598
  Hashtbl.add g.external_proofs p.prover_id a;
599 600 601
  let any = Proof_attempt a in
  !init_fun key any;
  !notify_fun any;
602 603
  a

604

MARCHE Claude's avatar
MARCHE Claude committed
605
(* [raw_add_goal parent name expl sum t] adds a goal to the given parent
606 607
   DOES NOT record the new goal in its parent, thus this should not be exported
*)
608
let raw_add_goal parent name expl sum topt exp =
609
  let parent_key = match parent with
610 611
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
612 613
  in
  let key = O.create ~parent:parent_key () in
614
  let sum = match topt with
MARCHE Claude's avatar
MARCHE Claude committed
615
    | None -> sum
616 617
    | Some t -> task_checksum t
  in
618 619 620
  let goal = { goal_name = name;
               goal_expl = expl;
	       parent = parent;
621
               task = topt ;
622
	       checksum = sum;
623 624 625 626
               goal_key = key;
               external_proofs = Hashtbl.create 7;
               transformations = Hashtbl.create 3;
               proved = false;
627
	       goal_expanded = exp;
628 629
             }
  in
630 631
  let any = Goal goal in
  !init_fun key any;
632
  !notify_fun any; (*useless ? *)
633 634 635 636 637 638
  goal


(* [raw_add_transformation g name adds a transformation to the given goal g
   Adds no subgoals, thus this should not be exported
*)
639
let raw_add_transformation g trans exp =
640 641
  let parent = g.goal_key in
  let key = O.create ~parent () in
642 643
  let tr = { transf = trans;
	     parent_goal = g;
644 645 646
             transf_proved = false;
             transf_key = key;
             subgoals = [];
647
             transf_expanded = exp;
648 649
           }
  in
650 651 652 653
  Hashtbl.add g.transformations trans.transformation_name tr;
  let any = Transformation tr in
  !init_fun key any;
  !notify_fun any;
654 655
  tr

656
let raw_add_theory mfile thopt thname exp =
657 658
  let parent = mfile.file_key in
  let key = O.create ~parent () in
659 660
  let mth = { theory_name = thname;
	      theory = thopt;
661 662 663
              theory_key = key;
              theory_parent = mfile;
              goals = [] ;
664 665 666
              verified = false;
	      theory_expanded = exp;
	    }
667
  in
668 669 670
  let any = Theory mth in
  !init_fun key any;
  !notify_fun any;
671 672 673 674
  mth



675
let add_theory mfile name th =
676
  let tasks = List.rev (Task.split_theory th None None) in
677
  let mth = raw_add_theory mfile (Some th) name true in
678 679 680 681 682 683
  let goals =
    List.fold_left
      (fun acc t ->
         let id = (Task.task_goal t).Decl.pr_name in
         let name = id.Ident.id_string in
         let expl = get_explanation id (Task.task_goal_fmla t) in
684
         let goal = raw_add_goal (Parent_theory mth) name expl "" (Some t) true in
685 686 687 688 689
         goal :: acc)
      []
      tasks
  in
  mth.goals <- List.rev goals;
MARCHE Claude's avatar
MARCHE Claude committed
690
  check_theory_proved mth;
691 692
  mth

693
let raw_add_file f exp =
694
  let key = O.create () in
695
  let mfile = { file_name = f;
696
                file_key = key;
697
                theories = [] ;
698 699 700
                file_verified = false;
		file_expanded = exp;
	      }
701 702
  in
  all_files := !all_files @ [mfile];
703 704 705
  let any = File mfile in
  !init_fun key any;
  !notify_fun any;
706 707
  mfile

MARCHE Claude's avatar
MARCHE Claude committed
708 709 710 711 712
let current_env = ref None
let project_dir = ref ""

let read_file fn =
  let fn = Filename.concat !project_dir fn in
MARCHE Claude's avatar
MARCHE Claude committed
713 714
  let env = match !current_env with
    | None -> assert false | Some e -> e
MARCHE Claude's avatar
MARCHE Claude committed
715 716
  in
  let theories = Env.read_file env fn in
717 718 719
  let theories =
    Theory.Mnm.fold
      (fun name th acc ->
720 721 722
         match th.Theory.th_name.Ident.id_loc with
           | Some l -> (l,name,th)::acc
           | None   -> (Loc.dummy_position,name,th)::acc)
723 724
      theories []
  in
MARCHE Claude's avatar
MARCHE Claude committed
725
  List.sort
726 727
    (fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
    theories
MARCHE Claude's avatar
MARCHE Claude committed
728 729 730

let add_file f =
  let theories = read_file f in
731
  let mfile = raw_add_file f true in
732 733
  let mths =
    List.fold_left
734 735
      (fun acc (_,name,t) ->
         let mth = add_theory mfile name t in
736 737 738 739
         mth :: acc)
      [] theories
  in
  mfile.theories <- List.rev mths;
740 741 742
  check_file_verified mfile;
  !notify_fun (File mfile)

743 744


745 746 747
let file_exists fn =
  List.exists (fun f -> f.file_name = fn) !all_files

748 749


750 751


752 753 754 755
(**********************************)
(* reload a file                  *)
(**********************************)

MARCHE Claude's avatar
MARCHE Claude committed
756 757 758 759 760
let reload_proof ~provers obsolete goal pid old_a =
  try
    let p = Util.Mstr.find pid provers in
    let old_res = old_a.proof_state in
    let obsolete = obsolete or old_a.proof_obsolete in
761
    (* eprintf "proof_obsolete : %b@." obsolete; *)
762 763
    let a =
      raw_add_external_proof ~obsolete ~edit:old_a.edited_as goal p old_res
MARCHE Claude's avatar
MARCHE Claude committed
764
    in
765
    !notify_fun (Goal a.proof_goal)
MARCHE Claude's avatar
MARCHE Claude committed
766 767 768 769 770 771 772
  with Not_found ->
    eprintf
      "Warning: prover %s appears in database but is not installed.@."
      pid

let rec reload_any_goal ~provers parent gid gname sum t old_goal goal_obsolete =
  let info = get_explanation gid (Task.task_goal_fmla t) in
773 774
  let exp = match old_goal with None -> true | Some g -> g.goal_expanded in
  let goal = raw_add_goal parent gname info sum (Some t) exp in
775
  goal.task <- Some t;
MARCHE Claude's avatar
MARCHE Claude committed
776 777 778 779 780 781 782
  begin
    match old_goal with
      | None -> ()
      | Some g ->
          Hashtbl.iter (reload_proof ~provers goal_obsolete goal) g.external_proofs;
          Hashtbl.iter (reload_trans ~provers goal_obsolete goal) g.transformations
  end;
783
  check_goal_proved goal;
784
  goal
MARCHE Claude's avatar
MARCHE Claude committed
785 786


787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875
and reload_trans ~provers _goal_obsolete goal _ tr =
  let trname = tr.transf.transformation_name in
  let gname = goal.goal_name in
  eprintf "[Reload] transformation %s for goal %s @." trname gname;
  let mtr = raw_add_transformation goal tr.transf tr.transf_expanded in
  let old_subgoals =
    List.fold_left
      (fun acc g -> Util.Mstr.add g.checksum g acc)
      Util.Mstr.empty tr.subgoals
  in
  let callback subgoals =
    (* we have an ordered list of new subgoals

           subgoals = [g1; g2; g3; ...]

       and a map of old subgoals indexed by their checksum

           old_subgoals = [s1,h1 ; s2, h2 ; ... ]

       we first associate each new goals for which there is an old goal 
       with the same checksum. E.g, imagine checksum of g2 is s1 :

       new_goals_map = [ (g1, None) ; (g2, Some h1) ; (g3, None) ; ]
       remaining = [ s2, h2 ; ... ]

    *)
    let new_goals_map,_remaining,_ =
      List.fold_left
        (fun (new_goals_map,old_subgoals,count) subtask ->
           let id = (Task.task_goal subtask).Decl.pr_name in
           let subgoal_name = gname ^ "." ^ (string_of_int count) in
           let sum = task_checksum subtask in
           let old_subgoal,old_subgoals =
             try
	       let g = Util.Mstr.find sum old_subgoals in
	       (* an old subgoal has the same checksum *)
	       (Some g, Util.Mstr.remove sum old_subgoals)
             with Not_found -> None,old_subgoals
           in
           ((count,id,subgoal_name,subtask,sum,old_subgoal) :: new_goals_map,
	    old_subgoals, count+1))
        ([],old_subgoals,1) subgoals
    in
    (* careful : new_goals is now in reverse order *)
    (* we now turn remaining back into a list in the same order as original *)
    let remaining =
      Util.Mstr.fold
        (fun _ g acc -> (g.goal_name,g)::acc)
        old_subgoals
        []
    in
    let remaining =
      List.sort (fun (s1,_) (s2,_) -> String.compare s1 s2) remaining
    in
    (* we now associate to each new goal which does not have an 
       associated old goal yet to an old goal in the same order 
       (arbitrary choice) 

       new_new_goals_map = [ [ (g1, h2) ; (g2, h1) ; (g3, fresh) ; ]

    *)
    let rec associate_remaining_goals new_goals_map remaining acc =
      match new_goals_map with
        | [] -> acc
        | (_,id,subgoal_name,subtask,sum,old_subgoal)::new_rem ->
            let ((obsolete,old_goal,rem) : bool * goal option * (string * goal) list) =
              match old_subgoal with
                | Some _ -> false,old_subgoal,remaining
                | None ->
                    match remaining with
                      | [] -> false,None,[]
                      | (_goal_name,g) :: rem -> true,Some g,rem
            in
            associate_remaining_goals new_rem rem 
              ((id,subgoal_name,sum,subtask,old_goal,obsolete)::acc)
    in
    let goals =
      associate_remaining_goals (List.rev new_goals_map) remaining []
    in
    let goals = List.fold_left
      (fun acc (id,subgoal_name,sum,subtask,old_g, subgoal_obsolete) ->
         let mg = 
           reload_any_goal ~provers
             (Parent_transf mtr) id
             subgoal_name sum subtask old_g subgoal_obsolete 
         in mg::acc)
      [] goals
    in
    mtr.subgoals <- goals;
876
    check_transf_proved mtr
877 878
  in
  apply_transformation ~callback tr.transf (get_task goal)
879 880


MARCHE Claude's avatar
MARCHE Claude committed
881 882
(* reloads the task [t] in theory mth (named tname) *)
let reload_root_goal ~provers mth tname old_goals t : goal =
883
  let id = (Task.task_goal t).Decl.pr_name in
MARCHE Claude's avatar
MARCHE Claude committed
884
  let gname = id.Ident.id_string in
885
  let sum = task_checksum t in
MARCHE Claude's avatar
MARCHE Claude committed
886 887 888 889 890 891
  let old_goal, goal_obsolete =
    try
      let old_goal = Util.Mstr.find gname old_goals in
      let old_sum = old_goal.checksum in
      (Some old_goal,sum <> old_sum)
    with Not_found -> (None,false)
892
  in
MARCHE Claude's avatar
MARCHE Claude committed
893 894 895 896 897 898 899 900
  if goal_obsolete then
    eprintf "Goal %s.%s has changed@." tname gname;
  reload_any_goal ~provers (Parent_theory mth) id gname sum t old_goal goal_obsolete

(* reloads a theory *)
let reload_theory ~provers mfile old_theories (_,tname,th) =
  eprintf "[Reload] theory '%s'@."tname;
  let tasks = List.rev (Task.split_theory th None None) in
901
  let old_goals, old_exp =
MARCHE Claude's avatar
MARCHE Claude committed
902 903
    try
      let old_mth = Util.Mstr.find tname old_theories in
904 905
      old_mth.goals, old_mth.theory_expanded
    with Not_found -> [], true
MARCHE Claude's avatar
MARCHE Claude committed
906
  in
907
  let mth = raw_add_theory mfile (Some th) tname old_exp in
MARCHE Claude's avatar
MARCHE Claude committed
908 909 910 911
  let goalsmap = List.fold_left
    (fun goalsmap g -> Util.Mstr.add g.goal_name g goalsmap)
    Util.Mstr.empty old_goals
  in
912
  !notify_fun (Theory mth);
MARCHE Claude's avatar
MARCHE Claude committed
913 914 915 916 917 918 919 920 921
  let new_goals = List.fold_left
    (fun acc t ->
       let g = reload_root_goal ~provers mth tname goalsmap t in
       g::acc)
    [] tasks
  in
  mth.goals <- List.rev new_goals;
  check_theory_proved mth;
  mth
922 923


MARCHE Claude's avatar
MARCHE Claude committed
924
(* reloads a file *)
925
let reload_file ~provers mf theories =
926
  let new_mf = raw_add_file mf.file_name mf.file_expanded in
MARCHE Claude's avatar
MARCHE Claude committed
927 928 929 930 931
  let old_theories = List.fold_left
    (fun acc t -> Util.Mstr.add t.theory_name t acc)
    Util.Mstr.empty
    mf.theories
  in
932
  !notify_fun (File new_mf);
MARCHE Claude's avatar
MARCHE Claude committed
933 934 935 936 937 938 939
  let mths = List.fold_left
    (fun acc th -> reload_theory ~provers new_mf old_theories th :: acc)
    [] theories
  in
  new_mf.theories <- List.rev mths;
  check_file_verified new_mf

MARCHE Claude's avatar
MARCHE Claude committed
940 941

(* reloads all files *)
MARCHE Claude's avatar
MARCHE Claude committed
942 943
let reload_all provers =
  let files = !all_files in
944
  let all_theories =
945
    List.map (fun mf ->
946
		eprintf "[Reload] file '%s'@." mf.file_name;
947
		(mf,read_file mf.file_name))
948 949
      files
  in
MARCHE Claude's avatar
MARCHE Claude committed
950 951
  all_files := [];
  O.reset ();
952
  List.iter (fun (mf,ths) -> reload_file ~provers mf ths) all_theories
953

954 955 956 957
(****************************)
(*     session opening      *)
(****************************)

958 959 960 961 962 963 964 965
let bool_attribute field r def =
  try
    match List.assoc field r.Xml.attributes with
      | "true" -> true
      | "false" -> false
      | _ -> assert false
  with Not_found -> def

MARCHE Claude's avatar
MARCHE Claude committed
966 967 968
let load_result r =
  match r.Xml.name with
    | "result" ->
MARCHE Claude's avatar
MARCHE Claude committed
969
	let status =
MARCHE Claude's avatar
MARCHE Claude committed
970 971 972
	  try List.assoc "status" r.Xml.attributes
	  with Not_found -> assert false
	in
MARCHE Claude's avatar
MARCHE Claude committed
973
	let answer =
MARCHE Claude's avatar
MARCHE Claude committed
974 975 976 977 978 979 980
	  match status with
	    | "valid" -> Call_provers.Valid
	    | "invalid" -> Call_provers.Invalid
	    | "unknown" -> Call_provers.Unknown ""
	    | "timeout" -> Call_provers.Timeout
	    | "failure" -> Call_provers.Failure ""
	    | "highfailure" -> Call_provers.Failure ""
MARCHE Claude's avatar
MARCHE Claude committed
981
	    | s ->
MARCHE Claude's avatar
MARCHE Claude committed
982 983
		eprintf "Session.load_result: unexpected status '%s'@."  s;
		assert false
MARCHE Claude's avatar
MARCHE Claude committed
984 985 986 987 988
	in
	let time =
	  try float_of_string (List.assoc "time" r.Xml.attributes)
	  with Not_found -> 0.0
	in
989 990
	Done { 
	  Call_provers.pr_answer = answer;
MARCHE Claude's avatar
MARCHE Claude committed
991 992 993
	  Call_provers.pr_time = time;
	  Call_provers.pr_output = "";
	}
994
    | "undone" -> Undone
MARCHE Claude's avatar
MARCHE Claude committed
995
    | s ->
MARCHE Claude's avatar
MARCHE Claude committed
996 997
	eprintf "Session.load_result: unexpected element '%s'@."  s;
	assert false
MARCHE Claude's avatar
MARCHE Claude committed
998 999 1000


let rec load_goal ~env ~provers parent acc g =
MARCHE Claude's avatar
MARCHE Claude committed
1001 1002
  match g.Xml.name with
    | "goal" ->
MARCHE Claude's avatar
MARCHE Claude committed
1003
	let gname =
MARCHE Claude's avatar
MARCHE Claude committed
1004 1005 1006
	  try List.assoc "name" g.Xml.attributes
	  with Not_found -> assert false
	in
MARCHE Claude's avatar
MARCHE Claude committed
1007
	let expl =
MARCHE Claude's avatar
MARCHE Claude committed
1008 1009 1010
	  try Some (List.assoc "expl" g.Xml.attributes)
	  with Not_found -> None
	in
MARCHE Claude's avatar
MARCHE Claude committed
1011 1012 1013 1014
	let sum =
	  try List.assoc "sum" g.Xml.attributes
	  with Not_found -> ""
	in
1015 1016
	let exp = bool_attribute "expanded" g true in
	let mg = raw_add_goal parent gname expl sum None exp in
MARCHE Claude's avatar
MARCHE Claude committed
1017 1018
	List.iter (load_proof_or_transf ~env ~provers mg) g.Xml.elements;
	mg::acc
MARCHE Claude's avatar
MARCHE Claude committed
1019
    | s ->
MARCHE Claude's avatar
MARCHE Claude committed
1020 1021
	eprintf "Session.load_goal: unexpected element '%s'@."  s;
	assert false
MARCHE Claude's avatar
MARCHE Claude committed
1022

1023

MARCHE Claude's avatar
MARCHE Claude committed
1024
and load_proof_or_transf ~env ~provers mg a =
MARCHE Claude's avatar
MARCHE Claude committed
1025
  match a.Xml.name with
MARCHE Claude's avatar
MARCHE Claude committed
1026 1027
    | "proof" ->
	let prover =
MARCHE Claude's avatar
MARCHE Claude committed
1028 1029 1030
	  try List.assoc "prover" a.Xml.attributes
	  with Not_found -> assert false
	in
MARCHE Claude's avatar
MARCHE Claude committed
1031
        let p =
MARCHE Claude's avatar
MARCHE Claude committed
1032
	  try
MARCHE Claude's avatar
MARCHE Claude committed
1033
	    Util.Mstr.find prover provers
MARCHE Claude's avatar
MARCHE Claude committed
1034 1035 1036
	  with Not_found -> assert false (* TODO *)
	in
	let res = match a.Xml.elements with
1037
	  | [r] -> load_result r
MARCHE Claude's avatar
MARCHE Claude committed
1038 1039 1040
	  | [] -> Undone
	  | _ -> assert false
	in
MARCHE Claude's avatar
MARCHE Claude committed
1041
	let edit =
MARCHE Claude's avatar
MARCHE Claude committed
1042 1043 1044
	  try List.assoc "edited" a.Xml.attributes
	  with Not_found -> assert false
	in
1045 1046
        let obsolete = bool_attribute "obsolete" a true in
	let _pa = raw_add_external_proof ~obsolete ~edit mg p res in
MARCHE Claude's avatar
MARCHE Claude committed
1047 1048 1049
	(* already done by raw_add_external_proof
	   Hashtbl.add mg.external_proofs prover pa *)
	()
MARCHE Claude's avatar
MARCHE Claude committed
1050 1051
    | "transf" ->
	let trname =
MARCHE Claude's avatar
MARCHE Claude committed
1052 1053 1054
	  try List.assoc "name" a.Xml.attributes
	  with Not_found -> assert false
	in
MARCHE Claude's avatar
MARCHE Claude committed
1055 1056 1057
        let tr =
	  try
	    lookup_transformation env trname
MARCHE Claude's avatar
MARCHE Claude committed
1058 1059
	  with Not_found -> assert false (* TODO *)
	in
MARCHE Claude's avatar
MARCHE Claude committed
1060
	let _proved =
MARCHE Claude's avatar
MARCHE Claude committed
1061 1062 1063
	  try List.assoc "proved" a.Xml.attributes
	  with Not_found -> assert false
	in
1064 1065
	let exp = bool_attribute "expanded" a true in
	let mtr = raw_add_transformation mg tr exp in
MARCHE Claude's avatar
MARCHE Claude committed
1066
	mtr.subgoals <-
MARCHE Claude's avatar
MARCHE Claude committed
1067 1068 1069
	  List.rev
	  (List.fold_left
	     (load_goal ~env ~provers (Parent_transf mtr))
MARCHE Claude's avatar
MARCHE Claude committed
1070 1071 1072
	     [] a.Xml.elements);
	(* already done by raw_add_transformation
	   Hashtbl.add mg.transformations trname mtr *)
MARCHE Claude's avatar
MARCHE Claude committed
1073
	()
MARCHE Claude's avatar
MARCHE Claude committed
1074
    | s ->
MARCHE Claude's avatar
MARCHE Claude committed
1075 1076 1077 1078 1079 1080
	eprintf "Session.load_proof_or_transf: unexpected element '%s'@."  s;
	assert false

let load_theory ~env ~provers mf acc th =
  match th.Xml.name with
    | "theory" ->
MARCHE Claude's avatar
MARCHE Claude committed
1081
	let thname =
MARCHE Claude's avatar
MARCHE Claude committed
1082 1083 1084
	  try List.assoc "name" th.Xml.attributes
	  with Not_found -> assert false
	in
1085 1086
	let exp = bool_attribute "expanded" th true in
	let mth = raw_add_theory mf None thname exp in
MARCHE Claude's avatar
MARCHE Claude committed
1087 1088 1089 1090
	mth.goals <-
	  List.rev
	  (List.fold_left
	     (load_goal ~env ~provers (Parent_theory mth))
MARCHE Claude's avatar
MARCHE Claude committed
1091 1092
	     [] th.Xml.elements);
	mth::acc
MARCHE Claude's avatar
MARCHE Claude committed
1093
    | s ->
MARCHE Claude's avatar
MARCHE Claude committed
1094 1095 1096 1097 1098 1099
	eprintf "Session.load_theory: unexpected element '%s'@."  s;
	assert false

let load_file ~env ~provers f =
  match f.Xml.name with
    | "file" ->
MARCHE Claude's avatar
MARCHE Claude committed
1100
	let fn =
MARCHE Claude's avatar
MARCHE Claude committed
1101 1102 1103
	  try List.assoc "name" f.Xml.attributes
	  with Not_found -> assert false
	in
1104 1105
	let exp = bool_attribute "expanded" f true in
	let mf = raw_add_file fn exp in
MARCHE Claude's avatar