Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

session.ml 46.8 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
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 ;
43 44 45 46 47 48 49
        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;
      }
50
      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 125 126 127 128 129 130 131
type prover_option =
  | Detected_prover of prover_data
  | Undetected_prover of string

let prover_id p = match p with
  | Detected_prover p -> p.prover_id
  | Undetected_prover s -> s

132
type proof_attempt =
133
    { prover : prover_option;
134 135 136
      proof_goal : goal;
      proof_key : O.key;
      mutable proof_state : proof_attempt_status;
137
      mutable timelimit : int;
138 139 140 141 142
      mutable proof_obsolete : bool;
      mutable edited_as : string;
    }

and goal_parent =
143 144
  | Parent_theory of theory
  | Parent_transf of transf
145 146 147 148 149

and goal =
    { goal_name : string;
      goal_expl : string option;
      parent : goal_parent;
150
      mutable task: Task.task option;
MARCHE Claude's avatar
MARCHE Claude committed
151
      mutable checksum : string;
152 153
      goal_key : O.key;
      mutable proved : bool;
154
      mutable goal_expanded : bool;
155 156 157 158 159
      external_proofs: (string, proof_attempt) Hashtbl.t;
      transformations : (string, transf) Hashtbl.t;
    }

and transf =
160 161
    { transf : transformation_data;
      parent_goal : goal;
162 163 164
      mutable transf_proved : bool;
      transf_key : O.key;
      mutable subgoals : goal list;
165
      mutable transf_expanded : bool;
166 167 168
    }

and theory =
169
    { theory_name : string;
MARCHE Claude's avatar
MARCHE Claude committed
170
      mutable theory : Theory.theory option;
171 172 173 174
      theory_key : O.key;
      theory_parent : file;
      mutable goals : goal list;
      mutable verified : bool;
175
      mutable theory_expanded : bool;
176 177 178 179 180 181 182
    }

and file =
    { file_name : string;
      file_key : O.key;
      mutable theories: theory list;
      mutable file_verified : bool;
183
      mutable file_expanded : bool;
184 185
    }

186 187 188 189 190 191 192
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
193 194 195 196
let theory_name t = t.theory_name
let theory_key t = t.theory_key
let verified t = t.verified
let goals t = t.goals
197 198
let theory_expanded t = t.theory_expanded

MARCHE Claude's avatar
MARCHE Claude committed
199

MARCHE Claude's avatar
MARCHE Claude committed
200 201 202
let get_theory t =
  match t.theory with
    | None ->
MARCHE Claude's avatar
MARCHE Claude committed
203 204
	eprintf "Session: theory not yet reimported, this should not happen@.";
	assert false
205 206
    | Some t -> t

MARCHE Claude's avatar
MARCHE Claude committed
207
let goal_name g = g.goal_name
MARCHE Claude's avatar
MARCHE Claude committed
208 209
let goal_expl g =
  match g.goal_expl with
MARCHE Claude's avatar
MARCHE Claude committed
210 211 212 213 214
    | 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
215 216
let external_proofs g = g.external_proofs
let goal_expanded g = g.goal_expanded
MARCHE Claude's avatar
MARCHE Claude committed
217

MARCHE Claude's avatar
MARCHE Claude committed
218 219 220
let get_task g =
  match g.task with
    | None ->
221 222 223 224 225 226 227 228
	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
229 230
    | Some t -> t

231

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

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

242
let set_theory_expanded t b =
243 244 245 246 247 248 249 250
  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
251

252 253
let all_files : file list ref = ref []

254
let get_all_files () = !all_files
MARCHE Claude's avatar
MARCHE Claude committed
255

256 257 258 259
(************************)
(* saving state on disk *)
(************************)

MARCHE Claude's avatar
MARCHE Claude committed
260
let save_result fmt r =
MARCHE Claude's avatar
MARCHE Claude committed
261
  fprintf fmt "@\n<result status=\"%s\" time=\"%.2f\"/>"
MARCHE Claude's avatar
MARCHE Claude committed
262 263 264 265 266 267 268 269 270 271 272
    (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
273
    | Undone | Scheduled | Running ->
MARCHE Claude's avatar
MARCHE Claude committed
274 275 276
        fprintf fmt "<undone/>@\n"
    | InternalFailure msg ->
        fprintf fmt "<internalfailure reason=\"%s\"/>@\n"
MARCHE Claude's avatar
MARCHE Claude committed
277
          (Printexc.to_string msg)
MARCHE Claude's avatar
MARCHE Claude committed
278 279 280
    | Done r -> save_result fmt r

let save_proof_attempt fmt _key a =
281
  fprintf fmt "@\n@[<v 1><proof prover=\"%s\" timelimit=\"%d\" edited=\"%s\" obsolete=\"%b\">"
282
    (prover_id a.prover) a.timelimit a.edited_as a.proof_obsolete;
MARCHE Claude's avatar
MARCHE Claude committed
283
  save_status fmt a.proof_state;
MARCHE Claude's avatar
MARCHE Claude committed
284
  fprintf fmt "@]@\n</proof>"
285 286 287 288 289 290

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

let rec save_goal fmt g =
291 292
  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;
293
  Hashtbl.iter (save_proof_attempt fmt) g.external_proofs;
MARCHE Claude's avatar
MARCHE Claude committed
294
  Hashtbl.iter (save_trans fmt) g.transformations;
MARCHE Claude's avatar
MARCHE Claude committed
295
  fprintf fmt "@]@\n</goal>"
296

MARCHE Claude's avatar
MARCHE Claude committed
297
and save_trans fmt _ t =
298 299
  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
300
  List.iter (save_goal fmt) t.subgoals;
MARCHE Claude's avatar
MARCHE Claude committed
301
  fprintf fmt "@]@\n</transf>"
302 303

let save_theory fmt t =
304 305
  fprintf fmt "@\n@[<v 1><theory name=\"%s\" verified=\"%b\" expanded=\"%b\">"
    t.theory_name t.verified t.theory_expanded;
306
  List.iter (save_goal fmt) t.goals;
MARCHE Claude's avatar
MARCHE Claude committed
307
  fprintf fmt "@]@\n</theory>"
308 309

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

314 315 316 317
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
318 319
  fprintf fmt "<!DOCTYPE why3session SYSTEM \"why3session.dtd\">@\n";
  fprintf fmt "@[<v 1><why3session name=\"%s\">" fname;
320
  List.iter (save_file fmt) (get_all_files());
MARCHE Claude's avatar
MARCHE Claude committed
321 322
  fprintf fmt "@]@\n</why3session>";
  fprintf fmt "@.";
323 324 325 326 327 328
  close_out ch

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

329 330 331 332
let init_fun = ref (fun (_:O.key) (_:any) -> ())

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

333 334
let check_file_verified f =
  let b = List.for_all (fun t -> t.verified) f.theories in
335 336
  f.file_verified <- b;
  !notify_fun (File f)
337 338 339

let check_theory_proved t =
  let b = List.for_all (fun g -> g.proved) t.goals in
340 341 342
  t.verified <- b;
  !notify_fun (Theory t);
  check_file_verified t.theory_parent
343 344 345 346 347 348 349 350 351 352 353

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
354 355 356 357 358
  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
359 360 361

and check_transf_proved t =
  let b = List.for_all (fun g -> g.proved) t.subgoals in
362 363 364
  t.transf_proved <- b;
  !notify_fun (Transformation t);
  check_goal_proved t.parent_goal
365 366 367 368

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

372 373
(*************************)
(*         Scheduler     *)
MARCHE Claude's avatar
MARCHE Claude committed
374
(*************************)
375 376 377 378


(* timeout handler *)

379 380 381 382
type timeout_action =
  | Check_prover of (proof_attempt_status -> unit) * Call_provers.prover_call
  | Any_timeout of (unit -> bool)

383 384 385 386 387 388 389 390 391 392 393 394
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
395 396 397 398 399 400 401 402 403 404 405
    (fun acc c ->
       match c with
         | Check_prover(callback,call)  ->
             (match Call_provers.query_call call with
	       | None -> c::acc
	       | Some post ->
	           let res = post () in callback (Done res);
	           acc)
         | Any_timeout callback ->
             let b = callback () in
             if b then c::acc else acc)
406 407 408 409 410 411 412 413
    [] !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
414
	(Check_prover(callback,call))::l
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
      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

444 445 446 447
let schedule_any_timeout callback =
  running_proofs := (Any_timeout callback) :: ! running_proofs;
  run_timeout_handler ()

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 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510
(* 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;
511
  running_proofs := (Check_prover(callback, precall ())) :: !running_proofs;
512 513 514 515 516 517
  run_timeout_handler ()

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

518 519 520 521 522 523
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)
524

525
let schedule_edit_proof ~debug:_ ~editor ~file ~driver ~callback goal =
526 527 528 529 530 531 532 533 534 535 536 537 538 539 540
  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;
541
  let command = editor ^ " \"" ^ file ^ "\"" in
542 543
  schedule_edition command callback

544 545 546 547 548 549 550 551 552

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


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

  let rec get_labels f =
553
    (match f.Term.t_node with
554 555 556
      | Term.Tbinop(Term.Timplies,_,f) -> get_labels f
      | Term.Tquant(Term.Tforall,fq) ->
	  let (_,_,f) = Term.t_open_quant fq in get_labels f
557 558 559 560
      | 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
561
      | _ -> [])
562
    @ f.Term.t_label
563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584

  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


585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604
(**********************)
(*     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


605 606 607 608 609

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

610
let raw_add_external_proof ~obsolete ~timelimit ~edit (g:goal) p result =
611
  let key = O.create ~parent:g.goal_key () in
612
  let a = { prover = p;
613 614 615 616
            proof_goal = g;
            proof_key = key;
            proof_obsolete = obsolete;
	    proof_state = result;
617
	    timelimit = timelimit;
618 619 620
            edited_as = edit;
          }
  in
621
  Hashtbl.add g.external_proofs (prover_id p) a;
622 623 624
  let any = Proof_attempt a in
  !init_fun key any;
  !notify_fun any;
625 626
  a

627

MARCHE Claude's avatar
MARCHE Claude committed
628
(* [raw_add_goal parent name expl sum t] adds a goal to the given parent
629 630
   DOES NOT record the new goal in its parent, thus this should not be exported
*)
631
let raw_add_goal parent name expl sum topt exp =
632
  let parent_key = match parent with
633 634
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
635 636
  in
  let key = O.create ~parent:parent_key () in
637
  let sum = match topt with
MARCHE Claude's avatar
MARCHE Claude committed
638
    | None -> sum
639 640
    | Some t -> task_checksum t
  in
641 642 643
  let goal = { goal_name = name;
               goal_expl = expl;
	       parent = parent;
644
               task = topt ;
645
	       checksum = sum;
646 647 648 649
               goal_key = key;
               external_proofs = Hashtbl.create 7;
               transformations = Hashtbl.create 3;
               proved = false;
650
	       goal_expanded = exp;
651 652
             }
  in
653 654
  let any = Goal goal in
  !init_fun key any;
655
  !notify_fun any; (*useless ? *)
656 657 658 659 660 661
  goal


(* [raw_add_transformation g name adds a transformation to the given goal g
   Adds no subgoals, thus this should not be exported
*)
662
let raw_add_transformation g trans exp =
663 664
  let parent = g.goal_key in
  let key = O.create ~parent () in
665 666
  let tr = { transf = trans;
	     parent_goal = g;
667 668 669
             transf_proved = false;
             transf_key = key;
             subgoals = [];
670
             transf_expanded = exp;
671 672
           }
  in
673 674 675 676
  Hashtbl.add g.transformations trans.transformation_name tr;
  let any = Transformation tr in
  !init_fun key any;
  !notify_fun any;
677 678
  tr

679
let raw_add_theory mfile thopt thname exp =
680 681
  let parent = mfile.file_key in
  let key = O.create ~parent () in
682 683
  let mth = { theory_name = thname;
	      theory = thopt;
684 685 686
              theory_key = key;
              theory_parent = mfile;
              goals = [] ;
687 688 689
              verified = false;
	      theory_expanded = exp;
	    }
690
  in
691 692 693
  let any = Theory mth in
  !init_fun key any;
  !notify_fun any;
694 695 696 697
  mth



698
let add_theory mfile name th =
699
  let tasks = List.rev (Task.split_theory th None None) in
700
  let mth = raw_add_theory mfile (Some th) name true in
701 702 703 704 705 706
  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
707
         let goal = raw_add_goal (Parent_theory mth) name expl "" (Some t) true in
708 709 710 711 712
         goal :: acc)
      []
      tasks
  in
  mth.goals <- List.rev goals;
MARCHE Claude's avatar
MARCHE Claude committed
713
  check_theory_proved mth;
714 715
  mth

716
let raw_add_file f exp =
717
  let key = O.create () in
718
  let mfile = { file_name = f;
719
                file_key = key;
720
                theories = [] ;
721 722 723
                file_verified = false;
		file_expanded = exp;
	      }
724 725
  in
  all_files := !all_files @ [mfile];
726 727 728
  let any = File mfile in
  !init_fun key any;
  !notify_fun any;
729 730
  mfile

MARCHE Claude's avatar
MARCHE Claude committed
731
let current_env = ref None
732
let current_provers = ref Util.Mstr.empty
MARCHE Claude's avatar
MARCHE Claude committed
733 734
let project_dir = ref ""

735 736
let get_provers () = !current_provers

MARCHE Claude's avatar
MARCHE Claude committed
737 738
let read_file fn =
  let fn = Filename.concat !project_dir fn in
MARCHE Claude's avatar
MARCHE Claude committed
739 740
  let env = match !current_env with
    | None -> assert false | Some e -> e
MARCHE Claude's avatar
MARCHE Claude committed
741 742
  in
  let theories = Env.read_file env fn in
743 744 745
  let theories =
    Theory.Mnm.fold
      (fun name th acc ->
746 747 748
         match th.Theory.th_name.Ident.id_loc with
           | Some l -> (l,name,th)::acc
           | None   -> (Loc.dummy_position,name,th)::acc)
749 750
      theories []
  in
MARCHE Claude's avatar
MARCHE Claude committed
751
  List.sort
752 753
    (fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
    theories
MARCHE Claude's avatar
MARCHE Claude committed
754 755 756

let add_file f =
  let theories = read_file f in
757
  let mfile = raw_add_file f true in
758 759
  let mths =
    List.fold_left
760 761
      (fun acc (_,name,t) ->
         let mth = add_theory mfile name t in
762 763 764 765
         mth :: acc)
      [] theories
  in
  mfile.theories <- List.rev mths;
766 767 768
  check_file_verified mfile;
  !notify_fun (File mfile)

769 770


771 772 773
let file_exists fn =
  List.exists (fun f -> f.file_name = fn) !all_files

774 775


776 777


778 779 780 781
(**********************************)
(* reload a file                  *)
(**********************************)

782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799
let reload_proof obsolete goal pid old_a =
  let p = 
    try
      Detected_prover (Util.Mstr.find pid !current_provers)
    with Not_found ->
      eprintf
        "Warning: prover %s appears in database but is not installed.@."
        pid;
      (Undetected_prover pid)
  in
  let old_res = old_a.proof_state in
  let obsolete = obsolete or old_a.proof_obsolete in
  (* eprintf "proof_obsolete : %b@." obsolete; *)
  let a =
    raw_add_external_proof ~obsolete ~timelimit:old_a.timelimit
      ~edit:old_a.edited_as goal p old_res
  in
  !notify_fun (Goal a.proof_goal)
MARCHE Claude's avatar
MARCHE Claude committed
800

801
let rec reload_any_goal parent gid gname sum t old_goal goal_obsolete =
MARCHE Claude's avatar
MARCHE Claude committed
802
  let info = get_explanation gid (Task.task_goal_fmla t) in
803 804
  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
805
  goal.task <- Some t;
MARCHE Claude's avatar
MARCHE Claude committed
806 807 808 809
  begin
    match old_goal with
      | None -> ()
      | Some g ->
810 811
          Hashtbl.iter (reload_proof goal_obsolete goal) g.external_proofs;
          Hashtbl.iter (reload_trans goal_obsolete goal) g.transformations
MARCHE Claude's avatar
MARCHE Claude committed
812
  end;
813
  check_goal_proved goal;
814
  goal
MARCHE Claude's avatar
MARCHE Claude committed
815 816


817
and reload_trans  _goal_obsolete goal _ tr =
818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835
  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 ; ... ]

836
       we first associate each new goals for which there is an old goal
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
       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
871 872 873
    (* 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)
874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889

       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
890
            associate_remaining_goals new_rem rem
891 892 893 894 895 896 897
              ((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) ->
898
         let mg =
899
           reload_any_goal (Parent_transf mtr) id
900
             subgoal_name sum subtask old_g subgoal_obsolete
901 902 903 904
         in mg::acc)
      [] goals
    in
    mtr.subgoals <- goals;
905
    check_transf_proved mtr
906 907
  in
  apply_transformation ~callback tr.transf (get_task goal)
908 909


MARCHE Claude's avatar
MARCHE Claude committed
910
(* reloads the task [t] in theory mth (named tname) *)
911
let reload_root_goal mth tname old_goals t : goal =
912
  let id = (Task.task_goal t).Decl.pr_name in
MARCHE Claude's avatar
MARCHE Claude committed
913
  let gname = id.Ident.id_string in
914
  let sum = task_checksum t in
MARCHE Claude's avatar
MARCHE Claude committed
915 916 917 918 919 920
  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)
921
  in
MARCHE Claude's avatar
MARCHE Claude committed
922 923
  if goal_obsolete then
    eprintf "Goal %s.%s has changed@." tname gname;
924
  reload_any_goal (Parent_theory mth) id gname sum t old_goal goal_obsolete
MARCHE Claude's avatar
MARCHE Claude committed
925 926

(* reloads a theory *)
927
let reload_theory mfile old_theories (_,tname,th) =
MARCHE Claude's avatar
MARCHE Claude committed
928 929
  eprintf "[Reload] theory '%s'@."tname;
  let tasks = List.rev (Task.split_theory th None None) in
930
  let old_goals, old_exp =
MARCHE Claude's avatar
MARCHE Claude committed
931 932
    try
      let old_mth = Util.Mstr.find tname old_theories in
933 934
      old_mth.goals, old_mth.theory_expanded
    with Not_found -> [], true
MARCHE Claude's avatar
MARCHE Claude committed
935
  in
936
  let mth = raw_add_theory mfile (Some th) tname old_exp in
MARCHE Claude's avatar
MARCHE Claude committed
937 938 939 940
  let goalsmap = List.fold_left
    (fun goalsmap g -> Util.Mstr.add g.goal_name g goalsmap)
    Util.Mstr.empty old_goals
  in
941
  !notify_fun (Theory mth);
MARCHE Claude's avatar
MARCHE Claude committed
942 943
  let new_goals = List.fold_left
    (fun acc t ->
944
       let g = reload_root_goal mth tname goalsmap t in
MARCHE Claude's avatar
MARCHE Claude committed
945 946 947 948 949 950
       g::acc)
    [] tasks
  in
  mth.goals <- List.rev new_goals;
  check_theory_proved mth;
  mth
951 952


MARCHE Claude's avatar
MARCHE Claude committed
953
(* reloads a file *)
954
let reload_file mf theories =
955
  let new_mf = raw_add_file mf.file_name mf.file_expanded in
MARCHE Claude's avatar
MARCHE Claude committed
956 957 958 959 960
  let old_theories = List.fold_left
    (fun acc t -> Util.Mstr.add t.theory_name t acc)
    Util.Mstr.empty
    mf.theories
  in
961
  !notify_fun (File new_mf);
MARCHE Claude's avatar
MARCHE Claude committed
962
  let mths = List.fold_left
963
    (fun acc th -> reload_theory new_mf old_theories th :: acc)
MARCHE Claude's avatar
MARCHE Claude committed
964 965 966 967 968
    [] theories
  in
  new_mf.theories <- List.rev mths;
  check_file_verified new_mf

MARCHE Claude's avatar
MARCHE Claude committed
969 970

(* reloads all files *)
971
let reload_all () =
MARCHE Claude's avatar
MARCHE Claude committed
972
  let files = !all_files in
973
  let all_theories =
974
    List.map (fun mf ->
975
		eprintf "[Reload] file '%s'@." mf.file_name;
976
		(mf,read_file mf.file_name))
977 978
      files
  in
MARCHE Claude's avatar
MARCHE Claude committed
979 980
  all_files := [];
  O.reset ();
981
  List.iter (fun (mf,ths) -> reload_file mf ths) all_theories
982

983 984 985 986
(****************************)
(*     session opening      *)
(****************************)

987 988 989 990 991 992 993 994
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

995 996 997 998 999
let int_attribute field r def =
  try
    int_of_string (List.assoc field r.Xml.attributes)
  with Not_found | Invalid_argument _ -> def

MARCHE Claude's avatar
MARCHE Claude committed
1000 1001 1002
let load_result r =
  match r.Xml.name with
    | "result" ->
MARCHE Claude's avatar
MARCHE Claude committed
1003
	let status =
MARCHE Claude's avatar
MARCHE Claude committed
1004 1005 1006
	  try List.assoc "status" r.Xml.attributes
	  with Not_found -> assert false
	in
MARCHE Claude's avatar
MARCHE Claude committed
1007
	let answer =
MARCHE Claude's avatar
MARCHE Claude committed
1008 1009 1010 1011 1012 1013 1014
	  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
1015
	    | s ->
MARCHE Claude's avatar
MARCHE Claude committed
1016 1017
		eprintf "Session.load_result: unexpected status '%s'@."  s;
		assert false
MARCHE Claude's avatar
MARCHE Claude committed
1018 1019 1020 1021 1022
	in
	let time =
	  try float_of_string (List.assoc "time" r.Xml.attributes)
	  with Not_found -> 0.0
	in
1023
	Done {
1024
	  Call_provers.pr_answer = answer;
MARCHE Claude's avatar
MARCHE Claude committed
1025 1026 1027
	  Call_provers.pr_time = time;
	  Call_provers.pr_output = "";
	}
1028
    | "undone" -> Undone
MARCHE Claude's avatar
MARCHE Claude committed
1029
    | s ->
MARCHE Claude's avatar
MARCHE Claude committed
1030 1031
	eprintf "Session.load_result: unexpected element '%s'@."  s;
	assert false
MARCHE Claude's avatar
MARCHE Claude committed
1032 1033


1034
let rec load_goal ~env parent acc g =
MARCHE Claude's avatar
MARCHE Claude committed
1035 1036
  match g.Xml.name with
    | "goal" ->
MARCHE Claude's avatar
MARCHE Claude committed
1037
	let gname =
MARCHE Claude's avatar
MARCHE Claude committed
1038 1039 1040
	  try List.assoc "name" g.Xml.attributes
	  with Not_found -> assert false
	in
MARCHE Claude's avatar
MARCHE Claude committed
1041
	let expl =
MARCHE Claude's avatar
MARCHE Claude committed
1042 1043 1044
	  try Some (List.assoc "expl" g.Xml.attributes)
	  with Not_found -> None
	in
MARCHE Claude's avatar
MARCHE Claude committed
1045 1046 1047 1048
	let sum =
	  try List.assoc "sum" g.Xml.attributes
	  with Not_found -> ""
	in
1049 1050
	let exp = bool_attribute "expanded" g true in
	let mg = raw_add_goal parent gname expl sum None exp in
1051
	List.iter (load_proof_or_transf ~env mg) g.Xml.elements;
MARCHE Claude's avatar
MARCHE Claude committed
1052
	mg::acc