session.mli 16.6 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 13 14 15 16 17
(** Proof sessions

    Define all the functions needed for managing a session:
    creation, saving, loading, modification, and so on.
    All the operations are immediately performed.
    Use session_scheduler if you want to queue operations.
François Bobot's avatar
François Bobot committed
18 19
*)

François Bobot's avatar
François Bobot committed
20 21
open Stdlib

François Bobot's avatar
François Bobot committed
22 23 24
val debug : Debug.flag
(** The debug flag "session" *)

25 26
module PHstr : Exthtbl.Private with type key = string
module PHprover : Exthtbl.Private with type key = Whyconf.prover
François Bobot's avatar
François Bobot committed
27 28 29 30 31

(** {2 Proof attempts} *)

(** State of a proof *)
type proof_attempt_status =
32 33 34 35 36
    | Unedited (** editor not yet run for interactive proof *)
    | JustEdited (** edited but not run yet *)
    | Interrupted (** external proof has never completed *)
    | Scheduled (** external proof attempt is scheduled *)
    | Running (** external proof attempt is in progress *)
François Bobot's avatar
François Bobot committed
37 38 39
    | Done of Call_provers.prover_result (** external proof done *)
    | InternalFailure of exn (** external proof aborted by internal error *)

François Bobot's avatar
François Bobot committed
40
type expl
François Bobot's avatar
François Bobot committed
41 42 43 44 45 46
(** An explanation gives hint about how the goal has been produced.
    Allow to reattach proof_attempt to goal when the source file has been
    modified.
*)

type task_option
47 48 49 50
(** The task can be removed and later reconstructible *)

type 'a hide
(** For internal use *)
François Bobot's avatar
François Bobot committed
51

52 53 54 55 56

type ident_path =
  { ip_library : string list;
    ip_theory : string;
    ip_qualid : string list;
François Bobot's avatar
François Bobot committed
57 58 59
  }

type meta_args = Theory.meta_arg list
60 61
module Mmeta_args : Extmap.S with type key = meta_args
module Smeta_args : Extset.S with module M = Mmeta_args
62

63 64
type metas_args = Smeta_args.t Mstr.t
module Mmetas_args : Extmap.S with type key = metas_args
François Bobot's avatar
François Bobot committed
65 66

type idpos = {
67 68 69
  idpos_ts : ident_path Ty.Mts.t;
  idpos_ls : ident_path Term.Mls.t;
  idpos_pr : ident_path Decl.Mpr.t;
François Bobot's avatar
François Bobot committed
70 71
}

François Bobot's avatar
François Bobot committed
72 73 74 75 76 77 78 79 80 81 82
(** {2 Session} *)

(** All the element of a session contain a key which can hold whatever
    information the user want. It is generated by the keygen argument
    of the functions of this module *)

type 'a goal = private
    { mutable goal_key  : 'a;
      goal_name : Ident.ident; (** The ident of the task *)
      goal_expl : expl;
      goal_parent : 'a goal_parent;
83
      mutable goal_checksum : Termcode.checksum option;  (** checksum of the task *)
84
      mutable goal_shape : Termcode.shape;  (** shape of the task *)
François Bobot's avatar
François Bobot committed
85
      mutable goal_verified : bool;
86
      mutable goal_task: task_option;
François Bobot's avatar
François Bobot committed
87 88 89
      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
90
      mutable goal_metas : 'a metas Mmetas_args.t;
François Bobot's avatar
François Bobot committed
91 92 93 94
    }

and 'a proof_attempt = private
    { proof_key : 'a;
95
      mutable proof_prover : Whyconf.prover;
François Bobot's avatar
François Bobot committed
96 97 98
      proof_parent : 'a goal;
      mutable proof_state : proof_attempt_status;
      mutable proof_timelimit : int;
99
      mutable proof_memlimit : int;
François Bobot's avatar
François Bobot committed
100
      mutable proof_obsolete : bool;
101
      mutable proof_archived : bool;
François Bobot's avatar
François Bobot committed
102 103 104 105 106 107
      mutable proof_edited_as : string option;
    }

and 'a goal_parent = private
                     | Parent_theory of 'a theory
                     | Parent_transf of 'a transf
François Bobot's avatar
François Bobot committed
108 109 110 111 112 113 114 115 116 117 118 119
                     | 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
120 121 122 123

and 'a transf = private
    { mutable transf_key : 'a;
      transf_name : string;
124
      (** Why3 transformation name *)
François Bobot's avatar
François Bobot committed
125 126 127 128 129 130 131 132 133 134 135
      transf_parent : 'a goal;
      mutable transf_verified : bool;
      mutable transf_goals : 'a goal list;
      (** Not mutated after the creation *)
      mutable transf_expanded : bool;
    }

and 'a theory = private
    { mutable theory_key : 'a;
      theory_name : Ident.ident;
      theory_parent : 'a file;
136
      mutable theory_checksum : Termcode.checksum option;
François Bobot's avatar
François Bobot committed
137 138 139 140
      mutable theory_goals : 'a goal list;
      (** Not mutated after the creation *)
      mutable theory_verified : bool;
      mutable theory_expanded : bool;
141
      mutable theory_task : Theory.theory hide;
François Bobot's avatar
François Bobot committed
142 143 144 145 146
    }

and 'a file = private
    { mutable file_key : 'a;
      file_name : string;
147
      file_format : string option;
François Bobot's avatar
François Bobot committed
148 149 150 151 152
      file_parent : 'a session;
      mutable file_theories: 'a theory list;
      (** Not mutated after the creation *)
      mutable file_verified : bool;
      mutable file_expanded : bool;
153
      mutable file_for_recovery : Theory.theory Mstr.t hide;
François Bobot's avatar
François Bobot committed
154 155 156 157
    }

and 'a session = private
    { session_files : 'a file PHstr.t;
MARCHE Claude's avatar
MARCHE Claude committed
158
      mutable session_shape_version : int;
159
      session_prover_ids : int PHprover.t;
François Bobot's avatar
François Bobot committed
160 161 162 163 164 165
      session_dir   : string;
    }

val print_session : Format.formatter -> 'a session -> unit
(** Print a session with a pstree format (cf Tree module) *)

166 167 168 169
val print_attempt_status : Format.formatter -> proof_attempt_status -> unit

val print_external_proof : Format.formatter -> 'key proof_attempt -> unit

MARCHE Claude's avatar
MARCHE Claude committed
170
val create_session : ?shape_version:int -> string -> 'key session
171
(** create a new session in the given directory. The directory is
François Bobot's avatar
François Bobot committed
172 173 174 175
    created if it doesn't exists yet. Don't change the current
    directory of the program if you give a relative path *)

val get_project_dir : string -> string
MARCHE Claude's avatar
MARCHE Claude committed
176
(** find the session which corresponds to the given file or return
François Bobot's avatar
François Bobot committed
177
    directly the given directory;
178
    return [Not_found] if the file or the directory doesn't exists
François Bobot's avatar
François Bobot committed
179 180
*)

181 182
(** {2 Read/Write} *)

François Bobot's avatar
François Bobot committed
183
type notask
184 185
(** A phantom type which is used for sessions which don't contain any task. The
    only such sessions are sessions that come from {!read_session} *)
François Bobot's avatar
François Bobot committed
186

187
val read_session : string -> notask session * bool
François Bobot's avatar
François Bobot committed
188
(** Read a session stored on the disk. It returns a session without any
189
    task attached to goals.
190 191 192 193 194 195 196 197 198

    The returned boolean is set when there was shapes read from disk.

    raises [SessionFileError msg] if the database file cannot be read
    correctly.

    raises [ShapesFileError msg] if the database extra file for shapes
    cannot be read.

199
*)
François Bobot's avatar
François Bobot committed
200

MARCHE Claude's avatar
MARCHE Claude committed
201
val save_session : Whyconf.config -> 'key session -> unit
François Bobot's avatar
François Bobot committed
202
(** Save a session on disk *)
François Bobot's avatar
François Bobot committed
203

François Bobot's avatar
François Bobot committed
204
(** {2 Context of a session} *)
François Bobot's avatar
François Bobot committed
205 206

(** A session which contains task and proof_attempt depends on an
François Bobot's avatar
François Bobot committed
207
    environment and a prover configuration.
François Bobot's avatar
François Bobot committed
208 209 210 211 212 213
    Loaded provers are cached in order to load drivers once *)

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

214
type loaded_provers = loaded_prover option PHprover.t
François Bobot's avatar
François Bobot committed
215 216 217

type 'a env_session = private
    { env : Env.env;
218
      mutable whyconf : Whyconf.config;
François Bobot's avatar
François Bobot committed
219
      loaded_provers : loaded_provers;
220
      mutable files : Theory.theory Stdlib.Mstr.t Stdlib.Mstr.t;
François Bobot's avatar
François Bobot committed
221 222
      session : 'a session}

223 224 225
val update_env_session_config : 'a env_session -> Whyconf.config -> unit
(** updates the configuration *)

226
val load_prover : 'a env_session -> Whyconf.prover -> loaded_prover option
François Bobot's avatar
François Bobot committed
227 228
(** load a prover *)

229
val unload_provers : 'a env_session -> unit
230
(** forces unloading of all provers,
231 232
    to force reading again the configuration *)

François Bobot's avatar
François Bobot committed
233 234 235 236 237 238
(** {2 Update session} *)

type 'key keygen = ?parent:'key -> unit -> 'key
(** type of functions which can generate keys *)

exception OutdatedSession
239 240 241
exception ShapesFileError of string
exception SessionFileError of string

242
type 'key update_context =
243 244 245 246
  { allow_obsolete_goals : bool;
    release_tasks : bool;
    use_shapes_for_pairing_sub_goals : bool;
    theory_is_fully_up_to_date : bool;
247
    keygen : 'key keygen;
248
  }
François Bobot's avatar
François Bobot committed
249

250 251
val update_session : ctxt:'key update_context -> 'a session ->
  Env.env -> Whyconf.config -> 'key env_session * bool * bool
François Bobot's avatar
François Bobot committed
252
(** reload the given session with the given environnement :
François Bobot's avatar
François Bobot committed
253
    - the files are reloaded
François Bobot's avatar
François Bobot committed
254
    - apply again the transformation
François Bobot's avatar
François Bobot committed
255
    - if some goals appear try to find to which goal
François Bobot's avatar
François Bobot committed
256 257 258
    in the given session it corresponds.

    The last case meant that the session was obsolete.
François Bobot's avatar
François Bobot committed
259
    It is authorized if [allow_obsolete] is [true],
260
    otherwise the exception {!OutdatedSession} is raised.
François Bobot's avatar
François Bobot committed
261 262
    If the session was obsolete is indicated by
    the second result.
263 264
    If the merge generated new unpaired goals is indicated by
    the third result.
François Bobot's avatar
François Bobot committed
265

266 267
    raises [OutdatedSession] if the session is obsolete and
    [allow_obsolete] is false]
François Bobot's avatar
François Bobot committed
268 269 270

*)

271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288
(** {2 Copy/Paste } *)

val copy_proof:  'a proof_attempt -> 'a proof_attempt
val copy_transf: 'a transf        -> 'a transf
val copy_metas:  'a metas         -> 'a metas
(** keys are copied *)

val add_proof_to_goal :
  keygen:'a keygen -> 'a env_session ->
  'a goal -> 'a proof_attempt ->'a proof_attempt
val add_transf_to_goal:
  keygen:'a keygen -> 'a env_session ->
  'a goal -> 'a transf        -> 'a transf
val add_metas_to_goal :
  keygen:'a keygen -> 'a env_session ->
  'a goal -> 'a metas         -> 'a metas
(** keys are normally generated *)

François Bobot's avatar
François Bobot committed
289 290
(** {2 Accessor} *)

François Bobot's avatar
François Bobot committed
291 292
exception NoTask
val goal_task : 'key goal -> Task.task
293 294
(** Return the task of a goal. Raise {!NoTask} if the goal doesn't contain a task
    (equivalent to ['key = notask] if {!release_task} is not used) *)
François Bobot's avatar
François Bobot committed
295 296

val goal_task_option : 'key goal -> Task.task option
François Bobot's avatar
François Bobot committed
297
(** Return the task of a goal. *)
François Bobot's avatar
François Bobot committed
298 299

val goal_expl : 'key goal -> string
François Bobot's avatar
François Bobot committed
300
(** Return the explication of a goal *)
François Bobot's avatar
François Bobot committed
301 302

val proof_verified : 'key proof_attempt -> bool
François Bobot's avatar
François Bobot committed
303 304 305
(** Return true if the proof is not obsolete and the result is valid *)


306
val get_used_provers : 'a session -> Whyconf.Sprover.t
François Bobot's avatar
François Bobot committed
307
(** Get the set of provers which appear in the session *)
François Bobot's avatar
François Bobot committed
308

François Bobot's avatar
François Bobot committed
309 310 311
(* val metas_of_virtuals : 'a metas -> Theory.Smeta.t *)
(* (\** Get the set of metas added (the parent goal must contain a task) *\) *)

François Bobot's avatar
François Bobot committed
312
(** {2 Modificator} *)
François Bobot's avatar
François Bobot committed
313 314

val set_transf_expanded : 'key transf -> bool -> unit
François Bobot's avatar
François Bobot committed
315
val set_metas_expanded : 'key metas -> bool -> unit
François Bobot's avatar
François Bobot committed
316 317 318 319 320
val set_goal_expanded : 'key goal -> bool -> unit
val set_theory_expanded : 'key theory -> bool -> unit
val set_file_expanded : 'key file -> bool -> unit
(** open one level or close all the sub-level *)

François Bobot's avatar
François Bobot committed
321
(** {2 General type} *)
François Bobot's avatar
François Bobot committed
322 323 324 325 326 327 328

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
329
  | Metas of 'a metas
François Bobot's avatar
François Bobot committed
330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345

val print_any : Format.formatter -> 'a any -> unit
(** Print a subtree with a pstree format (cf Tree module) *)

val key_any : 'a any -> 'a
(** return the key of an element of the tree *)

(** {2 External proof} *)

type 'key notify = 'key any -> unit
(** type of functions which notify modification of the verified field *)

val add_external_proof :
  ?notify:'key notify ->
  keygen:'key keygen ->
  obsolete:bool ->
346
  archived:bool ->
François Bobot's avatar
François Bobot committed
347
  timelimit:int ->
348
  memlimit:int ->
François Bobot's avatar
François Bobot committed
349 350
  edit:string option ->
  'key goal ->
351
  Whyconf.prover ->
François Bobot's avatar
François Bobot committed
352 353 354 355 356 357 358 359
  proof_attempt_status ->
  'key proof_attempt

val remove_external_proof : ?notify:'key notify -> 'key proof_attempt -> unit

val set_proof_state :
  ?notify:'key notify ->
  obsolete:bool ->
360
  archived:bool ->
François Bobot's avatar
François Bobot committed
361 362 363
  proof_attempt_status ->
  'key proof_attempt -> unit

364 365
val change_prover : 'a proof_attempt -> Whyconf.prover -> unit

366 367
val set_obsolete : ?notify:'key notify -> 'key proof_attempt -> unit

368
val set_archived : 'key proof_attempt -> bool -> unit
369

François Bobot's avatar
François Bobot committed
370 371
val set_edited_as : string option -> 'key proof_attempt -> unit

372
val get_edited_as_abs : 'key session -> 'k proof_attempt -> string option
373
(** return the edited filename after concatenation to [session_dir] *)
374

375 376 377 378 379 380
val update_edit_external_proof :
  'key env_session -> 'key proof_attempt -> string
(** return the absolute path of the edited file update with the
    current goal *)


François Bobot's avatar
François Bobot committed
381
val set_timelimit : int -> 'key proof_attempt -> unit
382
val set_memlimit : int -> 'key proof_attempt -> unit
François Bobot's avatar
François Bobot committed
383

384 385 386 387
val copy_external_proof :
  ?notify:'key notify ->
  keygen:'key keygen ->
  ?obsolete:bool ->
388
  ?archived:bool ->
389
  ?timelimit:int ->
390
  ?memlimit:int ->
391 392 393 394 395 396 397 398 399 400 401 402 403 404
  ?edit:string option ->
  ?goal:'key goal ->
  ?prover:Whyconf.prover ->
  ?attempt_status:proof_attempt_status ->
  ?env_session:'key env_session ->
  ?session:'key session ->
  'key proof_attempt -> 'key proof_attempt
(** copy an external proof.
    if env_session and session are given only env_session.session is
    taken into account.
    The edited file is copied and an env_session is not required if :
    {ul
    {- the goal is not modified}
    {- the prover is not modified}
405
    {- a session is given}
406 407 408 409 410 411 412 413 414 415 416
    }
    The edited file is regenerated if
    {ul
    {- the external proof contain an edited file}
    {- an env_session is given}
    {- the given goal (or the old one if not modified) contain a task}
    }
    In all the other case the resulting external proof is considered
    not edited.
*)

François Bobot's avatar
François Bobot committed
417 418 419
(** {2 Transformation} *)

val add_transformation :
420 421
  ?init:'key notify ->
  ?notify:'key notify ->
François Bobot's avatar
François Bobot committed
422
  keygen:'key keygen ->
423
  'key env_session ->
François Bobot's avatar
François Bobot committed
424 425
  string ->
  'key goal ->
MARCHE Claude's avatar
MARCHE Claude committed
426
  Task.task list ->
François Bobot's avatar
François Bobot committed
427 428 429 430 431 432 433 434 435 436
  'key transf
(** Add a transformation by its subgoals *)

val add_registered_transformation :
  keygen:'key keygen ->
  'key env_session ->
  string ->
  'key goal ->
  'key transf
(** Apply a real transformation by its why3 name,
437
    raise {!NoTask} if the goal doesn't contain a task.
438 439
    If the goal already has a transformation with this name,
    it is returned. *)
François Bobot's avatar
François Bobot committed
440 441

val remove_transformation : ?notify:'key notify -> 'key transf -> unit
François Bobot's avatar
François Bobot committed
442
  (** Remove a transformation *)
François Bobot's avatar
François Bobot committed
443

François Bobot's avatar
François Bobot committed
444 445 446 447 448 449 450
(** {2 Metas} *)
val add_registered_metas :
  keygen:'key keygen ->
  'key env_session ->
  (string * Theory.meta_arg list) list ->
  'key goal ->
  'key metas
451 452 453
(** Add some metas to a task. If the goal already contain a {!metas}
    with same metas, the old one is returned.
*)
François Bobot's avatar
François Bobot committed
454 455

val remove_metas : ?notify:'key notify -> 'key metas -> unit
456
(** Remove the addition of metas *)
François Bobot's avatar
François Bobot committed
457

François Bobot's avatar
François Bobot committed
458 459 460 461 462
(** {2 File} *)

val add_file :
  keygen:'key keygen ->
  'key env_session ->
463
  ?format:string ->
François Bobot's avatar
François Bobot committed
464 465
  string ->
  'key file
François Bobot's avatar
François Bobot committed
466 467
(** Add a real file by its filename. The filename must be relative to
    session_dir *)
François Bobot's avatar
François Bobot committed
468 469

val remove_file : 'key file -> unit
François Bobot's avatar
François Bobot committed
470 471
(** Remove a file *)

472 473 474 475 476 477 478 479 480 481 482 483
(** {2 Free and recover task} *)
(** Tasks are stored inside the goals. For releasing memory you can remove
    them. Later you can recompute them *)

val release_task: 'a goal -> unit
  (** remove the task stored in this goal*)

val release_sub_tasks: 'a goal -> unit
  (** apply the previous function on this goal and its its sub-goal *)

val recover_theory_tasks: 'a env_session -> 'a theory -> unit
  (** Recover all the sub-goal (not only strict) of this theory *)
François Bobot's avatar
François Bobot committed
484

485 486 487
val goal_task_or_recover: 'a env_session -> 'a goal -> Task.task
  (** same as goal_task but recover the task goal and all the one of this
      theory if this goal task have been released *)
François Bobot's avatar
François Bobot committed
488 489 490 491 492 493

(** {2 Iterators} *)

(** {3 recursive} *)

val goal_iter_proof_attempt : ('key proof_attempt -> unit) -> 'key goal -> unit
494
(* unused
François Bobot's avatar
François Bobot committed
495 496
val transf_iter_proof_attempt :
  ('key proof_attempt -> unit) -> 'key transf -> unit
497
*)
François Bobot's avatar
François Bobot committed
498 499 500 501 502 503 504 505 506 507 508 509 510 511 512
val theory_iter_proof_attempt :
  ('key proof_attempt -> unit) -> 'key theory -> unit
val transf_iter_proof_attempt :
  ('key proof_attempt -> unit) -> 'key transf -> unit
val file_iter_proof_attempt : ('key proof_attempt -> unit) -> 'key file -> unit
val session_iter_proof_attempt :
  ('key proof_attempt -> unit) -> 'key session -> unit
val iter_proof_attempt :
  ('key proof_attempt -> unit) -> 'key any -> unit

val goal_iter_leaf_goal :
  unproved_only:bool -> ('key goal -> unit) -> 'key goal -> unit
(** iter all the goals which are a leaf
    (no transformations are applied on it) *)

François Bobot's avatar
François Bobot committed
513
(** {3 not recursive} *)
François Bobot's avatar
François Bobot committed
514

François Bobot's avatar
François Bobot committed
515
val iter_goal :
François Bobot's avatar
François Bobot committed
516 517 518 519
  ('key proof_attempt -> unit) ->
  ('key transf -> unit) ->
  ('key metas -> unit) ->
  'key goal -> unit
François Bobot's avatar
François Bobot committed
520 521
val iter_transf :
  ('key goal -> unit) -> 'key transf -> unit
François Bobot's avatar
François Bobot committed
522 523
val iter_metas :
  ('key goal -> unit) -> 'key metas -> unit
524 525
val iter_theory :
  ('key goal -> unit) -> 'key theory -> unit
526 527 528 529
val iter_file :
  ('key theory -> unit) -> 'key file -> unit
val iter_session :
  ('key file -> unit) -> 'key session -> unit
François Bobot's avatar
François Bobot committed
530 531 532


val goal_iter : ('key any -> unit) -> 'key goal -> unit
533
(* unused
François Bobot's avatar
François Bobot committed
534
val transf_iter : ('key any -> unit) -> 'key transf -> unit
535
*)
François Bobot's avatar
François Bobot committed
536 537
val theory_iter : ('key any -> unit) -> 'key theory -> unit
val transf_iter : ('key any -> unit) -> 'key transf -> unit
François Bobot's avatar
François Bobot committed
538
val metas_iter : ('key any -> unit) -> 'key metas -> unit
François Bobot's avatar
François Bobot committed
539 540 541 542 543 544 545 546 547
val file_iter : ('key any -> unit) -> 'key file -> unit
val session_iter : ('key any -> unit) -> 'key session -> unit
val iter : ('key any -> unit) -> 'key any -> unit

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
End:
*)