Commit f3afc687 authored by MARCHE Claude's avatar MARCHE Claude

add ids and table for proof attempts, and tables in the GTK ui

parent 7bca0332
......@@ -190,7 +190,7 @@ let scrolled_task_view =
GBin.scrolled_window
~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
~shadow_type:`ETCHED_OUT
~packing:vbox222#add
~packing:(vbox222#pack ?from:None ~expand:true ~fill:true ?padding:None)
()
let task_view =
......@@ -204,7 +204,7 @@ let task_view =
let command_entry = GEdit.entry ~packing:vbox222#add ()
let message_zone =
GText.view ~editable:false ~cursor_visible:false
~packing:vbox222#add ()
~packing:(vbox222#pack ?from:None ~expand:true ~fill:true ?padding:None) ()
(********************************************)
......@@ -228,16 +228,19 @@ module C = Controller_itp.Make(S)
(* Mapping session to the GTK tree *)
(***********************************)
type index =
| Inone
| IproofAttempt of proofAttemptID
| IproofNode of proofNodeID
| Itransformation of transID
| Ifile of file
| Itheory of theory
| Iproofattempt of proof_attempt
let model_index : index Hint.t = Stdlib.Hint.create 17
(* To each proofnodeid we have the corresponding row_reference *)
let pn_id_to_gtree : GTree.row_reference Hpn.t = Hpn.create 17
let pan_id_to_gtree : GTree.row_reference Hpan.t = Hpan.create 17
let new_node =
let cpt = ref (-1) in
......@@ -248,13 +251,24 @@ let new_node =
let iter = goals_model#append ?parent () in
goals_model#set ~row:iter ~column:name_column name;
goals_model#set ~row:iter ~column:index_column !cpt;
goals_model#get_row_reference (goals_model#get_path iter)
let new_ref = goals_model#get_row_reference (goals_model#get_path iter) in
begin
match ind with
| IproofAttempt panid ->
Hpan.add pan_id_to_gtree panid new_ref
| IproofNode pnid ->
Hpn.add pn_id_to_gtree pnid new_ref
| _ -> ()
end;
new_ref
let build_subtree_proof_attempt_from_goal ses row_ref id =
List.iter
(fun pa ->
let _ = new_node ~parent:row_ref pa.prover.Whyconf.prover_name (Iproofattempt pa) in ())
(get_proof_attempts ses id)
Whyconf.Hprover.iter
(fun pa panid ->
let name = Pp.string_of Whyconf.print_prover pa in
ignore(new_node ~parent:row_ref name
(IproofAttempt panid)))
(get_proof_attempt_ids ses id)
let rec build_subtree_from_goal ses th_row_reference id =
let name = get_proof_name ses id in
......@@ -297,9 +311,6 @@ let build_tree_from_session ses =
(* actions *)
(******************)
(* To each proofnodeid we have the corresponding gtk_tree_iter *)
let pn_id_to_gtree = Hpn.create 17
(* TODO We currently use this for transformations etc... With strategies, we sure
do not want to move the current index with the computing of strategy. *)
let current_selected_index = ref Inone
......@@ -326,19 +337,18 @@ let run_strategy_on_task s =
(* TODO maybe an other file for callbacks *)
(* Callback of a transformation *)
let callback_update_tree_transform ses gtk_tree_iter = fun status ->
let callback_update_tree_transform ses row_reference = fun status ->
match status with
| TSdone trans_id ->
let row_reference = goals_model#get_row_reference (goals_model#get_path gtk_tree_iter) in
build_subtree_from_trans ses row_reference trans_id
| _ -> ()
let apply_transform ses =
match !current_selected_index with
| IproofNode id ->
let gtk_tree_index = Hpn.find pn_id_to_gtree id in (* TODO exception *)
let row_ref = Hpn.find pn_id_to_gtree id in (* TODO exception *)
let callback =
callback_update_tree_transform ses gtk_tree_index
callback_update_tree_transform ses row_ref
in
C.schedule_transformation cont id "cut" ["0=0"] ~callback
| _ -> printf "Error: Give the name of the transformation@."
......@@ -356,13 +366,26 @@ let remove_children iter =
*)
(* Callback of a proof_attempt *)
let callback_update_tree_proof ses gtk_tree_iter id = fun pa_status ->
let callback_update_tree_proof _ses row_ref _id name =
fun panid pa_status ->
match pa_status with
| Scheduled ->
begin
try
let _new_row_ref = Hpan.find pan_id_to_gtree panid in
() (* TODO: set icon to 'pause' *)
with Not_found ->
ignore(new_node ~parent:row_ref (name ^ " scheduled") (IproofAttempt panid))
end
| Done _pr ->
let row_reference = goals_model#get_row_reference (goals_model#get_path gtk_tree_iter) in
let _ = remove_children gtk_tree_iter in
build_subtree_proof_attempt_from_goal ses row_reference id
| _ -> () (* TODO *)
begin
try
let r = Hpan.find pan_id_to_gtree panid in
goals_model#set ~row:r#iter ~column:name_column (name ^ " done")
with Not_found -> assert false
end
| Running -> () (* TODO: set icon to 'play' *)
| _ -> () (* TODO ? *)
(* TODO to be replaced *)
(* Return the prover corresponding to given name. name is of the form
......@@ -383,10 +406,9 @@ let return_prover fmt name =
let test_schedule_proof_attempt ses =
match !current_selected_index with
| IproofNode id ->
let gtk_tree_index = Hpn.find pn_id_to_gtree id in
let callback = callback_update_tree_proof ses gtk_tree_index id in
let row_ref = Hpn.find pn_id_to_gtree id in
(* TODO put this somewhere else *)
let name, limit = match ["Alt-Ergo"; "1"] with
let name, limit = match ["Alt-Ergo,1.01"; "10"] with
(* TODO recover this
| [name] ->
let default_limit = Call_provers.{limit_time = Whyconf.timelimit main;
......@@ -406,6 +428,8 @@ let test_schedule_proof_attempt ses =
(match np with
| None -> ()
| Some p ->
let np = Pp.string_of Whyconf.print_prover p.Whyconf.prover in
let callback = callback_update_tree_proof ses row_ref id np in
C.schedule_proof_attempt
cont id p.Whyconf.prover
~limit ~callback)
......@@ -441,7 +465,7 @@ let on_selected_row r =
try
let session_element = Hint.find model_index index in
let () = match session_element with
| IproofNode id -> Hpn.add pn_id_to_gtree id r#iter (* TODO maybe not the good place to fill
| IproofNode id -> Hpn.add pn_id_to_gtree id r (* TODO maybe not the good place to fill
this table *)
| _ -> () in
current_selected_index := session_element;
......
......@@ -343,19 +343,21 @@ let run_timeout_handler () =
end
let schedule_proof_attempt_r c id pr ~limit ~callback =
graft_proof_attempt c.controller_session id pr ~timelimit:limit.Call_provers.limit_time;
Queue.add (c,id,pr,limit,callback) scheduled_proof_attempts;
callback Scheduled;
let panid =
graft_proof_attempt c.controller_session id pr ~timelimit:limit.Call_provers.limit_time
in
Queue.add (c,id,pr,limit,callback panid) scheduled_proof_attempts;
callback panid Scheduled;
run_timeout_handler ()
let schedule_proof_attempt c id pr ~limit ~callback =
let callback s = (match s with
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
| _ -> ());
callback s
callback panid s
in
schedule_proof_attempt_r c id pr ~limit:limit ~callback:callback
schedule_proof_attempt_r c id pr ~limit:limit ~callback
let schedule_transformation_r c id name args ~callback =
let apply_trans () =
......@@ -401,7 +403,7 @@ let run_strategy_on_goal c id strat ~callback =
else
match Array.get strat pc with
| Icall_prover(p,timelimit,memlimit) ->
let callback res =
let callback _panid res =
match res with
| Scheduled | Running -> (* nothing to do yet *) ()
| Done { Call_provers.pr_answer = Call_provers.Valid } ->
......
......@@ -150,7 +150,7 @@ val schedule_proof_attempt :
proofNodeID ->
Whyconf.prover ->
limit:Call_provers.resource_limit ->
callback:(proof_attempt_status -> unit) -> unit
callback:(proofAttemptID -> proof_attempt_status -> 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
......
......@@ -8,6 +8,7 @@ let debug = Debug.register_info_flag "session_itp"
type transID = int
type proofNodeID = int
type proofAttemptID = int
let print_proofNodeID fmt id =
Format.fprintf fmt "%d" id
......@@ -45,7 +46,7 @@ type proof_node = {
proofn_parent : proof_parent;
proofn_checksum : Termcode.checksum option;
proofn_shape : Termcode.shape;
proofn_attempts : proof_attempt_node Hprover.t;
proofn_attempts : proofAttemptID Hprover.t;
mutable proofn_transformations : transID list;
}
......@@ -81,8 +82,11 @@ end
module Hpn = Exthtbl.Make(Proofnodeid)
module Htn = Exthtbl.Make(Transid)
module Hpan = Hint
type session = {
proofAttempt_table : proof_attempt_node Hint.t;
mutable next_proofAttemptID : int;
proofNode_table : proof_node Hint.t;
mutable next_proofNodeID : int;
trans_table : transformation_node Hint.t;
......@@ -100,17 +104,12 @@ let init_Hpn (s : session) (h: 'a Hpn.t) (d: 'a) : unit =
let init_Htn (s : session) (h: 'a Htn.t) (d: 'a) : unit =
Hint.iter (fun k _pn -> Htn.replace h k d) s.trans_table
let session_iter_proofNode f s =
Hint.iter
(fun id pn -> if id < s.next_proofNodeID then f pn)
s.proofNode_table
let _session_iter_proofNode f s =
Hint.iter f s.proofNode_table
let session_iter_proof_attempt f =
session_iter_proofNode
(fun pn ->
Hprover.iter
(fun _ pan -> f pan.proofa_parent pan.proofa_attempt)
pn.proofn_attempts)
let session_iter_proof_attempt f s =
Hint.iter (fun _ pan -> f pan.proofa_parent pan.proofa_attempt)
s.proofAttempt_table
(* This is not needed. Keeping it as information on the structure
type tree = {
......@@ -176,8 +175,18 @@ let gen_proofNodeID (s : session) =
s.next_proofNodeID <- id + 1;
id
let gen_proofAttemptID (s : session) =
let id = s.next_proofAttemptID in
s.next_proofAttemptID <- id + 1;
id
exception BadID
let get_proofAttemptNode (s : session) (id : proofAttemptID) =
try
Hint.find s.proofAttempt_table id
with Not_found -> raise BadID
let get_proofNode (s : session) (id : proofNodeID) =
try
Hint.find s.proofNode_table id
......@@ -195,8 +204,14 @@ let get_transfNode (s : session) (id : transID) =
let get_transformations (s : session) (id : proofNodeID) =
(get_proofNode s id).proofn_transformations
let get_proof_attempt_ids (s : session) (id : proofNodeID) =
(get_proofNode s id).proofn_attempts
let get_proof_attempts (s : session) (id : proofNodeID) =
Hprover.fold (fun _ a l -> a.proofa_attempt :: l) (get_proofNode s id).proofn_attempts []
Hprover.fold (fun _ a l ->
let pa = get_proofAttemptNode s a in
pa.proofa_attempt :: l)
(get_proofNode s id).proofn_attempts []
let get_sub_tasks (s : session) (id : transID) =
(get_transfNode s id).transf_subtasks
......@@ -240,7 +255,10 @@ 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 -> f pan.proofa_attempt) pn.proofn_attempts) th
(fun pn -> Hprover.iter (fun _ pan ->
let pan = get_proofAttemptNode s pan in
f pan.proofa_attempt)
pn.proofn_attempts) th
open Format
open Ident
......@@ -262,7 +280,10 @@ let rec print_proof_node s (fmt: Format.formatter) p =
pn.proofn_name.id_string parent
(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 -> e.proofa_attempt :: l) pn.proofn_attempts [])
(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
and print_trans_node s fmt id =
......@@ -295,7 +316,9 @@ let empty_session ?shape_version dir =
| Some v -> v
| None -> Termcode.current_shape_version
in
{ proofNode_table = Hint.create 97;
{ proofAttempt_table = Hint.create 97;
next_proofAttemptID = 0;
proofNode_table = Hint.create 97;
next_proofNodeID = 0;
trans_table = Hint.create 97;
next_transID = 0;
......@@ -312,7 +335,17 @@ let empty_session ?shape_version dir =
let mk_proof_attempt session pid pa =
let pn = get_proofNode session pid in
let node = { proofa_parent = pid; proofa_attempt = pa } in
Hprover.replace pn.proofn_attempts pa.prover node
let id =
try Hprover.find pn.proofn_attempts pa.prover
with Not_found ->
let id = gen_proofAttemptID session in
Hprover.add pn.proofn_attempts pa.prover id;
id
in
Hint.replace session.proofAttempt_table id node;
id
let add_proof_attempt session prover limit state obsolete edit parentID =
let pa = { prover = prover;
......@@ -361,14 +394,14 @@ let mk_proof_node_no_task (s : session) (n : Ident.ident)
proofn_transformations = [] } in
Hint.add s.proofNode_table node_id pn
let mk_proof_node_task (s : session) (t : Task.task)
let _mk_proof_node_task (s : session) (t : Task.task)
(parent : proof_parent) (node_id : proofNodeID) =
let name,_,_ = Termcode.goal_expl_task ~root:false t in
mk_proof_node ~version:s.session_shape_version s name t parent node_id
let mk_transf_proof_node (s : session) (parent_name : string) (tid : transID) (index : int) (t : Task.task) =
let id = gen_proofNodeID s in
let gid,expl,_ = Termcode.goal_expl_task ~root:false t in
let gid,_expl,_ = Termcode.goal_expl_task ~root:false t in
(* let expl = match expl with
| None -> string_of_int index ^ "."
| Some e -> string_of_int index ^ ". " ^ e
......@@ -408,6 +441,7 @@ 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
......@@ -571,7 +605,7 @@ and load_proof_or_transf session old_provers pid a =
Call_provers.limit_mem = memlimit;
Call_provers.limit_steps = steplimit; }
in
add_proof_attempt session p limit res obsolete edit pid
ignore(add_proof_attempt session p limit res obsolete edit pid)
with Failure _ | Not_found ->
Warning.emit "[Error] prover id not listed in header '%s'@." prover;
raise (LoadError (a,"prover not listing in header"))
......@@ -847,15 +881,17 @@ 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
add_proof_attempt s old_pa.prover old_pa.limit
ignore (add_proof_attempt s old_pa.prover old_pa.limit
old_pa.proof_state true old_pa.proof_script
parent
parent)
in
let rec save_goal parent detached_goal_id id =
let detached_goal = get_proofNode old_s detached_goal_id in
mk_proof_node_no_task s detached_goal.proofn_name parent id None
(Termcode.shape_of_string "");
Hprover.iter (fun _ -> save_proof id) detached_goal.proofn_attempts;
Hprover.iter (fun _ pa ->
let pa = get_proofAttemptNode 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
new_trans.proofn_transformations <- List.rev new_trans.proofn_transformations
......@@ -888,9 +924,9 @@ let merge_proof new_s obsolete new_goal _ old_pa_n =
let old_pa = old_pa_n.proofa_attempt in
let obsolete = obsolete || old_pa.proof_obsolete in
found_obsolete := obsolete || !found_obsolete;
add_proof_attempt new_s old_pa.prover old_pa.limit
ignore (add_proof_attempt new_s old_pa.prover old_pa.limit
old_pa.proof_state obsolete old_pa.proof_script
new_goal
new_goal)
let add_registered_transformation s env old_tr goal_id =
let goal = get_proofNode s goal_id in
......@@ -907,7 +943,10 @@ let add_registered_transformation s env old_tr goal_id =
graft_transf s goal_id old_tr.transf_name old_tr.transf_args subgoals
let rec merge_goal ~use_shapes env new_s old_s obsolete old_goal new_goal_id =
Hprover.iter (merge_proof new_s obsolete new_goal_id) old_goal.proofn_attempts;
Hprover.iter (fun k pa ->
let pa = get_proofAttemptNode 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;
let new_trans = (get_proofNode new_s new_goal_id) in
new_trans.proofn_transformations <- List.rev new_trans.proofn_transformations
......@@ -1253,8 +1292,10 @@ let rec save_goal s ctxt fmt pnid =
Compress.Compress_z.output_string ctxt.ch_shapes shape;
Compress.Compress_z.output_char ctxt.ch_shapes '\n';
let l = Hprover.fold
(fun _ a acc -> (Mprover.find a.proofa_attempt.prover ctxt.provers,
a.proofa_attempt) :: acc)
(fun _ a acc ->
let a = get_proofAttemptNode s a in
(Mprover.find a.proofa_attempt.prover ctxt.provers,
a.proofa_attempt) :: acc)
pn.proofn_attempts [] in
let l = List.sort (fun ((i1,_,_,_),_) ((i2,_,_,_),_) -> compare i1 i2) l in
List.iter (save_proof_attempt fmt) l;
......
......@@ -19,11 +19,12 @@ type session
type proofNodeID
val print_proofNodeID : Format.formatter -> proofNodeID -> unit
type transID
type proofAttemptID
module Hpn: Exthtbl.S with type key = proofNodeID
module Htn: Exthtbl.S with type key = transID
module Hpan: Exthtbl.S with type key = proofAttemptID
val init_Hpn: session ->'a Hpn.t -> 'a -> unit
val init_Htn: session ->'a Htn.t -> 'a -> unit
......@@ -62,6 +63,8 @@ type proof_parent = Trans of transID | Theory of theory
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_attempts : session -> proofNodeID -> proof_attempt list
val get_sub_tasks : session -> transID -> proofNodeID list
val get_detached_sub_tasks : session -> transID -> proofNodeID list
......@@ -90,11 +93,12 @@ val add_file_section :
transformations to the goals of the new theory *)
val graft_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
timelimit:int -> unit
timelimit:int -> proofAttemptID
(** [graft_proof_attempt s id pr t] adds a proof attempt with prover
[pr] and timelimit [t] in the session [s] as a child of the task
[id]. If there already a proof attempt with the same prover,
it updates it with the new timelimit. *)
[id]. If there already a proof attempt with the same prover, it
updates it with the new timelimit. It returns the id of the
generated proof attempt. *)
val update_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
Call_provers.prover_result -> unit
......
......@@ -447,7 +447,7 @@ let then_print f fmt args =
let test_schedule_proof_attempt fmt (args: string list) =
(* temporary : get the first goal *)
let id = nearest_goal () in
let callback status =
let callback _panid status =
match status with
| Done _prover_result -> (display_session fmt []; test_print_goal fmt [];
fprintf fmt "status: %a@."
......
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