session.ml 86.9 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
François Bobot's avatar
François Bobot committed
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;
François Bobot's avatar
François Bobot committed
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
François Bobot's avatar
François Bobot committed
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
François Bobot's avatar
François Bobot committed
62
  if c <> 0 then c else
63
  let c = Lists.compare String.compare x.ip_qualid y.ip_qualid in
64
  c
François Bobot's avatar
François Bobot committed
65 66

module Pos = struct
67 68
  type t = ident_path
  let compare = compare_ident_path
François Bobot's avatar
François Bobot committed
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)
François Bobot's avatar
François Bobot committed
76 77 78

type meta_args = meta_arg list

79
module Mmeta_args = Extmap.Make(struct
François Bobot's avatar
François Bobot committed
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
François Bobot's avatar
François Bobot committed
102
end)
103 104

module Smeta_args = Extset.MakeOfMap(Mmeta_args)
François Bobot's avatar
François Bobot committed
105

Andrei Paskevich's avatar
Andrei Paskevich committed
106 107
type metas_args = Smeta_args.t Mstr.t

108
module Mmetas_args = Extmap.Make(struct
François Bobot's avatar
François Bobot committed
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;
François Bobot's avatar
François Bobot committed
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
François Bobot's avatar
François Bobot committed
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
*)
François Bobot's avatar
François Bobot committed
137

MARCHE Claude's avatar
MARCHE Claude committed
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;
MARCHE Claude's avatar
MARCHE Claude committed
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;
François Bobot's avatar
François Bobot committed
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
François Bobot's avatar
François Bobot committed
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
François Bobot's avatar
François Bobot committed
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;
François Bobot's avatar
François Bobot committed
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

François Bobot's avatar
François Bobot committed
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

François Bobot's avatar
François Bobot committed
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
François Bobot's avatar
François Bobot committed
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 *)
François Bobot's avatar
François Bobot committed
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;
François Bobot's avatar
François Bobot committed
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

François Bobot's avatar
François Bobot committed
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;
François Bobot's avatar
François Bobot committed
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

François Bobot's avatar
François Bobot committed
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
François Bobot's avatar
François Bobot committed
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
François Bobot's avatar
François Bobot committed
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
François Bobot's avatar
François Bobot committed
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

François Bobot's avatar
François Bobot committed
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

MARCHE Claude's avatar
MARCHE Claude committed
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\"/>"
MARCHE Claude's avatar
MARCHE Claude committed
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 =
MARCHE Claude's avatar
MARCHE Claude committed
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
MARCHE Claude's avatar
MARCHE Claude committed
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%a>@]"
François Bobot's avatar
François Bobot committed
602
    save_ident g.goal_name
603 604
    (opt_string "expl") g.goal_expl
    (opt save_checksum "sum") g.goal_checksum
605
    (save_bool_def "expanded" false) g.goal_expanded;
606 607 608 609 610 611
  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;
612 613 614
  Compr.output_char ctxt.ch_shapes ' ';
  Compr.output_string ctxt.ch_shapes shape;
  Compr.output_char ctxt.ch_shapes '\n';
615
(*
616
  Ident.Slab.iter (save_label fmt) g.goal_name.Ident.id_label;
617
*)
618
  let l = PHprover.fold
619
    (fun _ a acc -> (Mprover.find a.proof_prover ctxt.provers, a) :: acc)
620
    g.goal_external_proofs [] in
621
  let l = List.sort (fun ((i1,_,_),_) ((i2,_,_),_) -> compare i1 i2) l in
622 623 624
  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
625 626
  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
627 628
  fprintf fmt "@]@\n</goal>"

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

636
and save_metas ctxt fmt _ m =
637
  fprintf fmt "@\n@[<hov 1><metas%a>"
638
    (save_bool_def "expanded" false) m.metas_expanded;
François Bobot's avatar
François Bobot committed
639
  let save_pos fmt pos =
Andrei Paskevich's avatar
Andrei Paskevich committed
640
    fprintf fmt "ip_theory=\"%a\">" save_string pos.ip_theory;
641
    List.iter (fprintf fmt "@\n@[<hov 1><ip_library@ name=\"%a\"/>@]" save_string)
642
      pos.ip_library;
643
    List.iter (fprintf fmt "@\n@[<hov 1><ip_qualid@ name=\"%a\"/>@]" save_string)
644 645
      pos.ip_qualid;
  in
François Bobot's avatar
François Bobot committed
646
  let save_ts_pos fmt ts pos =
647
    fprintf fmt "@\n@[<hov 1><ts_pos@ name=\"%a\"@ arity=\"%i\"@ \
Andrei Paskevich's avatar
Andrei Paskevich committed
648
    id=\"%i\"@ %a@]@\n</ts_pos>"
François Bobot's avatar
François Bobot committed
649 650 651 652
      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? *)
653
    fprintf fmt "@\n@[<hov 1><ls_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</ls_pos>"
François Bobot's avatar
François Bobot committed
654
      save_string ls.ls_name.id_string
655
      (ls_hash ls) save_pos pos
François Bobot's avatar
François Bobot committed
656 657
  in
  let save_pr_pos fmt pr pos =
658
    fprintf fmt "@\n@[<hov 1><pr_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</pr_pos>"
François Bobot's avatar
François Bobot committed
659
      save_string pr.pr_name.id_string
660
      (pr_hash pr) save_pos pos
François Bobot's avatar
François Bobot committed
661 662 663 664 665 666
  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;
667
  save_goal ctxt fmt m.metas_goal;
François Bobot's avatar
François Bobot committed
668 669 670
  fprintf fmt "@]@\n</metas>"

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

and save_ty fmt ty =
  match ty.ty_node with
  | Tyvar tv ->
693
    fprintf fmt "@\n@[<hov 1><ty_var@ id=\"%i\"/>@]" (tv_hash tv)
François Bobot's avatar
François Bobot committed
694
  | Tyapp (ts,l) ->
695
    fprintf fmt "@\n@[<hov 1><ty_app@ id=\"%i\"/>" (ts_hash ts);
François Bobot's avatar
François Bobot committed
696 697 698
    List.iter (save_ty fmt) l;
    fprintf fmt "@]@\n</ty_app>"

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

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

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

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

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

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

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

812 813 814 815 816
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
817

François Bobot's avatar
François Bobot committed
818 819
let metas_verified m = m.metas_goal.goal_verified

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

826
let goal_verified g =
François Bobot's avatar
François Bobot committed
827 828 829 830 831 832 833 834 835
    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;
François Bobot's avatar
François Bobot committed
836 837 838
      Mmetas_args.iter
        (fun _ t -> if t.metas_verified then raise Exit)
        g.goal_metas;
François Bobot's avatar
François Bobot committed
839 840
      false
    with Exit -> true
841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858

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
859 860 861 862 863 864
  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
François Bobot's avatar
François Bobot committed
865
      | Parent_metas t -> check_metas_proved notify t
François Bobot's avatar
François Bobot committed
866 867 868
  end

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

François Bobot's avatar
François Bobot committed
876 877 878 879 880 881 882 883 884

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
885 886 887 888 889 890 891
(******************************)
(* raw additions to the model *)
(******************************)
type 'a keygen = ?parent:'a -> unit -> 'a

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


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

924 925 926 927 928 929
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
930

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

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

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

941
let set_archived a b = a.proof_archived <- b
942

943
let get_edited_as_abs session pr =
944
  Opt.map (Filename.concat session.session_dir) pr.proof_edited_as
945

François Bobot's avatar
François Bobot committed
946 947 948
(* [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
*)
949
let raw_add_no_task ~(keygen:'a keygen) ~(expanded:bool) parent name expl sum shape =
François Bobot's avatar
François Bobot committed
950 951 952
  let parent_key