session.mli 13.5 KB
Newer Older
François Bobot's avatar
François Bobot committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2011                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    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 *)
François Bobot's avatar
François Bobot committed
21
(** Define all the function needed for managing a session :
François Bobot's avatar
François Bobot committed
22 23 24 25 26 27 28 29 30
    Creation, saving, loading, modification, ...
    All the operation are immediately done.
    Use session_scheduler if you want to queue the operations
*)

val debug : Debug.flag
(** The debug flag "session" *)

module PHstr : Util.PrivateHashtbl with type key = string
31
module PHprover : Util.PrivateHashtbl with type key = Whyconf.prover
François Bobot's avatar
François Bobot committed
32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48

(** {2 Proof attempts} *)

(** State of proof without result *)
type undone_proof =
    | Scheduled (** external proof attempt is scheduled *)
    | Interrupted (** external proof has been interrupted or
                      has never been scheduled*)
    | Running (** external proof attempt is in progress *)
    | Unedited (** unedited but editable *)

(** State of a proof *)
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 *)

François Bobot's avatar
François Bobot committed
49
type expl
François Bobot's avatar
François Bobot committed
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
(** 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 *)

(** {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;
      goal_checksum : string;  (** checksum of the task *)
      goal_shape : string;     (** shape are produced by the module Termcode *)
      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;
    }

and 'a proof_attempt = private
    { proof_key : 'a;
81
      proof_prover : Whyconf.prover;
François Bobot's avatar
François Bobot committed
82 83 84 85
      proof_parent : 'a goal;
      mutable proof_state : proof_attempt_status;
      mutable proof_timelimit : int;
      mutable proof_obsolete : bool;
86
      mutable proof_archived : bool;
François Bobot's avatar
François Bobot committed
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
      mutable proof_edited_as : string option;
    }

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

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;
      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;
      session_dir   : string;
    }

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

133 134 135 136
val print_attempt_status : Format.formatter -> proof_attempt_status -> unit

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

François Bobot's avatar
François Bobot committed
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
val create_session : string -> 'key session
(** 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
*)

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
154
(** Read a session stored on the disk. It returns a session without any
François Bobot's avatar
François Bobot committed
155 156 157
    task attached to goals *)

val save_session : 'key session -> unit
François Bobot's avatar
François Bobot committed
158
(** Save a session on disk *)
François Bobot's avatar
François Bobot committed
159

François Bobot's avatar
François Bobot committed
160
(** {2 Context of a session} *)
François Bobot's avatar
François Bobot committed
161 162

(** A session which contains task and proof_attempt depends on an
François Bobot's avatar
François Bobot committed
163
    environment and a prover configuration.
François Bobot's avatar
François Bobot committed
164 165 166 167 168 169
    Loaded provers are cached in order to load drivers once *)

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

170
type loaded_provers = loaded_prover option PHprover.t
François Bobot's avatar
François Bobot committed
171 172 173 174 175 176 177

type 'a env_session = private
    { env : Env.env;
      whyconf : Whyconf.config;
      loaded_provers : loaded_provers;
      session : 'a session}

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

François Bobot's avatar
François Bobot committed
181 182 183 184 185 186 187 188 189 190 191
(** {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
192
    - the files are reloaded
François Bobot's avatar
François Bobot committed
193
    - apply again the transformation
François Bobot's avatar
François Bobot committed
194
    - if some goals appear try to find to which goal
François Bobot's avatar
François Bobot committed
195 196 197
    in the given session it corresponds.

    The last case meant that the session was obsolete.
François Bobot's avatar
François Bobot committed
198
    It is authorized if [allow_obsolete] is [true],
François Bobot's avatar
François Bobot committed
199 200 201 202 203 204 205 206 207 208
    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

*)

(** {2 Accessor} *)

François Bobot's avatar
François Bobot committed
209 210
exception NoTask
val goal_task : 'key goal -> Task.task
François Bobot's avatar
François Bobot committed
211
(** 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
212 213 214
    (equivalent to 'key = notask) *)

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

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

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


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

François Bobot's avatar
François Bobot committed
227
(** {2 Modificator} *)
François Bobot's avatar
François Bobot committed
228 229 230 231 232 233 234

val set_transf_expanded : 'key transf -> bool -> unit
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
235
(** {2 General type} *)
François Bobot's avatar
François Bobot committed
236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258

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

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 ->
259
  archived:bool ->
François Bobot's avatar
François Bobot committed
260 261 262
  timelimit:int ->
  edit:string option ->
  'key goal ->
263
  Whyconf.prover ->
François Bobot's avatar
François Bobot committed
264 265 266 267 268 269 270 271
  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 ->
272
  archived:bool ->
François Bobot's avatar
François Bobot committed
273 274 275
  proof_attempt_status ->
  'key proof_attempt -> unit

276 277
val set_obsolete : ?notify:'key notify -> 'key proof_attempt -> unit

278
val set_archived : 'key proof_attempt -> bool -> unit
279

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

282 283 284 285 286 287
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
288 289
val set_timelimit : int -> 'key proof_attempt -> unit

290 291 292 293
val copy_external_proof :
  ?notify:'key notify ->
  keygen:'key keygen ->
  ?obsolete:bool ->
294
  ?archived:bool ->
295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321
  ?timelimit:int ->
  ?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}
    {- a session or env_session is given}
    }
    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
322 323 324 325
(** {2 Transformation} *)

val add_transformation :
  keygen:'key keygen ->
François Bobot's avatar
François Bobot committed
326
  goal:('goal -> Ident.ident * expl * Task.task) ->
François Bobot's avatar
François Bobot committed
327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342
  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,
    raise NoTask if the goal doesn't contain a task *)

val remove_transformation : ?notify:'key notify -> 'key transf -> unit
François Bobot's avatar
François Bobot committed
343
  (** Remove a transformation *)
François Bobot's avatar
François Bobot committed
344 345 346 347 348 349 350 351

(** {2 File} *)

val add_file :
  keygen:'key keygen ->
  'key env_session ->
  string ->
  'key file
François Bobot's avatar
François Bobot committed
352
(** Add a real file by its filename *)
François Bobot's avatar
François Bobot committed
353 354

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

(** {2 Explanation} *)
François Bobot's avatar
François Bobot committed
358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383

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
384
(** {3 not recursive} *)
François Bobot's avatar
François Bobot committed
385

François Bobot's avatar
François Bobot committed
386 387 388 389 390 391 392 393 394 395 396 397 398 399
val iter_goal :
  ('key proof_attempt -> unit) -> ('key transf -> unit) -> 'key goal -> unit
val iter_transf :
  ('key goal -> unit) -> 'key transf -> unit


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
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
400
(** {2 Some functorized interface (not very useful...)}*)
François Bobot's avatar
François Bobot committed
401 402 403 404 405 406 407


module AddTransf (X : sig
  type key
  val keygen : key keygen

  type goal
François Bobot's avatar
François Bobot committed
408
  val goal : goal -> Ident.ident * expl * Task.task
François Bobot's avatar
François Bobot committed
409 410 411 412 413 414 415 416 417 418 419 420

  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

module AddFile(X : sig
  type key
  val keygen : key keygen

  type goal
François Bobot's avatar
François Bobot committed
421
  val goal : goal -> Ident.ident * expl * Task.task
François Bobot's avatar
François Bobot committed
422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440

  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
  val add_file : X.key session -> string -> X.file -> X.key file
end


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