session.ml 60 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
type proof_attempt_status =
  | Undone
  | Scheduled (** external proof attempt is scheduled *)
99
  | Interrupted
100 101 102
  | 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 *)
103 104


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

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

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

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

120 121 122 123
end

module Make(O : OBSERVER) = struct

124 125 126 127
(***************************)
(*     session state       *)
(***************************)

128 129 130 131 132 133 134 135
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

136
type proof_attempt =
137
    { prover : prover_option;
138 139 140
      proof_goal : goal;
      proof_key : O.key;
      mutable proof_state : proof_attempt_status;
141
      mutable timelimit : int;
142 143 144 145 146
      mutable proof_obsolete : bool;
      mutable edited_as : string;
    }

and goal_parent =
147 148
  | Parent_theory of theory
  | Parent_transf of transf
149 150 151 152 153

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

and transf =
165 166
    { transf : transformation_data;
      parent_goal : goal;
167 168 169
      mutable transf_proved : bool;
      transf_key : O.key;
      mutable subgoals : goal list;
170
      mutable transf_expanded : bool;
171 172 173
    }

and theory =
174
    { theory_name : string;
MARCHE Claude's avatar
MARCHE Claude committed
175
      mutable theory : Theory.theory option;
176 177 178 179
      theory_key : O.key;
      theory_parent : file;
      mutable goals : goal list;
      mutable verified : bool;
180
      mutable theory_expanded : bool;
181 182 183 184 185 186 187
    }

and file =
    { file_name : string;
      file_key : O.key;
      mutable theories: theory list;
      mutable file_verified : bool;
188
      mutable file_expanded : bool;
189 190
    }

191 192 193 194 195 196 197
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
198 199 200 201
let theory_name t = t.theory_name
let theory_key t = t.theory_key
let verified t = t.verified
let goals t = t.goals
202 203
let theory_expanded t = t.theory_expanded

MARCHE Claude's avatar
MARCHE Claude committed
204

MARCHE Claude's avatar
MARCHE Claude committed
205 206 207
let get_theory t =
  match t.theory with
    | None ->
208 209
        eprintf "Session: theory not yet reimported, this should not happen@.";
        assert false
210 211
    | Some t -> t

MARCHE Claude's avatar
MARCHE Claude committed
212
let goal_name g = g.goal_name
MARCHE Claude's avatar
MARCHE Claude committed
213 214
let goal_expl g =
  match g.goal_expl with
MARCHE Claude's avatar
MARCHE Claude committed
215 216 217 218 219
    | 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
220 221
let external_proofs g = g.external_proofs
let goal_expanded g = g.goal_expanded
MARCHE Claude's avatar
MARCHE Claude committed
222

MARCHE Claude's avatar
MARCHE Claude committed
223 224 225
let get_task g =
  match g.task with
    | None ->
226 227 228 229 230 231 232 233
        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
234 235
    | Some t -> t

236

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

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

247
let set_theory_expanded t b =
248 249 250 251 252 253 254 255
  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
256

257 258
let all_files : file list ref = ref []

259
let get_all_files () = !all_files
MARCHE Claude's avatar
MARCHE Claude committed
260

MARCHE Claude's avatar
MARCHE Claude committed
261 262 263 264 265 266
let current_env = ref None
let current_provers = ref Util.Mstr.empty
let project_dir = ref ""

let get_provers () = !current_provers

267 268 269 270
(************************)
(* saving state on disk *)
(************************)

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

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

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

let rec save_goal fmt g =
302
  assert (g.goal_shape <> "");
303
  fprintf fmt "@\n@[<v 1><goal@ name=\"%s\"@ %asum=\"%s\"@ proved=\"%b\"@ expanded=\"%b\"@ shape=\"%s\">"
MARCHE Claude's avatar
MARCHE Claude committed
304
    g.goal_name (opt "expl") g.goal_expl g.checksum g.proved  g.goal_expanded
305
    g.goal_shape;
306
  Hashtbl.iter (save_proof_attempt fmt) g.external_proofs;
MARCHE Claude's avatar
MARCHE Claude committed
307
  Hashtbl.iter (save_trans fmt) g.transformations;
MARCHE Claude's avatar
MARCHE Claude committed
308
  fprintf fmt "@]@\n</goal>"
309

MARCHE Claude's avatar
MARCHE Claude committed
310
and save_trans fmt _ t =
311
  fprintf fmt "@\n@[<v 1><transf@ name=\"%s\"@ proved=\"%b\"@ expanded=\"%b\">"
312
    t.transf.transformation_name t.transf_proved t.transf_expanded;
MARCHE Claude's avatar
MARCHE Claude committed
313
  List.iter (save_goal fmt) t.subgoals;
MARCHE Claude's avatar
MARCHE Claude committed
314
  fprintf fmt "@]@\n</transf>"
315 316

let save_theory fmt t =
317
  fprintf fmt "@\n@[<v 1><theory@ name=\"%s\"@ verified=\"%b\"@ expanded=\"%b\">"
318
    t.theory_name t.verified t.theory_expanded;
319
  List.iter (save_goal fmt) t.goals;
MARCHE Claude's avatar
MARCHE Claude committed
320
  fprintf fmt "@]@\n</theory>"
321 322

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

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

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

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

348 349 350 351
let init_fun = ref (fun (_:O.key) (_:any) -> ())

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

352 353
let check_file_verified f =
  let b = List.for_all (fun t -> t.verified) f.theories in
354 355
  f.file_verified <- b;
  !notify_fun (File f)
356 357 358

let check_theory_proved t =
  let b = List.for_all (fun g -> g.proved) t.goals in
359 360 361
  t.verified <- b;
  !notify_fun (Theory t);
  check_file_verified t.theory_parent
362 363 364 365

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

and check_transf_proved t =
  let b = List.for_all (fun g -> g.proved) t.subgoals in
382 383 384
  t.transf_proved <- b;
  !notify_fun (Transformation t);
  check_goal_proved t.parent_goal
385 386 387 388

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

392 393
(*************************)
(*         Scheduler     *)
MARCHE Claude's avatar
MARCHE Claude committed
394
(*************************)
395 396


397 398 399 400 401 402 403
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 ()

404 405
(* timeout handler *)

406 407 408 409
type timeout_action =
  | Check_prover of (proof_attempt_status -> unit) * Call_provers.prover_call
  | Any_timeout of (unit -> bool)

410 411 412 413 414 415 416 417 418 419 420 421
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
422 423 424 425
    (fun acc c ->
       match c with
         | Check_prover(callback,call)  ->
             (match Call_provers.query_call call with
426 427 428 429
               | None -> c::acc
               | Some post ->
                   let res = post () in callback (Done res);
                   acc)
430 431 432
         | Any_timeout callback ->
             let b = callback () in
             if b then c::acc else acc)
433 434 435 436 437
    [] !running_proofs
  in
  let l =
    if List.length l < !maximum_running_proofs then
      begin try
438 439 440 441
        let (callback,pre_call) = Queue.pop proof_attempts_queue in
        callback Running;
        let call = pre_call () in
        (Check_prover(callback,call))::l
442 443 444 445 446 447 448 449
      with Queue.Empty -> l
      end
    else l
  in
  running_proofs := l;
  let continue =
    match l with
      | [] ->
450
(**)
451
          eprintf "Info: timeout_handler stopped@.";
452
(**)
453 454 455
          false
      | _ -> true
  in
456 457 458
  O.notify_timer_state
    (Queue.length actions_queue)
    (Queue.length proof_attempts_queue) (List.length l);
459 460 461 462 463 464 465 466
  timeout_handler_activated := continue;
  timeout_handler_running := false;
  continue

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

473 474 475 476
let schedule_any_timeout callback =
  running_proofs := (Any_timeout callback) :: ! running_proofs;
  run_timeout_handler ()

477 478 479 480 481 482 483 484 485
(* idle handler *)


let idle_handler_activated = ref false

let idle_handler () =
  try
    begin
      match Queue.pop actions_queue with
486 487 488 489 490 491
        | 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
492 493 494 495 496 497 498 499 500 501 502 503
            begin
              try
                let pre_call =
                  Driver.prove_task ?old ~command ~timelimit ~memlimit driver goal
                in
                Queue.push (callback,pre_call) proof_attempts_queue;
                run_timeout_handler ()
              with e ->
                Format.eprintf "@[Exception raise in Session.idle_handler:@ %a@.@]"
                  Exn_printer.exn_printer e;
                callback (InternalFailure e)
            end
504 505 506 507 508
        | Action_delayed callback -> callback ()
    end;
    true
  with Queue.Empty ->
    idle_handler_activated := false;
509
(**)
510
    eprintf "Info: idle_handler stopped@.";
511
(**)
512
    false
MARCHE Claude's avatar
MARCHE Claude committed
513 514 515 516 517
    | e ->
      Format.eprintf "@[Exception raise in Session.idle_handler:@ %a@.@]"
        Exn_printer.exn_printer e;
      eprintf "Session.idle_handler stopped@.";
      false
518

519 520 521 522 523

let run_idle_handler () =
  if !idle_handler_activated then () else
    begin
      idle_handler_activated := true;
524
(**)
525
      eprintf "Info: idle_handler started@.";
526
(**)
527 528 529 530 531
      O.idle idle_handler
    end

(* main scheduling functions *)

532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553
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
      | Queue.Empty -> ()


554 555
let schedule_proof_attempt ~debug ~timelimit ~memlimit ?old
    ~command ~driver ~callback goal =
556 557 558
(**)
  eprintf "Scheduling a new proof attempt@.";
(**)
559 560
  Queue.push
    (Action_proof_attempt(debug,timelimit,memlimit,old,command,driver,
561
                        callback,goal))
562 563 564 565 566 567 568 569 570
    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;
571
  running_proofs := (Check_prover(callback, precall ())) :: !running_proofs;
572 573 574 575 576 577
  run_timeout_handler ()

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

578 579 580
let apply_transformation ~callback t task =
   match t.transformation with
    | Trans_one t ->
581
        callback [Trans.apply t task]
582
    | Trans_list t ->
583
        callback (Trans.apply t task)
584

585
let schedule_edit_proof ~debug:_ ~editor ~file ~driver ~callback goal =
586 587 588 589
  let old =
    if Sys.file_exists file
    then
      begin
590
        let backup = file ^ ".bak" in
591 592 593 594 595 596 597 598 599 600
        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;
601
  let command = editor ^ " \"" ^ file ^ "\"" in
602 603
  schedule_edition command callback

604 605

(*******************************)
606 607
(*          explanations       *)
(*******************************)
608 609 610

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

611 612 613 614 615 616 617
  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 =
618
    List.iter check_expl (List.rev f.Term.t_label);
619
    (match f.Term.t_node with
620
      | Term.Tbinop(Term.Timplies,_,f) -> get_expl_fmla f
621
      | Term.Tquant(Term.Tforall,fq) ->
622
          let (_,_,f) = Term.t_open_quant fq in get_expl_fmla f
623
      | Term.Tlet(_,fb) ->
624
          let (_,f) = Term.t_open_bound fb in get_expl_fmla f
625
      | Term.Tcase(_,[fb]) ->
626 627
          let (_,f) = Term.t_open_branch fb in get_expl_fmla f
      | _ -> ())
628 629

  let get_explanation id fmla =
630 631
    try
      get_expl_fmla fmla;
632
      List.iter check_expl (List.rev id.Ident.id_label);
633 634
      None
    with Found e -> Some e
635 636


637 638 639 640
(**********************)
(*     check sum      *)
(**********************)

641
(*
642
let task_checksum t =
643 644
  (* TODO: ignore print_locs and print_labels flag *)
  (* even better: compute check_sum directly, similar to the shape *)
645 646 647 648 649 650 651 652 653 654 655 656 657
  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
658
*)
659 660


661 662 663 664 665

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

666
let raw_add_external_proof ~obsolete ~timelimit ~edit (g:goal) p result =
667
  let key = O.create ~parent:g.goal_key () in
668
  let a = { prover = p;
669 670 671
            proof_goal = g;
            proof_key = key;
            proof_obsolete = obsolete;
672 673
            proof_state = result;
            timelimit = timelimit;
674 675 676
            edited_as = edit;
          }
  in
677
  Hashtbl.add g.external_proofs (prover_id p) a;
678 679 680
  let any = Proof_attempt a in
  !init_fun key any;
  !notify_fun any;
681 682
  a

683

MARCHE Claude's avatar
MARCHE Claude committed
684
(* [raw_add_goal parent name expl sum t] adds a goal to the given parent
685 686
   DOES NOT record the new goal in its parent, thus this should not be exported
*)
687
let raw_add_goal parent name expl sum shape topt exp =
688
  let parent_key = match parent with
689 690
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
691 692
  in
  let key = O.create ~parent:parent_key () in
693 694
  let sum,shape = match topt with
    | None -> sum,shape
695
    | Some t -> (Termcode.task_checksum t,
696
                 Termcode.t_shape_buf (Task.task_goal_fmla t))
697
  in
698 699
  let goal = { goal_name = name;
               goal_expl = expl;
700
               parent = parent;
701
               task = topt ;
702
               checksum = sum;
703
               goal_shape = shape;
704 705 706 707
               goal_key = key;
               external_proofs = Hashtbl.create 7;
               transformations = Hashtbl.create 3;
               proved = false;
708
               goal_expanded = exp;
709 710
             }
  in
711 712
  let any = Goal goal in
  !init_fun key any;
713
  !notify_fun any; (*useless ? *)
714 715 716 717 718 719
  goal


(* [raw_add_transformation g name adds a transformation to the given goal g
   Adds no subgoals, thus this should not be exported
*)
720
let raw_add_transformation g trans exp =
721 722
  let parent = g.goal_key in
  let key = O.create ~parent () in
723
  let tr = { transf = trans;
724
             parent_goal = g;
725 726 727
             transf_proved = false;
             transf_key = key;
             subgoals = [];
728
             transf_expanded = exp;
729 730
           }
  in
731 732 733 734
  Hashtbl.add g.transformations trans.transformation_name tr;
  let any = Transformation tr in
  !init_fun key any;
  !notify_fun any;
735 736
  tr

737
let raw_add_theory mfile thopt thname exp =
738 739
  let parent = mfile.file_key in
  let key = O.create ~parent () in
740
  let mth = { theory_name = thname;
741
              theory = thopt;
742 743 744
              theory_key = key;
              theory_parent = mfile;
              goals = [] ;
745
              verified = false;
746 747
              theory_expanded = exp;
            }
748
  in
749 750 751
  let any = Theory mth in
  !init_fun key any;
  !notify_fun any;
752 753 754 755
  mth



756
let add_theory mfile name th =
757
  let tasks = List.rev (Task.split_theory th None None) in
758
  let mth = raw_add_theory mfile (Some th) name true in
759 760 761 762 763 764
  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
765
         let goal = raw_add_goal (Parent_theory mth) name expl "" "" (Some t) true in
766 767 768 769 770
         goal :: acc)
      []
      tasks
  in
  mth.goals <- List.rev goals;
MARCHE Claude's avatar
MARCHE Claude committed
771
  check_theory_proved mth;
772 773
  mth

774
let raw_add_file f exp =
775
  let key = O.create () in
776
  let mfile = { file_name = f;
777
                file_key = key;
778
                theories = [] ;
779
                file_verified = false;
780 781
                file_expanded = exp;
              }
782 783
  in
  all_files := !all_files @ [mfile];
784 785 786
  let any = File mfile in
  !init_fun key any;
  !notify_fun any;
787 788
  mfile

789

MARCHE Claude's avatar
MARCHE Claude committed
790 791
let read_file fn =
  let fn = Filename.concat !project_dir fn in
MARCHE Claude's avatar
MARCHE Claude committed
792 793
  let env = match !current_env with
    | None -> assert false | Some e -> e
MARCHE Claude's avatar
MARCHE Claude committed
794 795
  in
  let theories = Env.read_file env fn in
796
  let theories =
797
    Util.Mstr.fold
798
      (fun name th acc ->
799 800 801
         match th.Theory.th_name.Ident.id_loc with
           | Some l -> (l,name,th)::acc
           | None   -> (Loc.dummy_position,name,th)::acc)
802 803
      theories []
  in
MARCHE Claude's avatar
MARCHE Claude committed
804
  List.sort
805 806
    (fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
    theories
MARCHE Claude's avatar
MARCHE Claude committed
807 808 809

let add_file f =
  let theories = read_file f in
810
  let mfile = raw_add_file f true in
811 812
  let mths =
    List.fold_left
813 814
      (fun acc (_,name,t) ->
         let mth = add_theory mfile name t in
815 816 817 818
         mth :: acc)
      [] theories
  in
  mfile.theories <- List.rev mths;
819 820 821
  check_file_verified mfile;
  !notify_fun (File mfile)

822 823


824 825 826
let file_exists fn =
  List.exists (fun f -> f.file_name = fn) !all_files

827 828


829 830


831 832 833 834 835 836 837 838 839 840 841 842 843
(*************************************************************)
(* 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
844
       (id,subgoal_name,subtask,sum,old_subgoal,obsolete)
845 846 847 848 849 850 851

   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
852
     obsolete = true when paired to an old goal with different checksum
853 854 855 856 857

*)


type any_goal =
858
  | New_goal of int
859 860
  | Old_goal of goal

861 862 863 864 865 866 867 868 869 870 871
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
872
  *)
873 874 875 876
  let old_goals_map = Hashtbl.create 7 in
  List.iter
    (fun g -> Hashtbl.add old_goals_map g.checksum g)
    old_goals;
877 878 879 880 881 882 883 884
  (*
     we make an array of new goals with their numbers and checksums 
  *)
  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
885
         let sum = Termcode.task_checksum g in
886 887
         (i,id,goal_name,g,sum))
      new_goals
888
  in
889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904
  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;
905
    Hashtbl.remove old_goals_map g.checksum
906 907 908 909
  in
  Array.iter
    (fun (i,_,_goal_name,_,sum) ->
       try
910
         let h = Hashtbl.find old_goals_map sum in
911 912 913 914 915 916 917 918 919 920 921 922 923 924 925
         (* 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,
926
     ordered by shapes, then by name *)
927
  let old_goals_without_pairing =
928
    Hashtbl.fold
929 930 931 932 933 934 935 936
      (fun _ g acc ->
         let s = g.goal_shape in
         if s = "" then
           (* We don't try to associate old goals without shapes:
              they will be paired in order in next phase *)
           acc
         else
           (s,Old_goal g)::acc)
937
      old_goals_map
938 939
      []
  in
940 941 942 943 944 945 946 947 948 949 950 951 952
  let all_goals_without_pairing =
    Array.fold_left
      (fun acc (i,_,_, g, _) ->
         match pairing_array.(i) with
           | Some _ -> acc
           | None ->
               let shape = 
                 Termcode.t_shape_buf (Task.task_goal_fmla g)
               in
               shape_array.(i) <- shape;
               (shape,New_goal i)::acc)
      old_goals_without_pairing
      new_goals_array
953
  in
954 955 956 957
  let sort_by_shape =
    List.sort (fun (s1,_) (s2,_) -> String.compare s1 s2) 
      all_goals_without_pairing
  in
958
(*
959 960 961 962 963 964 965 966 967
  eprintf "[Merge] pairing the following shapes:@.";
  List.iter
    (fun (s,g) ->
       match g with
         | New_goal _ ->
             eprintf "new: %s@." s
         | Old_goal _ ->
             eprintf "old: %s@." s)
    sort_by_shape;
968
*)
969 970 971 972 973
  let rec similarity_shape n s1 s2 =
    if String.length s1 <= n || String.length s2 <= n then n else
      if s1.[n] = s2.[n] then similarity_shape (n+1) s1 s2
      else n
  in
974
(*  let rec match_shape (opt:int option) goals : bool =
975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032
    (* when [opt] is [Some n] then it means [goals] starts with a goal g
       which is already claimed to be associated by the former goal h.
       We return a boolean which is true when that first goal g was also
       claimed by the next goal, with a proximity measure larger than n,
       meaning that the former goal h cannot associate with g
    *)
    match goals with
      | [] -> false
      | (si,New_goal i)::rem ->
          begin match rem with
            | [] -> false
            | (_,New_goal _)::_ ->
                let (_:bool) = match_shape None rem in false
            | (sh,Old_goal h)::_ ->
                try_associate si i sh h opt rem
          end
      | (sh,Old_goal h)::rem ->
          begin match rem with
            | [] -> false
            | (_,Old_goal _)::_ ->
                let (_:bool) = match_shape None rem in false
            | (si,New_goal i)::_ ->
                try_associate si i sh h opt rem
          end
  and try_associate si i sh h opt rem =
    let n = similarity_shape 0 si sh in
    eprintf "[Merge] try_associate: claiming similarity %d for new shape@\n%s@\nand old shape@\n%s@." n si sh;
    if (match opt with
      | None ->
          eprintf "[Merge] try_associate: no previous claim@.";
          true
      | Some m ->
          eprintf "[Merge] try_associate: previous claim was %d@." m;
          m < n)
    then
      (* try to associate i with h *)
      let b = match_shape (Some n) rem in
      if b then
        begin
          (* h or i was already paired in rem *)
          eprintf "[Merge] try_associate: failed because claimed further@.";
          false
        end
      else
        begin
          eprintf "[Merge] try_associate: succeeded to associate new goal@\n%s@\nwith old goal@\n%s@." si sh;
          associate_goals ~obsolete:true i h;
          true
        end
    else
      (* no need to try to associate i with h *)
      begin
        eprintf "[Merge] try_associate: no claim further attempted@.";
        let (_:bool) = match_shape None rem in
        false
      end
  in
  let (_:bool) = match_shape None sort_by_shape in
1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096
*)
  let rec match_shape (min:int) goals : bool * (string * any_goal) list =
    (* try to associate in [goals] each pair of old and new goal whose
       similarity is at least [min]. Returns a pair [(b,rem)] where
       [rem] is the sublist of [goals] made of goals which have not
       been paired, and [b] is a boolean telling that the head of
       [rem] is the same has the head of [goals] *)
    match goals with
      | [] -> (true, goals)
      | ((si,New_goal i) as hd)::rem ->
          begin match rem with
            | [] -> (true, goals)
            | (_,New_goal _)::_ ->
                let (b,rem2) = match_shape min rem in
                if b then
                  (true, hd::rem2)
                else
                  match_shape min (hd::rem2)
            | (sh,Old_goal h)::_ ->
                try_associate min si i sh h hd rem
          end
      | ((sh,Old_goal h) as hd)::rem ->
          begin match rem with
            | [] -> (true, goals)
            | (_,Old_goal _)::_ ->
                let (b,rem2) = match_shape min rem in
                if b then
                  (true, hd::rem2)
                else
                  match_shape min (hd::rem2)
            | (si,New_goal i)::_ ->
                try_associate min si i sh h hd rem
          end
  and try_associate min si i sh h hd rem =
    let n = similarity_shape 0 si sh in
(*
    eprintf "[Merge] try_associate: claiming similarity %d for new shape@\n%s@\nand old shape@\n%s@." n si sh;
*)
    if n < min then
      begin
(*
        eprintf "[Merge] try_associate: claiming dropped because similarity lower than min = %d@." min;
*)
        let (b,rem2) = match_shape min rem in