From f12b7a9f3440983a2f08bd3a9a131fdd13990b3f Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Mon, 1 Oct 2018 09:12:40 +0200
Subject: [PATCH] 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
---
src/session/controller_itp.ml | 10 +++++++---
src/session/controller_itp.mli | 21 ++++++++++++++++++++-
src/session/itp_server.ml | 5 +++++
3 files changed, 32 insertions(+), 4 deletions(-)
diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml
index c522ab49e..ea1615c44 100644
--- a/src/session/controller_itp.ml
+++ b/src/session/controller_itp.ml
@@ -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 ->
Debug.dprintf
debug
- "[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. *)
Debug.dprintf
debug
"[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
diff --git a/src/session/controller_itp.mli b/src/session/controller_itp.mli
index 85bd76b4a..21e7c44fa 100644
--- a/src/session/controller_itp.mli
+++ b/src/session/controller_itp.mli
@@ -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
+ removed.
+
+ *)
end
diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml
index 8406dc29b..39b748530 100644
--- a/src/session/itp_server.ml
+++ b/src/session/itp_server.ml
@@ -1197,6 +1197,11 @@ end
(Message
(Information
"for bisection please select some proof attempt"))
+ | C.CannotRunBisectionOn _ ->
+ P.notify
+ (Message
+ (Error
+ "for bisection please select a successful proof attempt"))
(* ----------------- run strategy -------------------- *)
--
GitLab