Commit 5e00fc66 authored by Sylvain Dailler's avatar Sylvain Dailler

fixes #2

Removing requests for mark_obsolete, clean_req and replay_req. Those are
now Command_req because they are contextual.
Only replay keeps a non-contextual mode for why3replay because we don't
have root node anymore (there can be several file nodes).
parent d5a8547d
......@@ -1864,10 +1864,22 @@ let unfocus_item =
let () =
connect_menu_item
replay_menu_item
~callback:(fun () -> send_request Replay_req);
~callback:(fun () ->
match get_selected_row_references () with
| [r] ->
let id = get_node_id r#iter in
send_request (Command_req (id, "replay"))
| _ -> print_message ~kind:1 ~mark:"Replay error"
"Select only one node to perform the replay action");
connect_menu_item
clean_menu_item
~callback:(fun _ -> send_request Clean_req);
~callback:(fun () ->
match get_selected_row_references () with
| [r] ->
let id = get_node_id r#iter in
send_request (Command_req (id, "clean"))
| _ -> print_message ~kind:1 ~mark:"Clean error"
"Select only one node to perform the clean action");
connect_menu_item
remove_item
~callback:(fun () ->
......@@ -1892,7 +1904,7 @@ let () =
match get_selected_row_references () with
| [r] ->
let id = get_node_id r#iter in
send_request (Mark_obsolete_req id)
send_request (Command_req (id, "mark"))
| _ -> print_message ~kind:1 ~mark:"Mark_obsolete error"
"Select only one node to perform the mark obsolete action");
connect_menu_item
......
......@@ -817,12 +817,12 @@ let proof_is_complete pa =
not pa.Session_itp.proof_obsolete &&
Call_provers.(pr.pr_answer = Valid)
let clean_session c ~removed =
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_session s
Session_itp.fold_all_any s
(fun () any ->
(match any with
| APa pa ->
......@@ -834,7 +834,7 @@ let clean_session c ~removed =
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
(* This function folds on any subelements of given node and tries to mark all
proof attempts it encounters *)
......@@ -951,7 +951,7 @@ let replay_print fmt (lr: (proofNodeID * Whyconf.prover * Call_provers.resource_
Format.fprintf fmt "%a@." (Pp.print_list Pp.newline pp_elem) lr
let replay ?(obsolete_only=true) ?(use_steps=false)
c ~callback ~notification ~final_callback =
c ~callback ~notification ~final_callback ~any =
let craft_report count s r id pr limits pa =
match s with
......@@ -979,8 +979,13 @@ let replay ?(obsolete_only=true) ?(use_steps=false)
(* TODO count the number of node in a more efficient way *)
(* Counting the number of proof_attempt to print report only once *)
Session_itp.session_iter_proof_attempt
(fun _ pa -> if pa.proof_obsolete || not obsolete_only then incr count) session;
(match any with
| None ->
Session_itp.session_iter_proof_attempt
(fun _ pa -> if pa.proof_obsolete || not obsolete_only then incr count) session
| Some nid ->
Session_itp.any_iter_proof_attempt session
(fun _ pa -> if pa.proof_obsolete || not obsolete_only then incr count) nid);
(* Replaying function *)
let replay_pa id pa =
......@@ -1008,7 +1013,9 @@ let replay ?(obsolete_only=true) ?(use_steps=false)
if !count = 0 then final_callback !report else
(* Calling replay on all the proof_attempts of the session *)
Session_itp.session_iter_proof_attempt replay_pa session
match any with
| None -> Session_itp.session_iter_proof_attempt replay_pa session
| Some nid -> Session_itp.any_iter_proof_attempt session replay_pa nid
......
......@@ -258,7 +258,7 @@ val run_strategy_on_goal :
[schedule_transformation]). [callback] is called on each step of
execution of the strategy. *)
val clean_session: controller -> removed:notifier -> unit
val clean: controller -> removed:notifier -> any -> 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. *)
......@@ -303,10 +303,11 @@ val replay:
notification:notifier ->
final_callback:
((proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list
-> unit) ->
-> unit) -> any: Session_itp.any option ->
unit
(** This function reruns all the proofs of the session, and produces a report
comparing the results with the former ones.
(** This function reruns all the proofs of the session under the given any (None
means the whole session), and produces a report comparing the results with
the former ones.
The proofs are replayed asynchronously, and the states of these proofs are
notified via [callback] similarly as for [schedule_proof_attempt].
......
......@@ -114,11 +114,8 @@ type ide_request =
| Copy_detached of node_ID
| Save_file_req of string * string
| Get_first_unproven_node of node_ID
| Mark_obsolete_req of node_ID
| Clean_req
| Save_req
| Reload_req
| Replay_req
| Exit_req
| Interrupt_req
......@@ -126,7 +123,7 @@ type ide_request =
let modify_session (r: ide_request) =
match r with
| Command_req _ | Add_file_req _ | Remove_subtree _ | Copy_paste _
| Copy_detached _ | Replay_req | Clean_req | Mark_obsolete_req _ -> true
| Copy_detached _ -> true
| Set_config_param _ | Get_file_contents _
| Get_task _ | Save_file_req _ | Get_first_unproven_node _
| Save_req | Reload_req | Exit_req
......
......@@ -130,16 +130,8 @@ type ide_request =
| Save_file_req of string * string
(** [Save_file_req(filename, content_of_file)] saves the file *)
| Get_first_unproven_node of node_ID
| Mark_obsolete_req of node_ID
| Clean_req
| Save_req
| Reload_req
| Replay_req
(** replay all the proof attempts whose result is obsolete. TODO
[priority high]: have a similar request with a node id as
argument, to replay only in the corresponding subtree. TODO
[priority low]: have a extra boolean argument to force replay
also of non-obsolete goals. *)
| Exit_req
| Interrupt_req
......
......@@ -263,11 +263,8 @@ let print_request fmt r =
| Copy_paste _ -> fprintf fmt "copy paste"
| Copy_detached _ -> fprintf fmt "copy detached"
| Save_file_req _ -> fprintf fmt "save file"
| Mark_obsolete_req _ -> fprintf fmt "mark obsolete"
| Clean_req -> fprintf fmt "clean"
| Save_req -> fprintf fmt "save"
| Reload_req -> fprintf fmt "reload"
| Replay_req -> fprintf fmt "replay"
| Exit_req -> fprintf fmt "exit"
| Interrupt_req -> fprintf fmt "interrupt"
......@@ -1159,9 +1156,9 @@ end
(* ----------------- Clean session -------------------- *)
let clean_session () =
let clean nid =
let d = get_server_data () in
C.clean_session d.cont ~removed
C.clean d.cont ~removed nid
let remove_node nid =
......@@ -1207,20 +1204,15 @@ end
| Some(loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,s)))
let replay_session () : unit =
let replay 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 ~use_steps:false ~obsolete_only:true d.cont
~callback ~notification:(notify_change_proved d.cont) ~final_callback
let () = register_command "replay" "replay obsolete proofs"
(Qnotask (fun _cont _args -> replay_session (); "replay in progress, be patient"))
let () = register_command "clean" "remove unsuccessful proof attempts that are below proved goals"
(Qnotask (fun _cont _args -> clean_session (); "Cleaning done"))
~callback ~notification:(notify_change_proved d.cont) ~final_callback ~any:(Some any)
(*
let () = register_command "edit" "remove unsuccessful proof attempts that are below proved goals"
......@@ -1276,7 +1268,6 @@ end
let config = d.cont.controller_config in
try (
match r with
| Clean_req -> clean_session ()
| Save_req -> save_session ()
| Reload_req -> reload_session ()
| Get_first_unproven_node ni ->
......@@ -1311,11 +1302,9 @@ end
C.copy_detached ~copy d.cont from_any
| Get_file_contents f ->
read_and_send f
| Mark_obsolete_req n -> mark_obsolete n
| Save_file_req (name, text) ->
save_file name text;
| Get_task(nid,b,c,loc) -> send_task nid b c loc
| Replay_req -> replay_session ()
| Interrupt_req -> C.interrupt ()
| Command_req (nid, cmd) ->
begin
......@@ -1331,6 +1320,11 @@ end
run_strategy_on_task ~counterexmp nid st
| Edit p -> schedule_edition nid p
| Bisect -> schedule_bisection nid
| Replay -> replay nid
| Clean ->
let any = any_from_node_ID nid in
clean any
| Mark_Obsolete -> mark_obsolete nid
| Help_message s -> P.notify (Message (Help s))
| QError s -> P.notify (Message (Query_Error (nid, s)))
| Other (s, _args) ->
......
......@@ -154,11 +154,8 @@ let convert_request_constructor (r: ide_request) =
| Copy_paste _ -> String "Copy_paste"
| Copy_detached _ -> String "Copy_detached"
| Get_first_unproven_node _ -> String "Get_first_unproven_node"
| Mark_obsolete_req _ -> String "Mark_obsolete_req"
| Clean_req -> String "Clean_req"
| Save_req -> String "Save_req"
| Reload_req -> String "Reload_req"
| Replay_req -> String "Replay_req"
| Exit_req -> String "Exit_req"
| Interrupt_req -> String "Interrupt_req"
......@@ -203,17 +200,10 @@ let print_request_to_json (r: ide_request): Json_base.json =
"node_ID", Int id]
| Unfocus_req ->
convert_record ["ide_request", cc r]
| Mark_obsolete_req n ->
convert_record ["ide_request", cc r;
"node_ID", Int n]
| Clean_req ->
convert_record ["ide_request", cc r]
| Save_req ->
convert_record ["ide_request", cc r]
| Reload_req ->
convert_record ["ide_request", cc r]
| Replay_req ->
convert_record ["ide_request", cc r]
| Exit_req ->
convert_record ["ide_request", cc r]
| Interrupt_req ->
......@@ -468,17 +458,10 @@ let parse_request (constr: string) j =
| "Copy_detached" ->
let n = get_int (get_field j "node_ID") in
Copy_detached n
| "Mark_obsolete_req" ->
let n = get_int (get_field j "node_ID") in
Mark_obsolete_req n
| "Clean_req" ->
Clean_req
| "Save_req" ->
Save_req
| "Reload_req" ->
Reload_req
| "Replay_req" ->
Replay_req
| "Exit_req" ->
Exit_req
| _ -> raise (NotRequest "")
......
......@@ -259,6 +259,7 @@ type query =
| Qnotask of (Controller_itp.controller -> string list -> string)
| Qtask of (Controller_itp.controller -> Trans.naming_table -> string list -> string)
let help_on_queries fmt commands =
let l = Stdlib.Hstr.fold (fun c (h,_) acc -> (c,h)::acc) commands [] in
let l = List.sort sort_pair l in
......@@ -354,6 +355,9 @@ type command =
| Strategies of string
| Edit of Whyconf.config_prover
| Bisect
| Replay
| Clean
| Mark_Obsolete
| Help_message of string
| Query of string
| QError of string
......@@ -361,18 +365,21 @@ type command =
let interp commands_table cont id s =
let cmd,args = split_args s in
try
let (_,f) = Stdlib.Hstr.find commands_table cmd in
match f,id with
| Qnotask f, _ -> Query (f cont args)
| Qtask f, Some (Session_itp.APn id) ->
let _,table = Session_itp.get_task cont.Controller_itp.controller_session id in
let s = try Query (f cont table args) with
| Undefined_id s -> QError ("No existing id corresponding to " ^ s)
| Number_of_arguments -> QError "Bad number of arguments"
in s
| Qtask _, _ -> QError "please select a goal first"
with Not_found ->
match Stdlib.Hstr.find commands_table cmd with
| (_, f) ->
begin
match f,id with
| Qnotask f, _ -> Query (f cont args)
| Qtask f, Some (Session_itp.APn id) ->
let _,table = Session_itp.get_task cont.Controller_itp.controller_session id in
let s = try Query (f cont table args) with
| Undefined_id s -> QError ("No existing id corresponding to " ^ s)
| Number_of_arguments -> QError "Bad number of arguments"
in s
| Qtask _, _ -> QError "please select a goal first"
end
| exception Not_found ->
begin
try
let t = Trans.lookup_trans cont.Controller_itp.controller_env cmd in
match id with
......@@ -414,6 +421,24 @@ let interp commands_table cont id s =
| Some (Session_itp.APa _) -> Bisect
| _ -> QError ("Please select a proof node in the task tree")
end
| "replay", _ ->
begin
match id with
| Some _ -> Replay
| _ -> QError ("Please select a node in the task tree")
end
| "mark", _ ->
begin
match id with
| Some _ -> Mark_Obsolete
| _ -> QError ("Please select a node in the task tree")
end
| "clean", _ ->
begin
match id with
| Some _ -> Clean
| _ -> QError ("Please select a node in the task tree")
end
| "help", [trans] ->
let print_trans_desc fmt r =
Format.fprintf fmt "@[%s:\n%a@]" trans Pp.formatted r
......@@ -431,6 +456,10 @@ let interp commands_table cont id s =
@ <prover shortcut> [<time limit> [<mem limit>]]@\n\
@ <query> [arguments]@\n\
@ <strategy shortcut>@\n\
@ mark @\n\
@ clean @\n\
@ replay @\n\
@ bisect @\n\
@ help <transformation_name> @\n\
@\n\
Available queries are:@\n@[%a@]" help_on_queries commands_table
......@@ -438,6 +467,7 @@ let interp commands_table cont id s =
Help_message text
| _ ->
Other (cmd, args)
end
(***********************)
(* First Unproven goal *)
......
......@@ -43,7 +43,8 @@ type query =
| Qnotask of (Controller_itp.controller -> string list -> string)
| Qtask of (Controller_itp.controller -> Trans.naming_table -> string list -> string)
(* The first argument is not used: these functions are supposed to be given to a
Qtask. *)
val print_id: 'a -> Trans.naming_table -> string list -> string
val search_id: 'a -> Trans.naming_table -> string list -> string
......@@ -65,6 +66,9 @@ type command =
| Strategies of string
| Edit of Whyconf.config_prover
| Bisect
| Replay
| Clean
| Mark_Obsolete
| Help_message of string
| Query of string
| QError of string
......
......@@ -391,9 +391,9 @@ let goal_iter_proof_attempt s f g =
fold_all_sub_goals_of_proofn
s
(fun _ pn -> Hprover.iter
(fun _ pan ->
let pan = get_proof_attempt_node s pan in
f pan)
(fun _ pa ->
let pan = get_proof_attempt_node s pa in
f pa pan)
pn.proofn_attempts) () g
let fold_all_sub_goals_of_theory s f acc th =
......@@ -406,9 +406,9 @@ let theory_iter_proofn s f th =
let theory_iter_proof_attempt s f th =
fold_all_sub_goals_of_theory s
(fun _ pn -> Hprover.iter (fun _ pan ->
let pan = get_proof_attempt_node s pan in
f pan)
(fun _ pn -> Hprover.iter (fun _ pa ->
let pan = get_proof_attempt_node s pa in
f pa pan)
pn.proofn_attempts) () th
let file_iter_proof_attempt s f file =
......@@ -416,7 +416,15 @@ let file_iter_proof_attempt s f file =
(theory_iter_proof_attempt s f)
(file_theories file)
let any_iter_proof_attempt s f any =
match any with
| AFile file -> file_iter_proof_attempt s f file
| ATh th -> theory_iter_proof_attempt s f th
| ATn tr ->
let subgoals = get_sub_tasks s tr in
List.iter (fun g -> goal_iter_proof_attempt s f g) subgoals
| APn pn -> goal_iter_proof_attempt s f pn
| APa pa -> f pa (get_proof_attempt_node s pa)
......
......@@ -124,13 +124,16 @@ val get_encapsulating_file: session -> any -> file
(** {2 iterators on sessions} *)
val goal_iter_proof_attempt:
session -> (proof_attempt_node -> unit) -> proofNodeID -> unit
session -> (proofAttemptID -> proof_attempt_node -> unit) -> proofNodeID -> unit
val theory_iter_proof_attempt:
session -> (proof_attempt_node -> unit) -> theory -> unit
session -> (proofAttemptID -> proof_attempt_node -> unit) -> theory -> unit
val file_iter_proof_attempt:
session -> (proof_attempt_node -> unit) -> file -> unit
session -> (proofAttemptID -> proof_attempt_node -> unit) -> file -> unit
val any_iter_proof_attempt:
session -> (proofAttemptID -> proof_attempt_node -> unit) -> any -> unit
val session_iter_proof_attempt:
(proofAttemptID -> proof_attempt_node -> unit) -> session -> unit
......
......@@ -247,7 +247,7 @@ let add_to_check_no_smoke some_merge_miss found_obs cont =
C.register_observer update_monitor;
if !opt_provers = [] then
let () =
C.replay ~obsolete_only:false ~use_steps:!opt_use_steps ~callback ~notification ~final_callback cont
C.replay ~obsolete_only:false ~use_steps:!opt_use_steps ~callback ~notification ~final_callback cont ~any:None
in ()
else
failwith "option -P not yet supported"
......
......@@ -91,7 +91,7 @@ module Table =
struct
let provers_stats s provers theory =
theory_iter_proof_attempt s (fun a ->
theory_iter_proof_attempt s (fun _ a ->
Hprover.replace provers a.prover a.prover) theory
let print_prover = Whyconf.print_prover
......
......@@ -248,7 +248,7 @@ let iter_proof_attempt_by_filter ses iter filters f =
let theory_iter_proof_attempt_by_filter s filters f th =
iter_proof_attempt_by_filter
s
(fun f s -> S.theory_iter_proof_attempt s f)
(fun f s -> S.theory_iter_proof_attempt s (fun _ -> f))
filters f th
let session_iter_proof_attempt_by_filter s filters f =
......@@ -305,21 +305,21 @@ let ask_yn_nonblock ~callback =
let get_used_provers_goal session g =
let sprover = ref Whyconf.Sprover.empty in
Session_itp.goal_iter_proof_attempt session
(fun pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
(fun _ pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
g;
!sprover
let get_used_provers_theory session th =
let sprover = ref Whyconf.Sprover.empty in
Session_itp.theory_iter_proof_attempt session
(fun pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
(fun _ pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
th;
!sprover
let get_used_provers_file session f =
let sprover = ref Whyconf.Sprover.empty in
Session_itp.file_iter_proof_attempt session
(fun pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
(fun _ pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
f;
!sprover
......
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