From 1fddf96b82849239eac5ea4658cab02d13026b0d Mon Sep 17 00:00:00 2001
From: Sylvain Dailler <dailler@adacore.com>
Date: Wed, 21 Jun 2017 11:18:16 +0200
Subject: [PATCH] Clean do clean transformations that are not successful

---
 src/session/controller_itp.ml | 26 ++++++++++++++++----------
 src/session/session_itp.ml    |  4 ++++
 src/session/session_itp.mli   |  3 +++
 3 files changed, 23 insertions(+), 10 deletions(-)

diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml
index 25944c1dd..b6ab29927 100644
--- a/src/session/controller_itp.ml
+++ b/src/session/controller_itp.ml
@@ -800,21 +800,27 @@ let schedule_tr_with_same_arguments
   let name = get_transf_name s tr in
   schedule_transformation c pn name args ~callback ~notification
 
-
-
 let clean_session c ~remove =
   let s = c.controller_session in
-  Session_itp.session_iter_proof_attempt
-    (fun id pa ->
-      if pn_proved c pa.parent then
-        match pa.Session_itp.proof_state with
-        | None -> ()
-        | Some pr ->
+  (* This function is applied on leafs first for the case of removes *)
+  Session_itp.fold_all_session s
+    (fun () any ->
+      (match any with
+      | APa pa ->
+        let pa = Session_itp.get_proof_attempt_node c.controller_session pa in
+        if pn_proved c pa.parent then
+          (match pa.Session_itp.proof_state with
+          | None -> ()
+          | Some pr ->
            if pa.Session_itp.proof_obsolete ||
                 Call_provers.(pr.pr_answer <> Valid)
            then
-             remove_subtree c ~removed:remove ~notification:(fun _ -> ()) (APa id))
-    s
+             remove_subtree c ~removed:remove ~notification:(fun _ -> ()) any)
+      | ATn tn ->
+        let pn = get_trans_parent c.controller_session tn in
+        if pn_proved c pn && not (tn_proved c tn) then
+          remove_subtree c ~removed:remove ~notification:(fun _ -> ()) (ATn tn)
+      | _ -> ())) ()
 
 (* This function folds on any subelements of given node and tries to mark all
    proof attempts it encounters *)
diff --git a/src/session/session_itp.ml b/src/session/session_itp.ml
index 3279b5b6f..7c0b61c82 100644
--- a/src/session/session_itp.ml
+++ b/src/session/session_itp.ml
@@ -358,6 +358,10 @@ let fold_all_any s f acc any =
   | ATn tn -> fold_all_any_of_transn s f acc tn
   | APa _ -> f acc any
 
+let fold_all_session s f acc =
+  let files = get_files s in
+  Hstr.fold (fun _key file acc -> fold_all_any s f acc (AFile file)) files acc
+
 exception RemoveError
 
 (* Cannot remove a proof_attempt that was scheduled but did not finish yet.
diff --git a/src/session/session_itp.mli b/src/session/session_itp.mli
index 9f6cc88c2..2e6cd0786 100644
--- a/src/session/session_itp.mli
+++ b/src/session/session_itp.mli
@@ -204,3 +204,6 @@ val remove_subtree: session -> any -> notification:(any -> unit) -> unit
 
 val fold_all_any: session -> ('a -> any -> 'a) -> 'a -> any -> 'a
 (** [fold_all_any s f acc any] folds on all the subnodes of any *)
+
+val fold_all_session: session -> ('a -> any -> 'a) -> 'a -> 'a
+(** [fold_all_session s f acc] folds on the whole session *)
-- 
GitLab