diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml index 88d46687fbd570b0432b097ce6602417fb046dc4..d6c4b5fd477f426746d75172680959989dcdd137 100644 --- a/src/session/controller_itp.ml +++ b/src/session/controller_itp.ml @@ -682,25 +682,32 @@ let schedule_tr_with_same_arguments let name = get_transf_name s tr in schedule_transformation c pn name args ~callback ~notification +let is_valid (pa: proof_attempt_node) : bool = + match pa.Session_itp.proof_state with + | None -> false + | Some pr -> + begin + match pr.Call_provers.pr_answer with + | Call_provers.Valid -> true + | _ -> false + end + +let is_running (pa: proof_attempt_node) : bool = + match pa.Session_itp.proof_state with + | None -> true + | Some pr -> false + let clean_session c ~remove ~node_change = - let is_valid (pa: proof_attempt_node) : bool = - match pa.Session_itp.proof_state with - | None -> false - | Some pr -> - begin - match pr.Call_provers.pr_answer with - | Call_provers.Valid -> true - | _ -> false - end - in let s = c.controller_session in Session_itp.session_iter_proof_attempt (fun _ pa -> let pnid = pa.parent in Hprover.iter (fun _ paid -> - if (not (is_valid (get_proof_attempt_node s paid))) then + let npa = get_proof_attempt_node s paid in + if (not (is_valid npa) && not (is_running npa)) then remove_subtree c ~removed:remove ~node_change (APa paid)) - (get_proof_attempt_ids s pnid)) s + (get_proof_attempt_ids s pnid)) + s (* 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.mli b/src/session/session_itp.mli index 151090f1dfab4e71387d3c20b5adaf2049b31d1e..c28d83ad2be7f3f6c3af5c9f94116ab770d71eda 100644 --- a/src/session/session_itp.mli +++ b/src/session/session_itp.mli @@ -65,7 +65,8 @@ type proof_attempt_node = { proof_script : string option; (* non empty for external ITP *) } -val session_iter_proof_attempt: (proofAttemptID -> proof_attempt_node -> unit) -> session -> unit +val session_iter_proof_attempt: + (proofAttemptID -> proof_attempt_node -> unit) -> session -> unit (* [is_below s a b] true if a is below b in the session tree *) val is_below: session -> any -> any -> bool