session.mli 5.45 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 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
open Why

type prover_data = private
    { prover_id : string;
      prover_name : string;
      prover_version : string;
      command : string;
      driver_name : string;
      driver : Driver.driver;
      mutable editor : string;
    }

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 *)
39 40

module type OBSERVER = sig
41

42 43 44
  type key
  val create: ?parent:key -> unit -> key
  val remove: key -> unit
45 46 47 48

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

49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
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 =
69 70
    | Parent_theory of theory
    | Parent_transf of transf
71 72 73

  and goal = private
      { goal_name : string;
74
	goal_expl : string option;
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 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
	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
      { parent_goal : goal;
	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      *)
  (*                           *)
  (*****************************)

MARCHE Claude's avatar
MARCHE Claude committed
119
  val open_session : notify:(any -> unit) -> string -> unit
120 121 122 123 124 125
    (** 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.

MARCHE Claude's avatar
MARCHE Claude committed
126 127
	the [notify] function is a function that will be called at each
	update of element of the state
128 129
    *)

MARCHE Claude's avatar
MARCHE Claude committed
130 131
  val maximum_running_proofs : int ref

132 133 134 135 136 137
    (* 
  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 *)

138 139 140 141
  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] *)

142

143 144 145 146 147
  (*
    val reload_files : unit -> unit 
  (** reloads all the files in the state, and performs the proper
    merging of old proof attemps and transformations *)
*)
148 149 150 151 152 153 154 155

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


156 157 158
  val run_prover : context_unproved_goals_only:bool -> 
    prover_data -> any -> unit
    (** [run_prover p a] runs prover [p] on all goals under [a] *)
159

160 161
  val replay : context_unproved_goals_only:bool -> any -> unit
    (** [replay a] reruns all valid but obsolete proofs under [a] *)
162

163 164 165
(*

  val remove_proof_attempt : proof_attempt -> unit
166 167 168 169 170

  val remove_transformation : transf -> unit

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

173 174
    *) 
end
175 176 177 178 179 180 181 182



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