session.mli 10.1 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
(** {2 Observers signature} *)

69
module type OBSERVER = sig
70

71
  type key
MARCHE Claude's avatar
MARCHE Claude committed
72
    (** type key allowing to uniquely identify an element of
73 74
        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
75

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

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

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

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

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

95 96 97 98 99
  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 *)
100 101
end

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

104 105
module Make(O: OBSERVER) : sig

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

  type goal
    (** a goal *)

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

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

MARCHE Claude's avatar
MARCHE Claude committed
123 124 125 126 127 128
  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
129 130
  val goal_expanded : goal -> bool
  val set_goal_expanded : goal -> bool -> unit
131

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

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
152 153 154 155 156
  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
157 158
  val theory_expanded : theory -> bool
  val set_theory_expanded : theory -> bool -> unit
159

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

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

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


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

180 181
  exception OutdatedSession

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

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

195 196
        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
197

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

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

        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

209 210
    *)

211 212
  val get_provers : unit -> prover_data Util.Mstr.t

213 214
  val maximum_running_proofs : int ref

215
  val save_session : unit -> unit
216
    (** enforces to save the session state on disk.
217 218 219
        this it supposed to be called only at exit,
        since the session manager also performs automatic saving
        some time to time *)
220

221 222
  val file_exists : string -> bool

MARCHE Claude's avatar
MARCHE Claude committed
223
  val add_file : string -> unit
224
    (** [add_file f] adds the file [f] in the proof session,
225 226
        the file name must be given relatively to the session dir
        given to [open_session] *)
227

228

229 230
  val get_all_files : unit -> file list

231
(** {2 Actions} *)
232 233


MARCHE Claude's avatar
MARCHE Claude committed
234 235
  val apply_transformation : callback:(Task.task list -> unit) ->
    transformation_data -> Task.task -> unit
236

237
  val run_prover : context_unproved_goals_only:bool ->
238
    timelimit:int -> prover_data -> any -> unit
239 240 241 242 243 244 245 246 247 248
    (** [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. *)
249

250
  val transform : context_unproved_goals_only:bool ->
251
    transformation_data -> any -> unit
252
    (** [apply_transformation tr a] applies transformation [trp]
253
        on all goals under [a] *)
254

255
  val edit_proof :
256
    default_editor:string -> project_dir:string -> proof_attempt -> unit
257
    (** edit the given proof attempt using the appropriate editor *)
258

259 260
  val replay :
    obsolete_only:bool ->
261
    context_unproved_goals_only:bool -> any -> unit
262
    (** [replay a] reruns proofs under [a]
263
        if obsolete_only is set then does not rerun non-obsolete proofs
264
        if context_unproved_goals_only is set then reruns only proofs
265
        with result was 'valid'
266
    *)
267

268 269 270
  val cancel : any -> unit
    (** [cancel a] marks all proofs under [a] as obsolete *)

271
  type report =
272
    | Wrong_result of Call_provers.prover_result * Call_provers.prover_result
273
    | CallFailed of exn
274 275
    | Prover_not_installed
    | No_former_result
276 277

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

285
  val reload_all: bool -> bool
286
    (** reloads all the files
287 288
        If for one of the file, the parsing or typing fails, then
        the complete old session state is kept, and an exception
289
        is raised
290 291 292

        raises [OutdatedSession] if [allow_obsolete] is false and any obsolete
        data for a goal is found in the session database
293 294 295 296

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

MARCHE Claude's avatar
MARCHE Claude committed
297
    *)
298

299
  val remove_proof_attempt : proof_attempt -> unit
300 301 302 303 304

  val remove_transformation : transf -> unit

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

307
end
308 309 310 311 312 313 314 315



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