Functor Controller_itp.Make

module Make: 
functor (S : Scheduler) -> sig .. end
Parameters:
S : Scheduler

val register_observer : (int -> int -> int -> unit) -> unit

records a hook that will be called with the number of waiting tasks, scheduled tasks, and running tasks, each time these numbers change

val interrupt : unit -> unit

discards all scheduled proof attempts or transformations, including the ones already running

val schedule_proof_attempt : Controller_itp.controller ->
Session_itp.proofNodeID ->
Whyconf.prover ->
?save_to:string ->
limit:Call_provers.resource_limit ->
callback:(Session_itp.proofAttemptID ->
Controller_itp.proof_attempt_status -> unit) ->
notification:Session_itp.notifier -> unit

schedule_proof_attempt c id p ~timelimit ~callback ~notification schedules a 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. 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.

val schedule_edition : Controller_itp.controller ->
Session_itp.proofNodeID ->
Whyconf.prover ->
callback:(Session_itp.proofAttemptID ->
Controller_itp.proof_attempt_status -> unit) ->
notification:Session_itp.notifier -> unit

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_itp.controller ->
?file:string ->
Session_itp.proofNodeID ->
Whyconf.prover ->
notification:Session_itp.notifier ->
Session_itp.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.

exception TransAlreadyExists of string * string
val schedule_transformation : Controller_itp.controller ->
Session_itp.proofNodeID ->
string ->
string list ->
callback:(Controller_itp.transformation_status -> unit) ->
notification:Session_itp.notifier -> unit

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_itp.controller ->
Session_itp.proofNodeID ->
Strategy.t ->
callback_pa:(Session_itp.proofAttemptID ->
Controller_itp.proof_attempt_status -> unit) ->
callback_tr:(string ->
string list -> Controller_itp.transformation_status -> unit) ->
callback:(Controller_itp.strategy_status -> unit) ->
notification:Session_itp.notifier -> unit

run_strategy_on_goal c id strat executes asynchronously the 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.

val clean : Controller_itp.controller ->
removed:Session_itp.notifier -> Session_itp.any option -> 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. On None, clean is done on the whole session.

val mark_as_obsolete : notification:Session_itp.notifier ->
Controller_itp.controller -> Session_itp.any option -> unit
exception BadCopyPaste
val copy_paste : notification:Session_itp.notifier ->
callback_pa:(Session_itp.proofAttemptID ->
Controller_itp.proof_attempt_status -> unit) ->
callback_tr:(string ->
string list -> Controller_itp.transformation_status -> unit) ->
Controller_itp.controller -> Session_itp.any -> Session_itp.any -> unit
type report = 
| Result of Call_provers.prover_result * Call_provers.prover_result (*

Result(new_result,old_result)

*)
| CallFailed of exn
| Replay_interrupted
| Prover_not_installed
| Edited_file_absent of string
| No_former_result of Call_provers.prover_result (*

Type for the reporting of a replayed call

*)
val replay_print : Format.formatter ->
(Session_itp.proofNodeID * Whyconf.prover * Call_provers.resource_limit *
report)
list -> unit
val replay : valid_only:bool ->
obsolete_only:bool ->
?use_steps:bool ->
?filter:(Session_itp.proof_attempt_node -> bool) ->
Controller_itp.controller ->
callback:(Session_itp.proofAttemptID ->
Controller_itp.proof_attempt_status -> unit) ->
notification:Session_itp.notifier ->
final_callback:(bool ->
(Session_itp.proofNodeID * Whyconf.prover *
Call_provers.resource_limit * report)
list -> unit) ->
any:Session_itp.any option -> unit

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.

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 a boolean telling if some prover was upgraded, and 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)

When filter is set, only the proof attempts on which the filter returns true are replayed

val bisect_proof_attempt : callback_tr:(string ->
string list -> Controller_itp.transformation_status -> unit) ->
callback_pa:(Session_itp.proofAttemptID ->
Controller_itp.proof_attempt_status -> unit) ->
notification:Session_itp.notifier ->
removed:Session_itp.notifier ->
Controller_itp.controller -> Session_itp.proofAttemptID -> unit