controller_itp.mli 14.8 KB
Newer Older
Clément Fumex's avatar
Clément Fumex committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
Clément Fumex's avatar
Clément Fumex committed
5 6 7 8 9 10 11
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

12 13 14
(** Controller to run provers and transformations asynchronously on goals of a session
 *)

Clément Fumex's avatar
Clément Fumex committed
15 16
open Session_itp

17 18
(** {2 State of a proof or transformation in progress} *)

Clément Fumex's avatar
Clément Fumex committed
19
type proof_attempt_status =
20 21 22 23 24
  | Undone   (** prover was never called *)
  | Scheduled (** external proof attempt is scheduled *)
  | Running (** external proof attempt is in progress *)
  | Done of Call_provers.prover_result (** external proof done *)
  | Interrupted (** external proof has never completed *)
25
  | Detached (** parent goal has no task, is detached *)
26 27
  | InternalFailure of exn (** external proof aborted by internal error *)
  | Uninstalled of Whyconf.prover (** prover is uninstalled *)
28
  | UpgradeProver of Whyconf.prover (** prover is upgraded *)
29
  | Removed of Whyconf.prover (** prover has been removed or upgraded *)
Clément Fumex's avatar
Clément Fumex committed
30

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

33 34 35 36
type transformation_status =
    TSscheduled
  | TSdone of transID
  | TSfailed of (proofNodeID * exn)
Sylvain Dailler's avatar
Sylvain Dailler committed
37 38 39
  (* We distinguish normal usage exception of transformation from fatal
     exception like assertion failure that should not be raised *)
  | TSfatal of (proofNodeID * exn)
40 41

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

43
type strategy_status = STSgoto of proofNodeID * int | STShalt
Sylvain Dailler's avatar
Sylvain Dailler committed
44 45 46 47
                     (* When a transformation fatally returns, we have to
                        fatally fail the strategy
                        [transformation_name, pid, exn] *)
                     | STSfatal of string * proofNodeID * exn
48 49 50

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

51 52
(** {2 Signature for asynchronous schedulers} *)

53 54 55
(** Default delay for the scheduler timeout *)
val default_delay_ms: int

56
module type Scheduler = sig
MARCHE Claude's avatar
MARCHE Claude committed
57 58 59 60 61 62

    (** 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. *)

63 64 65 66
    val blocking: bool
    (** Set to true when the scheduler should wait for results of why3server
        (script), false otherwise (ITP which needs reactive scheduling) *)

67 68 69 70 71
    val multiplier: int
    (** Number of allowed task given to why3server is this number times the
        number of allowed proc on the machine.
    *)

MARCHE Claude's avatar
MARCHE Claude committed
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
    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. *)

87 88
end

89 90 91

(** {2 Controllers} *)

92
type controller = private
93
  { mutable controller_session : Session_itp.session;
94
    mutable controller_config : Whyconf.config;
MARCHE Claude's avatar
MARCHE Claude committed
95
    mutable controller_env : Env.env;
96
    controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
97
    controller_strategies : (string * string * string * Strategy.instruction array) Wstdlib.Hstr.t;
98
    controller_running_proof_attempts : unit Hpan.t;
99
  }
100

101 102
val create_controller: Whyconf.config -> Env.env -> Session_itp.session -> controller
(** creates a controller for the given session.
103
    The config and env is used to load the drivers for the provers. *)
104

105 106 107 108 109

val set_session_max_tasks : int -> unit
(** sets the maximum number of proof tasks that can be running at the
    same time. Initially set to 1. *)

110 111 112
val set_session_prover_upgrade_policy :
  controller -> Whyconf.prover -> Whyconf.prover_upgrade_policy -> unit

113

114 115
val print_session : Format.formatter -> controller -> unit

116

117

118
exception Errors_list of exn list
119

120 121 122 123 124 125 126 127 128 129 130
val reload_files : controller -> shape_version:int option -> bool * bool
(** [reload_files] returns a pair [(o,d)]: [o] true means there are
    obsolete goals, [d] means there are missed objects (goals,
    transformations, theories or files) that are now detached in the
    session returned.

  If parsing or typing errors occurs, a list of errors is raised
  inside exception Errors_list.

  The detailed process of reloading the files of the given session is
  as follows.
131 132 133 134

  - 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,
135 136
    that is as if it was an empty file (detached mode)
    (those errors are returned as first component
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168

  - 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
169 170 171 172
    . 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.

Sylvain Dailler's avatar
Sylvain Dailler committed
173

174
 *)
175

176
val add_file : controller -> ?format:Env.fformat -> string -> unit
177
(** [add_file cont ?fmt fname] parses the source file
178
    [fname] and add the resulting theories to the session of [cont].
179
    parsing or typing errors are raised inside exception [Errors_list]
180
 *)
181

182 183 184 185 186
val remove_subtree: notification:notifier -> removed:notifier ->
   controller -> any -> unit
(** remove a subtree of the session, taking care of not removing any
    proof attempt in progress. raise [RemoveError] if removal is not
    possible. *)
187

188 189
val get_undetached_children_no_pa: Session_itp.session -> any -> any list

190

191 192
(** {2 Scheduled jobs} *)

193 194
module Make(S : Scheduler) : sig

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

200 201 202 203 204 205
(* TODO
val register_notifier : (any -> unit) -> unit
(** records a hook that will be called each time a node change status *)
 *)


206 207
val interrupt : unit -> unit
(** discards all scheduled proof attempts or transformations, including
208
    the ones already running *)
209

210 211 212 213
val schedule_proof_attempt :
  controller ->
  proofNodeID ->
  Whyconf.prover ->
214
  ?save_to:string ->
215
  limit:Call_provers.resource_limit ->
216
  callback:(proofAttemptID -> proof_attempt_status -> unit) ->
217
  notification:notifier -> unit
Sylvain Dailler's avatar
Sylvain Dailler committed
218
(** [schedule_proof_attempt c id p ~timelimit ~callback ~notification] schedules a
219 220 221 222
   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
223 224 225 226
   is updated.
   [save_to] is used to give a location for the file generated for the prover
   ( *.smt2). With debug flag keep_vcs, the file are saved at this location.
*)
227

Sylvain Dailler's avatar
Sylvain Dailler committed
228 229 230 231 232 233
val schedule_edition :
  controller ->
  proofNodeID ->
  Whyconf.prover ->
  callback:(proofAttemptID -> proof_attempt_status -> unit) ->
  notification:notifier -> unit
234 235 236 237 238 239 240 241 242
(** [schedule_edition c id pr ~callback ~notification] runs the editor
    for prover [pr] on proofnode [id] on a file whose name is
    automatically generated. 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).  *)

val prepare_edition :
  controller -> ?file:string -> proofNodeID -> Whyconf.prover ->
243 244 245 246 247 248
  notification:notifier -> proofAttemptID * string * Call_provers.prover_result option
(** [prepare_edition c ?file id pr] prepare for editing the proof of
    node [id] with prover [pr]. The editor is not launched. The result
    is [(pid,name,res)] where [pid] is the node id the proof_attempt,
    [name] is the name of the file to edit, made relative to the
    session directory, and [res] is the former result if any. *)
249

250
exception TransAlreadyExists of string * string
251
exception GoalNodeDetached of proofNodeID
Sylvain Dailler's avatar
Sylvain Dailler committed
252

253 254 255 256 257
val schedule_transformation :
  controller ->
  proofNodeID ->
  string ->
  string list ->
258
  callback:(transformation_status -> unit) ->
259
  notification:notifier -> unit
260 261 262 263 264 265 266 267 268
(** [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 ->
MARCHE Claude's avatar
MARCHE Claude committed
269
  callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
270
  callback_tr:(string -> string list -> transformation_status -> unit) ->
271
  callback:(strategy_status -> unit) ->
272
  notification:notifier -> unit
273
(** [run_strategy_on_goal c id strat] executes asynchronously the
MARCHE Claude's avatar
MARCHE Claude committed
274 275 276 277 278
    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.  *)
279

280
val clean: controller -> removed:notifier -> any option -> unit
281 282
(** Remove each proof attempt or transformation that are below proved
    goals, that are either obsolete or not valid. The [removed]
283 284
    notifier is called on each removed node.
    On None, clean is done on the whole session. *)
285

286
val mark_as_obsolete:
287
  notification:notifier ->
288
  controller -> any option -> unit
289

290 291
exception BadCopyPaste

Sylvain Dailler's avatar
Sylvain Dailler committed
292 293
(* [copy_paste c a b] try to copy subtree originating at node a to node b *)
val copy_paste:
294
    notification:notifier ->
Sylvain Dailler's avatar
Sylvain Dailler committed
295
    callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
296
    callback_tr:(string -> string list -> transformation_status -> unit) ->
Sylvain Dailler's avatar
Sylvain Dailler committed
297 298
    controller -> any -> any -> unit

299

300 301 302 303
type report =
  | Result of Call_provers.prover_result * Call_provers.prover_result
        (** Result(new_result,old_result) *)
  | CallFailed of exn
304
  | Replay_interrupted
305 306 307 308 309
  | Prover_not_installed
  | Edited_file_absent of string
  | No_former_result of Call_provers.prover_result
(** Type for the reporting of a replayed call *)

310 311 312
(* 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:
313 314 315
    Format.formatter ->
      (proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list ->
        unit
316 317

val replay:
318 319
    valid_only:bool ->
    obsolete_only:bool ->
320
    ?use_steps:bool ->
321
    ?filter:(proof_attempt_node -> bool) ->
322
    controller ->
323
    callback:(proofAttemptID -> proof_attempt_status -> unit) ->
324
    notification:notifier ->
325
    final_callback:
326 327 328
      (bool ->
       (proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list
       -> unit) -> any: Session_itp.any option ->
329
    unit
Sylvain Dailler's avatar
Sylvain Dailler committed
330 331 332
(** This function reruns all the proofs of the session under the given any (None
    means the whole session), and produces a report comparing the results with
    the former ones.
333 334 335 336 337 338 339

    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]

340 341 342
    When finished, call the callback [final_callback] with a boolean
    telling if some prover was upgraded, and the report, a list of
    4-uples [(goalID, prover, limits, report)]
343

344
    When [obsolete_only] is set, only obsolete proofs are replayed (default)
345

346
    When [use_steps] is set, replay use the recorded number of proof
347 348
    steps (not set by default)

349 350 351
    When [filter] is set, only the proof attempts on which the filter
    returns true are replayed

352
 *)
353

354
exception CannotRunBisectionOn of proofAttemptID
355

MARCHE Claude's avatar
MARCHE Claude committed
356
val bisect_proof_attempt:
357 358 359 360 361
  callback_tr:(string -> string list -> transformation_status -> unit) ->
  callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
  notification:notifier ->
  removed:notifier ->
  controller -> proofAttemptID -> unit
362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380
  (** [bisect_proof_attempt ~callback_tr ~callback_pa ~notification
                            ~removed cont id] runs a bisection process
      based on the proof attempt [id] of the session managed by [cont].

      The proof attempt [id] must be a successful one, otherwise,
      exception [CannotRunBisectionOn id] is raised.

      Bisection tries to remove from the context the largest number of
      definitions and axioms, using the `remove` transformation (bound
      to [Cut.remove_list]). It proceeeds by dichotomy of the
      context. Note that there is no garantee that the removed data at
      the end is globally maximal. During that process, [callback_tr]
      is called each time the `remove` transformation is added to the session,
      [callback_pa] is called each time the prover is called on a
      reduced task, [notification] is called when a proof node is
      created or modified, and [removed] is called when a node is
      removed.

   *)
381
end