Commit e2f51d1a authored by MARCHE Claude's avatar MARCHE Claude

ITP: enforce preservation of proof statuses with more robust code

parent 0f0dc89d
......@@ -56,15 +56,18 @@ let print_strategy_status fmt st =
open Ident
type proof_state = {
file_state: bool Stdlib.Hstr.t;
th_state: bool Hid.t;
tn_state: bool Htn.t;
pn_state : bool Hpn.t;
}
let init_proof_state () =
{th_state = Hid.create 7;
tn_state = Htn.create 42;
pn_state = Hpn.create 42}
let init_proof_state () = {
file_state = Stdlib.Hstr.create 3;
th_state = Hid.create 7;
tn_state = Htn.create 42;
pn_state = Hpn.create 42;
}
type controller =
{ mutable controller_session: Session_itp.session;
......@@ -75,6 +78,7 @@ type controller =
}
let clear_proof_state c =
Stdlib.Hstr.clear c.proof_state.file_state;
Hid.clear c.proof_state.th_state;
Htn.clear c.proof_state.tn_state;
Hpn.clear c.proof_state.pn_state
......@@ -131,90 +135,10 @@ let remove_any_proof_state cont any : unit =
| ATn tn -> Htn.remove cont.proof_state.tn_state tn
| APa _pa -> ()
(* Update the result of the theory according to its children *)
let update_theory_proof_state notification ps th =
let goals = theory_goals th in
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 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;
notification (APn id) new_state;
update_proof notification c id
end
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;
notification (ATn tid) new_state;
propagate_proof notification c (get_trans_parent c.controller_session tid)
end
and update_proof notification c id =
match get_proof_parent c.controller_session id with
| 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 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)
(** TODO make the whole reloading of proof_state more efficient and natural *)
......@@ -274,6 +198,70 @@ let get_undetached_children_no_pa s any : any list =
| APn pn -> List.map (fun tn -> ATn tn) (get_transformations s pn)
| APa _ -> []
(* status update *)
type notifier = any -> unit
let pa_ok pa =
not pa.proof_obsolete &&
match pa.Session_itp.proof_state
with
| Some { Call_provers.pr_answer = Call_provers.Valid} -> true
| _ -> false
(* [update_goal_node c id] update the proof status of node id
update is propagated to parents when required. *)
let update_file_node notification c f =
let ps = c.proof_state in
let ths = f.file_theories in
let proved = List.for_all (th_proved c) ths in
if proved <> file_proved c f then
begin
Stdlib.Hstr.replace ps.file_state f.file_name proved;
notification (AFile f);
end
let update_theory_node notification c th =
let ps = c.proof_state in
let goals = theory_goals th in
let proved = List.for_all (pn_proved c) goals in
if proved <> th_proved c th then
begin
Hid.replace ps.th_state (theory_name th) proved;
notification (ATh th);
update_file_node notification c (theory_parent c.controller_session th)
end
let rec update_goal_node notification c id =
let ses = c.controller_session in
let tr_list = get_transformations ses id in
let pa_list = get_proof_attempts ses id in
let proved = List.exists (tn_proved c) tr_list || List.exists pa_ok pa_list in
if proved <> pn_proved c id then
begin
Hpn.replace c.proof_state.pn_state id proved;
notification (APn id);
match get_proof_parent ses id with
| Trans trans_id -> update_trans_node notification c trans_id
| Theory th -> update_theory_node notification c th
end
and update_trans_node notification c trid =
let ses = c.controller_session in
let proof_list = get_sub_tasks ses trid in
let proved = List.for_all (pn_proved c) proof_list in
if proved <> tn_proved c trid then
begin
Htn.replace c.proof_state.tn_state trid proved;
notification (ATn trid);
update_goal_node notification c (get_trans_parent ses trid)
end
(* printing *)
module PSession = struct
......@@ -405,7 +393,7 @@ let add_file c ?format fname =
(* Update the proof_state according to new false state and then remove
the subtree *)
let remove_subtree c (n: any) ~removed ~node_change =
let remove_subtree c (n: any) ~removed ~notification =
let removed = (fun x -> removed x; remove_any_proof_state c x) in
let parent = get_any_parent c.controller_session n in
(* Note that this line can raise RemoveError when called on inappropriate
......@@ -422,7 +410,7 @@ let remove_subtree c (n: any) ~removed ~node_change =
if proved then
()
else
update_proof_node node_change c parent false
update_goal_node notification c parent
| Some _ ->
(* This case corresponds to removal of detached node. We don't need to
update the proof_state *)
......@@ -560,10 +548,7 @@ let schedule_proof_attempt_r c id pr ~limit ~callback =
let schedule_proof_attempt c id pr ~limit ~callback ~notification =
let callback panid s = callback panid s;
(match s with
| 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
| Scheduled | Done _ -> update_goal_node notification c id
| _ -> ())
in
schedule_proof_attempt_r c id pr ~limit ~callback
......@@ -600,13 +585,7 @@ let schedule_transformation_r c id name args ~callback =
let schedule_transformation c id name args ~callback ~notification =
let callback s = callback s; (match s with
| TSdone tid ->
let has_subtasks =
match get_sub_tasks c.controller_session tid with
| [] -> true
| _ -> false
in
update_trans_node notification c tid has_subtasks
| TSdone tid -> update_trans_node notification c tid
| TSfailed _e -> ()
| _ -> ()) in
schedule_transformation_r c id name args ~callback
......@@ -697,7 +676,7 @@ let is_running (pa: proof_attempt_node) : bool =
| None -> true
| Some _pr -> false
let clean_session c ~remove ~node_change =
let clean_session c ~remove ~notification =
let s = c.controller_session in
Session_itp.session_iter_proof_attempt
(fun _ pa ->
......@@ -705,27 +684,25 @@ let clean_session c ~remove ~node_change =
Hprover.iter (fun _ paid ->
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))
remove_subtree c ~removed:remove ~notification (APa paid))
(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 *)
let mark_as_obsolete ~node_change ~node_obsolete c any =
let mark_as_obsolete ~notification c any =
(* Case for proof attempt only *)
let mark_as_obsolete_pa ~node_change ~node_obsolete c n =
let mark_as_obsolete_pa c n =
let s = c.controller_session in
let parent = get_proof_attempt_parent s n in
Session_itp.mark_obsolete s n;
node_obsolete (APa n) true;
let b = reload_goal_proof_state c parent in
node_change (APn parent) b;
update_proof node_change c parent
notification (APa n);
update_goal_node notification c parent
in
let s = c.controller_session in
fold_all_any s
(fun () any -> match any with
| APa n -> mark_as_obsolete_pa ~node_change ~node_obsolete c n
| APa n -> mark_as_obsolete_pa c n
| _ -> ()) () any
exception BadCopyPaste
......
......@@ -61,15 +61,9 @@ module type Scheduler = sig
end
open Ident
(** Correspondance between a node of the proof tree
and its state (proved or not) *)
type proof_state = {
th_state: bool Hid.t;
tn_state: bool Htn.t;
pn_state : bool Hpn.t;
}
type proof_state
type controller = private
{ mutable controller_session : Session_itp.session;
......@@ -152,11 +146,14 @@ val add_file : controller -> ?format:Env.fformat -> string -> unit
val get_undetached_children_no_pa: Session_itp.session -> any -> any list
type notifier = any -> unit
val remove_subtree:
controller ->
any ->
removed:(any -> unit) ->
node_change:(any -> bool -> unit) -> unit
notification:notifier -> unit
module Make(S : Scheduler) : sig
......@@ -169,6 +166,12 @@ val register_observer : (int -> int -> int -> unit) -> unit
tasks, scheduled tasks, and running tasks, each time these numbers
change *)
(* TODO
val register_notifier : (any -> unit) -> unit
(** records a hook that will be called each time a node change status *)
*)
val interrupt : unit -> unit
(** discards all scheduled proof attempts or transformations, including
the ones already running *)
......@@ -179,7 +182,7 @@ val schedule_proof_attempt :
Whyconf.prover ->
limit:Call_provers.resource_limit ->
callback:(proofAttemptID -> proof_attempt_status -> unit) ->
notification:(any -> bool -> unit) -> unit
notification:notifier -> 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
......@@ -193,7 +196,7 @@ val schedule_transformation :
string ->
string list ->
callback:(transformation_status -> unit) ->
notification:(any -> bool -> unit) -> unit
notification:notifier -> 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
......@@ -206,7 +209,7 @@ val run_strategy_on_goal :
callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
callback_tr:(transformation_status -> unit) ->
callback:(strategy_status -> unit) ->
notification:(any -> bool -> unit) -> unit
notification:notifier -> 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
......@@ -217,17 +220,16 @@ val run_strategy_on_goal :
val clean_session:
controller ->
remove:(any -> unit) ->
node_change:(any -> bool -> unit) -> unit
notification:notifier -> unit
(** Remove proof_attempts that are not valid from the session *)
val mark_as_obsolete:
node_change:(any -> bool -> unit) ->
node_obsolete:(any -> bool -> unit) ->
notification:notifier ->
controller -> any -> unit
(* [copy_paste c a b] try to copy subtree originating at node a to node b *)
val copy_paste:
notification:(any -> bool -> unit) ->
notification:notifier ->
callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
callback_tr:(transformation_status -> unit) ->
controller -> any -> any -> unit
......@@ -258,7 +260,7 @@ val replay:
?use_steps:bool ->
controller ->
callback:(proofAttemptID -> proof_attempt_status -> unit) ->
notification:(any -> bool -> unit) ->
notification:notifier ->
final_callback:
((proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list
-> unit) ->
......
......@@ -909,11 +909,16 @@ let get_locations t =
let new_status = Proof_status_change (pa_status, false, limit) in
P.notify (Node_change (node_ID_from_pan panid, new_status))
let notify_change_proved x b =
try (
let notify_change_proved c x =
try
let node_ID = node_ID_from_any x in
P.notify (Node_change (node_ID, Proved b))
)
let b = any_proved c x in
P.notify (Node_change (node_ID, Proved b));
match x with
| APa pa ->
let obs = (get_proof_attempt_node c.controller_session pa).proof_obsolete in
P.notify (Node_change (node_ID, Obsolete obs))
| _ -> ()
with Not_found -> ()
let schedule_proof_attempt nid (p: Whyconf.config_prover) limit =
......@@ -922,7 +927,7 @@ let get_locations t =
let callback = callback_update_tree_proof d.cont in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
List.iter (fun id -> C.schedule_proof_attempt d.cont id prover
~limit ~callback ~notification:notify_change_proved)
~limit ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
(* ----------------- Schedule transformation -------------------- *)
......@@ -948,7 +953,7 @@ let get_locations t =
match any_from_node_ID nid with
| APn id ->
let callback = callback_update_tree_transform in
C.schedule_transformation d.cont id t args ~callback ~notification:notify_change_proved
C.schedule_transformation d.cont id t args ~callback ~notification:(notify_change_proved d.cont)
| APa panid ->
let parent_id = get_proof_attempt_parent d.cont.controller_session panid in
let parent = node_ID_from_pn parent_id in
......@@ -975,7 +980,7 @@ let get_locations t =
let callback_pa = callback_update_tree_proof d.cont in
let callback_tr st = callback_update_tree_transform st in
List.iter (fun id ->
C.run_strategy_on_goal d.cont id st ~callback_pa ~callback_tr ~callback ~notification:notify_change_proved)
C.run_strategy_on_goal d.cont id st ~callback_pa ~callback_tr ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
| _ -> Debug.dprintf debug_strat "[strategy_exec] strategy '%s' not found@." s
......@@ -983,14 +988,16 @@ let get_locations t =
(* ----------------- Clean session -------------------- *)
let clean_session () =
let d = get_server_data () in
let node_change x b =
(*
let notification x b =
let nid = node_ID_from_any x in
P.notify (Node_change (nid, Proved b)) in
*)
let remove x =
let nid = node_ID_from_any x in
remove_any_node_ID x;
P.notify (Remove nid) in
C.clean_session d.cont ~remove ~node_change
C.clean_session d.cont ~remove ~notification:(notify_change_proved d.cont)
(* ----------------- Save session --------------------- *)
......@@ -1024,7 +1031,7 @@ let get_locations t =
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 ~final_callback
~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"))
......@@ -1033,13 +1040,12 @@ let get_locations t =
let mark_obsolete n =
let d = get_server_data () in
let any = any_from_node_ID n in
let node_change x b =
let nid = node_ID_from_any x in
P.notify (Node_change (nid, Proved b)) 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 ~node_change d.cont any
*)
C.mark_as_obsolete (* ~node_obsolete *) ~notification:(notify_change_proved d.cont) d.cont any
(* ----------------- locate next unproven node -------------------- *)
......@@ -1096,8 +1102,7 @@ let get_locations t =
begin
try
Controller_itp.remove_subtree d.cont n
~node_change:(fun x b -> let nid = node_ID_from_any x in
P.notify (Node_change (nid, Proved b)))
~notification:(notify_change_proved d.cont)
~removed:(fun x ->
let nid = node_ID_from_any x in
remove_any_node_ID x;
......@@ -1108,7 +1113,7 @@ let get_locations t =
| Copy_paste (from_id, to_id) ->
let from_any = any_from_node_ID from_id in
let to_any = any_from_node_ID to_id in
C.copy_paste ~notification:notify_change_proved
C.copy_paste ~notification:(notify_change_proved d.cont)
~callback_pa:(callback_update_tree_proof d.cont)
~callback_tr:(callback_update_tree_transform)
d.cont from_any to_any
......
......@@ -250,7 +250,7 @@ let add_to_check_no_smoke some_merge_miss found_obs cont =
end
in
let callback _paid _pastatus = () in
let notification _any _bool = () in
let notification _any = () in
if !opt_provers = [] then
let () =
C.replay ~obsolete_only:false ~use_steps:!opt_use_steps ~callback ~notification ~final_callback cont
......
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