Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

session.mli 16.5 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
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

(** Proof sessions *)
22
(** Define all the functions needed for managing a session:
François Bobot's avatar
François Bobot committed
23
    Creation, saving, loading, modification, ...
24
    All the operations are immediately done.
François Bobot's avatar
François Bobot committed
25 26 27
    Use session_scheduler if you want to queue the operations
*)

François Bobot's avatar
François Bobot committed
28 29
open Stdlib

François Bobot's avatar
François Bobot committed
30 31 32 33
val debug : Debug.flag
(** The debug flag "session" *)

module PHstr : Util.PrivateHashtbl with type key = string
34
module PHprover : Util.PrivateHashtbl with type key = Whyconf.prover
François Bobot's avatar
François Bobot committed
35 36 37 38 39

(** {2 Proof attempts} *)

(** State of a proof *)
type proof_attempt_status =
40 41 42 43 44
    | 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
45 46 47
    | 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
48
type expl
François Bobot's avatar
François Bobot committed
49 50 51 52 53 54 55 56 57
(** 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
(** Currently just an option on a task, but later perhaps
    we should be able to release a task and rebuild it when needed *)

58 59 60 61 62

type ident_path =
  { ip_library : string list;
    ip_theory : string;
    ip_qualid : string list;
François Bobot's avatar
François Bobot committed
63 64 65 66 67 68 69 70 71
  }

type meta_args = Theory.meta_arg list
module Mmeta_args : Map.S with type key = meta_args
module Smeta_args : Mmeta_args.Set
type metas_args =  Smeta_args.t Util.Mstr.t
module Mmetas_args : Map.S with type key = metas_args

type idpos = {
72 73 74
  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
75 76
}

François Bobot's avatar
François Bobot committed
77 78 79 80 81 82 83 84 85 86 87
(** {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;
88 89
      mutable goal_checksum : Termcode.checksum;  (** checksum of the task *)
      mutable goal_shape : Termcode.shape;  (** shape of the task *)
François Bobot's avatar
François Bobot committed
90 91 92 93 94
      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
95
      mutable goal_metas : 'a metas Mmetas_args.t;
François Bobot's avatar
François Bobot committed
96 97 98 99
    }

and 'a proof_attempt = private
    { proof_key : 'a;
100
      mutable proof_prover : Whyconf.prover;
François Bobot's avatar
François Bobot committed
101 102 103
      proof_parent : 'a goal;
      mutable proof_state : proof_attempt_status;
      mutable proof_timelimit : int;
104
      mutable proof_memlimit : int;
François Bobot's avatar
François Bobot committed
105
      mutable proof_obsolete : bool;
106
      mutable proof_archived : bool;
François Bobot's avatar
François Bobot committed
107 108 109 110 111 112
      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
113 114 115 116 117 118 119 120 121 122 123 124
                     | 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
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149

and 'a transf = private
    { 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 *)
      mutable transf_expanded : bool;
    }

and 'a theory = private
    { mutable theory_key : 'a;
      theory_name : Ident.ident;
      theory_parent : 'a file;
      mutable theory_goals : 'a goal list;
      (** Not mutated after the creation *)
      mutable theory_verified : bool;
      mutable theory_expanded : bool;
    }

and 'a file = private
    { mutable file_key : 'a;
      file_name : string;
150
      file_format : string option;
François Bobot's avatar
François Bobot committed
151 152 153 154 155 156 157 158 159
      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 = private
    { session_files : 'a file PHstr.t;
MARCHE Claude's avatar
MARCHE Claude committed
160
      mutable session_shape_version : int;
François Bobot's avatar
François Bobot committed
161 162 163 164 165 166
      session_dir   : string;
    }

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

167 168 169 170
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
171
val create_session : ?shape_version:int -> string -> 'key session
François Bobot's avatar
François Bobot committed
172 173 174 175 176 177 178 179 180 181
(** create a new_session in the given directory. The directory is
    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
(** find the session which correspond to the given file or return
    directly the given directory;
    return {Not_found} if the file or the directory doesn't exists
*)

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

François Bobot's avatar
François Bobot committed
184 185 186 187 188 189
type notask
(** A phantom type which is used for session which doesn't contain task. The
    only session that can not contain task are session that come from the
    following function *)

val read_session : string -> notask session
François Bobot's avatar
François Bobot committed
190
(** Read a session stored on the disk. It returns a session without any
François Bobot's avatar
François Bobot committed
191 192
    task attached to goals *)

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

François Bobot's avatar
François Bobot committed
196
(** {2 Context of a session} *)
François Bobot's avatar
François Bobot committed
197 198

(** A session which contains task and proof_attempt depends on an
François Bobot's avatar
François Bobot committed
199
    environment and a prover configuration.
François Bobot's avatar
François Bobot committed
200 201 202 203 204 205
    Loaded provers are cached in order to load drivers once *)

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

206
type loaded_provers = loaded_prover option PHprover.t
François Bobot's avatar
François Bobot committed
207 208 209

type 'a env_session = private
    { env : Env.env;
210
      mutable whyconf : Whyconf.config;
François Bobot's avatar
François Bobot committed
211 212 213
      loaded_provers : loaded_provers;
      session : 'a session}

214 215 216
val update_env_session_config : 'a env_session -> Whyconf.config -> unit
(** updates the configuration *)

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

220
val unload_provers : 'a env_session -> unit
221
(** forces unloading of all provers,
222 223
    to force reading again the configuration *)

François Bobot's avatar
François Bobot committed
224 225 226 227 228 229 230 231 232 233 234
(** {2 Update session} *)

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

exception OutdatedSession

val update_session : keygen:'a keygen ->
  allow_obsolete:bool -> 'b session ->
  Env.env -> Whyconf.config -> 'a env_session * bool
(** reload the given session with the given environnement :
François Bobot's avatar
François Bobot committed
235
    - the files are reloaded
François Bobot's avatar
François Bobot committed
236
    - apply again the transformation
François Bobot's avatar
François Bobot committed
237
    - if some goals appear try to find to which goal
François Bobot's avatar
François Bobot committed
238 239 240
    in the given session it corresponds.

    The last case meant that the session was obsolete.
François Bobot's avatar
François Bobot committed
241
    It is authorized if [allow_obsolete] is [true],
François Bobot's avatar
François Bobot committed
242 243 244 245 246 247 248 249
    otherwise the exception [OutdatedSession] is raised.
    If the session was obsolete is indicated by
    the second result.

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

*)

250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267
(** {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
268 269
(** {2 Accessor} *)

François Bobot's avatar
François Bobot committed
270 271
exception NoTask
val goal_task : 'key goal -> Task.task
François Bobot's avatar
François Bobot committed
272
(** Return the task of a goal. Raise NoTask if the goal doesn't contain a task
François Bobot's avatar
François Bobot committed
273 274 275
    (equivalent to 'key = notask) *)

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

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

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


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

François Bobot's avatar
François Bobot committed
288 289 290
(* 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
291
(** {2 Modificator} *)
François Bobot's avatar
François Bobot committed
292 293

val set_transf_expanded : 'key transf -> bool -> unit
François Bobot's avatar
François Bobot committed
294
val set_metas_expanded : 'key metas -> bool -> unit
François Bobot's avatar
François Bobot committed
295 296 297 298 299
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
300
(** {2 General type} *)
François Bobot's avatar
François Bobot committed
301 302 303 304 305 306 307

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
308
  | Metas of 'a metas
François Bobot's avatar
François Bobot committed
309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324

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 ->
325
  archived:bool ->
François Bobot's avatar
François Bobot committed
326
  timelimit:int ->
327
  memlimit:int ->
François Bobot's avatar
François Bobot committed
328 329
  edit:string option ->
  'key goal ->
330
  Whyconf.prover ->
François Bobot's avatar
François Bobot committed
331 332 333 334 335 336 337 338
  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 ->
339
  archived:bool ->
François Bobot's avatar
François Bobot committed
340 341 342
  proof_attempt_status ->
  'key proof_attempt -> unit

343 344
val change_prover : 'a proof_attempt -> Whyconf.prover -> unit

345 346
val set_obsolete : ?notify:'key notify -> 'key proof_attempt -> unit

347
val set_archived : 'key proof_attempt -> bool -> unit
348

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

351 352 353
val get_edited_as_abs : 'key session -> 'k proof_attempt -> string option
(** return the edited filename after concatenation to session_dir *)

354 355 356 357 358 359
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
360
val set_timelimit : int -> 'key proof_attempt -> unit
361
val set_memlimit : int -> 'key proof_attempt -> unit
François Bobot's avatar
François Bobot committed
362

363 364 365 366
val copy_external_proof :
  ?notify:'key notify ->
  keygen:'key keygen ->
  ?obsolete:bool ->
367
  ?archived:bool ->
368
  ?timelimit:int ->
369
  ?memlimit:int ->
370 371 372 373 374 375 376 377 378 379 380 381 382 383
  ?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}
384
    {- a session is given}
385 386 387 388 389 390 391 392 393 394 395
    }
    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
396 397 398 399
(** {2 Transformation} *)

val add_transformation :
  keygen:'key keygen ->
François Bobot's avatar
François Bobot committed
400
  goal:('goal -> Ident.ident * expl * Task.task) ->
401
  'key env_session ->
François Bobot's avatar
François Bobot committed
402 403 404 405 406 407 408 409 410 411 412 413 414
  string ->
  'key goal ->
  'goal list ->
  '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,
415 416 417
    raise NoTask if the goal doesn't contain a task.
    If the goal already has a transformation with this name,
    it is returned. *)
François Bobot's avatar
François Bobot committed
418 419

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

François Bobot's avatar
François Bobot committed
422 423 424 425 426 427 428
(** {2 Metas} *)
val add_registered_metas :
  keygen:'key keygen ->
  'key env_session ->
  (string * Theory.meta_arg list) list ->
  'key goal ->
  'key metas
429 430 431
(** 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
432 433

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

François Bobot's avatar
François Bobot committed
436 437 438 439 440
(** {2 File} *)

val add_file :
  keygen:'key keygen ->
  'key env_session ->
441
  ?format:string ->
François Bobot's avatar
François Bobot committed
442 443
  string ->
  'key file
François Bobot's avatar
François Bobot committed
444 445
(** Add a real file by its filename. The filename must be relative to
    session_dir *)
François Bobot's avatar
François Bobot committed
446 447

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

(** {2 Explanation} *)
François Bobot's avatar
François Bobot committed
451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476

val get_explanation : Ident.ident -> Task.task -> expl
val goal_expl_task : Task.task -> Ident.ident * expl * Task.task

(** {2 Iterators} *)

(** {3 recursive} *)

val goal_iter_proof_attempt : ('key proof_attempt -> unit) -> 'key goal -> unit
val transf_iter_proof_attempt :
  ('key proof_attempt -> unit) -> 'key transf -> unit
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
477
(** {3 not recursive} *)
François Bobot's avatar
François Bobot committed
478

François Bobot's avatar
François Bobot committed
479
val iter_goal :
François Bobot's avatar
François Bobot committed
480 481 482 483
  ('key proof_attempt -> unit) ->
  ('key transf -> unit) ->
  ('key metas -> unit) ->
  'key goal -> unit
François Bobot's avatar
François Bobot committed
484 485
val iter_transf :
  ('key goal -> unit) -> 'key transf -> unit
François Bobot's avatar
François Bobot committed
486 487
val iter_metas :
  ('key goal -> unit) -> 'key metas -> unit
François Bobot's avatar
François Bobot committed
488 489 490 491 492 493


val goal_iter : ('key any -> unit) -> 'key goal -> unit
val transf_iter : ('key any -> unit) -> 'key transf -> unit
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
494
val metas_iter : ('key any -> unit) -> 'key metas -> unit
François Bobot's avatar
François Bobot committed
495 496 497 498
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

François Bobot's avatar
François Bobot committed
499
(** {2 Some functorized interface (not very useful...)}*)
François Bobot's avatar
François Bobot committed
500 501


502
(* Claude: if "not very useful" then -> removed
François Bobot's avatar
François Bobot committed
503 504 505 506 507
module AddTransf (X : sig
  type key
  val keygen : key keygen

  type goal
François Bobot's avatar
François Bobot committed
508
  val goal : goal -> Ident.ident * expl * Task.task
François Bobot's avatar
François Bobot committed
509 510 511 512 513 514

  type transf
  val fold_transf : ('a -> goal -> 'a) -> 'a -> Task.task -> transf -> 'a
end) : sig
  val add_transformation : X.key goal -> string -> X.transf -> X.key transf
end
515
*)
François Bobot's avatar
François Bobot committed
516

517
(*
François Bobot's avatar
François Bobot committed
518 519 520 521 522
module AddFile(X : sig
  type key
  val keygen : key keygen

  type goal
François Bobot's avatar
François Bobot committed
523
  val goal : goal -> Ident.ident * expl * Task.task
François Bobot's avatar
François Bobot committed
524 525 526 527 528 529 530 531 532 533

  type theory
  val fold_theory : ('a -> goal -> 'a) -> 'a -> theory -> 'a

  type file
  val fold_file :
    ('a -> Ident.ident (** thname *) -> theory -> 'a) ->
    'a -> file -> 'a

end) : sig
534 535
  val add_file :
    X.key session -> string -> ?format:string -> X.file -> X.key file
François Bobot's avatar
François Bobot committed
536
end
537
*)
François Bobot's avatar
François Bobot committed
538 539 540 541 542 543 544


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