Skip to content

GitLab

why3
why3
Commit be0cf6b3 authored by Clément Fumex's avatar Clément Fumex
Browse files
Options

merge proof_attempt and proof_attempt_node + fixe controller's proof_state update

parent ea12e95d
Hide whitespace changes
Inline Side-by-side
Showing with 44 additions and 56 deletions
src/ide/why3ide.ml
View file @ be0cf6b3
......@@ -448,7 +448,7 @@ let set_status_column_from_cont cont iter =
let image = match index with
| Inone -> assert false
| IproofAttempt panid ->
let pa = get_proof_attempt cont.controller_session panid in
let pa = get_proof_attempt_node cont.controller_session panid in
image_of_result ~obsolete:pa.proof_obsolete pa.Session_itp.proof_state
| IproofNode pn ->
if pn_proved cont pn
......@@ -579,7 +579,7 @@ let apply_transform cont t args =
(* Callback of a proof_attempt *)
let callback_update_tree_proof cont panid pa_status =
let ses = cont.controller_session in
let pa = get_proof_attempt ses panid in
let pa = get_proof_attempt_node ses panid in
let prover = pa.prover in
let name = Pp.string_of Whyconf.print_prover prover in
let obsolete = pa.proof_obsolete in
......
src/session/controller_itp.ml
View file @ be0cf6b3
......@@ -111,8 +111,10 @@ and update_proof c id =
(* [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 =
Hpn.replace c.proof_state.pn_state id b;
update_proof c id
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 *)
......@@ -161,7 +163,7 @@ module PSession = struct
| Theory of theory
| Goal of proofNodeID
| Transf of transID
| ProofAttempt of proof_attempt
| ProofAttempt of proof_attempt_node
type 'a t = { tcont : controller;
tkind : any }
......
src/session/session_itp.ml
View file @ be0cf6b3
......@@ -26,7 +26,8 @@ let theory_detached_goals t = t.theory_detached_goals
type proof_parent = Trans of transID | Theory of theory
type proof_attempt = {
type proof_attempt_node = {
parent : proofNodeID;
prover : Whyconf.prover;
limit : Call_provers.resource_limit;
mutable proof_state : Call_provers.prover_result option;
......@@ -35,11 +36,6 @@ type proof_attempt = {
proof_script : string option; (* non empty for external ITP *)
}
type proof_attempt_node = {
proofa_parent : proofNodeID;
proofa_attempt : proof_attempt;
}
type proof_node = {
proofn_name : Ident.ident;
proofn_task : Task.task;
......@@ -108,8 +104,7 @@ let _session_iter_proofNode f s =
Hint.iter f s.proofNode_table
let session_iter_proof_attempt f s =
Hint.iter (fun _ pan -> f pan.proofa_parent pan.proofa_attempt)
s.proofAttempt_table
Hint.iter f s.proofAttempt_table
(* This is not needed. Keeping it as information on the structure
type tree = {
......@@ -182,7 +177,7 @@ let gen_proofAttemptID (s : session) =
exception BadID
let get_proofAttemptNode (s : session) (id : proofAttemptID) =
let get_proof_attempt_node (s : session) (id : proofAttemptID) =
try
Hint.find s.proofAttempt_table id
with Not_found -> raise BadID
......@@ -207,16 +202,13 @@ let get_transformations (s : session) (id : proofNodeID) =
let get_proof_attempt_ids (s : session) (id : proofNodeID) =
(get_proofNode s id).proofn_attempts
let get_proof_attempt (s : session) (a : proofAttemptID) =
(get_proofAttemptNode s a).proofa_attempt
let get_proof_attempt_parent (s : session) (a : proofAttemptID) =
(get_proofAttemptNode s a).proofa_parent
(get_proof_attempt_node s a).parent
let get_proof_attempts (s : session) (id : proofNodeID) =
Hprover.fold (fun _ a l ->
let pa = get_proofAttemptNode s a in
pa.proofa_attempt :: l)
let pa = get_proof_attempt_node s a in
pa :: l)
(get_proofNode s id).proofn_attempts []
let get_sub_tasks (s : session) (id : transID) =
......@@ -262,9 +254,9 @@ let theory_iter_proofn s f th =
let theory_iter_proof_attempt s f th =
theory_iter_proofn s
(fun pn -> Hprover.iter (fun _ pan ->
let pan = get_proofAttemptNode s pan in
f pan.proofa_attempt)
pn.proofn_attempts) th
let pan = get_proof_attempt_node s pan in
f pan)
pn.proofn_attempts) th
open Format
open Ident
......@@ -287,10 +279,10 @@ let rec print_proof_node s (fmt: Format.formatter) p =
(Opt.fold (fun _ a -> Termcode.string_of_checksum a) "None" pn.proofn_checksum)
(Pp.print_list Pp.semi print_proof_attempt)
(Hprover.fold (fun _key e l ->
let e = get_proofAttemptNode s e in
e.proofa_attempt :: l)
pn.proofn_attempts [])
(Pp.print_list Pp.semi (print_trans_node s)) pn.proofn_transformations
let e = get_proof_attempt_node s e in
e :: l)
pn.proofn_attempts [])
(Pp.print_list Pp.semi (print_trans_node s)) pn.proofn_transformations
and print_trans_node s fmt id =
let tn = get_transfNode s id in
......@@ -338,9 +330,14 @@ let empty_session ?shape_version dir =
(* proof node/attempt/transformation manipulation *)
(**************************************************)
let mk_proof_attempt session pid pa =
let pn = get_proofNode session pid in
let node = { proofa_parent = pid; proofa_attempt = pa } in
let add_proof_attempt session prover limit state obsolete edit parentID =
let pa = { parent = parentID;
prover = prover;
limit = limit;
proof_state = state;
proof_obsolete = obsolete;
proof_script = edit } in
let pn = get_proofNode session parentID in
let id =
try Hprover.find pn.proofn_attempts pa.prover
with Not_found ->
......@@ -348,20 +345,9 @@ let mk_proof_attempt session pid pa =
Hprover.add pn.proofn_attempts pa.prover id;
id
in
Hint.replace session.proofAttempt_table id node;
Hint.replace session.proofAttempt_table id pa;
id
let add_proof_attempt session prover limit state obsolete edit parentID =
let pa = { prover = prover;
limit = limit;
proof_state = state;
proof_obsolete = obsolete;
proof_script = edit;
} in
mk_proof_attempt session parentID pa
let graft_proof_attempt (s : session) (id : proofNodeID) (pr : Whyconf.prover)
~timelimit =
let limit = { Call_provers.limit_time = timelimit;
......@@ -447,9 +433,9 @@ let remove_transformation (s : session) (id : transID) =
let update_proof_attempt s id pr st =
let n = get_proofNode s id in
let pa = Hprover.find n.proofn_attempts pr in
let pa = get_proofAttemptNode s pa in
pa.proofa_attempt.proof_state <- Some st;
pa.proofa_attempt.proof_obsolete <- false
let pa = get_proof_attempt_node s pa in
pa.proof_state <- Some st;
pa.proof_obsolete <- false
(****************************)
......@@ -886,7 +872,7 @@ let found_missed_goals_in_theory = ref false
let save_detached_goals old_s detached_goals_id s parent =
let save_proof parent old_pa_n =
let old_pa = old_pa_n.proofa_attempt in
let old_pa = old_pa_n in
ignore (add_proof_attempt s old_pa.prover old_pa.limit
old_pa.proof_state true old_pa.proof_script
parent)
......@@ -896,7 +882,7 @@ let save_detached_goals old_s detached_goals_id s parent =
mk_proof_node_no_task s detached_goal.proofn_name parent id None
(Termcode.shape_of_string "");
Hprover.iter (fun _ pa ->
let pa = get_proofAttemptNode old_s pa in
let pa = get_proof_attempt_node old_s pa in
save_proof id pa) detached_goal.proofn_attempts;
List.iter (save_trans id) detached_goal.proofn_transformations;
let new_trans = (get_proofNode s id) in
......@@ -927,7 +913,7 @@ let save_detached_theory old_s detached_theory s =
theory_detached_goals = [] }
let merge_proof new_s obsolete new_goal _ old_pa_n =
let old_pa = old_pa_n.proofa_attempt in
let old_pa = old_pa_n in
let obsolete = obsolete || old_pa.proof_obsolete in
found_obsolete := obsolete || !found_obsolete;
ignore (add_proof_attempt new_s old_pa.prover old_pa.limit
......@@ -950,7 +936,7 @@ let add_registered_transformation s env old_tr goal_id =
let rec merge_goal ~use_shapes env new_s old_s obsolete old_goal new_goal_id =
Hprover.iter (fun k pa ->
let pa = get_proofAttemptNode old_s pa in
let pa = get_proof_attempt_node old_s pa in
merge_proof new_s obsolete new_goal_id k pa)
old_goal.proofn_attempts;
List.iter (merge_trans ~use_shapes env old_s new_s new_goal_id) old_goal.proofn_transformations;
......@@ -1310,9 +1296,8 @@ let rec save_goal s ctxt fmt pnid =
Compress.Compress_z.output_char ctxt.ch_shapes '\n';
let l = Hprover.fold
(fun _ a acc ->
let a = get_proofAttemptNode s a in
(Mprover.find a.proofa_attempt.prover ctxt.provers,
a.proofa_attempt) :: acc)
let a = get_proof_attempt_node s a in
(Mprover.find a.prover ctxt.provers, a) :: acc)
pn.proofn_attempts [] in
let l = List.sort (fun ((i1,_,_,_),_) ((i2,_,_,_),_) -> compare i1 i2) l in
List.iter (save_proof_attempt fmt) l;
......
src/session/session_itp.mli
View file @ be0cf6b3
......@@ -47,7 +47,8 @@ val get_dir : session -> string
val get_shape_version : session -> int
type proof_attempt = {
type proof_attempt_node = {
parent : proofNodeID;
prover : Whyconf.prover;
limit : Call_provers.resource_limit;
mutable proof_state : Call_provers.prover_result option;
......@@ -56,7 +57,7 @@ type proof_attempt = {
proof_script : string option; (* non empty for external ITP *)
}
val session_iter_proof_attempt: (proofNodeID -> proof_attempt -> unit) -> session -> unit
val session_iter_proof_attempt: (proofNodeID -> proof_attempt_node -> unit) -> session -> unit
type proof_parent = Trans of transID | Theory of theory
......@@ -65,9 +66,9 @@ val get_task : session -> proofNodeID -> Task.task
val get_transformations : session -> proofNodeID -> transID list
val get_proof_attempt_ids :
session -> proofNodeID -> proofAttemptID Whyconf.Hprover.t
val get_proof_attempt : session -> proofAttemptID -> proof_attempt
val get_proof_attempt_node : session -> proofAttemptID -> proof_attempt_node
val get_proof_attempt_parent : session -> proofAttemptID -> proofNodeID
val get_proof_attempts : session -> proofNodeID -> proof_attempt list
val get_proof_attempts : session -> proofNodeID -> proof_attempt_node list
val get_sub_tasks : session -> transID -> proofNodeID list
val get_detached_sub_tasks : session -> transID -> 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