session.ml 92.5 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   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
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

58
59
(* dead code

60
let compare_ident_path x y =
61
  let c = Lists.compare String.compare x.ip_library y.ip_library in
François Bobot's avatar
François Bobot committed
62
  if c <> 0 then -c else (* in order to be bottom up *)
63
  let c = String.compare x.ip_theory y.ip_theory in
François Bobot's avatar
François Bobot committed
64
  if c <> 0 then c else
65
  let c = Lists.compare String.compare x.ip_qualid y.ip_qualid in
66
  c
François Bobot's avatar
François Bobot committed
67
68

module Pos = struct
69
70
  type t = ident_path
  let compare = compare_ident_path
François Bobot's avatar
François Bobot committed
71
72
73
74
  let equal x y = (x : t) = y
  let hash x = Hashtbl.hash (x : t)
end

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

79
*)
François Bobot's avatar
François Bobot committed
80
81
82

type meta_args = meta_arg list

83
module Mmeta_args = Extmap.Make(struct
François Bobot's avatar
François Bobot committed
84
85
86
87
88
89
90
91
92
93
94
95
  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
96
    (* These hash are in fact tag *)
François Bobot's avatar
François Bobot committed
97
98
99
100
101
102
103
104
    | 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)

105
  let compare = Lists.compare compare_meta_arg
François Bobot's avatar
François Bobot committed
106
end)
107
108

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

Andrei Paskevich's avatar
Andrei Paskevich committed
110
111
type metas_args = Smeta_args.t Mstr.t

112
module Mmetas_args = Extmap.Make(struct
François Bobot's avatar
François Bobot committed
113
114
115
116
117
  type t = metas_args
  let compare = Mstr.compare Smeta_args.compare
end)

type idpos = {
118
119
120
  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
121
122
123
124
125
126
127
128
129
}

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

130
(* dead code
François Bobot's avatar
François Bobot committed
131
132
133
134
135
136
137
138
139
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
140
*)
François Bobot's avatar
François Bobot committed
141

François Bobot's avatar
François Bobot committed
142
type 'a goal =
143
144
  { mutable goal_key  : 'a;
    goal_name : Ident.ident;
145
    mutable goal_expl : string option;
146
    goal_parent : 'a goal_parent;
147
    mutable goal_checksum : Tc.checksum option;
148
    mutable goal_shape : Tc.shape;
149
    mutable goal_verified : float option;
150
    mutable goal_task: task_option;
151
152
153
    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
154
    mutable goal_metas : 'a metas Mmetas_args.t;
155
  }
François Bobot's avatar
François Bobot committed
156
157

and 'a proof_attempt =
158
159
160
161
  { proof_key : 'a;
    mutable proof_prover : Whyconf.prover;
    proof_parent : 'a goal;
    mutable proof_state : proof_attempt_status;
162
    mutable proof_limit : Call_provers.resource_limit;
163
164
165
166
    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
François Bobot's avatar
François Bobot committed
171
172
173
174
175
176
177
  | Parent_metas  of 'a metas

and 'a metas =
  { mutable metas_key : 'a;
    metas_added : metas_args;
    metas_idpos : idpos;
    metas_parent : 'a goal;
178
    mutable metas_verified : float option;
François Bobot's avatar
François Bobot committed
179
180
181
182
    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

and 'a transf =
    { mutable transf_key : 'a;
      transf_name : string;
      (** Why3 tranformation name *)
      transf_parent : 'a goal;
189
      mutable transf_verified : float option;
François Bobot's avatar
François Bobot committed
190
191
192
      mutable transf_goals : 'a goal list;
      (** Not mutated after the creation of the session *)
      mutable transf_expanded : bool;
193
      mutable transf_detached : 'a detached option;
François Bobot's avatar
François Bobot committed
194
195
    }

196
197
198
and 'a detached =
    { detached_goals: 'a goal list; }

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

and 'a file =
    { mutable file_key : 'a;
      file_name : string;
214
      file_format : string option;
François Bobot's avatar
François Bobot committed
215
216
217
      file_parent : 'a session;
      mutable file_theories: 'a theory list;
      (** Not mutated after the creation *)
218
      mutable file_verified : float option;
François Bobot's avatar
François Bobot committed
219
      mutable file_expanded : bool;
220
      mutable file_for_recovery : Theory.theory Mstr.t hide;
François Bobot's avatar
François Bobot committed
221
222
223
224
    }

and 'a session =
    { session_files : 'a file PHstr.t;
MARCHE Claude's avatar
MARCHE Claude committed
225
      mutable session_shape_version : int;
226
      session_prover_ids : int PHprover.t;
François Bobot's avatar
François Bobot committed
227
228
229
230
231
232
233
      session_dir   : string; (** Absolute path *)
    }

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

234
type loaded_provers = loaded_prover option PHprover.t
François Bobot's avatar
François Bobot committed
235
236
237

type 'a env_session =
    { env : Env.env;
238
      mutable whyconf : Whyconf.config;
François Bobot's avatar
François Bobot committed
239
      loaded_provers : loaded_provers;
240
      mutable files : Theory.theory Stdlib.Mstr.t Stdlib.Mstr.t;
François Bobot's avatar
François Bobot committed
241
242
      session : 'a session}

243
244
245
246
247
248
249
250
let goal_key g = g.goal_key
let goal_name g = g.goal_name
let goal_verified g = g.goal_verified
let goal_external_proofs g = g.goal_external_proofs
let goal_transformations g = g.goal_transformations
let goal_metas g = g.goal_metas
let goal_expanded g = g.goal_expanded

251
let update_env_session_config e c = e.whyconf <- c
François Bobot's avatar
François Bobot committed
252
253
254
255
256
257
258
259
260
261

(*************************)
(**       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
262
  | Metas of 'a metas
François Bobot's avatar
François Bobot committed
263
264
265

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
266
267
  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
268
269
270
271

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
272
273
274
and metas_iter_proof_attempt f t =
  goal_iter_proof_attempt f t.metas_goal

François Bobot's avatar
François Bobot committed
275
276
277
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
278
279
280
let metas_iter_proof_attempt f m =
  goal_iter_proof_attempt f m.metas_goal

François Bobot's avatar
François Bobot committed
281
282
283
284
285
286
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

287
let iter_proof_attempt f = function
François Bobot's avatar
François Bobot committed
288
289
290
291
292
    | 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
293
    | Metas m -> metas_iter_proof_attempt f m
François Bobot's avatar
François Bobot committed
294
295

let rec goal_iter_leaf_goal ~unproved_only f g =
296
  if not (Opt.inhabited g.goal_verified && unproved_only) then
François Bobot's avatar
François Bobot committed
297
298
299
300
301
302
303
    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

304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
let rec fold_all_sub_goals_of_goal f acc g =
  let acc =
    PHstr.fold
      (fun _ tr acc ->
       List.fold_left (fold_all_sub_goals_of_goal f) acc tr.transf_goals)
      g.goal_transformations acc
  in
  let acc =
    Mmetas_args.fold
      (fun _ m acc ->
       fold_all_sub_goals_of_goal f acc m.metas_goal)
      g.goal_metas acc
  in
  f acc g

let fold_all_sub_goals_of_theory f acc th =
  List.fold_left (fold_all_sub_goals_of_goal f) acc th.theory_goals


François Bobot's avatar
François Bobot committed
323
(** iterators not reccursive *)
François Bobot's avatar
François Bobot committed
324
let iter_goal fp ft fm g =
François Bobot's avatar
François Bobot committed
325
  PHprover.iter (fun _ a -> fp a) g.goal_external_proofs;
François Bobot's avatar
François Bobot committed
326
327
  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
328
329
330
331

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

François Bobot's avatar
François Bobot committed
332
333
let iter_metas f t = f t.metas_goal

334
335
336
let iter_theory f t =
  List.iter f t.theory_goals

337
338
339
340
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
341
let goal_iter f g =
342
343
  PHprover.iter
    (fun _ a -> f (Proof_attempt a)) g.goal_external_proofs;
François Bobot's avatar
François Bobot committed
344
345
346
  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
347
348
349
350

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

François Bobot's avatar
François Bobot committed
351
352
353
let metas_iter f t =
  f (Goal t.metas_goal)

François Bobot's avatar
François Bobot committed
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
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
369
    | Metas m -> metas_iter f m
François Bobot's avatar
François Bobot committed
370
371
372
373
374
375
376
377
378

(** 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
379
        | File f ->
380
          if Opt.inhabited f.file_verified
381
382
383
          then f.file_name
          else f.file_name^"?"
        | Theory th ->
384
          if Opt.inhabited th.theory_verified
385
386
          then th.theory_name.Ident.id_string
          else th.theory_name.Ident.id_string^"?"
François Bobot's avatar
François Bobot committed
387
        | Goal g ->
388
          if Opt.inhabited g.goal_verified
389
390
          then g.goal_name.Ident.id_string
          else g.goal_name.Ident.id_string^"?"
391
        | Proof_attempt pr ->
392
          Pp.sprintf_wnl "%a%s%s%s%s"
393
            Whyconf.print_prover pr.proof_prover
394
395
396
397
            (match pr.proof_state with
              | Done { Call_provers.pr_answer = Call_provers.Valid} -> ""
              | InternalFailure _ -> "!"
              | _ -> "?")
398
399
400
            (if pr.proof_obsolete || pr.proof_archived then " " else "")
            (if pr.proof_obsolete then "O" else "")
            (if pr.proof_archived then "A" else "")
401
        | Transf tr ->
402
          if Opt.inhabited tr.transf_verified
403
          then tr.transf_name
François Bobot's avatar
François Bobot committed
404
405
          else tr.transf_name^"?"
        | Metas metas ->
406
          if Opt.inhabited metas.metas_verified
François Bobot's avatar
François Bobot committed
407
408
409
          then "metas..."
          else "metas..."^"?"
      in
François Bobot's avatar
François Bobot committed
410
411
412
413
414
415
      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;
416
417
418
      (* 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
419
420
      *)
      "",!l
François Bobot's avatar
François Bobot committed
421
422
423
424
425
426
427
428
429
430
431

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
432
433
434
435
436
437
438
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;
439
    session_prover_ids = PHprover.create 7;
MARCHE Claude's avatar
MARCHE Claude committed
440
441
442
443
    session_dir   = dir;
  }

let create_session ?shape_version project_dir =
François Bobot's avatar
François Bobot committed
444
445
  if not (Sys.file_exists project_dir) then
    begin
446
      Debug.dprintf debug
François Bobot's avatar
François Bobot committed
447
448
449
450
        "[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
451
  empty_session ?shape_version project_dir
François Bobot's avatar
François Bobot committed
452
453


454
(* dead code
François Bobot's avatar
François Bobot committed
455
456
457
458
459
460
461
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;
462
    loaded_provers = PHprover.create 5;
François Bobot's avatar
François Bobot committed
463
  }
464
*)
François Bobot's avatar
François Bobot committed
465
466
467
468
469

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

470
(* dead code
François Bobot's avatar
François Bobot committed
471
472
473
474
475
476
477
478
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
479
    | Parent_metas  metas -> get_session_metas metas
François Bobot's avatar
François Bobot committed
480

481

François Bobot's avatar
François Bobot committed
482
483
and get_session_trans transf = get_session_goal transf.transf_parent

François Bobot's avatar
François Bobot committed
484
485
and get_session_metas metas = get_session_goal metas.metas_parent

François Bobot's avatar
François Bobot committed
486
let get_session_proof_attempt pa = get_session_goal pa.proof_parent
487
*)
François Bobot's avatar
François Bobot committed
488

489
let get_used_provers session =
François Bobot's avatar
François Bobot committed
490
  let sprover = ref Sprover.empty in
491
   session_iter_proof_attempt
François Bobot's avatar
François Bobot committed
492
    (fun pa -> sprover := Sprover.add pa.proof_prover !sprover)
493
     session;
François Bobot's avatar
François Bobot committed
494
495
  !sprover

496
497
498
499
500
501
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
502
      let timelimits,steplimits,memlimits =
503
504
        try PHprover.find prover_table prover
        with Not_found ->
505
          let x = (Hashtbl.create 5,Hashtbl.create 5,Hashtbl.create 5) in
506
507
508
          PHprover.add prover_table prover x;
          x
      in
509
510
511
      let lim_time = pa.proof_limit.Call_provers.limit_time in
      let lim_mem = pa.proof_limit.Call_provers.limit_mem in
      let lim_steps = pa.proof_limit.Call_provers.limit_steps in
512
513
514
515
      let tf = try Hashtbl.find timelimits lim_time with Not_found -> 0 in
      let sf = try Hashtbl.find steplimits lim_steps with Not_found -> 0 in
      let mf = try Hashtbl.find memlimits lim_mem with Not_found -> 0 in
      Hashtbl.replace timelimits lim_time (tf+1);
Andrei Paskevich's avatar
Andrei Paskevich committed
516
517
      Hashtbl.replace steplimits lim_steps (sf+1);
      Hashtbl.replace memlimits lim_mem (mf+1))
518
519
520
    session;
  prover_table

François Bobot's avatar
François Bobot committed
521
522
exception NoTask

523
let goal_task g = Opt.get_exn NoTask g.goal_task
François Bobot's avatar
François Bobot committed
524
525
let goal_task_option g = g.goal_task

526
let goal_expl_lazy g =
MARCHE Claude's avatar
MARCHE Claude committed
527
  match g.goal_expl with
528
  | Some s -> s
529
  | None ->
MARCHE Claude's avatar
MARCHE Claude committed
530
531
532
533
534
     match g.goal_task with
     | Some t ->
        let _name,expl,_task = Termcode.goal_expl_task ~root:false t in
        g.goal_expl <- Some expl; expl
     | None -> ""
535
536
537
538
539
540
541

let goal_expl_or_name g =
  let s = goal_expl_lazy g in
  if s <> "" then s else
    try let _,_,l = restore_path g.goal_name in
        String.concat "." l
    with Not_found -> g.goal_name.Ident.id_string
François Bobot's avatar
François Bobot committed
542
543
544
545
546
547
548

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

let db_filename = "why3session.xml"
549
let shape_filename = "why3shapes"
550
let compressed_shape_filename = "why3shapes.gz"
551
let session_dir_for_save = ref "."
François Bobot's avatar
François Bobot committed
552

553
let save_string = Pp.html_string
MARCHE Claude's avatar
MARCHE Claude committed
554

555
556
557
let opt pr lab fmt = function
  | None -> ()
  | Some s -> fprintf fmt "@ %s=\"%a\"" lab pr s
MARCHE Claude's avatar
MARCHE Claude committed
558

François Bobot's avatar
François Bobot committed
559
let save_result fmt r =
560
  let steps = if  r.Call_provers.pr_steps >= 0 then
561
562
563
                Some  r.Call_provers.pr_steps
              else
                None
564
565
  in
  fprintf fmt "<result@ status=\"%s\"@ time=\"%.2f\"%a/>"
François Bobot's avatar
François Bobot committed
566
567
568
569
570
571
    (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"
572
       | Call_provers.OutOfMemory -> "outofmemory"
573
       | Call_provers.StepLimitExceeded -> "steplimitexceeded"
François Bobot's avatar
François Bobot committed
574
575
       | Call_provers.Invalid -> "invalid")
    r.Call_provers.pr_time
576
    (opt pp_print_int "steps") steps
François Bobot's avatar
François Bobot committed
577
578
579

let save_status fmt s =
  match s with
580
    | Unedited ->
581
        fprintf fmt "<unedited/>"
582
    | Scheduled | Running | Interrupted | JustEdited ->
583
        fprintf fmt "<undone/>"
François Bobot's avatar
François Bobot committed
584
    | InternalFailure msg ->
585
        fprintf fmt "<internalfailure@ reason=\"%a\"/>"
MARCHE Claude's avatar
MARCHE Claude committed
586
          save_string (Printexc.to_string msg)
François Bobot's avatar
François Bobot committed
587
588
589
    | Done r -> save_result fmt r


590
591
592
let save_bool_def name def fmt b =
  if b <> def then fprintf fmt "@ %s=\"%b\"" name b

593
594
595
let save_int_def name def fmt n =
  if n <> def then fprintf fmt "@ %s=\"%d\"" name n

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

598
let save_proof_attempt fmt ((id,tl,sl,ml),a) =
François Bobot's avatar
François Bobot committed
599
  fprintf fmt
600
    "@\n@[<h><proof@ prover=\"%i\"%a%a%a%a%a%a>"
601
    id
602
603
604
    (save_int_def "timelimit" tl) (a.proof_limit.Call_provers.limit_time)
    (save_int_def "steplimit" sl) (a.proof_limit.Call_provers.limit_steps)
    (save_int_def "memlimit" ml) (a.proof_limit.Call_provers.limit_mem)
605
    (opt_string "edited") a.proof_edited_as
606
607
    (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
608
  save_status fmt a.proof_state;
609
  fprintf fmt "</proof>@]"
François Bobot's avatar
François Bobot committed
610
611

let save_ident fmt id =
MARCHE Claude's avatar
MARCHE Claude committed
612
613
614
615
616
617
618
  let n=
    try
      let (_,_,l) = Theory.restore_path id in
      String.concat "." l
    with Not_found -> id.Ident.id_string
  in
  fprintf fmt "name=\"%a\"" save_string n
MARCHE Claude's avatar
details    
MARCHE Claude committed
619

620
621
module Compr = Compress.Compress_z

622
type save_ctxt = {
623
  prover_ids : int PHprover.t;
624
  provers : (int * int * int * int) Mprover.t;
625
  ch_shapes : Compr.out_channel;
626
627
}

628
629
630
let save_checksum fmt s =
  fprintf fmt "%s" (Tc.string_of_checksum s)

631
let rec save_goal ctxt fmt g =
632
633
  let shape = Tc.string_of_shape g.goal_shape in
  assert (shape <> "");
François Bobot's avatar
François Bobot committed
634
  fprintf fmt
635
    "@\n@[<v 0>@[<h><goal@ %a%a%a>@]"
François Bobot's avatar
François Bobot committed
636
    save_ident g.goal_name
637
    (opt_string "expl") g.goal_expl
638
    (save_bool_def "expanded" false) g.goal_expanded;
639
640
641
642
643
644
  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;
645
646
647
  Compr.output_char ctxt.ch_shapes ' ';
  Compr.output_string ctxt.ch_shapes shape;
  Compr.output_char ctxt.ch_shapes '\n';
648
(*
649
  Ident.Slab.iter (save_label fmt) g.goal_name.Ident.id_label;
650
*)
651
  let l = PHprover.fold
652
    (fun _ a acc -> (Mprover.find a.proof_prover ctxt.provers, a) :: acc)
653
    g.goal_external_proofs [] in
654
  let l = List.sort (fun ((i1,_,_,_),_) ((i2,_,_,_),_) -> compare i1 i2) l in
655
656
657
  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
658
659
  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
660
661
  fprintf fmt "@]@\n</goal>"

662
and save_trans ctxt fmt t =
663
  fprintf fmt "@\n@[<hov 1>@[<h><transf@ name=\"%a\"%a>@]"
664
    save_string t.transf_name
665
    (save_bool_def "expanded" false) t.transf_expanded;
666
  List.iter (save_goal ctxt fmt) t.transf_goals;
François Bobot's avatar
François Bobot committed
667
668
  fprintf fmt "@]@\n</transf>"

669
and save_metas ctxt fmt _ m =
670
  fprintf fmt "@\n@[<hov 1><metas%a>"
671
    (save_bool_def "expanded" false) m.metas_expanded;
François Bobot's avatar
François Bobot committed
672
  let save_pos fmt pos =
Andrei Paskevich's avatar
Andrei Paskevich committed
673
    fprintf fmt "ip_theory=\"%a\">" save_string pos.ip_theory;
674
    List.iter (fprintf fmt "@\n@[<hov 1><ip_library@ name=\"%a\"/>@]" save_string)
675
      pos.ip_library;
676
    List.iter (fprintf fmt "@\n@[<hov 1><ip_qualid@ name=\"%a\"/>@]" save_string)
677
678
      pos.ip_qualid;
  in
François Bobot's avatar
François Bobot committed
679
  let save_ts_pos fmt ts pos =
680
    fprintf fmt "@\n@[<hov 1><ts_pos@ name=\"%a\"@ arity=\"%i\"@ \
Andrei Paskevich's avatar
Andrei Paskevich committed
681
    id=\"%i\"@ %a@]@\n</ts_pos>"
François Bobot's avatar
François Bobot committed
682
683
684
      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 =
685
    (* TODO: add the signature? *)
686
    fprintf fmt "@\n@[<hov 1><ls_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</ls_pos>"
François Bobot's avatar
François Bobot committed
687
      save_string ls.ls_name.id_string
688
      (ls_hash ls) save_pos pos
François Bobot's avatar
François Bobot committed
689
690
  in
  let save_pr_pos fmt pr pos =
691
    fprintf fmt "@\n@[<hov 1><pr_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</pr_pos>"
François Bobot's avatar
François Bobot committed
692
      save_string pr.pr_name.id_string
693
      (pr_hash pr) save_pos pos
François Bobot's avatar
François Bobot committed
694
695
696
697
698
699
  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;
700
  save_goal ctxt fmt m.metas_goal;
François Bobot's avatar
François Bobot committed
701
702
703
  fprintf fmt "@]@\n</metas>"

and save_meta_args fmt s l =
704
  fprintf fmt "@\n@[<hov 1><meta@ name=\"%a\">" save_string s;
François Bobot's avatar
François Bobot committed
705
  let save_meta_arg fmt = function
706
    | MAty ty -> fprintf fmt "@\n@[<hov 1><meta_arg_ty/>";
François Bobot's avatar
François Bobot committed
707
708
709
      save_ty fmt ty;
      fprintf fmt "@]@\n</meta_arg_ty>"
    | MAts ts ->
710
      fprintf fmt "@\n@[<hov 1><meta_arg_ts@ id=\"%i\"/>@]" (ts_hash ts)
François Bobot's avatar
François Bobot committed
711
    | MAls ls ->
712
      fprintf fmt "@\n@[<hov 1><meta_arg_ls@ id=\"%i\"/>@]" (ls_hash ls)
François Bobot's avatar
François Bobot committed
713
    | MApr pr ->
714
      fprintf fmt "@\n@[<hov 1><meta_arg_pr@ id=\"%i\"/>@]" (pr_hash pr)
François Bobot's avatar
François Bobot committed
715
    | MAstr s ->
716
      fprintf fmt "@\n@[<hov 1><meta_arg_str@ val=\"%s\"/>@]" s
François Bobot's avatar
François Bobot committed
717
    | MAint i ->
718
      fprintf fmt "@\n@[<hov 1><meta_arg_int@ val=\"%i\"/>@]" i
François Bobot's avatar
François Bobot committed
719
720
  in
  List.iter (save_meta_arg fmt) l;
721
  fprintf fmt "@]@\n</meta>"
François Bobot's avatar
François Bobot committed
722
723
724
725

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

732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
module CombinedTheoryChecksum = struct

 let b = Buffer.create 1024

 let f () g =
    match g.goal_checksum with
    | None -> assert false
    | Some c -> Buffer.add_string b (Tc.string_of_checksum c)

 let compute th =
   let () = fold_all_sub_goals_of_theory f () th in
   let c = Tc.buffer_checksum b in
   Buffer.clear b; c

end

748
let save_theory ctxt fmt t =
749
750
  let c = CombinedTheoryChecksum.compute t in
  t.theory_checksum <- Some c;
François Bobot's avatar
François Bobot committed
751
  fprintf fmt
752
    "@\n@[<v 1>@[<h><theory@ %a%a%a>@]"
François Bobot's avatar
François Bobot committed
753
    save_ident t.theory_name
754
    (opt save_checksum "sum") t.theory_checksum
755
    (save_bool_def "expanded" false) t.theory_expanded;
756
  List.iter (save_goal ctxt fmt) t.theory_goals;
François Bobot's avatar
François Bobot committed
757
758
  fprintf fmt "@]@\n</theory>"

759
let save_file ctxt fmt _ f =
760
  fprintf fmt
761
    "@\n@[<v 0>@[<h><file@ name=\"%a\"%a%a>@]"
762
    save_string f.file_name (opt_string "format")
763
    f.file_format (save_bool_def "expanded" false) f.file_expanded;
764
  List.iter (save_theory ctxt fmt) f.file_theories;
François Bobot's avatar
François Bobot committed
765
766
  fprintf fmt "@]@\n</file>"

767
let get_prover_to_save prover_ids p (timelimits,steplimits,memlimits) provers =
768
769
770
771
772
773
  let mostfrequent_timelimit,_ =
    Hashtbl.fold
      (fun t f ((_,f') as t') -> if f > f' then (t,f) else t')
      timelimits
      (0,0)
  in
774
775
776
777
778
779
  let mostfrequent_steplimit,_ =
    Hashtbl.fold
      (fun s f ((_,f') as s') -> if f > f' then (s,f) else s')
      steplimits
      (0,0)
  in
780
781
782
783
784
785
  let mostfrequent_memlimit,_ =
    Hashtbl.fold
      (fun m f ((_,f') as m') -> if f > f' then (m,f) else m')
      memlimits
      (0,0)
  in
786
787
  let id =
    try
788
      PHprover.find prover_ids p
789
790
791
    with Not_found ->
      (* we need to find an unused prover id *)
      let occurs = Hashtbl.create 7 in
792
      PHprover.iter (fun _ n -> Hashtbl.add occurs n ()) prover_ids;
793
      let id = ref 0 in
794
795
      try
        while true do
796
797
798
          try
            let _ = Hashtbl.find occurs !id in incr id
          with Not_found -> raise Exit
799
        done;
800
        assert false
801
      with Exit ->
802
        PHprover.add prover_ids p !id;
803
804
        !id
  in
805
  Mprover.add p (id,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) provers
806
807


808
let save_prover fmt id (p,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) =
809
810
811
  let steplimit =
    if mostfrequent_steplimit < 0 then None else Some mostfrequent_steplimit
  in
812
  fprintf fmt "@\n@[<h><prover@ id=\"%i\"@ name=\"%a\"@ \
813
               version=\"%a\"%a@ timelimit=\"%d\"%a@ memlimit=\"%d\"/>@]"
MARCHE Claude's avatar
MARCHE Claude committed
814
    id save_string p.C.prover_name save_string p.C.prover_version
815
816
    (fun fmt s -> if s <> "" then fprintf fmt "@ alternative=\"%a\""
        save_string s)
817
    p.C.prover_altern
818
819
820
    mostfrequent_timelimit
    (opt pp_print_int "steplimit") steplimit
    mostfrequent_memlimit
François Bobot's avatar
François Bobot committed
821

822
let save fname shfname _config session =
François Bobot's avatar
François Bobot committed
823
  let ch = open_out fname in
824
  let chsh = Compr.open_out shfname in
François Bobot's avatar
François Bobot committed
825
826
  let fmt = formatter_of_out_channel ch in
  fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
827
  fprintf fmt "<!DOCTYPE why3session PUBLIC \"-//Why3//proof session v5//EN\"@ \"http://why3.lri.fr/why3session.dtd\">@\n";
828
829
830
  (*
    let rel_file = Sysutil.relativize_filename !session_dir_for_save fname in
    fprintf fmt "@[<hov 1><why3session@ name=\"%a\" shape_version=\"%d\">"
831
    save_string rel_file session.session_shape_version;
832
  *)
833
  fprintf fmt "@[<v 0><why3session shape_version=\"%d\">"
834
    session.session_shape_version;
835
(*
836
  Tc.reset_dict ();
837
*)
838
  let prover_ids = session.session_prover_ids in
839
  let provers =
840
841
    PHprover.fold (get_prover_to_save prover_ids)
      (get_used_provers_with_stats session) Mprover.empty
842
  in
843
844
  let provers_to_save =
    Mprover.fold
845
846
      (fun p (id,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) acc ->
        Mint.add id (p,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) acc)
847
848
849
850
851
      provers Mint.empty
  in
  Mint.iter (save_prover fmt) provers_to_save;
  let ctxt = { prover_ids = prover_ids; provers = provers; ch_shapes = chsh } in
  PHstr.iter (save_file ctxt fmt) session.session_files;
François Bobot's avatar
François Bobot committed
852
853
  fprintf fmt "@]@\n</why3session>";
  fprintf fmt "@.";
854
  close_out ch;
855
  Compr.close_out chsh
François Bobot's avatar
François Bobot committed
856

MARCHE Claude's avatar
MARCHE Claude committed
857
let save_session config session =
François Bobot's avatar
François Bobot committed
858
859
  let f = Filename.concat session.session_dir db_filename in
  Sysutil.backup_file f;
860
861
  let fs = Filename.concat session.session_dir shape_filename in
  Sysutil.backup_file fs;
862
863
  let fz = Filename.concat session.session_dir compressed_shape_filename in
  Sysutil.backup_file fz;
864
  session_dir_for_save := session.session_dir;
865
  let fs = if Compress.compression_supported then fz else fs in
866
  save f fs config session
François Bobot's avatar
François Bobot committed
867
868
869
870
871
872
873

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

874
let compute_verified get l =
875
  List.fold_left (fun acc t ->
876
877
878
879
    match acc,get t with
    | Some x, Some y -> Some (x +. y)
    | _ -> None) (Some 0.0) l

880
let file_verified f =
881
  compute_verified (fun t -> t.theory_verified) f.file_theories
François Bobot's avatar
François Bobot committed
882

883
let theory_verified t =
884
  compute_verified (fun g -> g.goal_verified) t.theory_goals
885
886

let transf_verified t =
887
  compute_verified (fun g -> g.goal_verified) t.transf_goals
François Bobot's avatar
François Bobot committed
888

François Bobot's avatar
François Bobot committed
889
890
let metas_verified m = m.metas_goal.goal_verified

François Bobot's avatar
François Bobot committed
891
let proof_verified a =
892
  if a.proof_obsolete then None else
François Bobot's avatar
François Bobot committed
893
    match a.proof_state with
894
895
896
      | Done { Call_provers.pr_answer = Call_provers.Valid;
               Call_provers.pr_time = t } -> Some t
      | _ -> None
François Bobot's avatar
François Bobot committed
897

898
let check_goal_verified g =
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
  let acc = ref None in
  let accumulate v =
    match v with
    | None -> ()
    | Some t ->
      match !acc with
      | Some x -> acc := Some (x +. t)
      | None -> acc := v
  in
  PHprover.iter
    (fun _ a -> accumulate (proof_verified a))
    g.goal_external_proofs;
  PHstr.iter
    (fun _ t -> accumulate t.transf_verified)
    g.goal_transformations;
  Mmetas_args.iter
      (fun _ t -> accumulate t.metas_verified)
    g.goal_metas;
  !acc
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934

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 =
935
  let b = check_goal_verified g in
François Bobot's avatar
François Bobot committed
936
937
938
939
940
941
  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
942
      | Parent_metas t -> check_metas_proved notify t
François Bobot's avatar
François Bobot committed
943
944
945
  end

and check_transf_proved notify t =
946
  let b = transf_verified t in
François Bobot's avatar
François Bobot committed
947
948
949
950
951
952
  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
953
954
955
956
957
958
959
960
961

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
962
963
964
965
966
967
968
(******************************)
(* raw additions to the model *)
(******************************)
type 'a keygen = ?parent:'a -> unit -> 'a

let add_external_proof
    ?(notify=notify)
969
    ~(keygen:'a keygen) ~obsolete
970
    ~archived ~limit ~edit (g:'a goal) p result =
971
  assert (edit <> Some "");
François Bobot's avatar
François Bobot committed
972
973
974
975
976
  let key = keygen ~parent:g.goal_key () in
  let a = { proof_prover = p;
            proof_parent = g;
            proof_key = key;
            proof_obsolete = obsolete;
977
            proof_archived = archived;
François Bobot's avatar
François Bobot committed
978
            proof_state = result;
979
            proof_limit = limit;
François Bobot's avatar
François Bobot committed
980
981
982
            proof_edited_as = edit;
          }
  in
983
  PHprover.replace g.goal_external_proofs p a;
François Bobot's avatar
François Bobot committed
984
985
986
987
988
989
990
991
992
  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


993
let set_proof_state ?(notify=notify) ~obsolete ~archived res a =
François Bobot's avatar
François Bobot committed
994
995
  a.proof_state <- res;
  a.proof_obsolete <- obsolete;
996
  a.proof_archived <- archived;
François Bobot's avatar
François Bobot committed
997
998
999
  notify (Proof_attempt a);
  check_goal_proved notify a.proof_parent