Scheduler ->
sig
val register_observer : (int -> int -> int -> unit) -> unit
val interrupt : Controller_itp.controller -> unit
val interrupt_proof_attempts_for_goal :
Controller_itp.controller -> Session_itp.proofNodeID -> unit
val schedule_proof_attempt :
?proof_script_filename:string ->
Controller_itp.controller ->
Session_itp.proofNodeID ->
Whyconf.prover ->
limits:Call_provers.resource_limits ->
callback:(Session_itp.proofAttemptID ->
Controller_itp.proof_attempt_status -> unit) ->
notification:Session_itp.notifier -> unit
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
val prepare_edition :
Controller_itp.controller ->
?file:Sysutil.file_path ->
Session_itp.proofNodeID ->
Whyconf.prover ->
notification:Session_itp.notifier ->
Session_itp.proofAttemptID * string * Call_provers.prover_result option
exception GoalNodeDetached of Session_itp.proofNodeID
val schedule_transformation :
Controller_itp.controller ->
Session_itp.proofNodeID ->
string ->
string list ->
callback:(Controller_itp.transformation_status -> unit) ->
notification:Session_itp.notifier -> unit
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 ->
removed:Session_itp.notifier -> unit
val run_strat_on_goal :
Controller_itp.controller ->
Session_itp.proofNodeID ->
string ->
Strategy.gen_strat ->
string list ->
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
val clean :
Controller_itp.controller ->
removed:Session_itp.notifier -> Session_itp.any option -> unit
val reset_proofs :
Controller_itp.controller ->
removed:Session_itp.notifier ->
notification:Session_itp.notifier -> Session_itp.any option -> unit
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
| CallFailed of exn
| Replay_interrupted
| Prover_not_installed
| Edited_file_absent of string
| No_former_result of Call_provers.prover_result
val replay_print :
Stdlib.Format.formatter ->
(Session_itp.proofNodeID * Whyconf.prover *
Call_provers.resource_limits * Controller_itp.Make.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_limits *
Controller_itp.Make.report)
list -> unit) ->
any:Session_itp.any option -> unit
exception CannotRunBisectionOn of Session_itp.proofAttemptID
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
end