session.ml 50.3 KB
Newer Older
François Bobot's avatar
François Bobot committed
1
2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
François Bobot's avatar
François Bobot committed
4
5
6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
François Bobot's avatar
François Bobot committed
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Stdlib
open Debug
23
open Util
François Bobot's avatar
François Bobot committed
24

25
26
27
28
module Mprover = Whyconf.Mprover
module Sprover = Whyconf.Sprover
module PHprover = Whyconf.Hprover
module C = Whyconf
29
module Tc = Termcode
30

François Bobot's avatar
François Bobot committed
31
let debug = Debug.register_flag "session"
32
  ~desc:"About the why3 session creation, reading and writing."
François Bobot's avatar
François Bobot committed
33
34
35
36
37
38
39
40
41
42

(** {2 Type definitions} *)

module PHstr = Util.Hstr

type undone_proof =
    | Scheduled (** external proof attempt is scheduled *)
    | Interrupted
    | Running (** external proof attempt is in progress *)
    | Unedited
43
    | JustEdited
François Bobot's avatar
François Bobot committed
44
45
46
47
48
49
50
51
52

type proof_attempt_status =
    | Undone of undone_proof
    | Done of Call_provers.prover_result (** external proof done *)
    | InternalFailure of exn (** external proof aborted by internal error *)

type task_option = Task.task option

type 'a goal =
53
54
55
56
57
58
59
60
61
62
63
64
  { mutable goal_key  : 'a;
    goal_name : Ident.ident;
    goal_expl : string option;
    goal_parent : 'a goal_parent;
    mutable goal_checksum : Tc.checksum;
    mutable goal_shape : Tc.shape;
    mutable goal_verified : bool;
    goal_task: task_option;
    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
65
66

and 'a proof_attempt =
67
68
69
70
71
72
73
74
75
76
  { 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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104

and 'a goal_parent =
  | Parent_theory of 'a theory
  | Parent_transf of 'a transf

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;
    }

and 'a file =
    { mutable file_key : 'a;
      file_name : string;
105
      file_format : string option;
François Bobot's avatar
François Bobot committed
106
107
108
109
110
111
112
113
114
      file_parent : 'a session;
      mutable file_theories: 'a theory list;
      (** Not mutated after the creation *)
      mutable file_verified : bool;
      mutable file_expanded : bool;
    }

and 'a session =
    { session_files : 'a file PHstr.t;
MARCHE Claude's avatar
MARCHE Claude committed
115
      mutable session_shape_version : int;
François Bobot's avatar
François Bobot committed
116
117
118
119
120
121
122
      session_dir   : string; (** Absolute path *)
    }

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

123
type loaded_provers = loaded_prover option PHprover.t
François Bobot's avatar
François Bobot committed
124
125
126

type 'a env_session =
    { env : Env.env;
127
      mutable whyconf : Whyconf.config;
François Bobot's avatar
François Bobot committed
128
129
130
      loaded_provers : loaded_provers;
      session : 'a session}

131
let update_env_session_config e c = e.whyconf <- c
François Bobot's avatar
François Bobot committed
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183

(*************************)
(**       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

let rec goal_iter_proof_attempt f g =
  PHprover.iter (fun _ a -> f a) g.goal_external_proofs;
  PHstr.iter (fun _ t -> transf_iter_proof_attempt f t) g.goal_transformations

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

let theory_iter_proof_attempt f t =
  List.iter (goal_iter_proof_attempt f) t.theory_goals

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

let rec iter_proof_attempt f = function
    | 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

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 *)
let iter_goal fp ft g =
  PHprover.iter (fun _ a -> fp a) g.goal_external_proofs;
  PHstr.iter (fun _ t -> ft t) g.goal_transformations

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

let goal_iter f g =
184
185
  PHprover.iter
    (fun _ a -> f (Proof_attempt a)) g.goal_external_proofs;
François Bobot's avatar
François Bobot committed
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
  PHstr.iter (fun _ t -> f (Transf t)) g.goal_transformations

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

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

(** 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
215
216
217
218
219
220
221
222
        | 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
223
        | Goal g ->
224
225
226
          if g.goal_verified
          then g.goal_name.Ident.id_string
          else g.goal_name.Ident.id_string^"?"
227
        | Proof_attempt pr ->
228
          Pp.sprintf_wnl "%a%s%s%s%s"
229
            Whyconf.print_prover pr.proof_prover
230
231
232
233
            (match pr.proof_state with
              | Done { Call_provers.pr_answer = Call_provers.Valid} -> ""
              | InternalFailure _ -> "!"
              | _ -> "?")
234
235
236
            (if pr.proof_obsolete || pr.proof_archived then " " else "")
            (if pr.proof_obsolete then "O" else "")
            (if pr.proof_archived then "A" else "")
237
238
239
240
        | Transf tr ->
          if tr.transf_verified
          then tr.transf_name
          else tr.transf_name^"?" in
François Bobot's avatar
François Bobot committed
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
      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;
      Filename.basename s.session_dir,!l

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
259
260
261
262
263
264
265
266
267
268
269
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
270
271
272
273
274
275
276
  if not (Sys.file_exists project_dir) then
    begin
      dprintf debug
        "[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
277
  empty_session ?shape_version project_dir
François Bobot's avatar
François Bobot committed
278
279
280
281
282
283
284
285
286


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;
287
    loaded_provers = PHprover.create 5;
François Bobot's avatar
François Bobot committed
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
  }

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

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

and get_session_trans transf = get_session_goal transf.transf_parent

let get_session_proof_attempt pa = get_session_goal pa.proof_parent

307
let get_used_provers session =
François Bobot's avatar
François Bobot committed
308
309
310
311
312
313
314
315
316
317
318
  let sprover = ref Sprover.empty in
  session_iter_proof_attempt
    (fun pa -> sprover := Sprover.add pa.proof_prover !sprover)
    session;
  !sprover

exception NoTask

let goal_task g = Util.exn_option NoTask g.goal_task
let goal_task_option g = g.goal_task

319
let goal_expl g = Util.def_option g.goal_name.Ident.id_string g.goal_expl
François Bobot's avatar
François Bobot committed
320
321
322
323
324
325
326
327

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

let db_filename = "why3session.xml"

MARCHE Claude's avatar
MARCHE Claude committed
328
329
330
331
332
333
334
335
336
337
338
339
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
340
341
342
343
344
345
346
347
let save_result fmt r =
  fprintf fmt "@\n<result status=\"%s\" time=\"%.2f\"/>"
    (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"
348
       | Call_provers.OutOfMemory -> "outofmemory"
François Bobot's avatar
François Bobot committed
349
350
351
352
353
354
355
356
357
358
       | Call_provers.Invalid -> "invalid")
    r.Call_provers.pr_time

let save_status fmt s =
  match s with
    | Undone Unedited ->
        fprintf fmt "<unedited/>@\n"
    | Undone _ ->
        fprintf fmt "<undone/>@\n"
    | InternalFailure msg ->
MARCHE Claude's avatar
MARCHE Claude committed
359
360
        fprintf fmt "<internalfailure reason=\"%a\"/>@\n"
          save_string (Printexc.to_string msg)
François Bobot's avatar
François Bobot committed
361
362
363
364
365
    | Done r -> save_result fmt r


let opt lab fmt = function
  | None -> ()
MARCHE Claude's avatar
MARCHE Claude committed
366
  | Some s -> fprintf fmt "%s=\"%a\"@ " lab save_string s
François Bobot's avatar
François Bobot committed
367
368
369

let save_proof_attempt provers fmt _key a =
  fprintf fmt
370
371
    "@\n@[<v 1><proof@ prover=\"%i\"@ timelimit=\"%d\"@ \
memlimit=\"%d\"@ %aobsolete=\"%b\"@ archived=\"%b\">"
François Bobot's avatar
François Bobot committed
372
    (Mprover.find a.proof_prover provers) a.proof_timelimit
373
    a.proof_memlimit
374
375
    (opt "edited") a.proof_edited_as a.proof_obsolete
    a.proof_archived;
François Bobot's avatar
François Bobot committed
376
377
378
379
  save_status fmt a.proof_state;
  fprintf fmt "@]@\n</proof>"

let save_ident fmt id =
MARCHE Claude's avatar
MARCHE Claude committed
380
  fprintf fmt "name=\"%a\"" save_string id.Ident.id_string;
François Bobot's avatar
François Bobot committed
381
382
383
384
385
  match id.Ident.id_loc with
    | None -> ()
    | Some loc ->
      let file,lnum,cnumb,cnume = Loc.get loc in
      fprintf fmt
MARCHE Claude's avatar
MARCHE Claude committed
386
387
        "@ locfile=\"%a\"@ loclnum=\"%i\" loccnumb=\"%i\" loccnume=\"%i\""
        save_string file lnum cnumb cnume
François Bobot's avatar
François Bobot committed
388
389

let save_label fmt s =
MARCHE Claude's avatar
MARCHE Claude committed
390
  fprintf fmt "@\n@[<v 1><label@ name=\"%a\"/>@]" save_string s.Ident.lab_string
391

François Bobot's avatar
François Bobot committed
392
let rec save_goal provers fmt g =
393
  assert (Tc.string_of_shape g.goal_shape <> "");
François Bobot's avatar
François Bobot committed
394
  fprintf fmt
MARCHE Claude's avatar
MARCHE Claude committed
395
    "@\n@[<v 1><goal@ %a@ %asum=\"%a\"@ proved=\"%b\"@ \
396
expanded=\"%b\"@ shape=\"%a\">"
François Bobot's avatar
François Bobot committed
397
398
    save_ident g.goal_name
    (opt "expl") g.goal_expl
399
400
401
    save_string (Tc.string_of_checksum g.goal_checksum)
    g.goal_verified  g.goal_expanded
    save_string (Tc.string_of_shape g.goal_shape);
402
  Ident.Slab.iter (save_label fmt) g.goal_name.Ident.id_label;
François Bobot's avatar
François Bobot committed
403
404
405
406
407
  PHprover.iter (save_proof_attempt provers fmt) g.goal_external_proofs;
  PHstr.iter (save_trans provers fmt) g.goal_transformations;
  fprintf fmt "@]@\n</goal>"

and save_trans provers fmt _ t =
MARCHE Claude's avatar
MARCHE Claude committed
408
409
  fprintf fmt "@\n@[<v 1><transf@ name=\"%a\"@ proved=\"%b\"@ expanded=\"%b\">"
    save_string t.transf_name t.transf_verified t.transf_expanded;
François Bobot's avatar
François Bobot committed
410
411
412
413
414
415
416
417
  List.iter (save_goal provers fmt) t.transf_goals;
  fprintf fmt "@]@\n</transf>"

let save_theory provers fmt t =
  fprintf fmt
    "@\n@[<v 1><theory@ %a@ verified=\"%b\"@ expanded=\"%b\">"
    save_ident t.theory_name
    t.theory_verified t.theory_expanded;
418
  Ident.Slab.iter (save_label fmt) t.theory_name.Ident.id_label;
François Bobot's avatar
François Bobot committed
419
420
421
422
  List.iter (save_goal provers fmt) t.theory_goals;
  fprintf fmt "@]@\n</theory>"

let save_file provers fmt _ f =
423
424
425
426
  fprintf fmt
    "@\n@[<v 1><file@ name=\"%a\"@ %averified=\"%b\"@ expanded=\"%b\">"
    save_string f.file_name (opt "format")
    f.file_format f.file_verified f.file_expanded;
François Bobot's avatar
François Bobot committed
427
428
429
430
  List.iter (save_theory provers fmt) f.file_theories;
  fprintf fmt "@]@\n</file>"

let save_prover fmt p (provers,id) =
431
  fprintf fmt "@\n@[<v 1><prover@ id=\"%i\"@ \
MARCHE Claude's avatar
MARCHE Claude committed
432
433
name=\"%a\"@ version=\"%a\"%a/>@]"
    id save_string p.C.prover_name save_string p.C.prover_version
434
435
    (fun fmt s -> if s <> "" then fprintf fmt "@ alternative=\"%a\""
        save_string s)
436
    p.C.prover_altern;
François Bobot's avatar
François Bobot committed
437
438
  Mprover.add p id provers, id+1

MARCHE Claude's avatar
MARCHE Claude committed
439
let save fname config session =
François Bobot's avatar
François Bobot committed
440
441
442
  let ch = open_out fname in
  let fmt = formatter_of_out_channel ch in
  fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
MARCHE Claude's avatar
MARCHE Claude committed
443
  fprintf fmt "<!DOCTYPE why3session SYSTEM \"%a\">@\n"
444
445
    save_string (Filename.concat (Whyconf.datadir (Whyconf.get_main config))
                   "why3session.dtd");
MARCHE Claude's avatar
MARCHE Claude committed
446
447
  fprintf fmt "@[<v 1><why3session@ name=\"%a\" shape_version=\"%d\">"
    save_string fname session.session_shape_version;
448
  let provers,_ = Sprover.fold (save_prover fmt) (get_used_provers session)
François Bobot's avatar
François Bobot committed
449
450
451
452
453
454
    (Mprover.empty,0) in
  PHstr.iter (save_file provers fmt) session.session_files;
  fprintf fmt "@]@\n</why3session>";
  fprintf fmt "@.";
  close_out ch

MARCHE Claude's avatar
MARCHE Claude committed
455
let save_session config session =
François Bobot's avatar
François Bobot committed
456
457
  let f = Filename.concat session.session_dir db_filename in
  Sysutil.backup_file f;
MARCHE Claude's avatar
MARCHE Claude committed
458
  save f config session
François Bobot's avatar
François Bobot committed
459
460
461
462
463
464
465
466
467
468

(*******************************)
(*          explanations       *)
(*******************************)

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

exception Found of string

let check_expl lab =
Andrei Paskevich's avatar
Andrei Paskevich committed
469
  let lab = lab.Ident.lab_string in
François Bobot's avatar
François Bobot committed
470
471
472
473
  if Str.string_match expl_regexp lab 0 then
    raise (Found (Str.matched_group 1 lab))

let rec get_expl_fmla f =
474
  Ident.Slab.iter check_expl f.Term.t_label;
François Bobot's avatar
François Bobot committed
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
  (match f.Term.t_node with
    | Term.Tbinop(Term.Timplies,_,f) -> get_expl_fmla f
    | Term.Tquant(Term.Tforall,fq) ->
      let (_,_,f) = Term.t_open_quant fq in get_expl_fmla f
    | Term.Tlet(_,fb) ->
      let (_,f) = Term.t_open_bound fb in get_expl_fmla f
    | Term.Tcase(_,[fb]) ->
      let (_,f) = Term.t_open_branch fb in get_expl_fmla f
    | _ -> ())

type expl = string option

let get_explanation id task =
  let fmla = Task.task_goal_fmla task in
  try
    get_expl_fmla fmla;
491
    Ident.Slab.iter check_expl id.Ident.id_label;
François Bobot's avatar
François Bobot committed
492
493
494
495
496
497
498
499
500
501
    None
  with Found e -> Some e


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

502
503
let file_verified f =
  List.for_all (fun t -> t.theory_verified) f.file_theories
François Bobot's avatar
François Bobot committed
504

505
506
507
508
509
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
510
511
512
513
514
515
516

let proof_verified a =
  (not a.proof_obsolete) &&
    match a.proof_state with
      | Done { Call_provers.pr_answer = Call_provers.Valid} -> true
      | _ -> false

517
let goal_verified g =
François Bobot's avatar
François Bobot committed
518
519
520
521
522
523
524
525
526
527
528
    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;
      false
    with Exit -> true
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546

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
547
548
549
550
551
552
553
554
555
  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
  end

and check_transf_proved notify t =
556
  let b = transf_verified t in
François Bobot's avatar
François Bobot committed
557
558
559
560
561
562
563
564
565
566
567
568
569
  if t.transf_verified <> b then begin
    t.transf_verified <- b;
    notify (Transf t);
    check_goal_proved notify t.transf_parent
  end

(******************************)
(* raw additions to the model *)
(******************************)
type 'a keygen = ?parent:'a -> unit -> 'a

let add_external_proof
    ?(notify=notify)
570
    ~(keygen:'a keygen) ~obsolete
571
    ~archived ~timelimit ~memlimit ~edit (g:'a goal) p result =
572
  assert (edit <> Some "");
François Bobot's avatar
François Bobot committed
573
574
575
576
577
  let key = keygen ~parent:g.goal_key () in
  let a = { proof_prover = p;
            proof_parent = g;
            proof_key = key;
            proof_obsolete = obsolete;
578
            proof_archived = archived;
François Bobot's avatar
François Bobot committed
579
580
            proof_state = result;
            proof_timelimit = timelimit;
581
            proof_memlimit = memlimit;
François Bobot's avatar
François Bobot committed
582
583
584
            proof_edited_as = edit;
          }
  in
585
  PHprover.replace g.goal_external_proofs p a;
François Bobot's avatar
François Bobot committed
586
587
588
589
590
591
592
593
594
  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


595
let set_proof_state ?(notify=notify) ~obsolete ~archived res a =
François Bobot's avatar
François Bobot committed
596
597
  a.proof_state <- res;
  a.proof_obsolete <- obsolete;
598
  a.proof_archived <- archived;
François Bobot's avatar
François Bobot committed
599
600
601
  notify (Proof_attempt a);
  check_goal_proved notify a.proof_parent

602
603
604
605
606
607
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
608

François Bobot's avatar
François Bobot committed
609
610
611
let set_edited_as edited_as a = a.proof_edited_as <- edited_as

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

614
615
616
617
618
let set_obsolete ?(notify=notify) a =
  a.proof_obsolete <- true;
  notify (Proof_attempt a);
  check_goal_proved notify a.proof_parent

619
let set_archived a b = a.proof_archived <- b
620

621
622
623
let get_edited_as_abs session pr =
  option_map (Filename.concat session.session_dir) pr.proof_edited_as

François Bobot's avatar
François Bobot committed
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
(* [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
*)
let raw_add_no_task ~(keygen:'a keygen) parent name expl sum shape exp =
  let parent_key = match parent with
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
  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;
               goal_verified = false;
               goal_expanded = exp;
             }
  in
  goal

648
let raw_add_task ~version ~(keygen:'a keygen) parent name expl t exp =
François Bobot's avatar
François Bobot committed
649
650
651
652
653
  let parent_key = match parent with
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
  in
  let key = keygen ~parent:parent_key () in
654
655
  let sum = Termcode.task_checksum ~version t in
  let shape = Termcode.t_shape_buf ~version
656
    (Task.task_goal_fmla t) in
François Bobot's avatar
François Bobot committed
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
  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;
               goal_verified = false;
               goal_expanded = exp;
             }
  in
  goal


(* [raw_add_transformation g name adds a transformation to the given goal g
   Adds no subgoals, thus this should not be exported
*)
let raw_add_transformation ~(keygen:'a keygen) g name exp =
  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 = [];
             transf_expanded = exp;
           }
  in
687
  PHstr.replace g.goal_transformations name tr;
François Bobot's avatar
François Bobot committed
688
689
690
691
692
693
694
695
  tr

let raw_add_theory ~(keygen:'a keygen) mfile thname exp =
  let parent = mfile.file_key in
  let key = keygen ~parent () in
  let mth = { theory_name = thname;
              theory_key = key;
              theory_parent = mfile;
696
              theory_goals = [];
François Bobot's avatar
François Bobot committed
697
698
699
700
701
702
              theory_verified = false;
              theory_expanded = exp;
            }
  in
  mth

703
let raw_add_file ~(keygen:'a keygen) session f fmt exp =
François Bobot's avatar
François Bobot committed
704
705
706
  let key = keygen () in
  let mfile = { file_name = f;
                file_key = key;
707
708
                file_format = fmt;
                file_theories = [];
François Bobot's avatar
François Bobot committed
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
                file_verified = false;
                file_expanded = exp;
                file_parent  = session;
              }
  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

let int_attribute field r def =
  try
    int_of_string (List.assoc field r.Xml.attributes)
  with Not_found | Invalid_argument _ -> def

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
763
            | "outofmemory" -> Call_provers.OutOfMemory
François Bobot's avatar
François Bobot committed
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
            | "failure" -> Call_provers.Failure ""
            | "highfailure" -> Call_provers.Failure ""
            | s ->
                eprintf
                  "[Warning] Session.load_result: unexpected status '%s'@." s;
                Call_provers.Failure ""
        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 = "";
779
          Call_provers.pr_status = Unix.WEXITED 0
François Bobot's avatar
François Bobot committed
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
        }
    | "undone" -> Undone Interrupted
    | "unedited" -> Undone Unedited
    | s ->
        eprintf "[Warning] Session.load_result: unexpected element '%s'@." s;
        Undone Interrupted

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
796
797
        | {Xml.name = "label"} ->
            let lab = string_attribute "name" label in
798
            Ident.Slab.add (Ident.create_label lab) acc
François Bobot's avatar
François Bobot committed
799
        | _ -> acc
800
    ) Ident.Slab.empty elt.Xml.elements in
François Bobot's avatar
François Bobot committed
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
  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

let rec load_goal ~old_provers parent acc g =
  match g.Xml.name with
    | "goal" ->
        let gname = load_ident g in
        let expl = load_option "expl" g in
819
820
        let sum = Tc.checksum_of_string (string_attribute_def "sum" g "") in
        let shape = Tc.shape_of_string (string_attribute_def "shape" g "") in
François Bobot's avatar
François Bobot committed
821
822
823
        let exp = bool_attribute "expanded" g true in
        let mg = raw_add_no_task ~keygen parent gname expl sum shape exp in
        List.iter (load_proof_or_transf ~old_provers mg) g.Xml.elements;
824
        mg.goal_verified <- goal_verified mg;
François Bobot's avatar
François Bobot committed
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
        mg::acc
    | "label" -> acc
    | s ->
        eprintf "[Warning] Session.load_goal: unexpected element '%s'@." s;
        acc

and load_proof_or_transf ~old_provers mg a =
  match a.Xml.name with
    | "proof" ->
        let prover = string_attribute "prover" a in
        let p =
          try
            let p = Util.Mstr.find prover old_provers in
            p
          with Not_found ->
            eprintf "[Error] prover not listing in header '%s'@." prover;
            raise (LoadError (a,"prover not listing in header"))
        in
        let res = match a.Xml.elements with
          | [r] -> load_result r
          | [] -> Undone Interrupted
          | _ ->
            eprintf "[Error] Too many result elements@.";
            raise (LoadError (a,"too many result elements"))

        in
        let edit = load_option "edited" a in
852
        let edit = match edit with None | Some "" -> None | _ -> edit in
François Bobot's avatar
François Bobot committed
853
        let obsolete = bool_attribute "obsolete" a true in
854
        let archived = bool_attribute "archived" a false in
855
856
857
        let timelimit = int_attribute "timelimit" a 2 in
        let memlimit = int_attribute "memlimit" a 0 in
(*
François Bobot's avatar
François Bobot committed
858
        if timelimit < 0 then begin
859
            eprintf "[Error] incorrect or unspecified  timelimit '%i'@."
François Bobot's avatar
François Bobot committed
860
861
862
863
              timelimit;
            raise (LoadError (a,sprintf "incorrect or unspecified timelimit %i"
              timelimit))
        end;
864
*)
François Bobot's avatar
François Bobot committed
865
        let (_ : 'a proof_attempt) =
866
          add_external_proof ~keygen ~archived ~obsolete
867
            ~timelimit ~memlimit ~edit mg p res
François Bobot's avatar
François Bobot committed
868
869
870
871
872
873
874
875
876
877
878
879
880
        in
        ()
    | "transf" ->
        let trname = string_attribute "name" a in
        let exp = bool_attribute "expanded" a true in
        let mtr = raw_add_transformation ~keygen mg trname exp in
        mtr.transf_goals <-
          List.rev
          (List.fold_left
             (load_goal ~old_provers (Parent_transf mtr))
             [] a.Xml.elements);
        (* already done by raw_add_transformation
           Hashtbl.add mg.transformations trname mtr *)
881
        mtr.transf_verified <- transf_verified mtr
François Bobot's avatar
François Bobot committed
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
    | "label" -> ()
    | s ->
        eprintf
          "[Warning] Session.load_proof_or_transf: unexpected element '%s'@."
          s

let load_theory ~old_provers mf acc th =
  match th.Xml.name with
    | "theory" ->
        let thname = load_ident th in
        let exp = bool_attribute "expanded" th true in
        let mth = raw_add_theory ~keygen mf thname exp in
        mth.theory_goals <-
          List.rev
          (List.fold_left
             (load_goal ~old_provers (Parent_theory mth))
             [] th.Xml.elements);
899
        mth.theory_verified <- theory_verified mth;
François Bobot's avatar
François Bobot committed
900
901
902
903
904
905
906
907
908
        mth::acc
    | s ->
        eprintf "[Warning] Session.load_theory: unexpected element '%s'@." s;
        acc

let load_file session old_provers f =
  match f.Xml.name with
    | "file" ->
        let fn = string_attribute "name" f in
909
        let fmt = load_option "format" f in
François Bobot's avatar
François Bobot committed
910
        let exp = bool_attribute "expanded" f true in
911
        let mf = raw_add_file ~keygen session fn fmt exp in
François Bobot's avatar
François Bobot committed
912
913
914
915
        mf.file_theories <-
          List.rev
          (List.fold_left
             (load_theory ~old_provers mf) [] f.Xml.elements);
916
        mf.file_verified <- file_verified mf;
François Bobot's avatar
François Bobot committed
917
918
        old_provers
    | "prover" ->
919
      (** The id is just for the session file *)
François Bobot's avatar
François Bobot committed
920
921
922
        let id = string_attribute "id" f in
        let name = string_attribute "name" f in
        let version = string_attribute "version" f in
923
924
925
926
        let altern = string_attribute_def "alternative" f "" in
        let p = {C.prover_name = name;
                   prover_version = version;
                   prover_altern = altern} in
François Bobot's avatar
François Bobot committed
927
928
929
930
931
932
933
934
935
        Util.Mstr.add id p old_provers
    | s ->
        eprintf "[Warning] Session.load_file: unexpected element '%s'@." s;
        old_provers

let old_provers = ref Util.Mstr.empty
let get_old_provers () = !old_provers

let load_session session xml =
MARCHE Claude's avatar
MARCHE Claude committed
936
  match xml.Xml.name with
François Bobot's avatar
François Bobot committed
937
    | "why3session" ->
MARCHE Claude's avatar
MARCHE Claude committed
938
939
940
      let shape_version = int_attribute "shape_version" xml 1 in
      session.session_shape_version <- shape_version;
      dprintf debug "[Info] load_session: shape version is %d@\n" shape_version;
François Bobot's avatar
François Bobot committed
941
      (** just to keep the old_provers somewhere *)
MARCHE Claude's avatar
MARCHE Claude committed
942
943
944
      old_provers :=
        List.fold_left (load_file session) Util.Mstr.empty xml.Xml.elements;
      dprintf debug "[Info] load_session: done@\n"
François Bobot's avatar
François Bobot committed
945
946
947
948
949
950
    | s ->
        eprintf "[Warning] Session.load_session: unexpected element '%s'@." s

exception OpenError of string
type notask = unit
let read_session dir =
François Bobot's avatar
François Bobot committed
951
952
953
  if not (Sys.file_exists dir && Sys.is_directory dir) then
    raise (OpenError (Pp.sprintf "%s is not an existing directory" dir));
  let xml_filename = Filename.concat dir db_filename in
MARCHE Claude's avatar
MARCHE Claude committed
954
  let session = empty_session dir in
François Bobot's avatar
François Bobot committed
955
956
  (** If the xml is present we read it, otherwise we consider it empty *)
  if Sys.file_exists xml_filename then begin
François Bobot's avatar
François Bobot committed
957
    try
François Bobot's avatar
François Bobot committed
958
959
      let xml = Xml.from_file xml_filename in
      try
MARCHE Claude's avatar
MARCHE Claude committed
960
        load_session session xml.Xml.content;
François Bobot's avatar
François Bobot committed
961
962
963
964
965
966
967
968
      with Sys_error msg ->
        failwith ("Open session: sys error " ^ msg)
    with
      | Sys_error _msg ->
      (* xml does not exist yet *)
        raise (OpenError "Can't open")
      | Xml.Parse_error s ->
        Format.eprintf "XML database corrupted, ignored (%s)@." s;
François Bobot's avatar
François Bobot committed
969
970
      (* failwith
         ("Open session: XML database corrupted (%s)@." ^ s) *)
François Bobot's avatar
François Bobot committed
971
972
973
974
        raise (OpenError "XML corrupted")
  end;
  session

François Bobot's avatar
François Bobot committed
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000

(*******************************)
(* Session modification        *)
(* expansion, add childs, ...  *)
(*******************************)

let rec set_goal_expanded g b =
  g.goal_expanded <- b;
  if not b then
    PHstr.iter (fun _ tr -> set_transf_expanded tr b) g.goal_transformations

and set_transf_expanded tr b =
  tr.transf_expanded <- b;
  if not b then
    List.iter (fun g -> set_goal_expanded g b) tr.transf_goals

let set_theory_expanded t b =
  t.theory_expanded <- b;
  if not b then
    List.iter (fun th -> set_goal_expanded th b) t.theory_goals

let set_file_expanded f b =
  f.file_expanded <- b;
  if not b then
    List.iter (fun th -> set_theory_expanded th b) f.file_theories

For faster browsing, not all history is shown. View entire blame