Functor Controller_itp.Make

module Make: functor (* : sig

end) -> sig .. end

Parameters:

* : 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 : Controller_itp.controller -> unit

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

val interrupt_proof_attempts_for_goal : Controller_itp.controller -> Session_itp.proofNodeID -> unit

discards all scheduled proof attempts for the given goal, including the ones that are already running

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

schedule_proof_attempt ?proof_script_filename 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. proof_script_filename is used to give a location for the files generated for the prover. With debug flag keep_vcs, the files 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:Sysutil.file_path ->
       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 system-dependent absolute path of the file to edit, and res is the former result if any.

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

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 -> removed: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 run_strat_on_goal : Controller_itp.controller ->
       Session_itp.proofNodeID ->
       (Env.env -> Task.task -> Strategy.strat) ->
       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_strat_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 reset_proofs : Controller_itp.controller ->
       removed:Session_itp.notifier ->
       notification:Session_itp.notifier -> Session_itp.any option -> unit

Remove each proof attempt or transformation that are below proved goals. 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 : Stdlib.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

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

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.