controller_itp.mli 10.7 KB
Newer Older
Clément Fumex's avatar
Clément Fumex committed
1 2 3 4 5 6 7 8 9 10 11 12 13
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

open Session_itp

14 15
exception Noprogress

Clément Fumex's avatar
Clément Fumex committed
16 17 18 19 20 21 22 23 24
(** State of a proof *)
type proof_attempt_status =
    | Unedited (** editor not yet run for interactive proof *)
    | JustEdited (** edited but not run yet *)
    | Interrupted (** external proof has never completed *)
    | 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 *)
25
    | Uninstalled of Whyconf.prover (** prover is uninstalled *)
Clément Fumex's avatar
Clément Fumex committed
26

MARCHE Claude's avatar
MARCHE Claude committed
27 28
val print_status : Format.formatter -> proof_attempt_status -> unit

29 30 31 32
type transformation_status =
    TSscheduled
  | TSdone of transID
  | TSfailed of (proofNodeID * exn)
33 34

val print_trans_status : Format.formatter -> transformation_status -> unit
35

MARCHE Claude's avatar
MARCHE Claude committed
36 37 38 39
type strategy_status = STSgoto of proofNodeID * int | STShalt

val print_strategy_status : Format.formatter -> strategy_status -> unit

40
module type Scheduler = sig
MARCHE Claude's avatar
MARCHE Claude committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61

    (** Any module of this signature should implement a scheduler,
    that allows the register functions to call, and call them
    depending on some time constraints: after a given delay, or simply
    when there is no more tasks with higher priority. *)

    val timeout: ms:int -> (unit -> bool) -> unit
    (** [timeout ~ms f] registers the function [f] as a function to be
    called every [ms] milliseconds. The function is called repeatedly
    until it returns false. the [ms] delay is not strictly guaranteed:
    it is only a minimum delay between the end of the last call and
    the beginning of the next call.  Several functions can be
    registered at the same time. *)

    val idle: prio:int -> (unit -> bool) -> unit
    (** [idle prio f] registers the function [f] as a function to be
    called whenever there is nothing else to do. Several functions can
    be registered at the same time.  Several functions can be
    registered at the same time. Functions registered with higher
    priority will be called first. *)

62 63
end

64
type controller = private
65
  { mutable controller_session : Session_itp.session;
66
    controller_config : Whyconf.config;
67
    controller_env : Env.env;
68 69
    controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
  }
70

71 72
val create_controller: Whyconf.config -> Env.env -> Session_itp.session -> controller
(** creates a controller for the given session.
73
    The config and env is used to load the drivers for the provers. *)
74

75 76
val print_session : Format.formatter -> controller -> unit

77 78 79 80 81 82 83 84

(*

  - TODO: the presence of obsolete goals should be returned somehow by
    that function, as the presence of unmatch old theories or goals

 *)
val reload_files : controller -> use_shapes:bool -> unit  (* (bool * bool) see above *)
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 119 120 121 122 123
(** reload the files of the given session:

  - each file is parsed again and theories/goals extracted from it. If
    some syntax error or parsing error occurs, then the corresponding
    file is kept in the session, without any corresponding new theory,
    that is as if it was an empty file (TODO: such errors should be
    returned somehow by the function [reload_files])

  - each new theory is associated to a theory of the former session if
    the names match exactly. In case of no match:

    . a new theory and its goals appear without any proof attempts in
      it in the new session

    . an unmatched old theory is kept in the new session together with
      its former goals, proof attempts and transformations, but
      without any tasks associated to goals and subgoals.

  - within a new theory with a corresponding old theory, each goal is
    in turn associated to a former goal if possible. the match is done
    either on the goal name, or if no name match exactly, on the goal
    shape.

    . a new goal without match is added with an empty set of proof
      attempts and transformations

    . an old goal without match is kept with all its former proof
      attempts and transformations, but no task is associated to it,
      neither to its subgoals.

  - on each new goal that has a matching old goal, old proof
    attempts are attached, with the status obsolete if the task has
    changed

  - on each new goal that has a matching old goal, old
    transformations are attached, and applied to the task, the
    generated subgoals are in turn matched to the old sub-goals, in
    the same manner as for goals in a theory

Clément Fumex's avatar
Clément Fumex committed
124 125 126 127 128
    . an old sub-goals without a match is kept with all its former
      proof attempts and transformations, but no task is associated to
      it, neither to its subgoals.

*)
129

130 131 132 133
val add_file : controller -> ?format:Env.fformat -> string -> unit
(** [add_fil cont ?fmt fname] parses the source file
    [fname] and add the resulting theories to the session of [cont] *)

Sylvain Dailler's avatar
Sylvain Dailler committed
134 135
val remove_subtree: controller -> notification:notifier -> removed:notifier ->
   any -> unit
136 137
(** Mapping to Session_itp.remove_subtree. Used for code using Why3's API *)

138 139
val get_undetached_children_no_pa: Session_itp.session -> any -> any list

140

141 142
module Make(S : Scheduler) : sig

143 144 145 146 147 148
val set_max_tasks : int -> unit
(** sets the maximum number of proof tasks that can be running at the
    same time. Initially set to 1. *)

val register_observer : (int -> int -> int -> unit) -> unit
(** records a hook that will be called with the number of waiting
149
    tasks, scheduled tasks, and running tasks, each time these numbers
150 151
    change *)

152 153 154 155 156 157
(* TODO
val register_notifier : (any -> unit) -> unit
(** records a hook that will be called each time a node change status *)
 *)


158 159
val interrupt : unit -> unit
(** discards all scheduled proof attempts or transformations, including
160
    the ones already running *)
161

162
val schedule_proof_attempt :
163
  ?proof_script:string ->
164 165 166
  controller ->
  proofNodeID ->
  Whyconf.prover ->
167
  counterexmp:bool ->
168
  limit:Call_provers.resource_limit ->
169
  callback:(proofAttemptID -> proof_attempt_status -> unit) ->
170
  notification:notifier -> unit
Sylvain Dailler's avatar
Sylvain Dailler committed
171
(** [schedule_proof_attempt c id p ~timelimit ~callback ~notification] schedules a
172 173 174 175 176 177
   proof attempt for a goal specified by [id] with the prover [p] with
   time limit [timelimit]; the function [callback] will be called each
   time the proof attempt status changes. Typically at Scheduled, then
   Running, then Done. If there is already a proof attempt with [p] it
   is updated. *)

Sylvain Dailler's avatar
Sylvain Dailler committed
178 179 180 181 182 183 184 185 186 187 188 189 190 191
val schedule_edition :
  controller ->
  proofNodeID ->
  Whyconf.prover ->
  ?file: string ->
  callback:(proofAttemptID -> proof_attempt_status -> unit) ->
  notification:notifier -> unit
(** [schedule_edition c id pr ?file ~callback ~notification] runs
    the editor for prover [pr] on proofnode [id] on a file automatically
    generated in [file] (or created path). It will runs callback each time
    the proof status changes and notification will be called each time a
    change is made to the proof_state (in the whole proof tree of the session)
*)

192 193 194 195 196
val schedule_transformation :
  controller ->
  proofNodeID ->
  string ->
  string list ->
197
  callback:(transformation_status -> unit) ->
198
  notification:notifier -> unit
199 200 201 202 203 204 205 206 207
(** [schedule_transformation c id cb] schedules a transformation for a
   goal specified by [id]; the function [cb] will be called each time
   the transformation status changes. Typically at Scheduled, then
   Done tid.*)

val run_strategy_on_goal :
  controller ->
  proofNodeID ->
  Strategy.t ->
208
  counterexmp:bool ->
MARCHE Claude's avatar
MARCHE Claude committed
209 210
  callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
  callback_tr:(transformation_status -> unit) ->
211
  callback:(strategy_status -> unit) ->
212
  notification:notifier -> unit
213
(** [run_strategy_on_goal c id strat] executes asynchronously the
MARCHE Claude's avatar
MARCHE Claude committed
214 215 216 217 218
    strategy [strat] on the goal [id].  [callback_pa] is called for
    each proof attempted (as in [schedule_proof_attempt]) and
    [callback_tr] is called for each transformation applied (as in
    [schedule_transformation]). [callback] is called on each step of
    execution of the strategy.  *)
219

220 221 222 223
val clean_session: controller -> removed:notifier -> unit
(** Remove each proof attempt or transformation that are below proved
    goals, that are either obsolete or not valid. The [removed]
    notifier is called on each removed node.  *)
224

225
val mark_as_obsolete:
226
  notification:notifier ->
227 228
  controller -> any -> unit

Sylvain Dailler's avatar
Sylvain Dailler committed
229 230
(* [copy_paste c a b] try to copy subtree originating at node a to node b *)
val copy_paste:
231
    notification:notifier ->
Sylvain Dailler's avatar
Sylvain Dailler committed
232 233 234 235 236 237 238
    callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
    callback_tr:(transformation_status -> unit) ->
    controller -> any -> any -> unit

val copy_detached:
    copy:(parent:any -> any -> unit) ->
    controller -> any -> unit
239

240 241 242 243
type report =
  | Result of Call_provers.prover_result * Call_provers.prover_result
        (** Result(new_result,old_result) *)
  | CallFailed of exn
244
  | Replay_interrupted
245 246 247 248 249
  | Prover_not_installed
  | Edited_file_absent of string
  | No_former_result of Call_provers.prover_result
(** Type for the reporting of a replayed call *)

250 251 252
(* Callback for the report printing of replay
   TODO to be removed when we have a better way to print the result of replay *)
val replay_print:
253 254 255
    Format.formatter ->
      (proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list ->
        unit
256 257

val replay:
258 259
    ?obsolete_only:bool ->
    ?use_steps:bool ->
260
    controller ->
261
    callback:(proofAttemptID -> proof_attempt_status -> unit) ->
262
    notification:notifier ->
263
    final_callback:
264 265 266
      ((proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list
            -> unit) ->
    unit
267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284
(** This function reruns all the proofs of the session, and produces a report
    comparing the results with the former ones.

    The proofs are replayed asynchronously, and the states of these proofs are
    notified via [callback] similarly as for [schedule_proof_attempt].

    The session state is changed, all changes are notified via the
    callback [notification]

    When finished, call the callback [final_callback] with the report,
a list of 4-uples [(goalID, prover, limits, report)]

    When obsolete_only is set, only obsolete proofs are replayed (default)

    When use_steps is set, replay use the recorded number of proof
    steps (not set by default)

 *)
285 286


287
end