session.mli 10.4 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

20
(** Proof sessions *)
21

22
open Why3
23

24 25
(** {2 Prover's data} *)

26
type prover_data = private
27 28 29 30 31 32 33
    { prover_id : string;
      prover_name : string;
      prover_version : string;
      command : string;
      driver_name : string;
      driver : Driver.driver;
      mutable editor : string;
34
      interactive : bool;
35
    }
MARCHE Claude's avatar
MARCHE Claude committed
36
    (** record of necessary data for a given external prover *)
37

38 39 40
(** {2 Transformation's data} *)

type transformation_data
MARCHE Claude's avatar
MARCHE Claude committed
41
  (** record data for transformations *)
42 43

val transformation_id : transformation_data -> string
MARCHE Claude's avatar
MARCHE Claude committed
44
  (** Why3 name of a transformation *)
45

46
val lookup_transformation : Env.env -> string -> transformation_data
MARCHE Claude's avatar
MARCHE Claude committed
47
  (** returns a transformation from its Why3 name *)
48

49 50
(** {2 Proof attempts} *)

51 52 53
type proof_attempt_status = private
    | Undone
    | Scheduled (** external proof attempt is scheduled *)
54
    | Interrupted
55 56 57
    | Running (** external proof attempt is in progress *)
    | Done of Call_provers.prover_result (** external proof done *)
    | InternalFailure of exn (** external proof aborted by internal error *)
58
    | Unedited (** interactive prover yet no proof script *)
59

60 61 62 63 64 65 66 67
(** {2 Smoke detector} *)

type smoke_detector =
  | SD_None (** No smoke detector *)
  | SD_Top  (** Negation added at the top of the goals *)
  | SD_Deep
(** Negation added under implication and universal quantification *)

68 69
(** {2 Observers signature} *)

70
module type OBSERVER = sig
71

72
  type key
MARCHE Claude's avatar
MARCHE Claude committed
73
    (** type key allowing to uniquely identify an element of
74 75
        of session: a goal, a transformation, a proof attempt,
        a theory or a file. See type [any] below *)
MARCHE Claude's avatar
MARCHE Claude committed
76

77
  val create: ?parent:key -> unit -> key
MARCHE Claude's avatar
MARCHE Claude committed
78 79
    (** returns a fresh key, a new child of the given parent if any *)

80
  val remove: key -> unit
MARCHE Claude's avatar
MARCHE Claude committed
81
    (** removes a key *)
82

MARCHE Claude's avatar
MARCHE Claude committed
83 84 85
  val reset: unit -> unit
    (** deletes all keys *)

86
  val timeout: ms:int -> (unit -> bool) -> unit
MARCHE Claude's avatar
MARCHE Claude committed
87
    (** a handler for functions that must be called after a given time
88 89
        elapsed, in milliseconds. When the given function returns
        true, it must be rescheduled *)
MARCHE Claude's avatar
MARCHE Claude committed
90

91
  val idle: (unit -> bool) -> unit
MARCHE Claude's avatar
MARCHE Claude committed
92
    (** a handler for a delayed function, that can be called when
93 94
        there is nothing else to do. When the given function returns
        true, it must be rescheduled *)
95

96 97 98 99 100
  val notify_timer_state : int -> int -> int -> unit
    (** this function is called when timer state changes.
        The first arg is the number of tasks waiting.
        The second arg is the number of scheduled proof tasks.
        The third arg is the number of running proof tasks *)
101 102
end

103 104
(** {2 Main functor} *)

105 106
module Make(O: OBSERVER) : sig

107
(** {2 static state of a session} *)
MARCHE Claude's avatar
MARCHE Claude committed
108 109 110 111 112 113

  type goal
    (** a goal *)

  type transf = private
      { transf : transformation_data;
114 115
        parent_goal : goal;
        mutable transf_proved : bool;
MARCHE Claude's avatar
MARCHE Claude committed
116 117
        transf_key : O.key;
        mutable subgoals : goal list;
118
        mutable transf_expanded : bool;
MARCHE Claude's avatar
MARCHE Claude committed
119 120 121
      }
    (** a transformation of a given goal *)

122 123
  val set_transf_expanded : transf -> bool -> unit

MARCHE Claude's avatar
MARCHE Claude committed
124 125 126 127 128 129
  val goal_name : goal -> string
  val goal_expl : goal -> string
  val get_task : goal -> Task.task
  val goal_key : goal -> O.key
  val goal_proved : goal -> bool
  val transformations : goal -> (string, transf) Hashtbl.t
130 131
  val goal_expanded : goal -> bool
  val set_goal_expanded : goal -> bool -> unit
132

133 134 135 136
  type prover_option =
    | Detected_prover of prover_data
    | Undetected_prover of string

137
  type proof_attempt = private
138
      { prover : prover_option;
139 140 141
        proof_goal : goal;
        proof_key : O.key;
        mutable proof_state : proof_attempt_status;
142
        mutable timelimit : int;
143 144 145
        mutable proof_obsolete : bool;
        mutable edited_as : string;
      }
MARCHE Claude's avatar
MARCHE Claude committed
146
    (** a proof attempt for a given goal *)
147

148 149
  val external_proofs : goal -> (string, proof_attempt) Hashtbl.t

150
  type theory
MARCHE Claude's avatar
MARCHE Claude committed
151
    (** a theory, holding a collection of goals *)
152

MARCHE Claude's avatar
MARCHE Claude committed
153 154 155 156 157
  val theory_name : theory -> string
  val get_theory : theory -> Theory.theory
  val theory_key : theory -> O.key
  val verified : theory -> bool
  val goals : theory -> goal list
158 159
  val theory_expanded : theory -> bool
  val set_theory_expanded : theory -> bool -> unit
160

MARCHE Claude's avatar
MARCHE Claude committed
161
  type file = private
162 163 164 165
      { file_name : string;
        file_key : O.key;
        mutable theories: theory list;
        mutable file_verified : bool;
166
        mutable file_expanded : bool;
167 168
      }

169 170
  val set_file_expanded : file -> bool -> unit

171 172 173 174 175 176 177 178
  type any =
    | File of file
    | Theory of theory
    | Goal of goal
    | Proof_attempt of proof_attempt
    | Transformation of transf


179
(** {2 Save and load a state}      *)
180

181 182
  exception OutdatedSession

183
  val open_session :
184
    allow_obsolete:bool ->
MARCHE Claude's avatar
MARCHE Claude committed
185
    env:Env.env ->
186
    config:Whyconf.config ->
187
    init:(O.key -> any -> unit) ->
188
    notify:(any -> unit) ->
189
    string -> bool
190
    (** starts a new proof session, using directory given as argument
MARCHE Claude's avatar
MARCHE Claude committed
191
        this reloads the previous session database if any.
192 193 194 195

        Opening a session must be done prior to any other actions.
        And it cannot be done twice.

196 197
        the [notify] function is a function that will be called at each
        update of element of the state
MARCHE Claude's avatar
MARCHE Claude committed
198

199 200
        the [init] function is a function that will be called at each
        creation of element of the state
201

202 203
        raises [OutdatedSession] if [allow_obsolete] is false and any obsolete
        data for a goal is found in the session database
204 205 206 207 208 209

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

        returns true if some obsolete goal was found (and
        [allow_obsolete] is true), false otherwise

210 211
    *)

212
  val get_provers : unit -> prover_data Util.Mstr.t
213 214 215 216
  (** The provers on this computer *)

  val get_old_provers : unit -> (string * string) Util.Mstr.t
  (** The provers in this session (name * version ) *)
217

218 219
  val maximum_running_proofs : int ref

220
  val save_session : unit -> unit
221
    (** enforces to save the session state on disk.
222 223 224
        this it supposed to be called only at exit,
        since the session manager also performs automatic saving
        some time to time *)
225

226 227
  val file_exists : string -> bool

MARCHE Claude's avatar
MARCHE Claude committed
228
  val add_file : string -> unit
229
    (** [add_file f] adds the file [f] in the proof session,
230 231
        the file name must be given relatively to the session dir
        given to [open_session] *)
232

233

234 235
  val get_all_files : unit -> file list

236
(** {2 Actions} *)
237 238


MARCHE Claude's avatar
MARCHE Claude committed
239 240
  val apply_transformation : callback:(Task.task list -> unit) ->
    transformation_data -> Task.task -> unit
241

242
  val run_prover : context_unproved_goals_only:bool ->
243
    timelimit:int -> prover_data -> any -> unit
244 245 246 247 248 249 250 251 252 253
    (** [run_prover p a] runs prover [p] on all goals under [a]
        the proof attempts are only scheduled for running, and they
        will be started asynchronously when processors are available
    *)

  val cancel_scheduled_proofs : unit -> unit
    (** cancels all currently scheduled proof attempts.
        note that the already running proof attempts are not
        stopped, the corresponding processes must terminate
        by their own. *)
254

255
  val transform : context_unproved_goals_only:bool ->
256
    transformation_data -> any -> unit
257
    (** [apply_transformation tr a] applies transformation [trp]
258
        on all goals under [a] *)
259

260
  val edit_proof :
261
    default_editor:string -> project_dir:string -> proof_attempt -> unit
262
    (** edit the given proof attempt using the appropriate editor *)
263

264 265
  val replay :
    obsolete_only:bool ->
266
    context_unproved_goals_only:bool -> any -> unit
267
    (** [replay a] reruns proofs under [a]
268
        if obsolete_only is set then does not rerun non-obsolete proofs
269
        if context_unproved_goals_only is set then reruns only proofs
270
        with result was 'valid'
271
    *)
272

273 274 275
  val cancel : any -> unit
    (** [cancel a] marks all proofs under [a] as obsolete *)

276
  type report =
277
    | Wrong_result of Call_provers.prover_result * Call_provers.prover_result
278
    | CallFailed of exn
279 280
    | Prover_not_installed
    | No_former_result
281 282

  val check_all: callback:((string * string * report) list -> unit) -> unit
283
    (** [check_all ()] reruns all the proofs of the session, and reports
284
        all difference with the current state
285
        (does not change the session state)
286
        When finished, calls the callback with the list of failed comparisons,
287
        which are triples (goal name, prover, report)
288 289
    *)

290
  val reload_all: bool -> bool
291
    (** reloads all the files
292 293
        If for one of the file, the parsing or typing fails, then
        the complete old session state is kept, and an exception
294
        is raised
295 296 297

        raises [OutdatedSession] if [allow_obsolete] is false and any obsolete
        data for a goal is found in the session database
298 299 300 301

        returns true if some obsolete goal was found (and
        [allow_obsolete] is true), false otherwise

MARCHE Claude's avatar
MARCHE Claude committed
302
    *)
303

304
  val remove_proof_attempt : proof_attempt -> unit
305 306 307 308 309

  val remove_transformation : transf -> unit

  val clean : any -> unit
    (** [clean a] removes failed attempts below [a] where
310
        there at least one successful attempt or transformation *)
311

312 313 314
  val smoke_detector : smoke_detector ref
    (** Define if the smoke detector is used *)

315
end
316 317 318 319 320 321 322 323



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