Commit b3eb5434 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Remove now actualize the controller so that it update proved theory/goal..

parent a892b84a
...@@ -123,6 +123,14 @@ let any_proved cont any : bool = ...@@ -123,6 +123,14 @@ let any_proved cont any : bool =
end end
end end
let remove_any_proof_state cont any : unit =
match any with
| AFile _file -> ()
| ATh th -> Hid.remove cont.proof_state.th_state (theory_name th)
| APn pn -> Hpn.remove cont.proof_state.pn_state pn
| ATn tn -> Htn.remove cont.proof_state.tn_state tn
| APa _pa -> ()
(* Update the result of the theory according to its children *) (* Update the result of the theory according to its children *)
let update_theory_proof_state notification ps th = let update_theory_proof_state notification ps th =
let goals = theory_goals th in let goals = theory_goals th in
...@@ -220,18 +228,18 @@ let exists_se f l = ...@@ -220,18 +228,18 @@ let exists_se f l =
List.exists (fun b -> b) (List.map f l) List.exists (fun b -> b) (List.map f l)
(* init proof state after reload *) (* init proof state after reload *)
let rec reload_goal_proof_state ps c g = let rec reload_goal_proof_state c g =
let ses = c.controller_session in let ses = c.controller_session in
let tr_list = get_transformations ses g in let tr_list = get_transformations ses g in
let pa_list = get_proof_attempts ses g in let pa_list = get_proof_attempts ses g in
let proved = exists_se (reload_trans_proof_state ps c) tr_list in let proved = exists_se (reload_trans_proof_state c) tr_list in
let proved = exists_se reload_pa_proof_state pa_list || proved in let proved = exists_se reload_pa_proof_state pa_list || proved in
Hpn.replace c.proof_state.pn_state g proved; Hpn.replace c.proof_state.pn_state g proved;
proved proved
and reload_trans_proof_state ps c tr = and reload_trans_proof_state c tr =
let proof_list = get_sub_tasks c.controller_session tr in let proof_list = get_sub_tasks c.controller_session tr in
let proved = for_all_se (reload_goal_proof_state ps c) proof_list in let proved = for_all_se (reload_goal_proof_state c) proof_list in
Htn.replace c.proof_state.tn_state tr proved; Htn.replace c.proof_state.tn_state tr proved;
proved proved
...@@ -244,7 +252,7 @@ and reload_pa_proof_state pa = ...@@ -244,7 +252,7 @@ and reload_pa_proof_state pa =
let reload_theory_proof_state c th = let reload_theory_proof_state c th =
let ps = c.proof_state in let ps = c.proof_state in
let goals = theory_goals th in let goals = theory_goals th in
let proved = for_all_se (reload_goal_proof_state ps c) goals in let proved = for_all_se (reload_goal_proof_state c) goals in
Hid.replace ps.th_state (theory_name th) proved Hid.replace ps.th_state (theory_name th) proved
(* to be called after reload *) (* to be called after reload *)
...@@ -395,14 +403,34 @@ let add_file c ?format fname = ...@@ -395,14 +403,34 @@ let add_file c ?format fname =
let theories = read_file c.controller_env ?format fname in let theories = read_file c.controller_env ?format fname in
add_file_section ~use_shapes:false c.controller_session fname theories format add_file_section ~use_shapes:false c.controller_session fname theories format
(* Update the proof_state according to new false state and then remove
the subtree *)
let remove_subtree c (n: any) ~removed ~node_change =
let removed = (fun x -> removed x; remove_any_proof_state c x) in
let parent = get_any_parent c.controller_session n in
match n with
| ATn _ | APa _ ->
Session_itp.remove_subtree c.controller_session n ~notification:removed;
(match parent with
| Some (APn parent) ->
(* If proof_state of the parent is actually changed update the branch
otherwise do nothing *)
let tr_list = get_transformations c.controller_session parent in
let pa_list = get_proof_attempts c.controller_session parent in
let proved = List.exists (tn_proved c) tr_list in
let proved = List.exists reload_pa_proof_state pa_list || proved in
if proved then
()
else
update_proof_node node_change c parent false
| _ -> assert false)
| _ -> ()
module type Scheduler = sig module type Scheduler = sig
val timeout: ms:int -> (unit -> bool) -> unit val timeout: ms:int -> (unit -> bool) -> unit
val idle: prio:int -> (unit -> bool) -> unit val idle: prio:int -> (unit -> bool) -> unit
end end
module Make(S : Scheduler) = struct module Make(S : Scheduler) = struct
let scheduled_proof_attempts = Queue.create () let scheduled_proof_attempts = Queue.create ()
......
...@@ -148,6 +148,12 @@ val add_file : controller -> ?format:Env.fformat -> string -> unit ...@@ -148,6 +148,12 @@ val add_file : controller -> ?format:Env.fformat -> string -> unit
val get_undetached_children_no_pa: Session_itp.session -> any -> any list val get_undetached_children_no_pa: Session_itp.session -> any -> any list
val remove_subtree:
controller ->
any ->
removed:(any -> unit) ->
node_change:(any -> bool -> unit) -> unit
module Make(S : Scheduler) : sig module Make(S : Scheduler) : sig
val set_max_tasks : int -> unit val set_max_tasks : int -> unit
......
...@@ -591,6 +591,29 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -591,6 +591,29 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
| APn pn -> node_ID_from_pn pn | APn pn -> node_ID_from_pn pn
| APa pan -> node_ID_from_pan pan | APa pan -> node_ID_from_pan pan
let remove_any_node_ID any =
match any with
| AFile file ->
let nid = Hstr.find file_to_node_ID file.file_name in
Hint.remove model_any nid;
Hstr.remove file_to_node_ID file.file_name
| ATh th ->
let nid = Ident.Hid.find th_to_node_ID (theory_name th) in
Hint.remove model_any nid;
Ident.Hid.remove th_to_node_ID (theory_name th)
| ATn tn ->
let nid = Htn.find tn_to_node_ID tn in
Hint.remove model_any nid;
Htn.remove tn_to_node_ID tn
| APn pn ->
let nid = Hpn.find pn_to_node_ID pn in
Hint.remove model_any nid;
Hpn.remove pn_to_node_ID pn
| APa pa ->
let nid = Hpan.find pan_to_node_ID pa in
Hint.remove model_any nid;
Hpan.remove pan_to_node_ID pa
let get_prover p = let get_prover p =
let d = get_server_data () in let d = get_server_data () in
match return_prover p d.config with match return_prover p d.config with
...@@ -994,8 +1017,12 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct ...@@ -994,8 +1017,12 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let n = any_from_node_ID nid in let n = any_from_node_ID nid in
begin begin
try try
Session_itp.remove_subtree d.cont.controller_session n ~notification:(fun x -> 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)))
~removed:(fun x ->
let nid = node_ID_from_any x in let nid = node_ID_from_any x in
remove_any_node_ID x;
P.notify (Remove nid)) P.notify (Remove nid))
with RemoveError -> (* TODO send an error instead of information *) with RemoveError -> (* TODO send an error instead of information *)
P.notify (Message (Information "Cannot remove a proof node or theory")) P.notify (Message (Information "Cannot remove a proof node or theory"))
......
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