session.mli 7.28 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)


21 22
open Why

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

35 36 37
val get_prover_data : 
  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
38
  (** loads all provers from the current configuration *)
39

MARCHE Claude's avatar
MARCHE Claude committed
40
(** {Transformation's data} *)
41
type transformation_data 
MARCHE Claude's avatar
MARCHE Claude committed
42
  (** record data for transformations *)
43 44

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

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

MARCHE Claude's avatar
MARCHE Claude committed
50
(** {Proof attempts} *)
51 52 53 54 55 56
type proof_attempt_status = private
    | Undone
    | Scheduled (** external proof attempt is scheduled *)
    | 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 *)
57

MARCHE Claude's avatar
MARCHE Claude committed
58
(** {Observers signature} *)
59
module type OBSERVER = sig
60

61
  type key
MARCHE Claude's avatar
MARCHE Claude committed
62 63 64 65
    (** type key allowing to uniquely identify an element of
	of session: a goal, a transformation, a proof attempt,
	a theory or a file. See type [any] below *)

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

69
  val remove: key -> unit
MARCHE Claude's avatar
MARCHE Claude committed
70
    (** removes a key *)
71 72

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

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

82 83
end

MARCHE Claude's avatar
MARCHE Claude committed
84
(** {Main functor} *)
85 86
module Make(O: OBSERVER) : sig

MARCHE Claude's avatar
MARCHE Claude committed
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
(** {static state of a session} *)

  type goal
    (** a goal *)

  type transf = private
      { transf : transformation_data;
	parent_goal : goal;
	mutable transf_proved : bool;
        transf_key : O.key;
        mutable subgoals : goal list;
      }
    (** a transformation of a given goal *)

  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
107 108 109 110 111 112 113 114 115

  type proof_attempt = private
      { prover : prover_data;
        proof_goal : goal;
        proof_key : O.key;
        mutable proof_state : proof_attempt_status;
        mutable proof_obsolete : bool;
        mutable edited_as : string;
      }
MARCHE Claude's avatar
MARCHE Claude committed
116
    (** a proof attempt for a given goal *)
117

MARCHE Claude's avatar
MARCHE Claude committed
118 119
  type theory 
    (** a theory, holding a collection of goals *)
120

MARCHE Claude's avatar
MARCHE Claude committed
121 122 123 124 125
  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
126

MARCHE Claude's avatar
MARCHE Claude committed
127
  type file = private
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147
      { file_name : string;
        file_key : O.key;
        mutable theories: theory list;
        mutable file_verified : bool;
      }

  type any =
    | File of file
    | Theory of theory
    | Goal of goal
    | Proof_attempt of proof_attempt
    | Transformation of transf


  (*****************************)
  (*                           *)
  (*      save/load state      *)
  (*                           *)
  (*****************************)

148
  val open_session : 
MARCHE Claude's avatar
MARCHE Claude committed
149
    env:Env.env ->
MARCHE Claude's avatar
MARCHE Claude committed
150
    provers:prover_data Util.Mstr.t ->
151 152
    init:(O.key -> any -> unit) ->
    notify:(any -> unit) -> string -> unit
153
    (** starts a new proof session, using directory given as argument 
MARCHE Claude's avatar
MARCHE Claude committed
154
        this reloads the previous session database if any.
155 156 157 158

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

159 160 161
	the [init] function is a function that will be called at each
	creation of element of the state

MARCHE Claude's avatar
MARCHE Claude committed
162 163
	the [notify] function is a function that will be called at each
	update of element of the state
164 165
    *)

MARCHE Claude's avatar
MARCHE Claude committed
166 167
  val maximum_running_proofs : int ref

168
  val save_session : unit -> unit
169 170 171 172
    (** enforces to save the session state on disk. 
	this it supposed to be called only at exit, 
	since the session manager also performs automatic saving 
	some time to time *)
173

174 175
  val file_exists : string -> bool

MARCHE Claude's avatar
MARCHE Claude committed
176 177 178 179
  val add_file : string -> unit
    (** [add_file adds the file [f] in the proof session,
	the file name must be given relatively to the session dir
	given to [open_session] *)
180

181

182 183
  val get_all_files : unit -> file list

MARCHE Claude's avatar
MARCHE Claude committed
184
  (* TODO
185 186 187 188
    val reload_files : unit -> unit 
  (** reloads all the files in the state, and performs the proper
    merging of old proof attemps and transformations *)
*)
189 190 191 192 193 194 195

(*****************************)
(*                           *)
(*      actions              *)
(*                           *)
(*****************************)

MARCHE Claude's avatar
MARCHE Claude committed
196 197
  val apply_transformation : callback:(Task.task list -> unit) ->
    transformation_data -> Task.task -> unit
198

199 200 201
  val run_prover : context_unproved_goals_only:bool -> 
    prover_data -> any -> unit
    (** [run_prover p a] runs prover [p] on all goals under [a] *)
202

203 204 205 206 207
  val transform : context_unproved_goals_only:bool -> 
    transformation_data -> any -> unit
    (** [apply_transformation tr a] applies transformation [trp] 
	on all goals under [a] *)

208 209 210
  val edit_proof : 
    default_editor:string -> project_dir:string -> proof_attempt -> unit

211 212
  val replay : context_unproved_goals_only:bool -> any -> unit
    (** [replay a] reruns all valid but obsolete proofs under [a] *)
213

214
(*
MARCHE Claude's avatar
MARCHE Claude committed
215
TODO
216

217
  val remove_proof_attempt : proof_attempt -> unit
218 219 220 221 222

  val remove_transformation : transf -> unit

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

225 226
    *) 
end
227 228 229 230 231 232 233 234



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