Commit 51c0880b authored by Sylvain Dailler's avatar Sylvain Dailler

Clear command after request is sent.

(ide) new_node returns the row_ref of new node. So that we can go to
the ggoal generated by transformation (convenience).
Changed the update of the proof_status in controller_itp. update_node
functions now take a callback called notification which is actually
P.notify (node_change).
Put type any inside session_itp.ml.
parent 90b61502
......@@ -530,8 +530,11 @@ let new_node ?parent ?(collapse=false) id typ info =
(* By default expand_path when creating a new node *)
if not collapse then goals_view#expand_to_path (goals_model#get_path iter);
Hint.add node_id_to_gtree id new_ref;
set_status_column iter
set_status_column iter;
new_ref
end
else
Hint.find node_id_to_gtree id
(*******************************)
(* commands of the "View" menu *)
......@@ -559,10 +562,11 @@ let (_ : GMenu.image_menu_item) =
view_factory#add_image_item ~key:GdkKeysyms._E
~label:"Expand all" ~callback:(fun () -> goals_view#expand_all ()) ()
(* let collapse_iter iter =
let collapse_iter iter =
let path = goals_model#get_path iter in
goals_view#collapse_row path
(*
let rec collapse_proven_goals_from_pn pn =
match pn_proved cont pn with
| true -> collapse_iter (row_from_pn pn)#iter
......@@ -670,55 +674,8 @@ let interp cmd =
else
root_node
in
send_request (Command_req cmd, id)
(*
let id =
match !current_selected_index with
| IproofNode id -> Some id
| _ -> None
in
try
match interp cont id cmd with
| Transform(s,_t,args) ->
clear_command_entry ();
apply_transform cont s args
| Query s ->
clear_command_entry ();
message_zone#buffer#set_text s
| Other(s,args) ->
begin
match parse_prover_name gconfig.config s args with
| Some (prover_config, limit) ->
clear_command_entry ();
test_schedule_proof_attempt cont prover_config limit
| None ->
match s with
| "auto" ->
let s =
match args with
| "2"::_ -> "2"
| _ -> "1"
in
clear_command_entry ();
run_strategy_on_task s
| "help" ->
clear_command_entry ();
let text = Pp.sprintf
"Please type a command among the following (automatic completion available)@\n\
@\n\
@ <transformation name> [arguments]@\n\
@ <prover name> [<time limit> [<mem limit>]]@\n\
@ <query> [arguments]@\n\
@ auto [auto level]@\n\
@\n\
Available queries are:@\n@[%a@]" help_on_queries ()
in
message_zone#buffer#set_text text
| _ ->
message_zone#buffer#set_text ("unknown command '"^s^"'")
end
with e when not (Debug.test_flag Debug.stack_trace) ->
message_zone#buffer#set_text (Pp.sprintf "anomaly: %a" Exn_printer.exn_printer e) *)
send_request (Command_req cmd, id);
clear_command_entry ()
let (_ : GtkSignal.id) =
command_entry#connect#activate
......@@ -762,7 +719,7 @@ let treat_message_notification msg = match msg with
| Help s -> add_to_msg_zone s
| Information s -> add_to_msg_zone s
| Task_Monitor (t, s, r) -> update_monitor t s r
(* TODO do not print it *)
(* TODO do not print this particular error *)
| Error s ->
if Debug.test_flag debug then
add_to_msg_zone s
......@@ -774,11 +731,15 @@ let treat_notification n = match n with
Hint.replace node_id_info id info;
set_status_column (get_node_row id)#iter
| New_node (id, pid, typ, info) ->
begin try
begin (try
let parent = get_node_row pid in
new_node ~parent id typ info
let row_ref = new_node ~parent id typ info in
(* TODO for easier testing of IDE *)
if typ = NGoal then goals_view#selection#select_iter row_ref#iter
with Not_found ->
new_node id typ info
let row_ref = new_node id typ info in
(* TODO for easier testing of IDE *)
if typ = NGoal then goals_view#selection#select_iter row_ref#iter);
end
| Remove _id -> (* TODO *)
add_to_msg_zone "got a Remove notification not yet supported\n"
......
......@@ -95,48 +95,89 @@ let file_proved c f =
List.for_all (fun th -> th_proved c th) f.file_theories
(* Update the result of the theory according to its children *)
let update_theory_proof_state ps th =
let update_theory_proof_state notification ps th =
let goals = theory_goals th in
Hid.replace ps.th_state (theory_name th)
(List.for_all (fun id -> Hpn.find_def ps.pn_state false id) goals)
if Hid.mem ps.th_state (theory_name th) then
begin
let old_state = Hid.find_def ps.th_state false (theory_name th) in
let new_state =
List.for_all (fun id -> Hpn.find_def ps.pn_state false id) goals in
if new_state != old_state then
begin
Hid.replace ps.th_state (theory_name th) new_state;
notification (ATh th) new_state
end
end
else
begin
let new_state =
List.for_all (fun id -> Hpn.find_def ps.pn_state false id) goals in
Hid.replace ps.th_state (theory_name th) new_state;
notification (ATh th) new_state
end
let rec propagate_proof c (id: Session_itp.proofNodeID) =
let rec propagate_proof notification c (id: Session_itp.proofNodeID) =
let tr_list = get_transformations c.controller_session id in
let new_state = List.exists (fun id -> tn_proved c id) tr_list in
if new_state != pn_proved c id then
begin
Hpn.replace c.proof_state.pn_state id new_state;
update_proof c id
notification (APn id) new_state;
update_proof notification c id
end
and propagate_trans c (tid: Session_itp.transID) =
and propagate_trans notification c (tid: Session_itp.transID) =
let proof_list = get_sub_tasks c.controller_session tid in
let cur_state = tn_proved c tid in
let new_state = List.for_all (fun id -> pn_proved c id) proof_list in
if cur_state != new_state then
begin
Htn.replace c.proof_state.tn_state tid new_state;
propagate_proof c (get_trans_parent c.controller_session tid)
notification (ATn tid) new_state;
propagate_proof notification c (get_trans_parent c.controller_session tid)
end
and update_proof c id =
and update_proof notification c id =
match get_proof_parent c.controller_session id with
| Theory th -> update_theory_proof_state c.proof_state th
| Trans tid -> propagate_trans c tid
| Theory th -> update_theory_proof_state notification c.proof_state th
| Trans tid -> propagate_trans notification c tid
(* [update_proof_node c id b] Update the whole proof_state
of c according to the result (id, b) *)
let update_proof_node c id b =
match pn_proved c id with
| true -> ()
| false -> Hpn.replace c.proof_state.pn_state id b;
update_proof c id
(* [update_trans_node c id b] Update the proof_state of c to take the result of (id,b). Then
propagates it to its parents *)
let update_trans_node c id b =
Htn.replace c.proof_state.tn_state id b;
propagate_proof c (get_trans_parent c.controller_session id)
let update_proof_node notification c id b =
if (Hpn.mem c.proof_state.pn_state id) then
begin
let b' = Hpn.find_def c.proof_state.pn_state false id in
if b != b' then
begin
Hpn.replace c.proof_state.pn_state id b;
notification (APn id) b;
update_proof notification c id
end
end
else
begin
Hpn.replace c.proof_state.pn_state id b;
notification (APn id) b;
update_proof notification c id
end
(* [update_trans_node c id b] Update the proof_state of c to take the result of
(id,b). Then propagates it to its parents *)
let update_trans_node notification c id b =
if (Htn.mem c.proof_state.tn_state id) then
begin
let b' = Htn.find_def c.proof_state.tn_state false id in
if b != b' then
begin
Htn.replace c.proof_state.tn_state id b;
notification (ATn id) b
end
end
else
(Htn.replace c.proof_state.tn_state id b;
notification (ATn id) b);
propagate_proof notification c (get_trans_parent c.controller_session id)
(* init proof state after reload *)
let rec reload_goal_proof_state ps c g =
......@@ -411,10 +452,10 @@ let schedule_proof_attempt_r c id pr ~limit ~callback =
callback panid Scheduled;
run_timeout_handler ()
let schedule_proof_attempt c id pr ~limit ~callback =
let schedule_proof_attempt c id pr ~limit ~callback ~notification =
let callback panid s = (match s with
| Done pr -> update_proof_node c id (pr.Call_provers.pr_answer == Call_provers.Valid)
| Interrupted | InternalFailure _ -> update_proof_node c id false
| Done pr -> update_proof_node notification c id (pr.Call_provers.pr_answer == Call_provers.Valid)
| Interrupted | InternalFailure _ -> update_proof_node notification c id false
| _ -> ());
callback panid s
in
......@@ -449,7 +490,7 @@ let schedule_transformation_r c id name args ~callback =
S.idle ~prio:0 apply_trans;
callback TSscheduled
let schedule_transformation c id name args ~callback =
let schedule_transformation c id name args ~callback ~notification =
let callback s = (match s with
| TSdone tid ->
let has_subtasks =
......@@ -457,14 +498,14 @@ let schedule_transformation c id name args ~callback =
| [] -> true
| _ -> false
in
update_trans_node c tid has_subtasks
update_trans_node notification c tid has_subtasks
| TSfailed _e -> ()
| _ -> ()); callback s in
schedule_transformation_r c id name args ~callback
open Strategy
let run_strategy_on_goal c id strat ~callback_pa ~callback_tr ~callback =
let run_strategy_on_goal c id strat ~callback_pa ~callback_tr ~callback ~notification =
let rec exec_strategy pc strat g =
if pc < 0 || pc >= Array.length strat then
callback STShalt
......@@ -491,7 +532,7 @@ let run_strategy_on_goal c id strat ~callback_pa ~callback_tr ~callback =
let limit = { Call_provers.empty_limit with
Call_provers.limit_time = timelimit;
limit_mem = memlimit} in
schedule_proof_attempt c g p ~limit ~callback
schedule_proof_attempt c g p ~limit ~callback ~notification
| Itransform(trname,pcsuccess) ->
let callback ntr =
callback_tr ntr;
......@@ -511,7 +552,7 @@ let run_strategy_on_goal c id strat ~callback_pa ~callback_tr ~callback =
S.idle ~prio:0 run_next)
(get_sub_tasks c.controller_session tid)
in
schedule_transformation c g trname [] ~callback
schedule_transformation c g trname [] ~callback ~notification
| Igoto pc ->
callback (STSgoto (g,pc));
exec_strategy pc strat g
......
......@@ -158,7 +158,8 @@ val schedule_proof_attempt :
proofNodeID ->
Whyconf.prover ->
limit:Call_provers.resource_limit ->
callback:(proofAttemptID -> proof_attempt_status -> unit) -> unit
callback:(proofAttemptID -> proof_attempt_status -> unit) ->
notification:(any -> bool -> unit) -> unit
(** [schedule_proof_attempt s id p ~timelimit ~callback] schedules a
proof attempt for a goal specified by [id] with the prover [p] with
time limit [timelimit]; the function [callback] will be called each
......@@ -171,7 +172,8 @@ val schedule_transformation :
proofNodeID ->
string ->
string list ->
callback:(transformation_status -> unit) -> unit
callback:(transformation_status -> unit) ->
notification:(any -> bool -> unit) -> unit
(** [schedule_transformation c id cb] schedules a transformation for a
goal specified by [id]; the function [cb] will be called each time
the transformation status changes. Typically at Scheduled, then
......@@ -183,7 +185,8 @@ val run_strategy_on_goal :
Strategy.t ->
callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
callback_tr:(transformation_status -> unit) ->
callback:(strategy_status -> unit) -> unit
callback:(strategy_status -> unit) ->
notification:(any -> bool -> unit) -> unit
(** [run_strategy_on_goal c id strat] executes asynchronously the
strategy [strat] on the goal [id]. [callback_pa] is called for
each proof attempted (as in [schedule_proof_attempt]) and
......
......@@ -174,13 +174,6 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
(* ----------------------------------- ------------------------------------- *)
type any =
| AFile of file
| ATh of theory
| ATn of transID
| APn of proofNodeID
| APa of proofAttemptID
let get_info_and_type ses (node: any) =
match node with
| AFile file ->
......@@ -407,6 +400,14 @@ exception Bad_prover_name of prover
end;
P.notify (Proof_update (node_ID_from_pan panid, pa_status))
let notify_change x b =
try (
let node_ID = node_ID_from_any x in
let _, node_info = get_info_and_type cont.controller_session x in
P.notify (Node_change (node_ID, {name = node_info.name; proved = b}))
)
with Not_found -> ()
let schedule_proof_attempt nid (p: Whyconf.config_prover) limit =
let prover = p.Whyconf.prover in
let callback = callback_update_tree_proof cont in
......@@ -423,7 +424,7 @@ exception Bad_prover_name of prover
| ATh th ->
List.rev (unproven_goals_below_th cont [] th)
in
List.iter (fun id -> C.schedule_proof_attempt cont id prover ~limit ~callback)
List.iter (fun id -> C.schedule_proof_attempt cont id prover ~limit ~callback ~notification:notify_change)
goals
(* ----------------- Schedule transformation -------------------- *)
......@@ -446,8 +447,11 @@ exception Bad_prover_name of prover
let rec apply_transform nid t args =
match any_from_node_ID nid with
| APn id ->
(* let node_ID = node_ID_from_any x in *)
(* let _, node_info = get_info_and_type cont.controller_session x in *)
(* P.notify (Node_change (node_ID, {name = node_info.name; proved = b})) in *)
let callback = callback_update_tree_transform in
C.schedule_transformation cont id t args ~callback
C.schedule_transformation cont id t args ~callback ~notification:notify_change
| APa panid ->
let parent_id = get_proof_attempt_parent cont.controller_session panid in
let parent = node_ID_from_pn parent_id in
......@@ -474,7 +478,7 @@ exception Bad_prover_name of prover
in
let callback_pa = callback_update_tree_proof cont in
let callback_tr st = callback_update_tree_transform st in
C.run_strategy_on_goal cont id st ~callback_pa ~callback_tr ~callback
C.run_strategy_on_goal cont id st ~callback_pa ~callback_tr ~callback ~notification:notify_change
| _ -> Format.printf "Strategy '%s' not found@." s
end
| _ -> ()
......@@ -551,7 +555,7 @@ exception Bad_prover_name of prover
with e -> P.notify (Message (Error (Pp.string_of
(fun fmt (r,nid,e) -> Format.fprintf fmt
"There was an unrecoverable error during treatment of request:\n %a\non node: %d\nwith exception: %a"
print_request (Obj.magic r) nid Exn_printer.exn_printer e ) (r, nid, e))))
print_request r nid Exn_printer.exn_printer e ) (r, nid, e))))
let treat_requests () : bool =
List.iter treat_request (P.get_requests ());
......
......@@ -63,6 +63,13 @@ type file = {
file_detached_theories : theory list;
}
type any =
| AFile of file
| ATh of theory
| ATn of transID
| APn of proofNodeID
| APa of proofAttemptID
module Proofnodeid = struct
type t = proofNodeID
let _compare (x : proofNodeID) y = Pervasives.compare x y
......
......@@ -39,6 +39,13 @@ type file = private {
file_detached_theories : theory list;
}
type any =
| AFile of file
| ATh of theory
| ATn of transID
| APn of proofNodeID
| APa of proofAttemptID
val theory_name : theory -> Ident.ident
val theory_goals : theory -> proofNodeID list
val theory_detached_goals : theory -> proofNodeID list
......
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