session.ml 63.2 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
    { prover_id : string;
      prover_name : string;
      prover_version : string;
      command : string;
      driver_name : string;
      driver : Driver.driver;
      mutable editor : string;
36
      interactive : bool;
37
    }
38

39 40 41 42 43
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 ;
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
        interactive = pr.Whyconf.interactive;
51
      }
52
      acc
MARCHE Claude's avatar
MARCHE Claude committed
53 54
  with e ->
    eprintf "Failed to load driver %s for prover %s (%a). prover disabled@."
MARCHE Claude's avatar
MARCHE Claude committed
55
      pr.Whyconf.driver
MARCHE Claude's avatar
MARCHE Claude committed
56 57 58
      pr.Whyconf.name
      Exn_printer.exn_printer e
      ;
59 60
    acc

61 62 63
(***************************)
(*      transformations    *)
(***************************)
64

65 66 67 68
type trans =
  | Trans_one of Task.task Trans.trans
  | Trans_list of Task.task Trans.tlist

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

let transformation_id t = t.transformation_name

76 77 78 79 80 81 82 83 84 85 86
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
87
    try
88 89 90
      Hashtbl.find h name
    with Not_found ->
      let t = {transformation_name = name;
91
               transformation = lookup_trans env name }
92 93
      in Hashtbl.add h name t; t

94 95 96 97
(***************************)
(*     proof status        *)
(***************************)

98 99 100
type proof_attempt_status =
  | Undone
  | Scheduled (** external proof attempt is scheduled *)
101
  | Interrupted
102 103 104
  | 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 *)
105
  | Unedited (** interactive prover yet no proof script *)
106

107 108 109 110 111
type smoke_detector =
  | SD_None (** no smoke detector *)
  | SD_Top  (** smoke_detector *)
  | SD_Deep (** smoke_detector_deep *)

112 113 114 115
(***************************)
(*     main functor        *)
(***************************)

116 117 118 119
module type OBSERVER = sig
  type key
  val create: ?parent:key -> unit -> key
  val remove: key -> unit
MARCHE Claude's avatar
MARCHE Claude committed
120
  val reset: unit -> unit
121 122 123

  val timeout: ms:int -> (unit -> bool) -> unit
  val idle: (unit -> bool) -> unit
124 125 126

  val notify_timer_state : int -> int -> int -> unit

127 128 129 130
end

module Make(O : OBSERVER) = struct

131 132 133 134
(***************************)
(*     session state       *)
(***************************)

135 136 137 138 139 140 141 142
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

143
type proof_attempt =
144
    { prover : prover_option;
145 146 147
      proof_goal : goal;
      proof_key : O.key;
      mutable proof_state : proof_attempt_status;
148
      mutable timelimit : int;
149 150 151 152 153
      mutable proof_obsolete : bool;
      mutable edited_as : string;
    }

and goal_parent =
154 155
  | Parent_theory of theory
  | Parent_transf of transf
156 157 158 159 160

and goal =
    { goal_name : string;
      goal_expl : string option;
      parent : goal_parent;
161
      mutable task: Task.task option;
MARCHE Claude's avatar
MARCHE Claude committed
162
      mutable checksum : string;
163
      goal_shape : string;
164 165
      goal_key : O.key;
      mutable proved : bool;
166
      mutable goal_expanded : bool;
167 168 169 170 171
      external_proofs: (string, proof_attempt) Hashtbl.t;
      transformations : (string, transf) Hashtbl.t;
    }

and transf =
172 173
    { transf : transformation_data;
      parent_goal : goal;
174 175 176
      mutable transf_proved : bool;
      transf_key : O.key;
      mutable subgoals : goal list;
177
      mutable transf_expanded : bool;
178 179 180
    }

and theory =
181
    { theory_name : string;
MARCHE Claude's avatar
MARCHE Claude committed
182
      mutable theory : Theory.theory option;
183 184 185 186
      theory_key : O.key;
      theory_parent : file;
      mutable goals : goal list;
      mutable verified : bool;
187
      mutable theory_expanded : bool;
188 189 190 191 192 193 194
    }

and file =
    { file_name : string;
      file_key : O.key;
      mutable theories: theory list;
      mutable file_verified : bool;
195
      mutable file_expanded : bool;
196 197
    }

198 199 200 201 202 203 204
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
205 206 207 208
let theory_name t = t.theory_name
let theory_key t = t.theory_key
let verified t = t.verified
let goals t = t.goals
209 210
let theory_expanded t = t.theory_expanded

211 212 213
let running a = match a.proof_state with
  | Scheduled | Running | Interrupted -> true
  | Undone | Done _ | InternalFailure _ | Unedited -> false
MARCHE Claude's avatar
MARCHE Claude committed
214

MARCHE Claude's avatar
MARCHE Claude committed
215 216 217
let get_theory t =
  match t.theory with
    | None ->
218 219
        eprintf "Session: theory not yet reimported, this should not happen@.";
        assert false
220 221
    | Some t -> t

MARCHE Claude's avatar
MARCHE Claude committed
222
let goal_name g = g.goal_name
MARCHE Claude's avatar
MARCHE Claude committed
223 224
let goal_expl g =
  match g.goal_expl with
MARCHE Claude's avatar
MARCHE Claude committed
225 226 227 228 229
    | 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
230 231
let external_proofs g = g.external_proofs
let goal_expanded g = g.goal_expanded
MARCHE Claude's avatar
MARCHE Claude committed
232

233 234
let smoke_detector = ref SD_None

MARCHE Claude's avatar
MARCHE Claude committed
235 236 237
let get_task g =
  match g.task with
    | None ->
238 239 240 241 242 243 244 245
        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
246 247
    | Some t -> t

248

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

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

259
let set_theory_expanded t b =
260 261 262 263 264 265 266 267
  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
268

269 270
let all_files : file list ref = ref []

271
let get_all_files () = !all_files
MARCHE Claude's avatar
MARCHE Claude committed
272

MARCHE Claude's avatar
MARCHE Claude committed
273 274 275 276 277 278
let current_env = ref None
let current_provers = ref Util.Mstr.empty
let project_dir = ref ""

let get_provers () = !current_provers

279 280 281 282
(************************)
(* saving state on disk *)
(************************)

MARCHE Claude's avatar
MARCHE Claude committed
283
let save_result fmt r =
MARCHE Claude's avatar
MARCHE Claude committed
284
  fprintf fmt "@\n<result status=\"%s\" time=\"%.2f\"/>"
MARCHE Claude's avatar
MARCHE Claude committed
285 286 287 288 289 290 291 292 293 294 295
    (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
296
    | Undone | Scheduled | Running | Interrupted ->
MARCHE Claude's avatar
MARCHE Claude committed
297
        fprintf fmt "<undone/>@\n"
298 299
    | Unedited ->
        fprintf fmt "<unedited/>@\n"
MARCHE Claude's avatar
MARCHE Claude committed
300 301
    | InternalFailure msg ->
        fprintf fmt "<internalfailure reason=\"%s\"/>@\n"
MARCHE Claude's avatar
MARCHE Claude committed
302
          (Printexc.to_string msg)
MARCHE Claude's avatar
MARCHE Claude committed
303 304 305
    | Done r -> save_result fmt r

let save_proof_attempt fmt _key a =
François Bobot's avatar
François Bobot committed
306 307 308
  fprintf fmt
    "@\n@[<v 1><proof@ prover=\"%s\"@ timelimit=\"%d\"@ edited=\"%s\"@ \
obsolete=\"%b\">"
309
    (prover_id a.prover) a.timelimit a.edited_as a.proof_obsolete;
MARCHE Claude's avatar
MARCHE Claude committed
310
  save_status fmt a.proof_state;
MARCHE Claude's avatar
MARCHE Claude committed
311
  fprintf fmt "@]@\n</proof>"
312 313 314

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

let rec save_goal fmt g =
318
  assert (g.goal_shape <> "");
François Bobot's avatar
François Bobot committed
319 320 321
  fprintf fmt
    "@\n@[<v 1><goal@ name=\"%s\"@ %asum=\"%s\"@ proved=\"%b\"@ \
expanded=\"%b\"@ shape=\"%s\">"
MARCHE Claude's avatar
MARCHE Claude committed
322
    g.goal_name (opt "expl") g.goal_expl g.checksum g.proved  g.goal_expanded
323
    g.goal_shape;
324
  Hashtbl.iter (save_proof_attempt fmt) g.external_proofs;
MARCHE Claude's avatar
MARCHE Claude committed
325
  Hashtbl.iter (save_trans fmt) g.transformations;
MARCHE Claude's avatar
MARCHE Claude committed
326
  fprintf fmt "@]@\n</goal>"
327

MARCHE Claude's avatar
MARCHE Claude committed
328
and save_trans fmt _ t =
329
  fprintf fmt "@\n@[<v 1><transf@ name=\"%s\"@ proved=\"%b\"@ expanded=\"%b\">"
330
    t.transf.transformation_name t.transf_proved t.transf_expanded;
MARCHE Claude's avatar
MARCHE Claude committed
331
  List.iter (save_goal fmt) t.subgoals;
MARCHE Claude's avatar
MARCHE Claude committed
332
  fprintf fmt "@]@\n</transf>"
333 334

let save_theory fmt t =
François Bobot's avatar
François Bobot committed
335 336
  fprintf fmt
    "@\n@[<v 1><theory@ name=\"%s\"@ verified=\"%b\"@ expanded=\"%b\">"
337
    t.theory_name t.verified t.theory_expanded;
338
  List.iter (save_goal fmt) t.goals;
MARCHE Claude's avatar
MARCHE Claude committed
339
  fprintf fmt "@]@\n</theory>"
340 341

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

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

351 352 353 354
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
355
  fprintf fmt "<!DOCTYPE why3session SYSTEM \"why3session.dtd\">@\n";
356
  fprintf fmt "@[<v 1><why3session@ name=\"%s\">" fname;
MARCHE Claude's avatar
MARCHE Claude committed
357
  Util.Mstr.iter (fun _ d -> save_prover fmt d) (get_provers ());
358
  List.iter (save_file fmt) (get_all_files());
MARCHE Claude's avatar
MARCHE Claude committed
359 360
  fprintf fmt "@]@\n</why3session>";
  fprintf fmt "@.";
361 362 363 364 365 366
  close_out ch

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

367 368 369 370
let init_fun = ref (fun (_:O.key) (_:any) -> ())

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

371 372
let check_file_verified f =
  let b = List.for_all (fun t -> t.verified) f.theories in
373 374
  f.file_verified <- b;
  !notify_fun (File f)
375 376 377

let check_theory_proved t =
  let b = List.for_all (fun g -> g.proved) t.goals in
378 379 380
  t.verified <- b;
  !notify_fun (Theory t);
  check_file_verified t.theory_parent
381 382 383 384

let rec check_goal_proved g =
  let b1 = Hashtbl.fold
    (fun _ a acc -> acc ||
385
       not a.proof_obsolete &&
386
       match a.proof_state with
387 388
         | Done { Call_provers.pr_answer = Call_provers.Valid} -> true
         | _ -> false) g.external_proofs false
389 390 391 392
  in
  let b = Hashtbl.fold
    (fun _ t acc -> acc || t.transf_proved) g.transformations b1
  in
393 394 395 396 397
  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
398 399 400

and check_transf_proved t =
  let b = List.for_all (fun g -> g.proved) t.subgoals in
401 402 403
  t.transf_proved <- b;
  !notify_fun (Transformation t);
  check_goal_proved t.parent_goal
404 405 406 407

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

411 412
(*************************)
(*         Scheduler     *)
MARCHE Claude's avatar
MARCHE Claude committed
413
(*************************)
414 415


416
type action =
François Bobot's avatar
François Bobot committed
417 418
  | Action_proof_attempt of bool * int * int * in_channel option * string *
      Driver.driver * (proof_attempt_status -> unit) * Task.task
419 420 421 422
  | Action_delayed of (unit -> unit)

let actions_queue = Queue.create ()

423 424
(* timeout handler *)

425 426 427 428
type timeout_action =
  | Check_prover of (proof_attempt_status -> unit) * Call_provers.prover_call
  | Any_timeout of (unit -> bool)

429 430 431 432 433 434 435 436 437 438 439 440
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
441 442 443 444
    (fun acc c ->
       match c with
         | Check_prover(callback,call)  ->
             (match Call_provers.query_call call with
445 446 447 448
               | None -> c::acc
               | Some post ->
                   let res = post () in callback (Done res);
                   acc)
449 450 451
         | Any_timeout callback ->
             let b = callback () in
             if b then c::acc else acc)
452 453 454 455 456
    [] !running_proofs
  in
  let l =
    if List.length l < !maximum_running_proofs then
      begin try
457 458 459 460
        let (callback,pre_call) = Queue.pop proof_attempts_queue in
        callback Running;
        let call = pre_call () in
        (Check_prover(callback,call))::l
461 462 463 464 465 466 467 468
      with Queue.Empty -> l
      end
    else l
  in
  running_proofs := l;
  let continue =
    match l with
      | [] ->
469
(*
470
          eprintf "Info: timeout_handler stopped@.";
471
*)
472 473 474
          false
      | _ -> true
  in
475 476 477
  O.notify_timer_state
    (Queue.length actions_queue)
    (Queue.length proof_attempts_queue) (List.length l);
478 479 480 481 482 483 484 485
  timeout_handler_activated := continue;
  timeout_handler_running := false;
  continue

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

492 493 494 495
let schedule_any_timeout callback =
  running_proofs := (Any_timeout callback) :: ! running_proofs;
  run_timeout_handler ()

496 497 498 499 500 501 502 503 504
(* idle handler *)


let idle_handler_activated = ref false

let idle_handler () =
  try
    begin
      match Queue.pop actions_queue with
505 506 507 508 509 510
        | 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;
MARCHE Claude's avatar
MARCHE Claude committed
511 512 513
            begin
              try
                let pre_call =
François Bobot's avatar
François Bobot committed
514 515
                  Driver.prove_task
                    ?old ~command ~timelimit ~memlimit driver goal
MARCHE Claude's avatar
MARCHE Claude committed
516 517 518 519
                in
                Queue.push (callback,pre_call) proof_attempts_queue;
                run_timeout_handler ()
              with e ->
François Bobot's avatar
François Bobot committed
520 521
                Format.eprintf "@[Exception raise in Session.idle_handler:@ \
%a@.@]"
MARCHE Claude's avatar
MARCHE Claude committed
522 523 524
                  Exn_printer.exn_printer e;
                callback (InternalFailure e)
            end
525 526 527 528 529
        | Action_delayed callback -> callback ()
    end;
    true
  with Queue.Empty ->
    idle_handler_activated := false;
530
(*
531
    eprintf "Info: idle_handler stopped@.";
532
*)
533
    false
MARCHE Claude's avatar
MARCHE Claude committed
534 535 536 537 538
    | e ->
      Format.eprintf "@[Exception raise in Session.idle_handler:@ %a@.@]"
        Exn_printer.exn_printer e;
      eprintf "Session.idle_handler stopped@.";
      false
539

540 541 542 543 544

let run_idle_handler () =
  if !idle_handler_activated then () else
    begin
      idle_handler_activated := true;
545
(*
546
      eprintf "Info: idle_handler started@.";
547
*)
548 549 550 551 552
      O.idle idle_handler
    end

(* main scheduling functions *)

553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571
let cancel_scheduled_proofs () =
  let new_queue = Queue.create () in
  try
    while true do
      match Queue.pop actions_queue with
        | Action_proof_attempt(_debug,_timelimit,_memlimit,_old,_command,
                               _driver,callback,_goal) ->
            callback Interrupted
        | Action_delayed _ as a->
            Queue.push a new_queue
    done
  with Queue.Empty ->
    Queue.transfer new_queue actions_queue;
    try
      while true do
        let (callback,_) = Queue.pop proof_attempts_queue in
        callback Interrupted
      done
    with
572
      | Queue.Empty ->
573
          O.notify_timer_state 0 0 (List.length !running_proofs)
574 575


576 577
let schedule_proof_attempt ~debug ~timelimit ~memlimit ?old
    ~command ~driver ~callback goal =
578 579 580
  (*
    eprintf "Scheduling a new proof attempt@.";
  *)
581 582
  Queue.push
    (Action_proof_attempt(debug,timelimit,memlimit,old,command,driver,
583
                        callback,goal))
584 585 586
    actions_queue;
  run_idle_handler ()

587
let schedule_edition command filename callback =
588
  let precall =
589 590
    Call_provers.call_on_file ~command ~regexps:[] ~timeregexps:[]
      ~exitcodes:[(0,Call_provers.Unknown "")] filename
591 592
  in
  callback Running;
593
  running_proofs := (Check_prover(callback, precall ())) :: !running_proofs;
594 595 596 597 598 599
  run_timeout_handler ()

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

600 601 602
let apply_transformation ~callback t task =
   match t.transformation with
    | Trans_one t ->
603
        callback [Trans.apply t task]
604
    | Trans_list t ->
605
        callback (Trans.apply t task)
606

607
let schedule_edit_proof ~debug:_ ~editor ~file ~driver ~callback goal =
608 609 610 611
  let old =
    if Sys.file_exists file
    then
      begin
612
        let backup = file ^ ".bak" in
613 614
        if Sys.file_exists backup
          then Sys.remove backup;
615 616 617 618 619 620 621 622 623 624
        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;
625
  schedule_edition editor file callback
626

627 628

(*******************************)
629 630
(*          explanations       *)
(*******************************)
631 632 633

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

634 635 636 637 638 639 640
  exception Found of string

  let check_expl lab =
    if Str.string_match expl_regexp lab 0 then
      raise (Found (Str.matched_group 1 lab))

  let rec get_expl_fmla f =
641
    List.iter check_expl (List.rev f.Term.t_label);
642
    (match f.Term.t_node with
643
      | Term.Tbinop(Term.Timplies,_,f) -> get_expl_fmla f
644
      | Term.Tquant(Term.Tforall,fq) ->
645
          let (_,_,f) = Term.t_open_quant fq in get_expl_fmla f
646
      | Term.Tlet(_,fb) ->
647
          let (_,f) = Term.t_open_bound fb in get_expl_fmla f
648
      | Term.Tcase(_,[fb]) ->
649 650
          let (_,f) = Term.t_open_branch fb in get_expl_fmla f
      | _ -> ())
651 652

  let get_explanation id fmla =
653 654
    try
      get_expl_fmla fmla;
655
      List.iter check_expl (List.rev id.Ident.id_label);
656 657
      None
    with Found e -> Some e
658 659


660 661 662 663
(**********************)
(*     check sum      *)
(**********************)

664
(*
665
let task_checksum t =
666 667
  (* TODO: ignore print_locs and print_labels flag *)
  (* even better: compute check_sum directly, similar to the shape *)
668 669 670 671 672 673 674 675 676 677 678 679 680
  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
681
*)
682 683


684 685 686 687 688

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

689
let raw_add_external_proof ~obsolete ~timelimit ~edit (g:goal) p result =
690
  let key = O.create ~parent:g.goal_key () in
691
  let a = { prover = p;
692 693 694
            proof_goal = g;
            proof_key = key;
            proof_obsolete = obsolete;
695 696
            proof_state = result;
            timelimit = timelimit;
697 698 699
            edited_as = edit;
          }
  in
700
  Hashtbl.add g.external_proofs (prover_id p) a;
701 702 703
  let any = Proof_attempt a in
  !init_fun key any;
  !notify_fun any;
704 705
  a

706

MARCHE Claude's avatar
MARCHE Claude committed
707
(* [raw_add_goal parent name expl sum t] adds a goal to the given parent
708 709
   DOES NOT record the new goal in its parent, thus this should not be exported
*)
710
let raw_add_goal parent name expl sum shape topt exp =
711
  let parent_key = match parent with
712 713
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
714 715
  in
  let key = O.create ~parent:parent_key () in
716 717
  let sum,shape = match topt with
    | None -> sum,shape
718
    | Some t -> (Termcode.task_checksum t,
719
                 Termcode.t_shape_buf (Task.task_goal_fmla t))
720
  in
721 722
  let goal = { goal_name = name;
               goal_expl = expl;
723
               parent = parent;
724
               task = topt ;
725
               checksum = sum;
726
               goal_shape = shape;
727 728 729 730
               goal_key = key;
               external_proofs = Hashtbl.create 7;
               transformations = Hashtbl.create 3;
               proved = false;
731
               goal_expanded = exp;
732 733
             }
  in
734 735
  let any = Goal goal in
  !init_fun key any;
736
  !notify_fun any; (*useless ? *)
737 738 739 740 741 742
  goal


(* [raw_add_transformation g name adds a transformation to the given goal g
   Adds no subgoals, thus this should not be exported
*)
743
let raw_add_transformation g trans exp =
744 745
  let parent = g.goal_key in
  let key = O.create ~parent () in
746
  let tr = { transf = trans;
747
             parent_goal = g;
748 749 750
             transf_proved = false;
             transf_key = key;
             subgoals = [];
751
             transf_expanded = exp;
752 753
           }
  in
754 755 756 757
  Hashtbl.add g.transformations trans.transformation_name tr;
  let any = Transformation tr in
  !init_fun key any;
  !notify_fun any;
758 759
  tr

760
let raw_add_theory mfile thopt thname exp =
761 762
  let parent = mfile.file_key in
  let key = O.create ~parent () in
763
  let mth = { theory_name = thname;
764
              theory = thopt;
765 766 767
              theory_key = key;
              theory_parent = mfile;
              goals = [] ;
768
              verified = false;
769 770
              theory_expanded = exp;
            }
771
  in
772 773 774
  let any = Theory mth in
  !init_fun key any;
  !notify_fun any;
775 776 777 778
  mth



779
let add_theory mfile name th =
780
  let tasks = List.rev (Task.split_theory th None None) in
781
  let mth = raw_add_theory mfile (Some th) name true in
782 783 784 785 786 787
  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
François Bobot's avatar
François Bobot committed
788 789 790
         let goal = raw_add_goal
           (Parent_theory mth) name expl "" "" (Some t)
true in
791 792 793 794 795
         goal :: acc)
      []
      tasks
  in
  mth.goals <- List.rev goals;
MARCHE Claude's avatar
MARCHE Claude committed
796
  check_theory_proved mth;
797 798
  mth

799
let raw_add_file f exp =
800
  let key = O.create () in
801
  let mfile = { file_name = f;
802
                file_key = key;
803
                theories = [] ;
804
                file_verified = false;
805 806
                file_expanded = exp;
              }
807 808
  in
  all_files := !all_files @ [mfile];
809 810 811
  let any = File mfile in
  !init_fun key any;
  !notify_fun any;
812 813
  mfile

814

MARCHE Claude's avatar
MARCHE Claude committed
815 816
let read_file fn =
  let fn = Filename.concat !project_dir fn in
MARCHE Claude's avatar
MARCHE Claude committed
817 818
  let env = match !current_env with
    | None -> assert false | Some e -> e
MARCHE Claude's avatar
MARCHE Claude committed
819 820
  in
  let theories = Env.read_file env fn in
821
  let theories =
822
    Util.Mstr.fold
823
      (fun name th acc ->
824 825 826
         match th.Theory.th_name.Ident.id_loc with
           | Some l -> (l,name,th)::acc
           | None   -> (Loc.dummy_position,name,th)::acc)
827 828
      theories []
  in
MARCHE Claude's avatar
MARCHE Claude committed
829
  List.sort
830 831
    (fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
    theories
MARCHE Claude's avatar
MARCHE Claude committed
832 833 834

let add_file f =
  let theories = read_file f in
835
  let mfile = raw_add_file f true in
836 837
  let mths =
    List.fold_left
838 839
      (fun acc (_,name,t) ->
         let mth = add_theory mfile name t in
840 841 842 843
         mth :: acc)
      [] theories
  in
  mfile.theories <- List.rev mths;
844 845 846
  check_file_verified mfile;
  !notify_fun (File mfile)

847 848


849 850 851
let file_exists fn =
  List.exists (fun f -> f.file_name = fn) !all_files

852 853


854 855


856 857 858 859 860 861 862 863 864 865 866 867 868
(*************************************************************)
(* pairing of new and old subgoals of a given transformation *)
(*************************************************************)

(* we have an ordered list of new subgoals

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

   and a list of old subgoals

          old_subgoals = [h1 ; h2 ; ... ]

   we build a map from each new subgoal g to tuples
869
       (id,subgoal_name,subtask,sum,old_subgoal,obsolete)
870 871 872 873 874 875 876

   where
     id = name of the goal of g
     subgoal_name = name of parent goal with "dot n" added
     subtask = the corresponding task
     sum = the checksum of that task
     old_subgoal = ref to an optional old subgoal which is paired with g
877
     obsolete = true when paired to an old goal with different checksum
878 879 880 881 882

*)


type any_goal =
883
  | New_goal of int
884 885
  | Old_goal of goal

886 887 888 889 890 891 892 893 894 895 896
let array_map_list f l =
  let r = ref l in
  Array.init (List.length l)
    (fun i ->
       match !r with
         | [] -> assert false
         | x::rem -> r := rem; f i x)

let associate_subgoals gname old_goals new_goals =
  (*
     we make a map of old goals indexed by their checksums
897
  *)
898 899 900 901
  let old_goals_map = Hashtbl.create 7 in
  List.iter
    (fun g -> Hashtbl.add old_goals_map g.checksum g)
    old_goals;
902
  (*
903
     we make an array of new goals with their numbers and checksums
904 905 906 907 908 909
  *)
  let new_goals_array =
    array_map_list
      (fun i g ->
         let id = (Task.task_goal g).Decl.pr_name in
         let goal_name = gname ^ "." ^ (string_of_int (i+1)) in
910
         let sum = Termcode.task_checksum g in
911 912
         (i,id,goal_name,g,sum))
      new_goals
913
  in
914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929
  let pairing_array =
    Array.make (Array.length new_goals_array) None
  in
  let shape_array =
    Array.make (Array.length new_goals_array) ""
  in
  let obsolete_array =
    Array.make (Array.length new_goals_array) false
  in
  (*
     Phase 1: we first associate each new goal for which there is an
     old goal with the same checksum.
  *)
  let associate_goals ~obsolete i g =
    pairing_array.(i) <- Some g;
    obsolete_array.(i) <- obsolete;
930
    Hashtbl.remove old_goals_map g.checksum
931 932 933 934
  in
  Array.iter
    (fun (i,_,_goal_name,_,sum) ->
       try
935
         let h = Hashtbl.find old_goals_map sum in
936 937 938 939 940 941 942 943 944 945 946 947 948 949 950
         (* an old goal has the same checksum *)
         (*
           eprintf "Merge phase 1: old goal '%s' -> new goal '%s'@."
           h.goal_name goal_name;
         *)
         shape_array.(i) <- h.goal_shape;
         associate_goals ~obsolete:false i h
       with Not_found ->
         (*
           eprintf "Merge phase 1: no old goal -> new goal '%s'@."
           subgoal_name;
         *)
         ())
    new_goals_array;
  (* Phase 2: we now build a list of all remaining new and old goals,
951
     ordered by shapes, then by name *)
952
  let old_goals_without_pairing =