Skip to content

GitLab

why3
why3
Commit d8294aba authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

ITP sessions: proved status in now inside the session static state and saved on disk

parent e556b0af
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 432 additions and 484 deletions
src/session/controller_itp.ml
View file @ d8294aba
......@@ -58,44 +58,19 @@ let print_strategy_status fmt st =
| STShalt -> fprintf fmt "halt"
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 () = {
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;
proof_state: proof_state;
controller_config : Whyconf.config;
controller_env: Env.env;
controller_provers:
(Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
}
(*
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
*)
let create_controller config env ses =
let c =
{
controller_session = ses;
proof_state = init_proof_state ();
controller_config = config;
controller_env = env;
controller_provers = Whyconf.Hprover.create 7;
......@@ -115,112 +90,11 @@ let create_controller config env ses =
provers;
c
let tn_proved c tid = Htn.find_def c.proof_state.tn_state false tid
let pn_proved c pid = Hpn.find_def c.proof_state.pn_state false pid
let th_proved c th =
if (theory_goals th = []) then
Hid.find_def c.proof_state.th_state true (theory_name th)
else
Hid.find_def c.proof_state.th_state false (theory_name th)
let file_proved c f =
if f.file_theories = [] then
Stdlib.Hstr.find_def c.proof_state.file_state true f.file_name
else
Stdlib.Hstr.find_def c.proof_state.file_state false f.file_name
let any_proved cont any : bool =
match any with
| AFile file -> file_proved cont file
| ATh th -> th_proved cont th
| ATn tn -> tn_proved cont tn
| APn pn -> pn_proved cont pn
| APa pa ->
begin
let pa = get_proof_attempt_node cont.controller_session pa in
match pa.Session_itp.proof_state with
| None -> false
| Some pa ->
begin
match pa.Call_provers.pr_answer with
| Call_provers.Valid -> true
| _ -> false
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 -> ()
(** TODO : REMOVE the following, it should be handle by session
make the whole reloading of proof_state more efficient and natural *)
(* Note that f has side effect on the elements of l. We want this effect to
happen. That's why we cannot use List.for_all (respectively List.exists)
directly (List.for_all stops on first element that evaluates to false) *)
let for_all_se f l =
List.for_all (fun b -> b) (List.map f l)
let exists_se f l =
List.exists (fun b -> b) (List.map f l)
(* init proof state after reload *)
let rec reload_goal_proof_state c g =
let ses = c.controller_session in
let tr_list = get_transformations ses g in
let pa_list = get_proof_attempts ses g 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
Hpn.replace c.proof_state.pn_state g proved;
proved
and reload_trans_proof_state c tr =
let proof_list = get_sub_tasks c.controller_session tr in
let proved = for_all_se (reload_goal_proof_state c) proof_list in
Htn.replace c.proof_state.tn_state tr proved;
proved
and reload_pa_proof_state pa =
match pa.proof_obsolete, pa.Session_itp.proof_state with
| false, Some pr when pr.Call_provers.pr_answer = Call_provers.Valid -> true
| _ -> false
(* to be called after reload *)
let reload_theory_proof_state c th =
let ps = c.proof_state in
let goals = theory_goals th in
let proved = for_all_se (reload_goal_proof_state c) goals in
Hid.replace ps.th_state (theory_name th) proved;
proved
(* to be called after reload *)
let reload_file_proof_state c f =
let ps = c.proof_state in
let proved = for_all_se (reload_theory_proof_state c) f.file_theories in
Stdlib.Hstr.replace ps.file_state f.file_name proved
(* to be called after reload *)
let reload_session_proof_state c =
Stdlib.Hstr.iter
(fun _ f -> reload_file_proof_state c f)
(get_files c.controller_session)
(*========== cut ================*)
(* Get children of any without proofattempts *)
let get_undetached_children_no_pa s any : any list =
match any with
| AFile f -> List.map (fun th -> ATh th) f.file_theories
| AFile f -> List.map (fun th -> ATh th) (file_theories f)
| ATh th -> List.map (fun g -> APn g) (theory_goals th)
| ATn tn -> List.map (fun pn -> APn pn) (get_sub_tasks s tn)
| APn pn -> List.map (fun tn -> ATn tn) (get_transformations s pn)
......@@ -229,67 +103,6 @@ let get_undetached_children_no_pa s any : any list =
(* 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
......@@ -313,15 +126,15 @@ module PSession = struct
match x.tkind with
| Session -> "", Hstr.fold (fun _ f -> n (File f)) (get_files s) []
| File f ->
f.file_name,
(file_name f),
List.fold_right
(fun th -> n (Theory th))
f.file_detached_theories
(List.fold_right (fun th -> n (Theory th)) f.file_theories [])
(file_detached_theories f)
(List.fold_right (fun th -> n (Theory th)) (file_theories f) [])
| Theory th ->
let id = theory_name th in
let name = id.Ident.id_string in
let name = if th_proved x.tcont th then name^"!" else name^"?" in
let name = if th_proved s th then name^"!" else name^"?" in
name,
List.fold_right
(fun g -> n (Goal g))
......@@ -330,7 +143,7 @@ module PSession = struct
| Goal id ->
let gid = get_proof_name s id in
let name = gid.Ident.id_string in
let name = if pn_proved x.tcont id then name^"!" else name^"?" in
let name = if pn_proved s id then name^"!" else name^"?" in
let pas = get_proof_attempts s id in
let trs = get_transformations s id in
name,
......@@ -345,7 +158,7 @@ module PSession = struct
(if pa.proof_obsolete then "O" else ""), []
| Transf id ->
let name = get_transf_name s id in
let name = if tn_proved x.tcont id then name^"!" else name^"?" in
let name = if tn_proved s id then name^"!" else name^"?" in
let sts = get_sub_tasks s id in
let dsts = get_detached_sub_tasks s id in
name,
......@@ -389,9 +202,9 @@ let read_file env ?format fn =
tasks associated to them *)
let merge_file (old_ses : session) (c : controller) ~use_shapes _ file =
let format = file.file_format in
let old_theories = file.file_theories in
let file_name = Filename.concat (get_dir old_ses) file.file_name in
let format = file_format file in
let old_theories = file_theories file in
let file_name = Filename.concat (get_dir old_ses) (file_name file) in
let new_theories =
try
read_file c.controller_env file_name ?format
......@@ -410,8 +223,6 @@ let reload_files (c : controller) ~use_shapes =
Stdlib.Hstr.iter
(fun f -> merge_file old_ses c ~use_shapes f)
(get_files old_ses);
(* TODO: remove that, it should be handle by session *)
reload_session_proof_state c
with e ->
c.controller_session <- old_ses;
raise e
......@@ -420,25 +231,6 @@ let add_file c ?format fname =
let theories = read_file c.controller_env ?format fname in
add_file_section 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 ~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
node (attached theory / goals) *)
Session_itp.remove_subtree c.controller_session n ~notification:removed;
(match parent with
| Some (APn parent) ->
update_goal_node notification c parent
| Some _ ->
(* This case corresponds to removal of detached node. We don't need to
update the proof_state *)
()
| None ->
(* Cannot remove root. Note that this should already have failed in call
to Session_itp.remove_subtree *)
raise RemoveError)
module type Scheduler = sig
val timeout: ms:int -> (unit -> bool) -> unit
......@@ -566,19 +358,24 @@ let schedule_proof_attempt_r ?proof_script c id pr ~counterexmp ~limit ~callback
let panid =
graft_proof_attempt c.controller_session id pr ~limit
in
Queue.add (c,id,pr,limit,proof_script,callback panid,counterexmp) scheduled_proof_attempts;
Queue.add (c,id,pr,limit,proof_script,callback panid,counterexmp)
scheduled_proof_attempts;
callback panid Scheduled;
run_timeout_handler ()
let schedule_proof_attempt ?proof_script c id pr ~counterexmp ~limit ~callback ~notification =
let schedule_proof_attempt ?proof_script c id pr
~counterexmp ~limit ~callback ~notification =
let callback panid s = callback panid s;
(match s with
| Scheduled | Running | Done _ -> update_goal_node notification c id
| Scheduled | Running | Done _ ->
update_goal_node notification c.controller_session id
| _ -> ())
in
(* proof_script is specific to interactive manual provers *)
let session_dir = Session_itp.get_dir c.controller_session in
let proof_script = Opt.map (Sysutil.absolutize_filename session_dir) proof_script in
let proof_script =
Opt.map (Sysutil.absolutize_filename session_dir) proof_script
in
schedule_proof_attempt_r ?proof_script c id pr ~counterexmp ~limit ~callback
(* TODO to be simplified *)
......@@ -591,7 +388,7 @@ let create_file_rel_path c pr pn =
let th = get_encapsulating_theory session (APn pn) in
let th_name = (Session_itp.theory_name th).Ident.id_string in
let f = get_encapsulating_file session (ATh th) in
let fn = f.file_name in
let fn = file_name f in
let file = Driver.file_of_task driver fn th_name task in
let file = Filename.concat session_dir file in
let file = Sysutil.uniquify file in
......@@ -643,7 +440,7 @@ let schedule_edition c id pr ?file ~callback ~notification =
(* Notification node *)
let callback panid s = callback panid s;
match s with
| Scheduled | Running | Done _ -> update_goal_node notification c id
| Scheduled | Running | Done _ -> update_goal_node notification c.controller_session id
| _ -> ()
in
......@@ -724,7 +521,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 -> update_trans_node notification c tid
| TSdone tid -> update_trans_node notification c.controller_session tid
| TSfailed _e -> ()
| _ -> ()) in
schedule_transformation_r c id name args ~callback
......@@ -800,43 +597,44 @@ let schedule_tr_with_same_arguments
let name = get_transf_name s tr in
schedule_transformation c pn name args ~callback ~notification
let clean_session c ~remove =
let clean_session c ~removed =
(* 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
(fun () any ->
(match any with
| APa pa ->
let pa = Session_itp.get_proof_attempt_node c.controller_session pa in
if pn_proved c pa.parent then
let pa = Session_itp.get_proof_attempt_node s pa in
if pn_proved s pa.parent then
(match pa.Session_itp.proof_state with
| None -> ()
| Some pr ->
if pa.Session_itp.proof_obsolete ||
Call_provers.(pr.pr_answer <> Valid)
then
remove_subtree c ~removed:remove ~notification:(fun _ -> ()) any)
remove_subtree ~notification ~removed s any)
| ATn tn ->
let pn = get_trans_parent c.controller_session tn in
if pn_proved c pn && not (tn_proved c tn) then
remove_subtree c ~removed:remove ~notification:(fun _ -> ()) (ATn tn)
let pn = get_trans_parent s tn in
if pn_proved s pn && not (tn_proved s tn) then
remove_subtree s ~notification ~removed (ATn tn)
| _ -> ())) ()
(* This function folds on any subelements of given node and tries to mark all
proof attempts it encounters *)
let mark_as_obsolete ~notification c any =
let s = c.controller_session in
(* Case for proof attempt only *)
let mark_as_obsolete_pa c n =
let s = c.controller_session in
let mark_as_obsolete_pa n =
let parent = get_proof_attempt_parent s n in
Session_itp.mark_obsolete s n;
notification (APa n);
update_goal_node notification c parent
update_goal_node notification s parent
in
let s = c.controller_session in
fold_all_any s
(fun () any -> match any with
| APa n -> mark_as_obsolete_pa c n
| APa n -> mark_as_obsolete_pa n
| _ -> ()) () any
exception BadCopyPaste
......
src/session/controller_itp.mli
View file @ d8294aba
......@@ -61,13 +61,8 @@ module type Scheduler = sig
end
(** Correspondance between a node of the proof tree
and its state (proved or not) *)
type proof_state
type controller = private
{ mutable controller_session : Session_itp.session;
proof_state : proof_state;
controller_config : Whyconf.config;
controller_env : Env.env;
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
......@@ -77,13 +72,6 @@ val create_controller: Whyconf.config -> Env.env -> Session_itp.session -> contr
(** creates a controller for the given session.
The config and env is used to load the drivers for the provers. *)
(** Used to find if a proof/trans node or theory is proved or not *)
val tn_proved: controller -> Session_itp.transID -> bool
val pn_proved: controller -> Session_itp.proofNodeID -> bool
val th_proved: controller -> Session_itp.theory -> bool
val file_proved: controller -> Session_itp.file -> bool
val any_proved: controller -> any -> bool
val print_session : Format.formatter -> controller -> unit
......@@ -145,14 +133,6 @@ 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) ->
notification:notifier -> unit
module Make(S : Scheduler) : sig
......@@ -233,11 +213,10 @@ val run_strategy_on_goal :
[schedule_transformation]). [callback] is called on each step of
execution of the strategy. *)
val clean_session:
controller ->
remove:(any -> unit) -> unit
(** Remove proof_attempts below proved goals, although thet are either obsoloete or not valid
*)
val clean_session: controller -> removed:notifier -> 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. *)
val mark_as_obsolete:
notification:notifier ->
......
src/session/itp_server.ml
View file @ d8294aba
......@@ -15,25 +15,28 @@ exception Bad_prover_name of string
Else, return the concatenation of the reversed list of unproven
goals below the transformation and acc *)
let rec unproven_goals_below_tn cont acc tn =
if tn_proved cont tn then
let s = cont.controller_session in
if tn_proved s tn then
acc (* we ignore "dead" goals *)
else
let sub_tasks = get_sub_tasks cont.controller_session tn in
let sub_tasks = get_sub_tasks s tn in
List.fold_left (unproven_goals_below_pn cont) acc sub_tasks
(* Same as unproven_goals_below_tn; note that if goal is not proved
and there is no transformation, goal is returned (else it is not) *)
and unproven_goals_below_pn cont acc goal =
if pn_proved cont goal then
let s = cont.controller_session in
if pn_proved s goal then
acc (* we ignore "dead" transformations *)
else
match get_transformations cont.controller_session goal with
match get_transformations s goal with
| [] -> goal :: acc
| tns -> List.fold_left (unproven_goals_below_tn cont) acc tns
(* Same as unproven_goals_below_tn *)
let unproven_goals_below_th cont acc th =
if th_proved cont th then
let s = cont.controller_session in
if th_proved s th then
acc
else
let goals = theory_goals th in
......@@ -41,10 +44,11 @@ let unproven_goals_below_th cont acc th =
(* Same as unproven_goals_below_tn *)
let unproven_goals_below_file cont file =
if file_proved cont file then
let s = cont.controller_session in
if file_proved s file then
[]
else
let theories = file.file_theories in
let theories = file_theories file in
List.fold_left (unproven_goals_below_th cont) [] theories
let unproven_goals_below_id cont id =
......@@ -413,7 +417,7 @@ let () =
let node_ID_from_pn pn = Hpn.find pn_to_node_ID pn
let node_ID_from_tn tn = Htn.find tn_to_node_ID tn
let node_ID_from_th th = Ident.Hid.find th_to_node_ID (theory_name th)
let node_ID_from_file file = Hstr.find file_to_node_ID (file.file_name)
let node_ID_from_file file = Hstr.find file_to_node_ID (file_name file)
let node_ID_from_any any =
match any with
......@@ -426,9 +430,9 @@ let () =
let remove_any_node_ID any =
match any with
| AFile file ->
let nid = Hstr.find file_to_node_ID file.file_name in
let nid = Hstr.find file_to_node_ID (file_name file) in
Hint.remove model_any nid;
Hstr.remove file_to_node_ID file.file_name
Hstr.remove file_to_node_ID (file_name file)
| ATh th ->
let nid = Ident.Hid.find th_to_node_ID (theory_name th) in
Hint.remove model_any nid;
......@@ -454,7 +458,7 @@ let () =
let add_node_to_table node new_id =
match node with
| AFile file -> Hstr.add file_to_node_ID file.file_name new_id
| AFile file -> Hstr.add file_to_node_ID (file_name file) new_id
| ATh th -> Ident.Hid.add th_to_node_ID (theory_name th) new_id
| ATn tn -> Htn.add tn_to_node_ID tn new_id
| APn pn -> Hpn.add pn_to_node_ID pn new_id
......@@ -609,8 +613,8 @@ end
let s = d.cont.controller_session in
let files = Session_itp.get_files s in
Stdlib.Hstr.iter (fun _ f ->
Format.eprintf "File : %s@." f.file_name;
read_and_send f.file_name) files
Format.eprintf "File : %s@." (file_name f);
read_and_send (file_name f)) files
let relativize_location s loc =
let f, l, b, e = Loc.get loc in
......@@ -670,10 +674,8 @@ end
let get_node_name (node: any) =
let d = get_server_data () in
match node with
| AFile file ->
file.file_name
| ATh th ->
(theory_name th).Ident.id_string
| AFile file -> file_name file
| ATh th -> (theory_name th).Ident.id_string
| ATn tn ->
let name = get_transf_name d.cont.controller_session tn in
let args = get_transf_args d.cont.controller_session tn in
......@@ -696,17 +698,18 @@ end
let get_node_proved new_id (node: any) =
let d = get_server_data () in
let cont = d.cont in
let s = cont.controller_session in
match node with
| AFile file ->
P.notify (Node_change (new_id, Proved (file_proved cont file)))
P.notify (Node_change (new_id, Proved (file_proved s file)))
| ATh th ->
P.notify (Node_change (new_id, Proved (th_proved cont th)))
P.notify (Node_change (new_id, Proved (th_proved s th)))
| ATn tn ->
P.notify (Node_change (new_id, Proved (tn_proved cont tn)))
P.notify (Node_change (new_id, Proved (tn_proved s tn)))
| APn pn ->
P.notify (Node_change (new_id, Proved (pn_proved cont pn)))
P.notify (Node_change (new_id, Proved (pn_proved s pn)))
| APa pa ->
let pa = get_proof_attempt_node cont.controller_session pa in
let pa = get_proof_attempt_node s pa in
let obs = pa.proof_obsolete in
let limit = pa.limit in
let res =
......@@ -807,8 +810,7 @@ end
(f: parent:node_ID -> any -> unit) parent file =
f ~parent (AFile file);
let nid = node_ID_from_file file in
List.iter (iter_subtree_from_theory f nid)