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


21
open Why3
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
      Hashtbl.find h name
    with Not_found ->
      let t = {transformation_name = name;
89
               transformation = lookup_trans env name }
90 91
      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 ->
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

MARCHE Claude's avatar
MARCHE Claude committed
256 257 258 259 260 261
let current_env = ref None
let current_provers = ref Util.Mstr.empty
let project_dir = ref ""

let get_provers () = !current_provers

262 263 264 265
(************************)
(* saving state on disk *)
(************************)

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

let save_proof_attempt fmt _key a =
287
  fprintf fmt "@\n@[<v 1><proof prover=\"%s\" timelimit=\"%d\" edited=\"%s\" obsolete=\"%b\">"
288
    (prover_id a.prover) a.timelimit a.edited_as a.proof_obsolete;
MARCHE Claude's avatar
MARCHE Claude committed
289
  save_status fmt a.proof_state;
MARCHE Claude's avatar
MARCHE Claude committed
290
  fprintf fmt "@]@\n</proof>"
291 292 293 294 295 296

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

let rec save_goal fmt g =
MARCHE Claude's avatar
MARCHE Claude committed
297 298 299
  fprintf fmt "@\n@[<v 1><goal name=\"%s\" %asum=\"%s\" proved=\"%b\" expanded=\"%b\" shape=\"%s\">"
    g.goal_name (opt "expl") g.goal_expl g.checksum g.proved  g.goal_expanded
    (Termcode.t_shape_buf (Task.task_goal_fmla (get_task g)));
300
  Hashtbl.iter (save_proof_attempt fmt) g.external_proofs;
MARCHE Claude's avatar
MARCHE Claude committed
301
  Hashtbl.iter (save_trans fmt) g.transformations;
MARCHE Claude's avatar
MARCHE Claude committed
302
  fprintf fmt "@]@\n</goal>"
303

MARCHE Claude's avatar
MARCHE Claude committed
304
and save_trans fmt _ t =
305 306
  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
307
  List.iter (save_goal fmt) t.subgoals;
MARCHE Claude's avatar
MARCHE Claude committed
308
  fprintf fmt "@]@\n</transf>"
309 310

let save_theory fmt t =
311 312
  fprintf fmt "@\n@[<v 1><theory name=\"%s\" verified=\"%b\" expanded=\"%b\">"
    t.theory_name t.verified t.theory_expanded;
313
  List.iter (save_goal fmt) t.goals;
MARCHE Claude's avatar
MARCHE Claude committed
314
  fprintf fmt "@]@\n</theory>"
315 316

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

MARCHE Claude's avatar
MARCHE Claude committed
322 323 324 325
let save_prover fmt p =
  fprintf fmt "@\n@[<v 1><prover id=\"%s\" name=\"%s\" version=\"%s\"/>@]"
    p.prover_id p.prover_name p.prover_version

326 327 328 329
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
330 331
  fprintf fmt "<!DOCTYPE why3session SYSTEM \"why3session.dtd\">@\n";
  fprintf fmt "@[<v 1><why3session name=\"%s\">" fname;
MARCHE Claude's avatar
MARCHE Claude committed
332
  Util.Mstr.iter (fun _ d -> save_prover fmt d) (get_provers ());
333
  List.iter (save_file fmt) (get_all_files());
MARCHE Claude's avatar
MARCHE Claude committed
334 335
  fprintf fmt "@]@\n</why3session>";
  fprintf fmt "@.";
336 337 338 339 340 341
  close_out ch

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

342 343 344 345
let init_fun = ref (fun (_:O.key) (_:any) -> ())

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

346 347
let check_file_verified f =
  let b = List.for_all (fun t -> t.verified) f.theories in
348 349
  f.file_verified <- b;
  !notify_fun (File f)
350 351 352

let check_theory_proved t =
  let b = List.for_all (fun g -> g.proved) t.goals in
353 354 355
  t.verified <- b;
  !notify_fun (Theory t);
  check_file_verified t.theory_parent
356 357 358 359

let rec check_goal_proved g =
  let b1 = Hashtbl.fold
    (fun _ a acc -> acc ||
360
       not a.proof_obsolete &&
361
       match a.proof_state with
362 363
         | Done { Call_provers.pr_answer = Call_provers.Valid} -> true
         | _ -> false) g.external_proofs false
364 365 366 367
  in
  let b = Hashtbl.fold
    (fun _ t acc -> acc || t.transf_proved) g.transformations b1
  in
368 369 370 371 372
  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
373 374 375

and check_transf_proved t =
  let b = List.for_all (fun g -> g.proved) t.subgoals in
376 377 378
  t.transf_proved <- b;
  !notify_fun (Transformation t);
  check_goal_proved t.parent_goal
379 380 381 382

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

386 387
(*************************)
(*         Scheduler     *)
MARCHE Claude's avatar
MARCHE Claude committed
388
(*************************)
389 390 391 392


(* timeout handler *)

393 394 395 396
type timeout_action =
  | Check_prover of (proof_attempt_status -> unit) * Call_provers.prover_call
  | Any_timeout of (unit -> bool)

397 398 399 400 401 402 403 404 405 406 407 408
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
409 410 411 412
    (fun acc c ->
       match c with
         | Check_prover(callback,call)  ->
             (match Call_provers.query_call call with
413 414 415 416
               | None -> c::acc
               | Some post ->
                   let res = post () in callback (Done res);
                   acc)
417 418 419
         | Any_timeout callback ->
             let b = callback () in
             if b then c::acc else acc)
420 421 422 423 424
    [] !running_proofs
  in
  let l =
    if List.length l < !maximum_running_proofs then
      begin try
425 426 427 428
        let (callback,pre_call) = Queue.pop proof_attempts_queue in
        callback Running;
        let call = pre_call () in
        (Check_prover(callback,call))::l
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
      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

458 459 460 461
let schedule_any_timeout callback =
  running_proofs := (Any_timeout callback) :: ! running_proofs;
  run_timeout_handler ()

462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477
(* 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
478 479 480 481 482 483 484 485 486 487 488
        | 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 ()
489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514
        | 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,
515
                        callback,goal))
516 517 518 519 520 521 522 523 524
    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;
525
  running_proofs := (Check_prover(callback, precall ())) :: !running_proofs;
526 527 528 529 530 531
  run_timeout_handler ()

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

532 533 534
let apply_transformation ~callback t task =
   match t.transformation with
    | Trans_one t ->
535
        callback [Trans.apply t task]
536
    | Trans_list t ->
537
        callback (Trans.apply t task)
538

539
let schedule_edit_proof ~debug:_ ~editor ~file ~driver ~callback goal =
540 541 542 543
  let old =
    if Sys.file_exists file
    then
      begin
544
        let backup = file ^ ".bak" in
545 546 547 548 549 550 551 552 553 554
        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;
555
  let command = editor ^ " \"" ^ file ^ "\"" in
556 557
  schedule_edition command callback

558 559 560 561 562 563 564 565 566

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


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

  let rec get_labels f =
567
    (match f.Term.t_node with
568 569
      | Term.Tbinop(Term.Timplies,_,f) -> get_labels f
      | Term.Tquant(Term.Tforall,fq) ->
570
          let (_,_,f) = Term.t_open_quant fq in get_labels f
571
      | Term.Tlet(_,fb) ->
572
          let (_,f) = Term.t_open_bound fb in get_labels f
573
      | Term.Tcase(_,[fb]) ->
574
          let (_,f) = Term.t_open_branch fb in get_labels f
575
      | _ -> [])
576
    @ f.Term.t_label
577 578 579 580 581 582 583 584 585 586 587 588

  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
589
             let e = Str.matched_group 1 s in
590
(*
591
             Format.eprintf "found explanation: '%s'" e;
592
*)
593 594
             r := Some e
           end)
595 596 597 598
      (id.Ident.id_label @ get_labels fmla);
    !r


599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618
(**********************)
(*     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


619 620 621 622 623

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

624
let raw_add_external_proof ~obsolete ~timelimit ~edit (g:goal) p result =
625
  let key = O.create ~parent:g.goal_key () in
626
  let a = { prover = p;
627 628 629
            proof_goal = g;
            proof_key = key;
            proof_obsolete = obsolete;
630 631
            proof_state = result;
            timelimit = timelimit;
632 633 634
            edited_as = edit;
          }
  in
635
  Hashtbl.add g.external_proofs (prover_id p) a;
636 637 638
  let any = Proof_attempt a in
  !init_fun key any;
  !notify_fun any;
639 640
  a

641

MARCHE Claude's avatar
MARCHE Claude committed
642
(* [raw_add_goal parent name expl sum t] adds a goal to the given parent
643 644
   DOES NOT record the new goal in its parent, thus this should not be exported
*)
645
let raw_add_goal parent name expl sum topt exp =
646
  let parent_key = match parent with
647 648
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
649 650
  in
  let key = O.create ~parent:parent_key () in
651
  let sum = match topt with
MARCHE Claude's avatar
MARCHE Claude committed
652
    | None -> sum
653 654
    | Some t -> task_checksum t
  in
655 656
  let goal = { goal_name = name;
               goal_expl = expl;
657
               parent = parent;
658
               task = topt ;
659
               checksum = sum;
660 661 662 663
               goal_key = key;
               external_proofs = Hashtbl.create 7;
               transformations = Hashtbl.create 3;
               proved = false;
664
               goal_expanded = exp;
665 666
             }
  in
667 668
  let any = Goal goal in
  !init_fun key any;
669
  !notify_fun any; (*useless ? *)
670 671 672 673 674 675
  goal


(* [raw_add_transformation g name adds a transformation to the given goal g
   Adds no subgoals, thus this should not be exported
*)
676
let raw_add_transformation g trans exp =
677 678
  let parent = g.goal_key in
  let key = O.create ~parent () in
679
  let tr = { transf = trans;
680
             parent_goal = g;
681 682 683
             transf_proved = false;
             transf_key = key;
             subgoals = [];
684
             transf_expanded = exp;
685 686
           }
  in
687 688 689 690
  Hashtbl.add g.transformations trans.transformation_name tr;
  let any = Transformation tr in
  !init_fun key any;
  !notify_fun any;
691 692
  tr

693
let raw_add_theory mfile thopt thname exp =
694 695
  let parent = mfile.file_key in
  let key = O.create ~parent () in
696
  let mth = { theory_name = thname;
697
              theory = thopt;
698 699 700
              theory_key = key;
              theory_parent = mfile;
              goals = [] ;
701
              verified = false;
702 703
              theory_expanded = exp;
            }
704
  in
705 706 707
  let any = Theory mth in
  !init_fun key any;
  !notify_fun any;
708 709 710 711
  mth



712
let add_theory mfile name th =
713
  let tasks = List.rev (Task.split_theory th None None) in
714
  let mth = raw_add_theory mfile (Some th) name true in
715 716 717 718 719 720
  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
721
         let goal = raw_add_goal (Parent_theory mth) name expl "" (Some t) true in
722 723 724 725 726
         goal :: acc)
      []
      tasks
  in
  mth.goals <- List.rev goals;
MARCHE Claude's avatar
MARCHE Claude committed
727
  check_theory_proved mth;
728 729
  mth

730
let raw_add_file f exp =
731
  let key = O.create () in
732
  let mfile = { file_name = f;
733
                file_key = key;
734
                theories = [] ;
735
                file_verified = false;
736 737
                file_expanded = exp;
              }
738 739
  in
  all_files := !all_files @ [mfile];
740 741 742
  let any = File mfile in
  !init_fun key any;
  !notify_fun any;
743 744
  mfile

745

MARCHE Claude's avatar
MARCHE Claude committed
746 747
let read_file fn =
  let fn = Filename.concat !project_dir fn in
MARCHE Claude's avatar
MARCHE Claude committed
748 749
  let env = match !current_env with
    | None -> assert false | Some e -> e
MARCHE Claude's avatar
MARCHE Claude committed
750 751
  in
  let theories = Env.read_file env fn in
752
  let theories =
753
    Util.Mstr.fold
754
      (fun name th acc ->
755 756 757
         match th.Theory.th_name.Ident.id_loc with
           | Some l -> (l,name,th)::acc
           | None   -> (Loc.dummy_position,name,th)::acc)
758 759
      theories []
  in
MARCHE Claude's avatar
MARCHE Claude committed
760
  List.sort
761 762
    (fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
    theories
MARCHE Claude's avatar
MARCHE Claude committed
763 764 765

let add_file f =
  let theories = read_file f in
766
  let mfile = raw_add_file f true in
767 768
  let mths =
    List.fold_left
769 770
      (fun acc (_,name,t) ->
         let mth = add_theory mfile name t in
771 772 773 774
         mth :: acc)
      [] theories
  in
  mfile.theories <- List.rev mths;
775 776 777
  check_file_verified mfile;
  !notify_fun (File mfile)

778 779


780 781 782
let file_exists fn =
  List.exists (fun f -> f.file_name = fn) !all_files

783 784


785 786


787 788 789 790
(**********************************)
(* reload a file                  *)
(**********************************)

791
let reload_proof obsolete goal pid old_a =
792
  let p =
793 794 795 796 797 798 799 800 801
    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
802
  let obsolete = obsolete || old_a.proof_obsolete in
803 804 805 806 807 808
  (* 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
809

810 811 812 813 814 815 816 817 818 819 820


(*
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
    (* eprintf "proof_obsolete : %b@." obsolete; *)
    let a =
      raw_add_external_proof ~obsolete ~timelimit:old_a.timelimit
821
        ~edit:old_a.edited_as goal p old_res
822 823 824 825 826 827 828 829
    in
    !notify_fun (Goal a.proof_goal)
  with Not_found ->
    eprintf
      "Warning: prover %s appears in database but is not installed.@."
      pid
*)

830
let rec reload_any_goal parent gid gname sum t old_goal goal_obsolete =
MARCHE Claude's avatar
MARCHE Claude committed
831
  let info = get_explanation gid (Task.task_goal_fmla t) in
832 833
  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
834
  goal.task <- Some t;
MARCHE Claude's avatar
MARCHE Claude committed
835 836 837 838
  begin
    match old_goal with
      | None -> ()
      | Some g ->
839 840
          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
841
  end;
842
  check_goal_proved goal;
843
  goal
MARCHE Claude's avatar
MARCHE Claude committed
844 845


846
and reload_trans  _goal_obsolete goal _ tr =
847 848
  let trname = tr.transf.transformation_name in
  let gname = goal.goal_name in
849
  eprintf "[Reload] transformation %s for goal %s @\n" trname gname;
850 851 852 853 854 855 856 857 858 859 860 861 862 863 864
  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 ; ... ]

865
       we first associate each new goals for which there is an old goal
866 867 868 869 870 871
       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 ; ... ]

    *)
872
    let new_goals_map,old_subgoals,_ =
873 874 875 876 877 878 879
      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
880 881
               let g = Util.Mstr.find sum old_subgoals in
               (* an old subgoal has the same checksum *)
882 883 884 885
(*
               eprintf "Merge phase 1: old goal '%s' -> new goal '%s'@."
                 g.goal_name subgoal_name;
*)
886
               (Some g, Util.Mstr.remove sum old_subgoals)
887
             with Not_found ->
888 889 890 891 892
(*
               eprintf "Merge phase 1: no old goal -> new goal '%s'@."
                 subgoal_name;
*)
               (None,old_subgoals)
893 894
           in
           ((count,id,subgoal_name,subtask,sum,old_subgoal) :: new_goals_map,
895
            old_subgoals, count+1))
896 897 898 899 900 901 902 903 904 905 906 907 908
        ([],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
909 910 911
    (* 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)
912 913 914

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

915 916 917 918 919 920 921 922 923 924 925 926
       TODO: use the distance Term.t_dist to obtain a better match

       other solution: sort in some arbitrary total order

       g1 < g2 < ... <

       h1 < h2 < ... <

       then identical goals can be detected by a merge_like algorithm :

       if merged list starts with g :

927
       g1 < ... gk <= h1 < ... <
928

929
       then g1 .. g{k-1} are new and gk associated to h1, and then
930 931 932 933
       recursively merge g{k+1} ... and h2 ...

       otherwise, list starts

934
       h1 < ... hk <= g1 <= ... <
935 936 937 938 939 940

       ....

       Another formulation :

       if merged list starts with
941 942 943

       1) g1 g2 ...

944 945 946 947 948 949 950
       associate g1 to nothing and recursively process g2 ...

       2) g1 h1 g2 ... with d(g1,h1) < d(h1,g2)

       associate g1 to h1 and recursively process g2 ...

       3) g1 h1 g2 ... with d(g1,h1) > d(h1,g2)
951

952 953 954 955
       ?

       4) g1 h1 h2 ...

956

957
       PRELIMINARY: store the shape of the conclusion of the goal in the XML
958
       file.
959 960


961 962 963
    *)
    let rec associate_remaining_goals new_goals_map remaining acc =
      match new_goals_map with
964
        | [] ->
965 966 967 968 969
(*
            eprintf "Merge phase 3: dropping %d old goals@."
              (List.length remaining);
*)
            acc
970 971 972
        | (_,id,subgoal_name,subtask,sum,old_subgoal)::new_rem ->
            let ((obsolete,old_goal,rem) : bool * goal option * (string * goal) list) =
              match old_subgoal with
973
                | Some _g ->
974 975 976 977 978
(*
                    eprintf "Merge phase 2: old goal '%s' -> new goal '%s'@."
                      g.goal_name subgoal_name;
*)
                    (false,old_subgoal,remaining)
979 980
                | None ->
                    match remaining with
981
                      | [] ->
982 983 984 985 986
(*
                          eprintf "Merge phase 2: no old goal -> new goal '%s'@."
                            subgoal_name;
*)
                          (false,None,[])
987
                      | (_goal_name,g) :: rem ->
988 989 990 991 992
(*
                          eprintf "Merge phase 2: old goal '%s' -> new goal '%s'@."
                            g.goal_name subgoal_name;
*)
                          (true,Some g,rem)
993
            in
994
            associate_remaining_goals new_rem rem
995 996 997 998 999 1000 1001
              ((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) ->
1002
         let mg =
1003
           reload_any_goal (Parent_transf mtr) id
1004
             subgoal_name sum subtask old_g subgoal_obsolete
1005
         in mg::acc)
1006
      [] (List.rev goals)
1007
    in
1008
    mtr.subgoals <- (List.rev goals);
1009
    check_transf_proved mtr
1010 1011
  in
  apply_transformation ~callback tr.transf (get_task goal)
1012 1013


MARCHE Claude's avatar
MARCHE Claude committed
1014
(* reloads the task [t] in theory mth (named tname) *)
1015
let reload_root_goal mth tname old_goals t : goal =