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

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;
    }
33 34 35 36

type transformation_data 

val transformation_id : transformation_data -> string
37 38 39 40 41 42 43

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 *)
44 45

module type OBSERVER = sig
46

47 48 49
  type key
  val create: ?parent:key -> unit -> key
  val remove: key -> unit
50 51 52 53

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

54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
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 =
74 75
    | Parent_theory of theory
    | Parent_transf of transf
76 77 78

  and goal = private
      { goal_name : string;
79
	goal_expl : string option;
80 81 82 83 84 85 86 87 88
	parent : goal_parent;
        task: Task.task;
        goal_key : O.key;
        mutable proved : bool;
        external_proofs: (string, proof_attempt) Hashtbl.t;
        transformations : (string, transf) Hashtbl.t;
      }

  and transf = private
89 90
      { transf : transformation_data;
	parent_goal : goal;
91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
	mutable transf_proved : bool;
        transf_key : O.key;
        mutable subgoals : goal list;
      }

  and theory = private
      { theory : Theory.theory;
        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


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

125 126 127
  val open_session : 
    init:(O.key -> any -> unit) ->
    notify:(any -> unit) -> string -> unit
128 129 130 131 132 133
    (** 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.

134 135 136
	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
137 138
	the [notify] function is a function that will be called at each
	update of element of the state
139 140
    *)

MARCHE Claude's avatar
MARCHE Claude committed
141 142
  val maximum_running_proofs : int ref

143 144 145 146 147 148
    (* 
  val save_session : unit -> unit
    (** enforces to save the session state on disk. *)
       this is not necessary since the session manager handles this itself
       using add_timeout *)

149 150
  val file_exists : string -> bool

151 152 153 154
  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] *)

155

156 157
  val get_all_files : unit -> file list

158 159 160 161 162
  (*
    val reload_files : unit -> unit 
  (** reloads all the files in the state, and performs the proper
    merging of old proof attemps and transformations *)
*)
163 164 165 166 167 168 169

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

170 171 172 173 174
  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
175

176 177 178
  val run_prover : context_unproved_goals_only:bool -> 
    prover_data -> any -> unit
    (** [run_prover p a] runs prover [p] on all goals under [a] *)
179

180 181 182
  val edit_proof : 
    default_editor:string -> project_dir:string -> proof_attempt -> unit

183 184
  val replay : context_unproved_goals_only:bool -> any -> unit
    (** [replay a] reruns all valid but obsolete proofs under [a] *)
185

186 187
(*

188

189
  val remove_proof_attempt : proof_attempt -> unit
190 191 192 193 194

  val remove_transformation : transf -> unit

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

197 198
    *) 
end
199 200 201 202 203 204 205 206



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