Module Controller_itp

module Controller_itp: sig .. end

Controller to run provers and transformations asynchronously on goals of a session


State of a proof or transformation in progress

type proof_attempt_status = 
| 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

*)
| Detached (*

parent goal has no task, is detached

*)
| InternalFailure of exn (*

external proof aborted by internal error

*)
| Uninstalled of Whyconf.prover (*

prover is uninstalled

*)
| UpgradeProver of Whyconf.prover (*

prover is upgraded

*)
val print_status : Format.formatter -> proof_attempt_status -> unit
type transformation_status = 
| TSscheduled
| TSdone of Session_itp.transID
| TSfailed of (Session_itp.proofNodeID * exn)
val print_trans_status : Format.formatter -> transformation_status -> unit
type strategy_status = 
| STSgoto of Session_itp.proofNodeID * int
| STShalt
val print_strategy_status : Format.formatter -> strategy_status -> unit

Signature for asynchronous schedulers

val default_delay_ms : int

Default delay for the scheduler timeout

module type Scheduler = sig .. end

Controllers

type 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 -> controller

creates a controller for the given session. The config and env is used to load the drivers for the provers.

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.

val set_session_prover_upgrade_policy : controller ->
Whyconf.prover -> Whyconf.prover_upgrade_policy -> unit
val print_session : Format.formatter -> controller -> unit
exception Errors_list of exn list
val reload_files : controller -> use_shapes:bool -> bool * bool

reload the files of the given session:

. 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.

. 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.

. 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.

reload_files It 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.

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. parsing or typing errors are raised inside exception Errors_list

val remove_subtree : notification:Session_itp.notifier ->
removed:Session_itp.notifier ->
controller -> Session_itp.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.

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

Scheduled jobs

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