session.ml 82.8 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
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 Why3
13
open Stdlib
14 15 16 17 18 19
open Ty
open Ident
open Decl
open Term
open Theory
open Task
François Bobot's avatar
François Bobot committed
20

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

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

(** {2 Type definitions} *)

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

35 36 37 38
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
39 40 41 42 43 44
    | 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
45
type 'a hide = 'a option
François Bobot's avatar
François Bobot committed
46

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

53 54 55 56 57 58 59
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 =
60
  let c = Lists.compare String.compare x.ip_library y.ip_library in
61
  if c <> 0 then -c else (* in order to be bottom up *)
62
  let c = String.compare x.ip_theory y.ip_theory in
63
  if c <> 0 then c else
64
  let c = Lists.compare String.compare x.ip_qualid y.ip_qualid in
65
  c
66 67

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

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

type meta_args = meta_arg list

80
module Mmeta_args = Extmap.Make(struct
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
  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)

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

module Smeta_args = Extset.MakeOfMap(Mmeta_args)
106

107 108
type metas_args = Smeta_args.t Mstr.t

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

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

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

127
(* dead code
128 129 130 131 132 133 134 135 136
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
137
*)
138

MARCHE Claude's avatar
MARCHE Claude committed
139 140
type expl = string option

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

and 'a proof_attempt =
157 158 159 160 161 162 163 164 165 166
  { 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
167 168 169 170

and 'a goal_parent =
  | Parent_theory of 'a theory
  | Parent_transf of 'a transf
171 172 173 174 175 176 177 178 179 180 181 182
  | 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
183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201

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;
      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;
François Bobot's avatar
François Bobot committed
220 221 222 223 224 225 226
      session_dir   : string; (** Absolute path *)
    }

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

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

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

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

(*************************)
(**       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
247
  | Metas of 'a metas
François Bobot's avatar
François Bobot committed
248 249 250

let rec goal_iter_proof_attempt f g =
  PHprover.iter (fun _ a -> f a) g.goal_external_proofs;
251 252
  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
253 254 255 256

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

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

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

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

François Bobot's avatar
François Bobot committed
266 267 268 269 270 271
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

272
let iter_proof_attempt f = function
François Bobot's avatar
François Bobot committed
273 274 275 276 277
    | 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
278
    | Metas m -> metas_iter_proof_attempt f m
François Bobot's avatar
François Bobot committed
279 280 281 282 283 284 285 286 287 288 289

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 *)
290
let iter_goal fp ft fm g =
François Bobot's avatar
François Bobot committed
291
  PHprover.iter (fun _ a -> fp a) g.goal_external_proofs;
292 293
  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
294 295 296 297

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

298 299
let iter_metas f t = f t.metas_goal

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

303 304 305 306
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
307
let goal_iter f g =
308 309
  PHprover.iter
    (fun _ a -> f (Proof_attempt a)) g.goal_external_proofs;
310 311 312
  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
313 314 315 316

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

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

François Bobot's avatar
François Bobot committed
320 321 322 323 324 325 326 327 328 329 330 331 332 333 334
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
335
    | Metas m -> metas_iter f m
François Bobot's avatar
François Bobot committed
336 337 338 339 340 341 342 343 344

(** 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
345 346 347 348 349 350 351 352
        | 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
353
        | Goal g ->
354 355 356
          if g.goal_verified
          then g.goal_name.Ident.id_string
          else g.goal_name.Ident.id_string^"?"
357
        | Proof_attempt pr ->
358
          Pp.sprintf_wnl "%a%s%s%s%s"
359
            Whyconf.print_prover pr.proof_prover
360 361 362 363
            (match pr.proof_state with
              | Done { Call_provers.pr_answer = Call_provers.Valid} -> ""
              | InternalFailure _ -> "!"
              | _ -> "?")
364 365 366
            (if pr.proof_obsolete || pr.proof_archived then " " else "")
            (if pr.proof_obsolete then "O" else "")
            (if pr.proof_archived then "A" else "")
367 368 369
        | Transf tr ->
          if tr.transf_verified
          then tr.transf_name
370 371 372 373 374 375
          else tr.transf_name^"?"
        | Metas metas ->
          if metas.metas_verified
          then "metas..."
          else "metas..."^"?"
      in
François Bobot's avatar
François Bobot committed
376 377 378 379 380 381
      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;
382 383 384 385 386
      (** 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
387 388 389 390 391 392 393 394 395 396 397

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
398 399 400 401 402 403 404 405 406 407 408
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;
    session_dir   = dir;
  }

let create_session ?shape_version project_dir =
François Bobot's avatar
François Bobot committed
409 410
  if not (Sys.file_exists project_dir) then
    begin
411
      Debug.dprintf debug
François Bobot's avatar
François Bobot committed
412 413 414 415
        "[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
416
  empty_session ?shape_version project_dir
François Bobot's avatar
François Bobot committed
417 418


419
(* dead code
François Bobot's avatar
François Bobot committed
420 421 422 423 424 425 426
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;
427
    loaded_provers = PHprover.create 5;
François Bobot's avatar
François Bobot committed
428
  }
429
*)
François Bobot's avatar
François Bobot committed
430 431 432 433 434

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

435
(* dead code
François Bobot's avatar
François Bobot committed
436 437 438 439 440 441 442 443
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
444
    | Parent_metas  metas -> get_session_metas metas
François Bobot's avatar
François Bobot committed
445

446

François Bobot's avatar
François Bobot committed
447 448
and get_session_trans transf = get_session_goal transf.transf_parent

449 450
and get_session_metas metas = get_session_goal metas.metas_parent

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

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

461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486
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
487 488
exception NoTask

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

492
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
493 494 495 496 497 498 499

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

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

MARCHE Claude's avatar
MARCHE Claude committed
504 505 506 507 508 509 510 511 512 513 514 515
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
516
let save_result fmt r =
517
  fprintf fmt "<result@ status=\"%s\"@ time=\"%.2f\"/>"
François Bobot's avatar
François Bobot committed
518 519 520 521 522 523
    (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"
524
       | Call_provers.OutOfMemory -> "outofmemory"
François Bobot's avatar
François Bobot committed
525 526 527 528 529
       | Call_provers.Invalid -> "invalid")
    r.Call_provers.pr_time

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


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

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

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

550
let save_proof_attempt fmt ((id,tl,ml),a) =
François Bobot's avatar
François Bobot committed
551
  fprintf fmt
552
    "@\n@[<h><proof@ prover=\"%i\"%a%a%a%a%a>"
553 554 555 556
    id
    (save_int_def "timelimit" tl) a.proof_timelimit
    (save_int_def "memlimit" ml) a.proof_memlimit
    (opt "edited") a.proof_edited_as
557 558
    (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
559
  save_status fmt a.proof_state;
560
  fprintf fmt "</proof>@]"
François Bobot's avatar
François Bobot committed
561 562

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

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

582 583
module Compr = Compress.Compress_z

584
type save_ctxt = {
585 586
  provers : (int * int * int) Mprover.t;
  ch_shapes : Compr.out_channel;
587 588 589
}

let rec save_goal ctxt fmt g =
590 591
  let shape = Tc.string_of_shape g.goal_shape in
  assert (shape <> "");
592
  let checksum = Tc.string_of_checksum g.goal_checksum in
François Bobot's avatar
François Bobot committed
593
  fprintf fmt
594
    "@\n@[<v 0>@[<h><goal@ %a%a@ sum=\"%a\"%a>@]"
François Bobot's avatar
François Bobot committed
595 596
    save_ident g.goal_name
    (opt "expl") g.goal_expl
597 598
    save_string checksum
    (save_bool_def "expanded" false) g.goal_expanded;
599 600 601 602
  Compr.output_string ctxt.ch_shapes checksum ;
  Compr.output_char ctxt.ch_shapes ' ';
  Compr.output_string ctxt.ch_shapes shape;
  Compr.output_char ctxt.ch_shapes '\n';
603
(*
604
  Ident.Slab.iter (save_label fmt) g.goal_name.Ident.id_label;
605
*)
606
  let l = PHprover.fold
607
    (fun _ a acc -> (Mprover.find a.proof_prover ctxt.provers, a) :: acc)
608
    g.goal_external_proofs [] in
609
  let l = List.sort (fun ((i1,_,_),_) ((i2,_,_),_) -> compare i1 i2) l in
610 611 612
  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
613 614
  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
615 616
  fprintf fmt "@]@\n</goal>"

617
and save_trans ctxt fmt t =
618
  fprintf fmt "@\n@[<hov 1>@[<h><transf@ name=\"%a\"%a>@]"
619
    save_string t.transf_name
620
    (save_bool_def "expanded" false) t.transf_expanded;
621
  List.iter (save_goal ctxt fmt) t.transf_goals;
François Bobot's avatar
François Bobot committed
622 623
  fprintf fmt "@]@\n</transf>"

624
and save_metas ctxt fmt _ m =
625
  fprintf fmt "@\n@[<hov 1><metas%a>"
626
    (save_bool_def "expanded" false) m.metas_expanded;
627
  let save_pos fmt pos =
Andrei Paskevich's avatar
Andrei Paskevich committed
628
    fprintf fmt "ip_theory=\"%a\">" save_string pos.ip_theory;
629
    List.iter (fprintf fmt "@\n@[<hov 1><ip_library@ name=\"%a\"/>@]" save_string)
630
      pos.ip_library;
631
    List.iter (fprintf fmt "@\n@[<hov 1><ip_qualid@ name=\"%a\"/>@]" save_string)
632 633
      pos.ip_qualid;
  in
634
  let save_ts_pos fmt ts pos =
635
    fprintf fmt "@\n@[<hov 1><ts_pos@ name=\"%a\"@ arity=\"%i\"@ \
Andrei Paskevich's avatar
Andrei Paskevich committed
636
    id=\"%i\"@ %a@]@\n</ts_pos>"
637 638 639 640
      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? *)
641
    fprintf fmt "@\n@[<hov 1><ls_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</ls_pos>"
642
      save_string ls.ls_name.id_string
643
      (ls_hash ls) save_pos pos
644 645
  in
  let save_pr_pos fmt pr pos =
646
    fprintf fmt "@\n@[<hov 1><pr_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</pr_pos>"
647
      save_string pr.pr_name.id_string
648
      (pr_hash pr) save_pos pos
649 650 651 652 653 654
  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;
655
  save_goal ctxt fmt m.metas_goal;
656 657 658
  fprintf fmt "@]@\n</metas>"

and save_meta_args fmt s l =
659
  fprintf fmt "@\n@[<hov 1><meta@ name=\"%a\">" save_string s;
660
  let save_meta_arg fmt = function
661
    | MAty ty -> fprintf fmt "@\n@[<hov 1><meta_arg_ty/>";
662 663 664
      save_ty fmt ty;
      fprintf fmt "@]@\n</meta_arg_ty>"
    | MAts ts ->
665
      fprintf fmt "@\n@[<hov 1><meta_arg_ts@ id=\"%i\"/>@]" (ts_hash ts)
666
    | MAls ls ->
667
      fprintf fmt "@\n@[<hov 1><meta_arg_ls@ id=\"%i\"/>@]" (ls_hash ls)
668
    | MApr pr ->
669
      fprintf fmt "@\n@[<hov 1><meta_arg_pr@ id=\"%i\"/>@]" (pr_hash pr)
670
    | MAstr s ->
671
      fprintf fmt "@\n@[<hov 1><meta_arg_str@ val=\"%s\"/>@]" s
672
    | MAint i ->
673
      fprintf fmt "@\n@[<hov 1><meta_arg_int@ val=\"%i\"/>@]" i
674 675
  in
  List.iter (save_meta_arg fmt) l;
676
  fprintf fmt "@]@\n</meta>"
677 678 679 680

and save_ty fmt ty =
  match ty.ty_node with
  | Tyvar tv ->
681
    fprintf fmt "@\n@[<hov 1><ty_var@ id=\"%i\"/>@]" (tv_hash tv)
682
  | Tyapp (ts,l) ->
683
    fprintf fmt "@\n@[<hov 1><ty_app@ id=\"%i\"/>" (ts_hash ts);
684 685 686
    List.iter (save_ty fmt) l;
    fprintf fmt "@]@\n</ty_app>"

687
let save_theory ctxt fmt t =
François Bobot's avatar
François Bobot committed
688
  fprintf fmt
689
    "@\n@[<v 1>@[<h><theory@ %a%a>@]"
François Bobot's avatar
François Bobot committed
690
    save_ident t.theory_name
691
    (save_bool_def "expanded" false) t.theory_expanded;
692
(*
693
  Ident.Slab.iter (save_label fmt) t.theory_name.Ident.id_label;
694
*)
695
  List.iter (save_goal ctxt fmt) t.theory_goals;
François Bobot's avatar
François Bobot committed
696 697
  fprintf fmt "@]@\n</theory>"

698
let save_file ctxt fmt _ f =
699
  fprintf fmt
700
    "@\n@[<v 0>@[<h><file@ name=\"%a\"%a%a>@]"
701
    save_string f.file_name (opt "format")
702
    f.file_format (save_bool_def "expanded" false) f.file_expanded;
703
  List.iter (save_theory ctxt fmt) f.file_theories;
François Bobot's avatar
François Bobot committed
704 705
  fprintf fmt "@]@\n</file>"

706 707 708 709 710 711 712 713 714 715 716 717 718
let save_prover fmt p (timelimits,memlimits) (provers,id) =
  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
719
  fprintf fmt "@\n@[<h><prover@ id=\"%i\"@ name=\"%a\"@ \
720
               version=\"%a\"%a@ timelimit=\"%d\"@ memlimit=\"%d\"/>@]"
MARCHE Claude's avatar
MARCHE Claude committed
721
    id save_string p.C.prover_name save_string p.C.prover_version
722 723
    (fun fmt s -> if s <> "" then fprintf fmt "@ alternative=\"%a\""
        save_string s)
724 725 726
    p.C.prover_altern
    mostfrequent_timelimit mostfrequent_memlimit;
  Mprover.add p (id,mostfrequent_timelimit,mostfrequent_memlimit) provers, id+1
François Bobot's avatar
François Bobot committed
727

728
let save fname shfname _config session =
François Bobot's avatar
François Bobot committed
729
  let ch = open_out fname in
730
  let chsh = Compr.open_out shfname in
François Bobot's avatar
François Bobot committed
731 732
  let fmt = formatter_of_out_channel ch in
  fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
733
  fprintf fmt "<!DOCTYPE why3session PUBLIC \"-//Why3//proof session v5//EN\"@ \"http://why3.lri.fr/why3session.dtd\">@\n";
734 735 736
  (*
    let rel_file = Sysutil.relativize_filename !session_dir_for_save fname in
    fprintf fmt "@[<hov 1><why3session@ name=\"%a\" shape_version=\"%d\">"
737
    save_string rel_file session.session_shape_version;
738
  *)
739
  fprintf fmt "@[<v 0><why3session shape_version=\"%d\">"
740
    session.session_shape_version;
741
  Tc.reset_dict ();
742
  let provers,_ = PHprover.fold (save_prover fmt) (get_used_provers_with_stats session)
François Bobot's avatar
François Bobot committed
743
    (Mprover.empty,0) in
744 745 746
  PHstr.iter
    (save_file { provers = provers; ch_shapes = chsh} fmt)
    session.session_files;
François Bobot's avatar
François Bobot committed
747 748
  fprintf fmt "@]@\n</why3session>";
  fprintf fmt "@.";
749
  close_out ch;
750
  Compr.close_out chsh
François Bobot's avatar
François Bobot committed
751

MARCHE Claude's avatar
MARCHE Claude committed
752
let save_session config session =
François Bobot's avatar
François Bobot committed
753 754
  let f = Filename.concat session.session_dir db_filename in
  Sysutil.backup_file f;
755 756
  let fs = Filename.concat session.session_dir shape_filename in
  Sysutil.backup_file fs;
757 758
  let fz = Filename.concat session.session_dir compressed_shape_filename in
  Sysutil.backup_file fz;
759
  session_dir_for_save := session.session_dir;
760
  let fs = if Compress.compression_supported then fz else fs in
761
  save f fs config session
François Bobot's avatar
François Bobot committed
762 763 764 765 766 767 768

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

769 770
let file_verified f =
  List.for_all (fun t -> t.theory_verified) f.file_theories
François Bobot's avatar
François Bobot committed
771

772 773 774 775 776
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
777

778 779
let metas_verified m = m.metas_goal.goal_verified

François Bobot's avatar
François Bobot committed
780 781 782 783 784 785
let proof_verified a =
  (not a.proof_obsolete) &&
    match a.proof_state with
      | Done { Call_provers.pr_answer = Call_provers.Valid} -> true
      | _ -> false

786
let goal_verified g =
François Bobot's avatar
François Bobot committed
787 788 789 790 791 792 793 794 795
    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;
796 797 798
      Mmetas_args.iter
        (fun _ t -> if t.metas_verified then raise Exit)
        g.goal_metas;
François Bobot's avatar
François Bobot committed
799 800
      false
    with Exit -> true
801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818

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
819 820 821 822 823 824
  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
825
      | Parent_metas t -> check_metas_proved notify t
François Bobot's avatar
François Bobot committed
826 827 828
  end

and check_transf_proved notify t =
829
  let b = transf_verified t in
François Bobot's avatar
François Bobot committed
830 831 832 833 834 835
  if t.transf_verified <> b then begin
    t.transf_verified <- b;
    notify (Transf t);
    check_goal_proved notify t.transf_parent
  end

836 837 838 839 840 841 842 843 844

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
845 846 847 848 849 850 851
(******************************)
(* raw additions to the model *)
(******************************)
type 'a keygen = ?parent:'a -> unit -> 'a

let add_external_proof
    ?(notify=notify)
852
    ~(keygen:'a keygen) ~obsolete
853
    ~archived ~timelimit ~memlimit ~edit (g:'a goal) p result =
854
  assert (edit <> Some "");
François Bobot's avatar
François Bobot committed
855 856 857 858 859
  let key = keygen ~parent:g.goal_key () in
  let a = { proof_prover = p;
            proof_parent = g;
            proof_key = key;
            proof_obsolete = obsolete;
860
            proof_archived = archived;
François Bobot's avatar
François Bobot committed
861 862
            proof_state = result;
            proof_timelimit = timelimit;
863
            proof_memlimit = memlimit;
François Bobot's avatar
François Bobot committed
864 865 866
            proof_edited_as = edit;
          }
  in
867
  PHprover.replace g.goal_external_proofs p a;
François Bobot's avatar
François Bobot committed
868 869 870 871 872 873 874 875 876
  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


877
let set_proof_state ?(notify=notify) ~obsolete ~archived res a =
François Bobot's avatar
François Bobot committed
878 879
  a.proof_state <- res;
  a.proof_obsolete <- obsolete;
880
  a.proof_archived <- archived;
François Bobot's avatar
François Bobot committed
881 882 883
  notify (Proof_attempt a);
  check_goal_proved notify a.proof_parent

884 885 886 887 888 889
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
890

François Bobot's avatar
François Bobot committed
891 892 893
let set_edited_as edited_as a = a.proof_edited_as <- edited_as

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

896 897 898 899 900
let set_obsolete ?(notify=notify) a =
  a.proof_obsolete <- true;
  notify (Proof_attempt a);
  check_goal_proved notify a.proof_parent

901
let set_archived a b = a.proof_archived <- b
902

903
let get_edited_as_abs session pr =
904
  Opt.map (Filename.concat session.session_dir) pr.proof_edited_as
905

François Bobot's avatar
François Bobot committed
906 907 908
(* [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
*)
909
let raw_add_no_task ~(keygen:'a keygen) ~(expanded:bool) parent name expl sum shape =
François Bobot's avatar
François Bobot committed
910 911 912
  let parent_key = match parent with
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
913
    | Parent_metas  mms -> mms.metas_key
François Bobot's avatar
François Bobot committed
914 915 916 917 918 919 920 921 922 923 924
  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;
925
               goal_metas = Mmetas_args.empty;
François Bobot's avatar
François Bobot committed
926
               goal_verified = false;
927
               goal_expanded = expanded;
François Bobot's avatar
François Bobot committed
928 929 930 931
             }
  in
  goal

932
let raw_add_task ~version ~(keygen:'a keygen) ~(expanded:bool) parent name expl t =
François Bobot's avatar
François Bobot committed
933 934 935
  let parent_key = match parent with
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
936
    | Parent_metas  mms -> mms.metas_key
François Bobot's avatar
François Bobot committed
937 938
  in
  let key = keygen ~parent:parent_key () in
939
  let sum = Termcode.task_checksum ~version t in
940 941
  (* 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
942 943 944 945 946 947 948 949 950
  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;
951
               goal_metas = Mmetas_args.empty;
François Bobot's avatar
François Bobot committed
952
               goal_verified = false;
953
               goal_expanded = expanded;
François Bobot's avatar
François Bobot committed
954 955 956 957 958 959 960 961
             }
  in
  goal


(* [raw_add_transformation g name adds a transformation to the given goal g
   Adds no subgoals, thus this should not be exported
*)
962
let raw_add_transformation ~(keygen:'a keygen) ~(expanded:bool) g name =
François Bobot's avatar
François Bobot committed
963 964 965 966 967 968 969
  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 = [];
970
             transf_expanded = expanded;
François Bobot's avatar
François Bobot committed
971 972
           }
  in
973
  PHstr.replace g.goal_transformations name tr;
François Bobot's avatar
François Bobot committed
974 975
  tr

976
let raw_add_metas ~(keygen:'a keygen) ~(expanded:bool) g added idpos =
977 978 979 980 981 982 983 984
  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;
985
             metas_expanded = expanded;
986 987 988 989 990
           }
  in
  g.goal_metas <- Mmetas_args.add added ms g.goal_metas;
  ms

991
let raw_add_theory ~(keygen:'a keygen) ~(expanded:bool) mfile thname =
François Bobot's avatar
François Bobot committed
992 993 994 995 996
  let parent = mfile.file_key in
  let key = keygen ~parent () in
  let mth = { theory_name = thname;
              theory_key = key;
              theory_parent = mfile;
997
              theory_goals = [];
François Bobot's avatar
François Bobot committed
998
              theory_verified = false;
999
              theory_expanded = expanded;
1000
              theory_task = None;
François Bobot's avatar
François Bobot committed
1001 1002 1003 1004
            }
  in
  mth

1005
let raw_add_file ~(keygen:'a keygen) ~(expanded:bool) session f fmt =
François Bobot's avatar
François Bobot committed
1006 1007 1008
  let key = keygen () in
  let mfile = { file_name = f;
                file_key = key;
1009 1010
                file_format = fmt;
                file_theories = [];
François Bobot's avatar
François Bobot committed
1011
                file_verified = false;
1012
                file_expanded = expanded;
François Bobot's avatar
François Bobot committed
1013
                file_parent  = session;
1014
                file_for_recovery = None;
François Bobot's avatar
François Bobot committed
1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035
              }
  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

1036
let int_attribute_def field r def =
François Bobot's avatar
François Bobot committed
1037 1038 1039 1040
  try
    int_of_string (List.assoc field r.Xml.attributes)
  with Not_found | Invalid_argument _ -> def

1041 1042 1043 1044 1045 1046 1047 1048 1049
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
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
let string_attribute_def field r def=
  try
    List.assoc field r.Xml.attributes
  with Not_found -> def

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

let keygen ?parent:_ () = ()

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
1075
            | "outofmemory" -> Call_provers.OutOfMemory
François Bobot's avatar
François Bobot committed
1076
            | "failure" -> Call_provers.Failure ""
1077
            | "highfailure" -> Call_provers.HighFailure
François Bobot's avatar
François Bobot committed
1078 1079 1080
            | s ->
                eprintf
                  "[Warning] Session.load_result: unexpected status '%s'@." s;
1081
                Call_provers.HighFailure
François Bobot's avatar
François Bobot committed
1082 1083 1084 1085 1086 1087 1088 1089 1090
        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 = "";
1091
          Call_provers.pr_status = Unix.WEXITED 0
François Bobot's avatar
François Bobot committed
1092
        }
1093 1094
    | "undone" -> Interrupted
    | "unedited" -> Unedited
François Bobot's avatar
François Bobot committed
1095 1096
    | s ->
        eprintf "[Warning] Session.load_result: unexpected element '%s'@." s;
1097
        Interrupted
François Bobot's avatar
François Bobot committed
1098 1099 1100 1101 1102 1103 1104 1105 1106 1107

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
Andrei Paskevich's avatar
Andrei Paskevich committed
1108 1109
        | {Xml.name = "label"} ->
            let lab = string_attribute "name" label in
1110
            Ident.Slab.add (Ident.create_label lab) acc
François Bobot's avatar
François Bobot committed
1111
        | _ -> acc
1112
    ) Ident.Slab.empty elt.Xml.elements in
François Bobot's avatar
François Bobot committed
1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125
  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

1126 1127
type load_ctxt = {
  old_provers : (Whyconf.prover * int * int) Mstr.t ;
1128
  shapes : ((string, Tc.shape) Hashtbl.t) option
1129 1130 1131
}

let rec load_goal ctxt parent acc g =
François Bobot's avatar
François Bobot committed
1132 1133 1134 1135
  match g.Xml.name with
    | "goal" ->
        let gname = load_ident g in
        let expl = load_option "expl" g in
1136 1137 1138 1139
        let csum = string_attribute_def "sum" g "" in
        let sum = Tc.checksum_of_string csum in
        let shape =
          try Tc.shape_of_string (List.assoc "shape" g.Xml.attributes)
1140 1141 1142 1143 1144 1145 1146 1147
          with Not_found ->
            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 ""
1148
        in
1149
        let expanded = bool_attribute "expanded" g false in