Commit bf002e52 authored by Sylvain Dailler's avatar Sylvain Dailler

replay, mark_obsolete and clean on whole session

Commands replay, mark_obsolete and clean are now executed on the whole
session when no node is selected.
parent d12292d9
......@@ -768,15 +768,16 @@ let proof_is_complete pa =
not pa.Session_itp.proof_obsolete &&
Call_provers.(pr.pr_answer = Valid)
let clean c ~removed nid =
(* clean should not change proved status *)
let notification _ = assert false in
let s = c.controller_session in
(* This function is applied on leafs first for the case of removes *)
Session_itp.fold_all_any s
(fun () any ->
(match any with
| APa pa ->
let clean_aux () any =
match any with
| APa pa ->
let pa = Session_itp.get_proof_attempt_node s pa in
if pn_proved s pa.parent then
if not (proof_is_complete pa) then
......@@ -785,7 +786,14 @@ let clean c ~removed nid =
let pn = get_trans_parent s tn in
if pn_proved s pn && not (tn_proved s tn) then
remove_subtree ~notification ~removed c (ATn tn)
| _ -> ())) () nid
| _ -> ()
in
match nid with
| Some nid ->
Session_itp.fold_all_any s clean_aux () nid
| None ->
Session_itp.fold_all_session s clean_aux ()
(* This function folds on any subelements of given node and tries to mark all
proof attempts it encounters *)
......@@ -798,10 +806,16 @@ let mark_as_obsolete ~notification c any =
notification (APa n);
update_goal_node notification s parent
in
fold_all_any s
(fun () any -> match any with
| APa n -> mark_as_obsolete_pa n
| _ -> ()) () any
match any with
| Some any ->
fold_all_any s
(fun () any -> match any with
| APa n -> mark_as_obsolete_pa n
| _ -> ()) () any
| None ->
session_iter_proof_attempt
(fun pa _pan ->
mark_as_obsolete_pa pa) s
exception BadCopyPaste
......
......@@ -258,14 +258,15 @@ val run_strategy_on_goal :
[schedule_transformation]). [callback] is called on each step of
execution of the strategy. *)
val clean: controller -> removed:notifier -> any -> unit
val clean: controller -> removed:notifier -> 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. *)
notifier is called on each removed node.
On None, clean is done on the whole session. *)
val mark_as_obsolete:
notification:notifier ->
controller -> any -> unit
controller -> any option -> unit
(* [copy_paste c a b] try to copy subtree originating at node a to node b *)
val copy_paste:
......
......@@ -1206,13 +1206,12 @@ end
let replay ~valid_only nid : unit =
let d = get_server_data () in
let any = any_from_node_ID nid in
let callback = callback_update_tree_proof d.cont in
let final_callback lr =
P.notify (Message (Replay_Info (Pp.string_of C.replay_print lr))) in
(* TODO make replay print *)
C.replay ~valid_only ~use_steps:false ~obsolete_only:true d.cont
~callback ~notification:(notify_change_proved d.cont) ~final_callback ~any:(Some any)
~callback ~notification:(notify_change_proved d.cont) ~final_callback ~any:nid
(*
let () = register_command "edit" "remove unsuccessful proof attempts that are below proved goals"
......@@ -1231,13 +1230,7 @@ end
(* ---------------- Mark obsolete ------------------ *)
let mark_obsolete n =
let d = get_server_data () in
let any = any_from_node_ID n in
(*
let node_obsolete x b =
let nid = node_ID_from_any x in
P.notify (Node_change (nid, Obsolete b)) in
*)
C.mark_as_obsolete (* ~node_obsolete *) ~notification:(notify_change_proved d.cont) d.cont any
C.mark_as_obsolete ~notification:(notify_change_proved d.cont) d.cont n
(* ----------------- locate next unproven node -------------------- *)
......@@ -1320,11 +1313,9 @@ end
run_strategy_on_task ~counterexmp nid st
| Edit p -> schedule_edition nid p
| Bisect -> schedule_bisection nid
| Replay valid_only -> replay ~valid_only nid
| Clean ->
let any = any_from_node_ID nid in
clean any
| Mark_Obsolete -> mark_obsolete nid
| Replay valid_only -> replay ~valid_only snid
| Clean -> clean snid
| Mark_Obsolete -> mark_obsolete snid
| Help_message s -> P.notify (Message (Help s))
| QError s -> P.notify (Message (Query_Error (nid, s)))
| Other (s, _args) ->
......
......@@ -423,33 +423,15 @@ let interp commands_table cont id s =
end
| "replay", args ->
begin
match id with
| Some _ ->
begin
match args with
| [] -> Replay true
| ["all"] -> Replay false
| _ -> QError ("replay expects either no arguments or `all`")
end
| _ -> (* TODO: replay the whole tree instead *)
QError ("Please select a node in the task tree")
match args with
| [] -> Replay true
| ["all"] -> Replay false
| _ -> QError ("replay expects either no arguments or `all`")
end
| "mark", _ ->
begin
match id with
| Some _ -> Mark_Obsolete
| _ ->
(* TODO: replay the whole tree instead *)
QError ("Please select a node in the task tree")
end
Mark_Obsolete
| "clean", _ ->
begin
match id with
| Some _ -> Clean
| _ ->
(* TODO: replay the whole tree instead *)
QError ("Please select a node in the task tree")
end
Clean
| "help", [trans] ->
let print_trans_desc fmt r =
Format.fprintf fmt "@[%s:\n%a@]" trans Pp.formatted r
......
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