type proof_attempt_status = | Undone| Scheduled| Running| Done of Call_provers.prover_result| Interrupted| Detached| InternalFailure of exn| Uninstalled of Whyconf.prover| UpgradeProver of Whyconf.prover| Removed of Whyconf.proverval print_status : Format.formatter -> proof_attempt_status -> unittype transformation_status = | TSscheduled| TSdone of Session_itp.transID| TSfailed of Session_itp.proofNodeID * exn| TSfatal of Session_itp.proofNodeID * exnval print_trans_status : Format.formatter -> transformation_status -> unittype strategy_status = | STSgoto of Session_itp.proofNodeID * int| STShalt| STSfatal of string * Session_itp.proofNodeID * exnval print_strategy_status : Format.formatter -> strategy_status -> unitmodule type Scheduler = sig ... endtype controller = private {mutable controller_session : Session_itp.session;mutable controller_config : Whyconf.config;mutable controller_env : Env.env;controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;controller_strategies : (string * string * string * Strategy.instruction array)
Wstdlib.Hstr.t;controller_running_proof_attempts : unit Session_itp.Hpan.t;}val create_controller :
Whyconf.config ->
Env.env ->
Session_itp.session ->
controllerval set_session_prover_upgrade_policy :
controller ->
Whyconf.prover ->
Whyconf.prover_upgrade_policy ->
unitval print_session : Format.formatter -> controller -> unitval reload_files : controller -> shape_version:int option -> bool * boolval add_file : controller -> ?format:Env.fformat -> string -> unitval remove_subtree :
notification:Session_itp.notifier ->
removed:Session_itp.notifier ->
controller ->
Session_itp.any ->
unitval get_undetached_children_no_pa :
Session_itp.session ->
Session_itp.any ->
Session_itp.any list