Commit f12b7a9f authored by MARCHE Claude's avatar MARCHE Claude

fix issue #134: bisect does not raise `Invalid_argument` anymore

also, the callback for transformation `remove` is not called when transformation fails,
preventing the display of numerous error messages in the IDE
parent dcd1cd96
......@@ -1151,11 +1151,14 @@ let create_rem_list =
Buffer.contents b
exception CannotRunBisectionOn of proofAttemptID
let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_id =
let ses = c.controller_session in
let pa = get_proof_attempt_node ses pa_id in
if not (proof_is_complete pa) then
invalid_arg "bisect: proof attempt should be valid";
raise (CannotRunBisectionOn pa_id); (* proof attempt should be valid *)
let goal_id = pa.parent in
let prover = pa.prover in
let limit = { pa.limit with
......@@ -1221,12 +1224,12 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
let rem = create_rem_list rem in
let callback st =
callback_tr "remove" [rem] st;
begin match st with
| TSscheduled ->
"[Bisect] transformation 'remove' scheduled@."
"[Bisect] transformation 'remove' scheduled@.";
callback_tr "remove" [rem] st;
| TSfailed(_,exn) ->
(* may happen if removing a type or a lsymbol that is used
later on. We do has if proof fails. *)
......@@ -1244,6 +1247,7 @@ later on. We do has if proof fails. *)
"[Bisect] transformation 'remove' succeeds@.";
callback_tr "remove" [rem] st;
match get_sub_tasks ses trid with
| [pn] ->
let limit = { limit with Call_provers.limit_time = !timelimit; } in
......@@ -343,6 +343,7 @@ val replay:
exception CannotRunBisectionOn of proofAttemptID
val bisect_proof_attempt:
callback_tr:(string -> string list -> transformation_status -> unit) ->
......@@ -350,5 +351,23 @@ val bisect_proof_attempt:
notification:notifier ->
removed:notifier ->
controller -> 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
......@@ -1197,6 +1197,11 @@ end
"for bisection please select some proof attempt"))
| C.CannotRunBisectionOn _ ->
"for bisection please select a successful proof attempt"))
(* ----------------- run strategy -------------------- *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment