session.mli 10.5 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
(* stays here until old IDE is deleted *)
39
val get_prover_data :
40 41
  Env.env -> Util.Mstr.key -> Whyconf.config_prover ->
  prover_data Util.Mstr.t -> prover_data Util.Mstr.t
MARCHE Claude's avatar
MARCHE Claude committed
42
  (** loads all provers from the current configuration *)
43

44

45 46 47
(** {2 Transformation's data} *)

type transformation_data
MARCHE Claude's avatar
MARCHE Claude committed
48
  (** record data for transformations *)
49 50

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

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

56 57
(** {2 Proof attempts} *)

58 59 60
type proof_attempt_status = private
    | Undone
    | Scheduled (** external proof attempt is scheduled *)
61
    | Interrupted
62 63 64
    | 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 *)
65
    | Unedited (** interactive prover yet no proof script *)
66

67 68 69 70 71 72 73 74
(** {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 *)

75 76
(** {2 Observers signature} *)

77
module type OBSERVER = sig
78

79
  type key
MARCHE Claude's avatar
MARCHE Claude committed
80
    (** type key allowing to uniquely identify an element of
81 82
        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
83

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

87
  val remove: key -> unit
MARCHE Claude's avatar
MARCHE Claude committed
88
    (** removes a key *)
89

MARCHE Claude's avatar
MARCHE Claude committed
90 91 92
  val reset: unit -> unit
    (** deletes all keys *)

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

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

103 104 105 106 107
  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 *)
108 109
end

110 111
(** {2 Main functor} *)

112 113
module Make(O: OBSERVER) : sig

114
(** {2 static state of a session} *)
MARCHE Claude's avatar
MARCHE Claude committed
115 116 117 118 119 120

  type goal
    (** a goal *)

  type transf = private
      { transf : transformation_data;
121 122
        parent_goal : goal;
        mutable transf_proved : bool;
MARCHE Claude's avatar
MARCHE Claude committed
123 124
        transf_key : O.key;
        mutable subgoals : goal list;
125
        mutable transf_expanded : bool;
MARCHE Claude's avatar
MARCHE Claude committed
126 127 128
      }
    (** a transformation of a given goal *)

129 130
  val set_transf_expanded : transf -> bool -> unit

MARCHE Claude's avatar
MARCHE Claude committed
131 132 133 134 135 136
  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
137 138
  val goal_expanded : goal -> bool
  val set_goal_expanded : goal -> bool -> unit
139

140 141 142 143
  type prover_option =
    | Detected_prover of prover_data
    | Undetected_prover of string

144
  type proof_attempt = private
145
      { prover : prover_option;
146 147 148
        proof_goal : goal;
        proof_key : O.key;
        mutable proof_state : proof_attempt_status;
149
        mutable timelimit : int;
150 151 152
        mutable proof_obsolete : bool;
        mutable edited_as : string;
      }
MARCHE Claude's avatar
MARCHE Claude committed
153
    (** a proof attempt for a given goal *)
154

155 156
  val external_proofs : goal -> (string, proof_attempt) Hashtbl.t

157
  type theory
MARCHE Claude's avatar
MARCHE Claude committed
158
    (** a theory, holding a collection of goals *)
159

MARCHE Claude's avatar
MARCHE Claude committed
160 161 162 163 164
  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
165 166
  val theory_expanded : theory -> bool
  val set_theory_expanded : theory -> bool -> unit
167

MARCHE Claude's avatar
MARCHE Claude committed
168
  type file = private
169 170 171 172
      { file_name : string;
        file_key : O.key;
        mutable theories: theory list;
        mutable file_verified : bool;
173
        mutable file_expanded : bool;
174 175
      }

176 177
  val set_file_expanded : file -> bool -> unit

178 179 180 181 182 183 184 185
  type any =
    | File of file
    | Theory of theory
    | Goal of goal
    | Proof_attempt of proof_attempt
    | Transformation of transf


186
(** {2 Save and load a state}      *)
187

188 189
  exception OutdatedSession

190
  val open_session :
191
    allow_obsolete:bool ->
MARCHE Claude's avatar
MARCHE Claude committed
192
    env:Env.env ->
193
    config:Whyconf.config ->
194
    init:(O.key -> any -> unit) ->
195
    notify:(any -> unit) ->
196
    string -> bool
197
    (** starts a new proof session, using directory given as argument
MARCHE Claude's avatar
MARCHE Claude committed
198
        this reloads the previous session database if any.
199 200 201 202

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

203 204
        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
205

206 207
        the [init] function is a function that will be called at each
        creation of element of the state
208

209 210
        raises [OutdatedSession] if [allow_obsolete] is false and any obsolete
        data for a goal is found in the session database
211 212 213 214 215 216

        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

217 218
    *)

219 220
  val get_provers : unit -> prover_data Util.Mstr.t

MARCHE Claude's avatar
MARCHE Claude committed
221 222
  val maximum_running_proofs : int ref

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

229 230
  val file_exists : string -> bool

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

236

237 238
  val get_all_files : unit -> file list

239
(** {2 Actions} *)
240 241


MARCHE Claude's avatar
MARCHE Claude committed
242 243
  val apply_transformation : callback:(Task.task list -> unit) ->
    transformation_data -> Task.task -> unit
244

245
  val run_prover : context_unproved_goals_only:bool ->
246
    timelimit:int -> prover_data -> any -> unit
247 248 249 250 251 252 253 254 255 256
    (** [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. *)
257

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

263
  val edit_proof :
264
    default_editor:string -> project_dir:string -> proof_attempt -> unit
265
    (** edit the given proof attempt using the appropriate editor *)
266

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

276 277 278
  val cancel : any -> unit
    (** [cancel a] marks all proofs under [a] as obsolete *)

279
  type report =
280
    | Wrong_result of Call_provers.prover_result * Call_provers.prover_result
281
    | CallFailed of exn
282 283
    | Prover_not_installed
    | No_former_result
284 285

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

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

        raises [OutdatedSession] if [allow_obsolete] is false and any obsolete
        data for a goal is found in the session database
301 302 303 304

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

MARCHE Claude's avatar
MARCHE Claude committed
305
    *)
306

307
  val remove_proof_attempt : proof_attempt -> unit
308 309 310 311 312

  val remove_transformation : transf -> unit

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

315 316 317
  val smoke_detector : smoke_detector ref
    (** Define if the smoke detector is used *)

318
end
319 320 321 322 323 324 325 326



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