session.mli 6.83 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

23
type prover_data = private
24 25 26 27 28 29 30 31
    { prover_id : string;
      prover_name : string;
      prover_version : string;
      command : string;
      driver_name : string;
      driver : Driver.driver;
      mutable editor : string;
    }
32

33 34 35 36
val get_prover_data : 
  Env.env -> Util.Mstr.key -> Whyconf.config_prover ->
  prover_data Util.Mstr.t -> prover_data Util.Mstr.t

37
(* transformations *)
38 39 40
type transformation_data 

val transformation_id : transformation_data -> string
41

42 43
val lookup_transformation : Env.env -> string -> transformation_data

44 45 46 47 48 49
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 *)
50 51

module type OBSERVER = sig
52

53 54 55
  type key
  val create: ?parent:key -> unit -> key
  val remove: key -> unit
56 57 58 59

  val timeout: ms:int -> (unit -> bool) -> unit
  val idle: (unit -> bool) -> unit

60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
end

module Make(O: OBSERVER) : sig

(*****************************)
(*                           *)
(* static state of a session *)
(*                           *)
(*****************************)

  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;
      }

  and goal_parent =
80 81
    | Parent_theory of theory
    | Parent_transf of transf
82 83 84

  and goal = private
      { goal_name : string;
85
	goal_expl : string option;
86
	parent : goal_parent;
87
        task: Task.task option;
88 89 90 91 92 93 94
        goal_key : O.key;
        mutable proved : bool;
        external_proofs: (string, proof_attempt) Hashtbl.t;
        transformations : (string, transf) Hashtbl.t;
      }

  and transf = private
95 96
      { transf : transformation_data;
	parent_goal : goal;
97 98 99 100 101 102
	mutable transf_proved : bool;
        transf_key : O.key;
        mutable subgoals : goal list;
      }

  and theory = private
103 104
      { theory_name : string;
	theory : Theory.theory option;
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125
        theory_key : O.key;
        theory_parent : file;
        mutable goals : goal list;
        mutable verified : bool;
      }

  and file = private
      { 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


126 127 128 129
  val get_theory : theory -> Theory.theory

  val get_task : goal -> Task.task

130 131 132 133 134 135
  (*****************************)
  (*                           *)
  (*      save/load state      *)
  (*                           *)
  (*****************************)

136
  val open_session : 
MARCHE Claude's avatar
MARCHE Claude committed
137
    env:Env.env ->
MARCHE Claude's avatar
MARCHE Claude committed
138
    provers:prover_data Util.Mstr.t ->
139 140
    init:(O.key -> any -> unit) ->
    notify:(any -> unit) -> string -> unit
141 142 143 144 145 146
    (** starts a new proof session, using directory given as argument 
        this reloads the previous session if any.

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

147 148 149
	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
150 151
	the [notify] function is a function that will be called at each
	update of element of the state
152 153
    *)

MARCHE Claude's avatar
MARCHE Claude committed
154 155
  val maximum_running_proofs : int ref

MARCHE Claude's avatar
MARCHE Claude committed
156
(*
157
  val test_save : unit -> unit
MARCHE Claude's avatar
MARCHE Claude committed
158 159
  val test_load : unit -> Xml.t
*)
MARCHE Claude's avatar
MARCHE Claude committed
160

161
  val save_session : unit -> unit
162 163 164 165
    (** 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 *)
166

167 168
  val file_exists : string -> bool

169 170 171 172
  val add_file : string -> Theory.theory Theory.Mnm.t -> unit
    (** [add_file f ths] adds a new file in the proof session, that is
	a collection of name [f] of theories [ths] *)

173

174 175
  val get_all_files : unit -> file list

176 177 178 179 180
  (*
    val reload_files : unit -> unit 
  (** reloads all the files in the state, and performs the proper
    merging of old proof attemps and transformations *)
*)
181 182 183 184 185 186 187

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

188
(*
189 190 191 192 193
  val apply_transformation : 
    callback:('a -> 'b) -> 'a Why.Trans.trans -> Why.Task.task -> 'b

  val apply_transformation_l : 
    callback:('a -> 'b) -> 'a Why.Trans.trans -> Why.Task.task -> 'b
194 195 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 215
(*

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:
*)