session.ml 87 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
François Bobot's avatar
François Bobot committed
11

12
open Stdlib
13 14 15 16 17 18
open Ty
open Ident
open Decl
open Term
open Theory
open Task
François Bobot's avatar
François Bobot committed
19

20 21 22 23
module Mprover = Whyconf.Mprover
module Sprover = Whyconf.Sprover
module PHprover = Whyconf.Hprover
module C = Whyconf
24
module Tc = Termcode
25

26
let debug = Debug.register_info_flag "session"
Andrei Paskevich's avatar
Andrei Paskevich committed
27 28
  ~desc:"Pring@ debugging@ messages@ about@ Why3@ session@ \
         creation,@ reading@ and@ writing."
François Bobot's avatar
François Bobot committed
29 30 31

(** {2 Type definitions} *)

32
module PHstr = Hstr
François Bobot's avatar
François Bobot committed
33

34 35 36 37
type proof_attempt_status =
    | Unedited (** editor not yet run for interactive proof *)
    | JustEdited (** edited but not run yet *)
    | Interrupted (** external proof has never completed *)
François Bobot's avatar
François Bobot committed
38 39 40 41 42 43
    | 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 *)

type task_option = Task.task option
44
type 'a hide = 'a option
François Bobot's avatar
François Bobot committed
45

46 47 48 49
type ident_path =
  { ip_library : string list;
    ip_theory : string;
    ip_qualid : string list;
50 51
  }

52 53 54 55 56 57 58
let print_ident_path fmt ip =
  Format.fprintf fmt "%a.%s.%a"
    (Pp.print_list Pp.dot Pp.string) ip.ip_library
    ip.ip_theory
    (Pp.print_list Pp.dot Pp.string) ip.ip_qualid

let compare_ident_path x y =
59
  let c = Lists.compare String.compare x.ip_library y.ip_library in
60
  if c <> 0 then -c else (* in order to be bottom up *)
61
  let c = String.compare x.ip_theory y.ip_theory in
62
  if c <> 0 then c else
63
  let c = Lists.compare String.compare x.ip_qualid y.ip_qualid in
64
  c
65 66

module Pos = struct
67 68
  type t = ident_path
  let compare = compare_ident_path
69 70 71 72
  let equal x y = (x : t) = y
  let hash x = Hashtbl.hash (x : t)
end

73 74 75
module Mpos = Extmap.Make(Pos)
module Spos = Extset.MakeOfMap(Mpos)
module Hpos = Exthtbl.Make(Pos)
76 77 78

type meta_args = meta_arg list

79
module Mmeta_args = Extmap.Make(struct
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
  type t = meta_args

  let meta_arg_id = function
    | MAty _  -> 0
    | MAts _  -> 1
    | MAls _  -> 2
    | MApr _  -> 3
    | MAstr _ -> 4
    | MAint _ -> 5

  let compare_meta_arg x y =
    match x,y with
  (** These hash are in fact tag *)
    | MAty  x, MAty  y -> compare (ty_hash x) (ty_hash y)
    | MAts  x, MAts  y -> compare (ts_hash x) (ts_hash y)
    | MAls  x, MAls  y -> compare (ls_hash x) (ls_hash y)
    | MApr  x, MApr  y -> compare (pr_hash x) (pr_hash y)
    | MAstr x, MAstr y -> String.compare x y
    | MAint x, MAint y -> compare x y
    | _ -> compare (meta_arg_id x) (meta_arg_id y)

101
  let compare = Lists.compare compare_meta_arg
102
end)
103 104

module Smeta_args = Extset.MakeOfMap(Mmeta_args)
105

106 107
type metas_args = Smeta_args.t Mstr.t

108
module Mmetas_args = Extmap.Make(struct
109 110 111 112 113
  type t = metas_args
  let compare = Mstr.compare Smeta_args.compare
end)

type idpos = {
114 115 116
  idpos_ts : ident_path Mts.t;
  idpos_ls : ident_path Mls.t;
  idpos_pr : ident_path Mpr.t;
117 118 119 120 121 122 123 124 125
}

let empty_idpos =
  {
    idpos_ts = Mts.empty;
    idpos_ls = Mls.empty;
    idpos_pr = Mpr.empty;
  }

126
(* dead code
127 128 129 130 131 132 133 134 135
let posid_of_idpos idpos =
  let posid = Mpos.empty in
  let posid = Mts.fold (fun ts pos ->
    Mpos.add pos (MAts ts)) idpos.idpos_ts posid  in
  let posid = Mls.fold (fun ls pos ->
    Mpos.add pos (MAls ls)) idpos.idpos_ls posid  in
  let posid = Mpr.fold (fun pr pos ->
    Mpos.add pos (MApr pr)) idpos.idpos_pr posid  in
  posid
136
*)
137

138 139
type expl = string option

François Bobot's avatar
François Bobot committed
140
type 'a goal =
141 142
  { mutable goal_key  : 'a;
    goal_name : Ident.ident;
143
    goal_expl : expl;
144
    goal_parent : 'a goal_parent;
145
    mutable goal_checksum : Tc.checksum option;
146 147
    mutable goal_shape : Tc.shape;
    mutable goal_verified : bool;
148
    mutable goal_task: task_option;
149 150 151
    mutable goal_expanded : bool;
    goal_external_proofs : 'a proof_attempt PHprover.t;
    goal_transformations : 'a transf PHstr.t;
152
    mutable goal_metas : 'a metas Mmetas_args.t;
153
  }
François Bobot's avatar
François Bobot committed
154 155

and 'a proof_attempt =
156 157 158 159 160 161 162 163 164 165
  { proof_key : 'a;
    mutable proof_prover : Whyconf.prover;
    proof_parent : 'a goal;
    mutable proof_state : proof_attempt_status;
    mutable proof_timelimit : int;
    mutable proof_memlimit : int;
    mutable proof_obsolete : bool;
    mutable proof_archived : bool;
    mutable proof_edited_as : string option;
  }
François Bobot's avatar
François Bobot committed
166 167 168 169

and 'a goal_parent =
  | Parent_theory of 'a theory
  | Parent_transf of 'a transf
170 171 172 173 174 175 176 177 178 179 180 181
  | Parent_metas  of 'a metas

and 'a metas =
  { mutable metas_key : 'a;
    metas_added : metas_args;
    metas_idpos : idpos;
    metas_parent : 'a goal;
    mutable metas_verified : bool;
    mutable metas_goal : 'a goal;
    (** Not mutated after the creation *)
    mutable metas_expanded : bool;
  }
François Bobot's avatar
François Bobot committed
182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197

and 'a transf =
    { mutable transf_key : 'a;
      transf_name : string;
      (** Why3 tranformation name *)
      transf_parent : 'a goal;
      mutable transf_verified : bool;
      mutable transf_goals : 'a goal list;
      (** Not mutated after the creation of the session *)
      mutable transf_expanded : bool;
    }

and 'a theory =
    { mutable theory_key : 'a;
      theory_name : Ident.ident;
      theory_parent : 'a file;
198
      mutable theory_checksum : Termcode.checksum option;
François Bobot's avatar
François Bobot committed
199 200 201
      mutable theory_goals : 'a goal list;
      mutable theory_verified : bool;
      mutable theory_expanded : bool;
202
      mutable theory_task : Theory.theory hide;
François Bobot's avatar
François Bobot committed
203 204 205 206 207
    }

and 'a file =
    { mutable file_key : 'a;
      file_name : string;
208
      file_format : string option;
François Bobot's avatar
François Bobot committed
209 210 211 212 213
      file_parent : 'a session;
      mutable file_theories: 'a theory list;
      (** Not mutated after the creation *)
      mutable file_verified : bool;
      mutable file_expanded : bool;
214
      mutable file_for_recovery : Theory.theory Mstr.t hide;
François Bobot's avatar
François Bobot committed
215 216 217 218
    }

and 'a session =
    { session_files : 'a file PHstr.t;
MARCHE Claude's avatar
MARCHE Claude committed
219
      mutable session_shape_version : int;
220
      session_prover_ids : int PHprover.t;
François Bobot's avatar
François Bobot committed
221 222 223 224 225 226 227
      session_dir   : string; (** Absolute path *)
    }

type loaded_prover =
    { prover_config : Whyconf.config_prover;
      prover_driver : Driver.driver}

228
type loaded_provers = loaded_prover option PHprover.t
François Bobot's avatar
François Bobot committed
229 230 231

type 'a env_session =
    { env : Env.env;
232
      mutable whyconf : Whyconf.config;
François Bobot's avatar
François Bobot committed
233
      loaded_provers : loaded_provers;
234
      mutable files : Theory.theory Stdlib.Mstr.t Stdlib.Mstr.t;
François Bobot's avatar
François Bobot committed
235 236
      session : 'a session}

237
let update_env_session_config e c = e.whyconf <- c
François Bobot's avatar
François Bobot committed
238 239 240 241 242 243 244 245 246 247

(*************************)
(**       Iterators      *)
(*************************)
type 'a any =
  | File of 'a file
  | Theory of 'a theory
  | Goal of 'a goal
  | Proof_attempt of 'a proof_attempt
  | Transf of 'a transf
248
  | Metas of 'a metas
François Bobot's avatar
François Bobot committed
249 250 251

let rec goal_iter_proof_attempt f g =
  PHprover.iter (fun _ a -> f a) g.goal_external_proofs;
252 253
  PHstr.iter (fun _ t -> transf_iter_proof_attempt f t) g.goal_transformations;
  Mmetas_args.iter (fun _ t -> metas_iter_proof_attempt f t) g.goal_metas;
François Bobot's avatar
François Bobot committed
254 255 256 257

and transf_iter_proof_attempt f t =
  List.iter (goal_iter_proof_attempt f) t.transf_goals

258 259 260
and metas_iter_proof_attempt f t =
  goal_iter_proof_attempt f t.metas_goal

François Bobot's avatar
François Bobot committed
261 262 263
let theory_iter_proof_attempt f t =
  List.iter (goal_iter_proof_attempt f) t.theory_goals

264 265 266
let metas_iter_proof_attempt f m =
  goal_iter_proof_attempt f m.metas_goal

François Bobot's avatar
François Bobot committed
267 268 269 270 271 272
let file_iter_proof_attempt f t =
  List.iter (theory_iter_proof_attempt f) t.file_theories

let session_iter_proof_attempt f s =
  PHstr.iter (fun _ file -> file_iter_proof_attempt f file) s.session_files

273
let iter_proof_attempt f = function
François Bobot's avatar
François Bobot committed
274 275 276 277 278
    | Goal g -> goal_iter_proof_attempt f g
    | Theory th -> theory_iter_proof_attempt f th
    | File file -> file_iter_proof_attempt f file
    | Proof_attempt a -> f a
    | Transf tr -> transf_iter_proof_attempt f tr
279
    | Metas m -> metas_iter_proof_attempt f m
François Bobot's avatar
François Bobot committed
280 281 282 283 284 285 286 287 288 289 290

let rec goal_iter_leaf_goal ~unproved_only f g =
  if not (g.goal_verified && unproved_only) then
    let r = ref true in
    PHstr.iter
      (fun _ t -> r := false;
        List.iter (goal_iter_leaf_goal ~unproved_only f) t.transf_goals)
      g.goal_transformations;
    if !r then f g

(** iterators not reccursive *)
291
let iter_goal fp ft fm g =
François Bobot's avatar
François Bobot committed
292
  PHprover.iter (fun _ a -> fp a) g.goal_external_proofs;
293 294
  PHstr.iter (fun _ t -> ft t) g.goal_transformations;
  Mmetas_args.iter (fun _ t -> fm t) g.goal_metas
François Bobot's avatar
François Bobot committed
295 296 297 298

let iter_transf f t =
  List.iter (fun g -> f g) t.transf_goals

299 300
let iter_metas f t = f t.metas_goal

301 302 303
let iter_theory f t =
  List.iter f t.theory_goals

304 305 306 307
let iter_file f fi = List.iter f fi.file_theories

let iter_session f s = PHstr.iter (fun _ th -> f th) s.session_files

François Bobot's avatar
François Bobot committed
308
let goal_iter f g =
309 310
  PHprover.iter
    (fun _ a -> f (Proof_attempt a)) g.goal_external_proofs;
311 312 313
  PHstr.iter (fun _ t -> f (Transf t)) g.goal_transformations;
  Mmetas_args.iter (fun _ t -> f (Metas t)) g.goal_metas

François Bobot's avatar
François Bobot committed
314 315 316 317

let transf_iter f t =
  List.iter (fun g -> f (Goal g)) t.transf_goals

318 319 320
let metas_iter f t =
  f (Goal t.metas_goal)

François Bobot's avatar
François Bobot committed
321 322 323 324 325 326 327 328 329 330 331 332 333 334 335
let theory_iter f t =
  List.iter (fun g -> f (Goal g)) t.theory_goals

let file_iter f t =
  List.iter (fun th -> f (Theory th)) t.file_theories

let session_iter f s =
  PHstr.iter (fun _ file -> f (File file)) s.session_files

let iter f = function
    | Goal g -> goal_iter f g
    | Theory th -> theory_iter f th
    | File file -> file_iter f file
    | Proof_attempt _ -> ()
    | Transf tr -> transf_iter f tr
336
    | Metas m -> metas_iter f m
François Bobot's avatar
François Bobot committed
337 338 339 340 341 342 343 344 345

(** Print session *)


module PTreeT = struct
  type 'a t = | Any of 'a any | Session of 'a session
  let decomp = function
    | Any t ->
      let s = match t with
346 347 348 349 350 351 352 353
        | File f ->
          if f.file_verified
          then f.file_name
          else f.file_name^"?"
        | Theory th ->
          if th.theory_verified
          then th.theory_name.Ident.id_string
          else th.theory_name.Ident.id_string^"?"
François Bobot's avatar
François Bobot committed
354
        | Goal g ->
355 356 357
          if g.goal_verified
          then g.goal_name.Ident.id_string
          else g.goal_name.Ident.id_string^"?"
358
        | Proof_attempt pr ->
359
          Pp.sprintf_wnl "%a%s%s%s%s"
360
            Whyconf.print_prover pr.proof_prover
361 362 363 364
            (match pr.proof_state with
              | Done { Call_provers.pr_answer = Call_provers.Valid} -> ""
              | InternalFailure _ -> "!"
              | _ -> "?")
365 366 367
            (if pr.proof_obsolete || pr.proof_archived then " " else "")
            (if pr.proof_obsolete then "O" else "")
            (if pr.proof_archived then "A" else "")
368 369 370
        | Transf tr ->
          if tr.transf_verified
          then tr.transf_name
371 372 373 374 375 376
          else tr.transf_name^"?"
        | Metas metas ->
          if metas.metas_verified
          then "metas..."
          else "metas..."^"?"
      in
François Bobot's avatar
François Bobot committed
377 378 379 380 381 382
      let l = ref [] in
      iter (fun a -> l := (Any a)::!l) t;
      s,!l
    | Session s ->
      let l = ref [] in
      session_iter (fun a -> l := (Any a)::!l) s;
383 384 385 386 387
      (** Previously "" was `Filename.basename s.session_dir` but
          the tree depend on the filename given in input and not the content
          which is not easy for diffing
      *)
      "",!l
François Bobot's avatar
François Bobot committed
388 389 390 391 392 393 394 395 396 397 398

end

module PTree = Print_tree.PMake(PTreeT)

let print_any fmt any = PTree.print fmt (PTreeT.Any any)

let print_session fmt s = PTree.print fmt (PTreeT.Session s)

(** 2 Create a session *)

MARCHE Claude's avatar
MARCHE Claude committed
399 400 401 402 403 404 405
let empty_session ?shape_version dir =
  let shape_version = match shape_version with
    | Some v -> v
    | None -> Termcode.current_shape_version
  in
  { session_files = PHstr.create 3;
    session_shape_version = shape_version;
406
    session_prover_ids = PHprover.create 7;
MARCHE Claude's avatar
MARCHE Claude committed
407 408 409 410
    session_dir   = dir;
  }

let create_session ?shape_version project_dir =
François Bobot's avatar
François Bobot committed
411 412
  if not (Sys.file_exists project_dir) then
    begin
413
      Debug.dprintf debug
François Bobot's avatar
François Bobot committed
414 415 416 417
        "[Info] '%s' does not exists. Creating directory of that name \
 for the project@." project_dir;
      Unix.mkdir project_dir 0o777
    end;
MARCHE Claude's avatar
MARCHE Claude committed
418
  empty_session ?shape_version project_dir
François Bobot's avatar
François Bobot committed
419 420


421
(* dead code
François Bobot's avatar
François Bobot committed
422 423 424 425 426 427 428
let load_env_session ?(includes=[]) session conf_path_opt =
  let config = Whyconf.read_config conf_path_opt in
  let loadpath = (Whyconf.loadpath (Whyconf.get_main config)) @ includes in
  let env = Env.create_env loadpath in
  { session = session;
    env = env;
    whyconf = config;
429
    loaded_provers = PHprover.create 5;
François Bobot's avatar
François Bobot committed
430
  }
431
*)
François Bobot's avatar
François Bobot committed
432 433 434 435 436

(************************)
(* session accessor     *)
(************************)

437
(* dead code
François Bobot's avatar
François Bobot committed
438 439 440 441 442 443 444 445
let get_session_file file = file.file_parent

let get_session_theory th = get_session_file th.theory_parent

let rec get_session_goal goal =
  match goal.goal_parent with
    | Parent_transf trans -> get_session_trans trans
    | Parent_theory th    -> get_session_theory th
446
    | Parent_metas  metas -> get_session_metas metas
François Bobot's avatar
François Bobot committed
447

448

François Bobot's avatar
François Bobot committed
449 450
and get_session_trans transf = get_session_goal transf.transf_parent

451 452
and get_session_metas metas = get_session_goal metas.metas_parent

François Bobot's avatar
François Bobot committed
453
let get_session_proof_attempt pa = get_session_goal pa.proof_parent
454
*)
François Bobot's avatar
François Bobot committed
455

456
let get_used_provers session =
François Bobot's avatar
François Bobot committed
457
  let sprover = ref Sprover.empty in
458
   session_iter_proof_attempt
François Bobot's avatar
François Bobot committed
459
    (fun pa -> sprover := Sprover.add pa.proof_prover !sprover)
460
     session;
François Bobot's avatar
François Bobot committed
461 462
  !sprover

463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488
let get_used_provers_with_stats session =
  let prover_table = PHprover.create 5 in
  session_iter_proof_attempt
    (fun pa ->
      (* record mostly used pa.proof_timelimit pa.proof_memlimit *)
      let prover = pa.proof_prover in
      let timelimits,memlimits =
        try PHprover.find prover_table prover
        with Not_found ->
          let x = (Hashtbl.create 5,Hashtbl.create 5) in
          PHprover.add prover_table prover x;
          x
      in
      let tf =
        try Hashtbl.find timelimits pa.proof_timelimit
        with Not_found -> 0
      in
      let mf =
        try Hashtbl.find memlimits pa.proof_timelimit
        with Not_found -> 0
      in
      Hashtbl.replace timelimits pa.proof_timelimit (tf+1);
      Hashtbl.replace memlimits pa.proof_memlimit (mf+1))
    session;
  prover_table

François Bobot's avatar
François Bobot committed
489 490
exception NoTask

491
let goal_task g = Opt.get_exn NoTask g.goal_task
François Bobot's avatar
François Bobot committed
492 493
let goal_task_option g = g.goal_task

494
let goal_expl g = Opt.get_def g.goal_name.Ident.id_string g.goal_expl
François Bobot's avatar
François Bobot committed
495 496 497 498 499 500 501

(************************)
(* saving state on disk *)
(************************)
open Format

let db_filename = "why3session.xml"
502
let shape_filename = "why3shapes"
503
let compressed_shape_filename = "why3shapes.gz"
504
let session_dir_for_save = ref "."
François Bobot's avatar
François Bobot committed
505

506 507 508 509 510 511 512 513 514 515 516 517
let save_string fmt s =
  for i=0 to String.length s - 1 do
    match String.get s i with
      | '\"' -> pp_print_string fmt "&quot;"
      | '\'' -> pp_print_string fmt "&apos;"
      | '<' -> pp_print_string fmt "&lt;"
      | '>' -> pp_print_string fmt "&gt;"
      | '&' -> pp_print_string fmt "&amp;"
      | c -> pp_print_char fmt c
  done


François Bobot's avatar
François Bobot committed
518
let save_result fmt r =
519
  fprintf fmt "<result@ status=\"%s\"@ time=\"%.2f\"/>"
François Bobot's avatar
François Bobot committed
520 521 522 523 524 525
    (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"
526
       | Call_provers.OutOfMemory -> "outofmemory"
François Bobot's avatar
François Bobot committed
527 528 529 530 531
       | Call_provers.Invalid -> "invalid")
    r.Call_provers.pr_time

let save_status fmt s =
  match s with
532
    | Unedited ->
533
        fprintf fmt "<unedited/>"
534
    | Scheduled | Running | Interrupted | JustEdited ->
535
        fprintf fmt "<undone/>"
François Bobot's avatar
François Bobot committed
536
    | InternalFailure msg ->
537
        fprintf fmt "<internalfailure@ reason=\"%a\"/>"
538
          save_string (Printexc.to_string msg)
François Bobot's avatar
François Bobot committed
539 540 541
    | Done r -> save_result fmt r


542 543 544
let save_bool_def name def fmt b =
  if b <> def then fprintf fmt "@ %s=\"%b\"" name b

545 546 547
let save_int_def name def fmt n =
  if n <> def then fprintf fmt "@ %s=\"%d\"" name n

548
let opt pr lab fmt = function
François Bobot's avatar
François Bobot committed
549
  | None -> ()
550 551 552
  | Some s -> fprintf fmt "@ %s=\"%a\"" lab pr s

let opt_string = opt save_string
François Bobot's avatar
François Bobot committed
553

554
let save_proof_attempt fmt ((id,tl,ml),a) =
François Bobot's avatar
François Bobot committed
555
  fprintf fmt
556
    "@\n@[<h><proof@ prover=\"%i\"%a%a%a%a%a>"
557 558 559
    id
    (save_int_def "timelimit" tl) a.proof_timelimit
    (save_int_def "memlimit" ml) a.proof_memlimit
560
    (opt_string "edited") a.proof_edited_as
561 562
    (save_bool_def "obsolete" false) a.proof_obsolete
    (save_bool_def "archived" false) a.proof_archived;
François Bobot's avatar
François Bobot committed
563
  save_status fmt a.proof_state;
564
  fprintf fmt "</proof>@]"
François Bobot's avatar
François Bobot committed
565 566

let save_ident fmt id =
567
  fprintf fmt "name=\"%a\"" save_string id.Ident.id_string;
568 569
(* location info is useless, and takes a lot of place *)
(*
François Bobot's avatar
François Bobot committed
570 571 572 573
  match id.Ident.id_loc with
    | None -> ()
    | Some loc ->
      let file,lnum,cnumb,cnume = Loc.get loc in
574
      let file = Sysutil.relativize_filename !session_dir_for_save file in
François Bobot's avatar
François Bobot committed
575
      fprintf fmt
576 577
        "@ locfile=\"%a\"@ loclnum=\"%i\" loccnumb=\"%i\" loccnume=\"%i\""
        save_string file lnum cnumb cnume
578 579
*)
  ()
François Bobot's avatar
François Bobot committed
580

581
(*
François Bobot's avatar
François Bobot committed
582
let save_label fmt s =
583
  fprintf fmt "@\n@[<hov 1><label@ name=\"%a\"/>@]" save_string s.Ident.lab_string
584
*)
585

586 587
module Compr = Compress.Compress_z

588
type save_ctxt = {
589
  prover_ids : int PHprover.t;
590 591
  provers : (int * int * int) Mprover.t;
  ch_shapes : Compr.out_channel;
592 593
}

594 595 596
let save_checksum fmt s =
  fprintf fmt "%s" (Tc.string_of_checksum s)

597
let rec save_goal ctxt fmt g =
598 599
  let shape = Tc.string_of_shape g.goal_shape in
  assert (shape <> "");
François Bobot's avatar
François Bobot committed
600
  fprintf fmt
601
    "@\n@[<v 0>@[<h><goal@ %a%a%a>@]"
François Bobot's avatar
François Bobot committed
602
    save_ident g.goal_name
603
    (opt_string "expl") g.goal_expl
604
(* no more checksum in why3session.xml
605
    (opt save_checksum "sum") g.goal_checksum
606
*)
607
    (save_bool_def "expanded" false) g.goal_expanded;
608 609 610 611 612 613
  let sum =
    match g.goal_checksum with
    | None -> assert false
    | Some s -> Tc.string_of_checksum s
  in
  Compr.output_string ctxt.ch_shapes sum;
614 615 616
  Compr.output_char ctxt.ch_shapes ' ';
  Compr.output_string ctxt.ch_shapes shape;
  Compr.output_char ctxt.ch_shapes '\n';
617
(*
618
  Ident.Slab.iter (save_label fmt) g.goal_name.Ident.id_label;
619
*)
620
  let l = PHprover.fold
621
    (fun _ a acc -> (Mprover.find a.proof_prover ctxt.provers, a) :: acc)
622
    g.goal_external_proofs [] in
623
  let l = List.sort (fun ((i1,_,_),_) ((i2,_,_),_) -> compare i1 i2) l in
624 625 626
  List.iter (save_proof_attempt fmt) l;
  let l = PHstr.fold (fun _ t acc -> t :: acc) g.goal_transformations [] in
  let l = List.sort (fun t1 t2 -> compare t1.transf_name t2.transf_name) l in
627 628
  List.iter (save_trans ctxt fmt) l;
  Mmetas_args.iter (save_metas ctxt fmt) g.goal_metas;
François Bobot's avatar
François Bobot committed
629 630
  fprintf fmt "@]@\n</goal>"

631
and save_trans ctxt fmt t =
632
  fprintf fmt "@\n@[<hov 1>@[<h><transf@ name=\"%a\"%a>@]"
633
    save_string t.transf_name
634
    (save_bool_def "expanded" false) t.transf_expanded;
635
  List.iter (save_goal ctxt fmt) t.transf_goals;
François Bobot's avatar
François Bobot committed
636 637
  fprintf fmt "@]@\n</transf>"

638
and save_metas ctxt fmt _ m =
639
  fprintf fmt "@\n@[<hov 1><metas%a>"
640
    (save_bool_def "expanded" false) m.metas_expanded;
641
  let save_pos fmt pos =
Andrei Paskevich's avatar
Andrei Paskevich committed
642
    fprintf fmt "ip_theory=\"%a\">" save_string pos.ip_theory;
643
    List.iter (fprintf fmt "@\n@[<hov 1><ip_library@ name=\"%a\"/>@]" save_string)
644
      pos.ip_library;
645
    List.iter (fprintf fmt "@\n@[<hov 1><ip_qualid@ name=\"%a\"/>@]" save_string)
646 647
      pos.ip_qualid;
  in
648
  let save_ts_pos fmt ts pos =
649
    fprintf fmt "@\n@[<hov 1><ts_pos@ name=\"%a\"@ arity=\"%i\"@ \
Andrei Paskevich's avatar
Andrei Paskevich committed
650
    id=\"%i\"@ %a@]@\n</ts_pos>"
651 652 653 654
      save_string ts.ts_name.id_string (List.length ts.ts_args)
      (ts_hash ts) save_pos pos in
  let save_ls_pos fmt ls pos =
    (** TODO: add the signature? *)
655
    fprintf fmt "@\n@[<hov 1><ls_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</ls_pos>"
656
      save_string ls.ls_name.id_string
657
      (ls_hash ls) save_pos pos
658 659
  in
  let save_pr_pos fmt pr pos =
660
    fprintf fmt "@\n@[<hov 1><pr_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</pr_pos>"
661
      save_string pr.pr_name.id_string
662
      (pr_hash pr) save_pos pos
663 664 665 666 667 668
  in
  Mts.iter (save_ts_pos fmt) m.metas_idpos.idpos_ts;
  Mls.iter (save_ls_pos fmt) m.metas_idpos.idpos_ls;
  Mpr.iter (save_pr_pos fmt) m.metas_idpos.idpos_pr;
  Mstr.iter (fun s smeta_args ->
    Smeta_args.iter (save_meta_args fmt s) smeta_args) m.metas_added;
669
  save_goal ctxt fmt m.metas_goal;
670 671 672
  fprintf fmt "@]@\n</metas>"

and save_meta_args fmt s l =
673
  fprintf fmt "@\n@[<hov 1><meta@ name=\"%a\">" save_string s;
674
  let save_meta_arg fmt = function
675
    | MAty ty -> fprintf fmt "@\n@[<hov 1><meta_arg_ty/>";
676 677 678
      save_ty fmt ty;
      fprintf fmt "@]@\n</meta_arg_ty>"
    | MAts ts ->
679
      fprintf fmt "@\n@[<hov 1><meta_arg_ts@ id=\"%i\"/>@]" (ts_hash ts)
680
    | MAls ls ->
681
      fprintf fmt "@\n@[<hov 1><meta_arg_ls@ id=\"%i\"/>@]" (ls_hash ls)
682
    | MApr pr ->
683
      fprintf fmt "@\n@[<hov 1><meta_arg_pr@ id=\"%i\"/>@]" (pr_hash pr)
684
    | MAstr s ->
685
      fprintf fmt "@\n@[<hov 1><meta_arg_str@ val=\"%s\"/>@]" s
686
    | MAint i ->
687
      fprintf fmt "@\n@[<hov 1><meta_arg_int@ val=\"%i\"/>@]" i
688 689
  in
  List.iter (save_meta_arg fmt) l;
690
  fprintf fmt "@]@\n</meta>"
691 692 693 694

and save_ty fmt ty =
  match ty.ty_node with
  | Tyvar tv ->
695
    fprintf fmt "@\n@[<hov 1><ty_var@ id=\"%i\"/>@]" (tv_hash tv)
696
  | Tyapp (ts,l) ->
697
    fprintf fmt "@\n@[<hov 1><ty_app@ id=\"%i\"/>" (ts_hash ts);
698 699 700
    List.iter (save_ty fmt) l;
    fprintf fmt "@]@\n</ty_app>"

701
let save_theory ctxt fmt t =
François Bobot's avatar
François Bobot committed
702
  fprintf fmt
703
    "@\n@[<v 1>@[<h><theory@ %a%a%a>@]"
François Bobot's avatar
François Bobot committed
704
    save_ident t.theory_name
705
    (opt save_checksum "sum") t.theory_checksum
706
    (save_bool_def "expanded" false) t.theory_expanded;
707
(*
708
  Ident.Slab.iter (save_label fmt) t.theory_name.Ident.id_label;
709
*)
710
  List.iter (save_goal ctxt fmt) t.theory_goals;
François Bobot's avatar
François Bobot committed
711 712
  fprintf fmt "@]@\n</theory>"

713
let save_file ctxt fmt _ f =
714
  fprintf fmt
715
    "@\n@[<v 0>@[<h><file@ name=\"%a\"%a%a>@]"
716
    save_string f.file_name (opt_string "format")
717
    f.file_format (save_bool_def "expanded" false) f.file_expanded;
718
  List.iter (save_theory ctxt fmt) f.file_theories;
François Bobot's avatar
François Bobot committed
719 720
  fprintf fmt "@]@\n</file>"

721
let save_prover ctxt fmt p (timelimits,memlimits) provers =
722 723 724 725 726 727 728 729 730 731 732 733
  let mostfrequent_timelimit,_ =
    Hashtbl.fold
      (fun t f ((_,f') as t') -> if f > f' then (t,f) else t')
      timelimits
      (0,0)
  in
  let mostfrequent_memlimit,_ =
    Hashtbl.fold
      (fun m f ((_,f') as m') -> if f > f' then (m,f) else m')
      memlimits
      (0,0)
  in
734 735 736 737 738 739 740 741
  let id =
    try
      PHprover.find ctxt.prover_ids p
    with Not_found ->
      (* we need to find an unused prover id *)
      let occurs = Hashtbl.create 7 in
      PHprover.iter (fun _ n -> Hashtbl.add occurs n ()) ctxt.prover_ids;
      let id = ref 0 in
742 743
      try
        while true do
744 745 746 747 748
          try
            let _ = Hashtbl.find occurs !id in incr id
          with Not_found -> raise Exit
            done;
        assert false
749
      with Exit ->
750 751 752
        PHprover.add ctxt.prover_ids p !id;
        !id
  in
753
  fprintf fmt "@\n@[<h><prover@ id=\"%i\"@ name=\"%a\"@ \
754
               version=\"%a\"%a@ timelimit=\"%d\"@ memlimit=\"%d\"/>@]"
755
    id save_string p.C.prover_name save_string p.C.prover_version
756 757
    (fun fmt s -> if s <> "" then fprintf fmt "@ alternative=\"%a\""
        save_string s)
758 759
    p.C.prover_altern
    mostfrequent_timelimit mostfrequent_memlimit;
760
  Mprover.add p (id,mostfrequent_timelimit,mostfrequent_memlimit) provers
François Bobot's avatar
François Bobot committed
761

762
let save fname shfname _config session =
François Bobot's avatar
François Bobot committed
763
  let ch = open_out fname in
764
  let chsh = Compr.open_out shfname in
François Bobot's avatar
François Bobot committed
765 766
  let fmt = formatter_of_out_channel ch in
  fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
767
  fprintf fmt "<!DOCTYPE why3session PUBLIC \"-//Why3//proof session v5//EN\"@ \"http://why3.lri.fr/why3session.dtd\">@\n";
768 769 770
  (*
    let rel_file = Sysutil.relativize_filename !session_dir_for_save fname in
    fprintf fmt "@[<hov 1><why3session@ name=\"%a\" shape_version=\"%d\">"
771
    save_string rel_file session.session_shape_version;
772
  *)
773
  fprintf fmt "@[<v 0><why3session shape_version=\"%d\">"
774
    session.session_shape_version;
775
  Tc.reset_dict ();
776 777 778 779 780 781 782 783 784
  let ctxt =
    { prover_ids = session.session_prover_ids;
      provers = Mprover.empty;
      ch_shapes = chsh;
    }
  in
  let provers =
    PHprover.fold (save_prover ctxt fmt) (get_used_provers_with_stats session)
      Mprover.empty
785
  in
786
  PHstr.iter
787
    (save_file { ctxt with provers = provers; ch_shapes = chsh} fmt)
788
    session.session_files;
François Bobot's avatar
François Bobot committed
789 790
  fprintf fmt "@]@\n</why3session>";
  fprintf fmt "@.";
791
  close_out ch;
792
  Compr.close_out chsh
François Bobot's avatar
François Bobot committed
793

MARCHE Claude's avatar
MARCHE Claude committed
794
let save_session config session =
François Bobot's avatar
François Bobot committed
795 796
  let f = Filename.concat session.session_dir db_filename in
  Sysutil.backup_file f;
797 798
  let fs = Filename.concat session.session_dir shape_filename in
  Sysutil.backup_file fs;
799 800
  let fz = Filename.concat session.session_dir compressed_shape_filename in
  Sysutil.backup_file fz;
801
  session_dir_for_save := session.session_dir;
802
  let fs = if Compress.compression_supported then fz else fs in
803
  save f fs config session
François Bobot's avatar
François Bobot committed
804 805 806 807 808 809 810

(*****************************)
(*   update verified field   *)
(*****************************)
type 'a notify = 'a any -> unit
let notify : 'a notify = fun _ -> ()

811 812
let file_verified f =
  List.for_all (fun t -> t.theory_verified) f.file_theories
François Bobot's avatar
François Bobot committed
813

814 815 816 817 818
let theory_verified t =
  List.for_all (fun g -> g.goal_verified) t.theory_goals

let transf_verified t =
  List.for_all (fun g -> g.goal_verified) t.transf_goals
François Bobot's avatar
François Bobot committed
819

820 821
let metas_verified m = m.metas_goal.goal_verified

François Bobot's avatar
François Bobot committed
822 823 824 825 826 827
let proof_verified a =
  (not a.proof_obsolete) &&
    match a.proof_state with
      | Done { Call_provers.pr_answer = Call_provers.Valid} -> true
      | _ -> false

828
let goal_verified g =
François Bobot's avatar
François Bobot committed
829 830 831 832 833 834 835 836 837
    try
      PHprover.iter
        (fun _ a ->
          if proof_verified a
          then raise Exit)
        g.goal_external_proofs;
      PHstr.iter
        (fun _ t -> if t.transf_verified then raise Exit)
        g.goal_transformations;
838 839 840
      Mmetas_args.iter
        (fun _ t -> if t.metas_verified then raise Exit)
        g.goal_metas;
François Bobot's avatar
François Bobot committed
841 842
      false
    with Exit -> true
843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860

let check_file_verified notify f =
  let b = file_verified f in
  if f.file_verified <> b then begin
    f.file_verified <- b;
    notify (File f)
  end

let check_theory_proved notify t =
  let b = theory_verified t in
  if t.theory_verified <> b then begin
    t.theory_verified <- b;
    notify (Theory t);
    check_file_verified notify t.theory_parent
  end

let rec check_goal_proved notify g =
  let b = goal_verified g in
François Bobot's avatar
François Bobot committed
861 862 863 864 865 866
  if g.goal_verified <> b then begin
    g.goal_verified <- b;
    notify (Goal g);
    match g.goal_parent with
      | Parent_theory t -> check_theory_proved notify t
      | Parent_transf t -> check_transf_proved notify t
867
      | Parent_metas t -> check_metas_proved notify t
François Bobot's avatar
François Bobot committed
868 869 870
  end

and check_transf_proved notify t =
871
  let b = transf_verified t in
François Bobot's avatar
François Bobot committed
872 873 874 875 876 877
  if t.transf_verified <> b then begin
    t.transf_verified <- b;
    notify (Transf t);
    check_goal_proved notify t.transf_parent
  end

878 879 880 881 882 883 884 885 886

and check_metas_proved notify m =
  let b = metas_verified m in
  if m.metas_verified <> b then begin
    m.metas_verified <- b;
    notify (Metas m);
    check_goal_proved notify m.metas_parent
  end

François Bobot's avatar
François Bobot committed
887 888 889 890 891 892 893
(******************************)
(* raw additions to the model *)
(******************************)
type 'a keygen = ?parent:'a -> unit -> 'a

let add_external_proof
    ?(notify=notify)
894
    ~(keygen:'a keygen) ~obsolete
895
    ~archived ~timelimit ~memlimit ~edit (g:'a goal) p result =
896
  assert (edit <> Some "");
François Bobot's avatar
François Bobot committed
897 898 899 900 901
  let key = keygen ~parent:g.goal_key () in
  let a = { proof_prover = p;
            proof_parent = g;
            proof_key = key;
            proof_obsolete = obsolete;
902
            proof_archived = archived;
François Bobot's avatar
François Bobot committed
903 904
            proof_state = result;
            proof_timelimit = timelimit;
905
            proof_memlimit = memlimit;
François Bobot's avatar
François Bobot committed
906 907 908
            proof_edited_as = edit;
          }
  in
909
  PHprover.replace g.goal_external_proofs p a;
François Bobot's avatar
François Bobot committed
910 911 912 913 914 915 916 917 918
  check_goal_proved notify g;
  a

let remove_external_proof ?(notify=notify) a =
  let g = a.proof_parent in
  PHprover.remove g.goal_external_proofs a.proof_prover;
  check_goal_proved notify g


919
let set_proof_state ?(notify=notify) ~obsolete ~archived res a =
François Bobot's avatar
François Bobot committed
920 921
  a.proof_state <- res;
  a.proof_obsolete <- obsolete;
922
  a.proof_archived <- archived;
François Bobot's avatar
François Bobot committed
923 924 925
  notify (Proof_attempt a);
  check_goal_proved notify a.proof_parent

926 927 928 929 930 931
let change_prover a p =
  let g = a.proof_parent in
  PHprover.remove g.goal_external_proofs a.proof_prover;
  PHprover.add g.goal_external_proofs p a;
  a.proof_prover <- p;
  a.proof_obsolete <- true
932

François Bobot's avatar
François Bobot committed
933 934 935
let set_edited_as edited_as a = a.proof_edited_as <- edited_as

let set_timelimit timelimit a = a.proof_timelimit <- timelimit
936
let set_memlimit memlimit a = a.proof_memlimit <- memlimit
François Bobot's avatar
François Bobot committed
937

938 939 940 941 942
let set_obsolete ?(notify=notify) a =
  a.proof_obsolete <- true;
  notify (Proof_attempt a);
  check_goal_proved notify a.proof_parent

943
let set_archived a b = a.proof_archived <- b
944

945
let get_edited_as_abs session pr =
946
  Opt.map (Filename.concat session.session_dir) pr.proof_edited_as
947

François Bobot's avatar
François Bobot committed
948 949 950
(* [raw_add_goal parent name expl sum t] adds a goal to the given parent
   DOES NOT record the new goal in its parent, thus this should not be exported
*)
951
let raw_add_no_task ~(keygen:'a keygen) ~(expanded:bool) parent name expl sum shape =
François Bobot's avatar
François Bobot committed
952 953 954
  let parent_key = match parent with
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
955
    | Parent_metas  mms -> mms.metas_key
François Bobot's avatar
François Bobot committed
956 957 958 959 960 961 962 963 964 965 966
  in
  let key = keygen ~parent:parent_key () in
  let goal = { goal_name = name;
               goal_expl = expl;
               goal_parent = parent;
               goal_task = None ;
               goal_checksum = sum;
               goal_shape = shape;
               goal_key = key;
               goal_external_proofs = PHprover.create 7;
               goal_transformations = PHstr.create 3;
967
               goal_metas = Mmetas_args.empty;
François Bobot's avatar
François Bobot committed
968
               goal_verified = false;
969
               goal_expanded = expanded;
François Bobot's avatar
François Bobot committed
970 971 972 973
             }
  in
  goal

974
let raw_add_task ~version ~(keygen:'a keygen) ~(expanded:bool) parent name expl t =
François Bobot's avatar
François Bobot committed
975 976 977
  let parent_key = match parent with
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
978
    | Parent_metas  mms -> mms.metas_key
François Bobot's avatar
François Bobot committed
979 980
  in
  let key = keygen ~parent:parent_key () in
981
  let sum = Some (Termcode.task_checksum ~version t) in
982 983
  (* let shape = Termcode.t_shape_buf ~version (Task.task_goal_fmla t) in *)
  let shape = Termcode.t_shape_task ~version t in
François Bobot's avatar
François Bobot committed
984 985 986 987 988 989 990 991 992
  let goal = { goal_name = name;
               goal_expl = expl;
               goal_parent = parent;
               goal_task = Some t ;
               goal_checksum = sum;
               goal_shape = shape;
               goal_key = key;
               goal_external_proofs = PHprover.create 7;
               goal_transformations = PHstr.create 3;
993
               goal_metas = Mmetas_args.empty;
François Bobot's avatar
François Bobot committed
994
               goal_verified = false;
995
               goal_expanded = expanded;
François Bobot's avatar
François Bobot committed
996 997 998 999 1000 1001 1002 1003
             }
  in
  goal


(* [raw_add_transformation g name adds a transformation to the given goal g
   Adds no subgoals, thus this should not be exported
*)
1004
let raw_add_transformation ~(keygen:'a keygen) ~(expanded:bool) g name =
François Bobot's avatar
François Bobot committed
1005 1006 1007 1008 1009 1010 1011
  let parent = g.goal_key in
  let key = keygen ~parent () in
  let tr = { transf_name = name;
             transf_parent = g;
             transf_verified = false;
             transf_key = key;
             transf_goals = [];
1012
             transf_expanded = expanded;
François Bobot's avatar
François Bobot committed
1013 1014
           }
  in
1015
  PHstr.replace g.goal_transformations name tr;
François Bobot's avatar
François Bobot committed
1016 1017
  tr

1018
let raw_add_metas ~(keygen:'a keygen) ~(expanded:bool) g added idpos =
1019 1020 1021 1022 1023 1024 1025 1026
  let parent = g.goal_key in
  let key = keygen ~parent () in
  let ms = { metas_added = added;
             metas_idpos = idpos;
             metas_parent = g;
             metas_verified = false;
             metas_key = key;
             metas_goal = g;
1027
             metas_expanded = expanded;
1028 1029 1030 1031 1032
           }
  in
  g.goal_metas <- Mmetas_args.add added ms g.goal_metas;
  ms

1033 1034
let raw_add_theory ~(keygen:'a keygen) ~(expanded:bool)
    ~(checksum:Tc.checksum option) mfile thname =
François Bobot's avatar
François Bobot committed
1035 1036 1037 1038 1039
  let parent = mfile.file_key in
  let key = keygen ~parent () in
  let mth = { theory_name = thname;
              theory_key = key;
              theory_parent = mfile;
1040
              theory_checksum = checksum;
1041
              theory_goals = [];
François Bobot's avatar
François Bobot committed
1042
              theory_verified = false;
1043
              theory_expanded = expanded;
1044
              theory_task = None;
François Bobot's avatar
François Bobot committed
1045 1046 1047 1048
            }
  in
  mth

1049
let raw_add_file ~(keygen:'a keygen) ~(expanded:bool) session f fmt =
François Bobot's avatar
François Bobot committed
1050 1051 1052
  let key = keygen () in
  let mfile = { file_name = f;
                file_key = key;
1053 1054
                file_format = fmt;
                file_theories = [];
François Bobot's avatar
François Bobot committed
1055
                file_verified = false;
1056
                file_expanded = expanded;
François Bobot's avatar
François Bobot committed
1057
                file_parent  = session;
1058
                file_for_recovery = None;
François Bobot's avatar
François Bobot committed
1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079
              }
  in
  PHstr.replace session.session_files f mfile;
  mfile


(****************************)
(*     session opening      *)
(****************************)

exception LoadError of Xml.element * string
(** LoadError (xml,messg) *)

let bool_attribute field r def =
  try
    match List.assoc field r.Xml.attributes with
      | "true" -> true
      | "false" -> false
      | _ -> assert false
  with Not_found -> def

1080
let int_attribute_def field r def =
François Bobot's avatar
François Bobot committed
1081 1082 1083 1084
  try
    int_of_string (List.assoc field r.Xml.attributes)
  with Not_found | Invalid_argument _ -> def

1085 1086 1087 1088 1089 1090 1091 1092 1093
let int_attribute field r =
  try
    int_of_string (List.assoc field r.Xml.attributes)
  with Not_found | Invalid_argument _ ->
    (** TODO: use real error *)
    eprintf "[Error] missing required attribute '%s' from element '%s'@."
      field r.Xml.name;
    assert false

François Bobot's avatar
François Bobot committed
1094 1095 1096 1097 1098
let string_attribute_def field r def=
  try
    List.assoc field r.Xml.attributes
  with Not_found -> def

1099 1100 1101 1102 1103
let string_attribute_opt field r =
  try
    Some (List.assoc field r.Xml.attributes)
  with Not_found -> None

François Bobot's avatar
François Bobot committed
1104 1105 1106 1107 1108 1109 1110 1111
let string_attribute field r =
  try
    List.assoc field r.Xml.attributes
  with Not_found ->
    eprintf "[Error] missing required attribute '%s' from element '%s'@."
      field r.Xml.name;
    assert false

1112
let dummy_keygen ?parent:_ () = ()
François Bobot's avatar
François Bobot committed
1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123

let load_result r =
  match r.Xml.name with
    | "result" ->
        let status = string_attribute "status" r in
        let answer =
          match status with
            | "valid" -> Call_provers.Valid
            | "invalid" -> Call_provers.Invalid
            | "unknown" -> Call_provers.Unknown ""
            | "timeout" -> Call_provers.Timeout
1124
            | "outofmemory" -> Call_provers.OutOfMemory
François Bobot's avatar
François Bobot committed
1125
            | "failure" -> Call_provers.Failure ""
1126
            | "highfailure" -> Call_provers.HighFailure
François Bobot's avatar
François Bobot committed
1127 1128 1129
            | s ->
                eprintf
                  "[Warning] Session.load_result: unexpected status '%s'@." s;
1130
                Call_provers.HighFailure
François Bobot's avatar
François Bobot committed
1131 1132 1133 1134 1135 1136 1137 1138 1139
        in
        let time =
          try float_of_string (List.assoc "time" r.Xml.attributes)
          with Not_found -> 0.0
        in
        Done {
          Call_provers.pr_answer = answer;
          Call_provers.pr_time = time;
          Call_provers.pr_output = "";
1140
          Call_provers.pr_status = Unix.WEXITED 0
François Bobot's avatar
François Bobot committed
1141
        }
1142 1143
    | "undone" -> Interrupted
    | "unedited" -> Unedited
François Bobot's avatar
François Bobot committed
1144 1145
    | s ->
        eprintf "[Warning] Session.load_result: unexpected element '%s'@." s;
1146
        Interrupted
François Bobot's avatar
François Bobot committed
1147 1148 1149 1150 1151 1152 1153 1154 1155 1156

let load_option attr g =
  try Some (List.assoc attr g.Xml.attributes)
  with Not_found -> None

let load_ident elt =
  let name = string_attribute "name" elt in
  let label = List.fold_left
    (fun acc label ->
      match label with
1157 1158
        | {Xml.name = "label"} ->
            let lab = string_attribute "name" label in
1159
            Ident.Slab.add (Ident.create_label lab) acc
François Bobot's avatar
François Bobot committed
1160
        | _ -> acc
1161
    ) Ident.Slab.empty elt.Xml.elements in
François Bobot's avatar
François Bobot committed
1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174
  let preid =
    try
      let load_exn attr g = List.assoc attr g.Xml.attributes in
      let file = load_exn "locfile" elt in
      let lnum =  int_of_string (load_exn "loclnum" elt) in
      let cnumb = int_of_string (load_exn "loccnumb" elt) in
      let cnume = int_of_string (load_exn "loccnume" elt) in
      let pos = Loc.user_position file lnum cnumb cnume in
      Ident.id_user ~label name pos
    with Not_found | Invalid_argument _ ->
      Ident.id_fresh ~label name in
  Ident.id_register preid

1175
type load_ctxt = {
1176
  old_provers : (Whyconf.prover * int * int) Mint.t ;
1177
(*
1178
  shapes : ((string, Tc.shape) Hashtbl.t) option
1179
*)
1180 1181 1182
}

let rec load_goal ctxt parent acc g =
François Bobot's avatar
François Bobot committed
1183 1184 1185 1186
  match g.Xml.name with
    | "goal" ->
        let gname = load_ident g in
        let expl = load_option "expl" g in
1187 1188
        let csum = string_attribute_opt "sum" g in
        let sum = Opt.map Tc.checksum_of_string csum in
1189 1190
        let shape =
          try Tc.shape_of_string (List.assoc "shape" g.Xml.attributes)
1191 1192
          with Not_found -> Tc.shape_of_string ""
(*
1193 1194 1195 1196 1197 1198 1199
            match ctxt.shapes with
              | None -> Tc.shape_of_string ""
              | Some h ->
                try Hashtbl.find h csum
                with Not_found ->
                  Format.eprintf "[Warning] shape not found for goal %s@." csum;
                  Tc.shape_of_string ""
1200
*)
1201
        in
1202
        let expanded = bool_attribute "expanded" g false in
1203
        let mg =
1204
          raw_add_no_task ~keygen:dummy_keygen ~expanded parent gname expl sum shape
1205
        in
1206
        List.iter (load_proof_or_transf ctxt mg) g.Xml.elements;
1207
        mg.goal_verified <- goal_verified mg;
François Bobot's avatar
François Bobot committed
1208 1209 1210 1211 1212 1213
        mg::acc
    | "label" -> acc
    | s ->
        eprintf "[Warning] Session.load_goal: unexpected element '%s'@." s;
        acc

1214
and load_proof_or_transf ctxt mg a =
François Bobot's avatar
François Bobot committed
1215 1216
  match a.Xml.name with
    | "proof" ->
1217
      begin
François Bobot's avatar
François Bobot committed
1218
        let prover = string_attribute "prover" a in
1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243
        try
          let prover = int_of_string prover in
          let (p,timelimit,memlimit) =Mint.find prover ctxt.old_provers in
          let res = match a.Xml.elements with
            | [r] -> load_result r
            | [] -> Interrupted
            | _ ->
              eprintf "[Error] Too many result elements@.";
              raise (LoadError (a,"too many result elements"))
          in
          let edit = load_option "edited" a in
          let edit = match edit with None | Some "" -> None | _ -> edit in
          let obsolete = bool_attribute "obsolete" a false in
          let archived = bool_attribute "archived" a false in
          let timelimit = int_attribute_def "timelimit" a timelimit in
          let memlimit = int_attribute_def "memlimit" a memlimit in
        (*
          if timelimit < 0 then begin
          eprintf "[Error] incorrect or unspecified  timelimit '%i'@."
          timelimit;
          raise (LoadError (a,sprintf "incorrect or unspecified timelimit %i"
          timelimit))
          end;
        *)
          let (_ : 'a proof_attempt) =
1244
            add_external_proof ~keygen:dummy_keygen ~archived ~obsolete
1245 1246 1247 1248 1249 1250 1251
              ~timelimit ~memlimit ~edit mg p res
          in
          ()
        with Failure _ | Not_found ->
          eprintf "[Error] prover id not listed in header '%s'@." prover;
          raise (LoadError (a,"prover not listing in header"))
      end
François Bobot's avatar
François Bobot committed
1252 1253
    | "transf" ->
        let trname = string_attribute "name" a in
1254
        let expanded = bool_attribute "expanded" a false in
1255
        let mtr = raw_add_transformation ~keygen:dummy_keygen ~expanded mg trname in
François Bobot's avatar
François Bobot committed
1256 1257 1258
        mtr.transf_goals <-
          List.rev
          (List.fold_left
1259
             (load_goal ctxt (Parent_transf mtr))
François Bobot's avatar
François Bobot committed
1260
             [] a.Xml.elements);
1261
        (* already done by raw_add_transformation:
François Bobot's avatar
François Bobot committed
1262
           Hashtbl.add mg.transformations trname mtr *)
1263
        (** The attribute "proved" is required but not read *)
1264
        mtr.transf_verified <- transf_verified mtr
1265
    | "metas" -> load_metas ctxt mg a;
François Bobot's avatar
François Bobot committed
1266 1267 1268 1269 1270 1271
    | "label" -> ()
    | s ->
        eprintf
          "[Warning] Session.load_proof_or_transf: unexpected element '%s'@."
          s

1272
and load_metas ctxt mg a =
1273 1274 1275 1276 1277 1278 1279 1280 1281
  let hts = Hint.create 10 in
  let hls = Hint.create 10 in
  let hpr = Hint.create 10 in
  let idpos, metas_args, goal =
    List.fold_left (fun (idpos, metas, goal) a ->
      match a.Xml.name with
      | "ts_pos" | "ls_pos" | "pr_pos" ->
        let name = string_attribute "name" a in
        let intid = int_attribute "id" a in
1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292
        let library, qualid =
          List.fold_left (fun (library,qualid) a ->
            match a.Xml.name with
            | "ip_library" -> string_attribute "name" a::library, qualid
            | "ip_qualid" -> library, string_attribute "name" a::qualid
            | _ ->
              raise (LoadError(a,"Unexpected element")))
            ([],[]) a.Xml.elements in
        let pos = { ip_library = List.rev library;
                    ip_theory = string_attribute "ip_theory" a;
                    ip_qualid = List.rev qualid;
1293 1294 1295 1296
                  } in
        let idpos = begin match a.Xml.name with
          | "ts_pos" ->
            let arity = int_attribute "arity" a in
1297
            let tvs = Util.foldi (fun l _ ->
1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361