Commit de318423 authored by MARCHE Claude's avatar MARCHE Claude

protect access to fields of type Session.goal

parent ae071502
......@@ -534,7 +534,7 @@ let get_selected_row_references () =
let row_expanded b iter _path =
session_needs_saving := true;
let expand_g g = goals_view#expand_row g.S.goal_key#path in
let expand_g g = goals_view#expand_row (S.goal_key g)#path in
let expand_tr _ tr = goals_view#expand_row tr.S.transf_key#path in
let expand_m _ m = goals_view#expand_row m.S.metas_key#path in
match get_any_from_iter iter with
......@@ -545,8 +545,8 @@ let row_expanded b iter _path =
| S.Goal g ->
S.set_goal_expanded g b;
if b then begin
Session.PHstr.iter expand_tr g.S.goal_transformations;
Session.Mmetas_args.iter expand_m g.S.goal_metas
Session.PHstr.iter expand_tr (S.goal_transformations g);
Session.Mmetas_args.iter expand_m (S.goal_metas g)
end
| S.Transf tr ->
S.set_transf_expanded tr b;
......@@ -739,7 +739,7 @@ let notify any =
session_needs_saving := true;
let row,expanded =
match any with
| S.Goal g -> g.S.goal_key, g.S.goal_expanded
| S.Goal g -> (S.goal_key g), (S.goal_expanded g)
| S.Theory t -> t.S.theory_key, t.S.theory_expanded
| S.File f -> f.S.file_key, f.S.file_expanded
| S.Proof_attempt a -> a.S.proof_key,false
......@@ -770,7 +770,7 @@ let notify any =
goals_view#collapse_row row#path;
match any with
| S.Goal g ->
set_row_status row g.S.goal_verified
set_row_status row (S.goal_verified g)
| S.Theory th ->
set_row_status row th.S.theory_verified
| S.File file ->
......@@ -1409,8 +1409,8 @@ let (_ : GMenu.image_menu_item) =
~label:"Expand all" ~callback:(fun () -> goals_view#expand_all ()) ()
let rec collapse_verified = function
| S.Goal g when Opt.inhabited g.S.goal_verified ->
let row = g.S.goal_key in
| S.Goal g when Opt.inhabited (S.goal_verified g) ->
let row = S.goal_key g in
goals_view#collapse_row row#path
| S.Theory th when Opt.inhabited th.S.theory_verified ->
let row = th.S.theory_key in
......
......@@ -240,6 +240,14 @@ type 'a env_session =
mutable files : Theory.theory Stdlib.Mstr.t Stdlib.Mstr.t;
session : 'a session}
let goal_key g = g.goal_key
let goal_name g = g.goal_name
let goal_verified g = g.goal_verified
let goal_external_proofs g = g.goal_external_proofs
let goal_transformations g = g.goal_transformations
let goal_metas g = g.goal_metas
let goal_expanded g = g.goal_expanded
let update_env_session_config e c = e.whyconf <- c
(*************************)
......@@ -517,13 +525,13 @@ let goal_task_option g = g.goal_task
let goal_expl g =
match g.goal_expl with
| Some s -> s
| Some s -> assert (s <> ""); s
| None ->
let s =
try let _,_,l = restore_path g.goal_name in
String.concat "." l
with Not_found -> g.goal_name.Ident.id_string
in g.goal_expl <- Some s; s
in assert (s <> ""); g.goal_expl <- Some s; s
(************************)
(* saving state on disk *)
......@@ -880,7 +888,7 @@ let proof_verified a =
Call_provers.pr_time = t } -> Some t
| _ -> None
let goal_verified g =
let check_goal_verified g =
let acc = ref None in
let accumulate v =
match v with
......@@ -917,7 +925,7 @@ let check_theory_proved notify t =
end
let rec check_goal_proved notify g =
let b = goal_verified g in
let b = check_goal_verified g in
if g.goal_verified <> b then begin
g.goal_verified <- b;
notify (Goal g);
......@@ -1049,8 +1057,9 @@ let raw_add_task ~version ~(keygen:'a keygen) ~(expanded:bool) parent name expl
let sum = Some (Termcode.task_checksum ~version t) in
(* let shape = Termcode.t_shape_buf ~version (Task.task_goal_fmla t) in *)
let shape = Termcode.t_shape_task ~version ~expl t in
let expl = if expl = "" then None else Some expl in
let goal = { goal_name = name;
goal_expl = Some expl;
goal_expl = expl;
goal_parent = parent;
goal_task = Some t ;
goal_checksum = sum;
......
......@@ -69,7 +69,9 @@ type idpos = {
information the user want. It is generated by the keygen argument
of the functions of this module *)
type 'a goal = private
type 'a goal
(*
= private
{ mutable goal_key : 'a;
goal_name : Ident.ident; (** ident of the task *)
mutable goal_expl : string option;
......@@ -83,6 +85,7 @@ type 'a goal = private
goal_transformations : 'a transf PHstr.t;
mutable goal_metas : 'a metas Mmetas_args.t;
}
*)
and 'a proof_attempt = private
{ proof_key : 'a;
......@@ -158,6 +161,14 @@ and 'a session = private
session_dir : string;
}
val goal_key : 'a goal -> 'a
val goal_name : 'a goal -> Ident.ident
val goal_verified : 'a goal -> float option
val goal_external_proofs : 'a goal -> 'a proof_attempt PHprover.t
val goal_transformations : 'a goal -> 'a transf PHstr.t
val goal_metas : 'a goal -> 'a metas Mmetas_args.t
val goal_expanded : 'a goal -> bool
val print_session : Format.formatter -> 'a session -> unit
(** Print a session with a pstree format (cf Tree module) *)
......
......@@ -329,7 +329,7 @@ let find_prover eS a =
let g = a.proof_parent in
begin
try
let _ = PHprover.find g.goal_external_proofs new_p in
let _ = PHprover.find (goal_external_proofs g) new_p in
(* yes, then we do nothing *)
None
with Not_found ->
......@@ -349,7 +349,7 @@ let find_prover eS a =
let g = a.proof_parent in
begin
try
let _ = PHprover.find g.goal_external_proofs new_p in
let _ = PHprover.find (goal_external_proofs g) new_p in
(* yes, then we do nothing *)
None
with Not_found ->
......@@ -533,7 +533,7 @@ let run_external_proof eS eT ?(cntexample=false) ?callback a =
let prover_on_goal eS eT ?callback ?(cntexample=false) ~limit p g =
let a =
try
let a = PHprover.find g.goal_external_proofs p in
let a = PHprover.find (goal_external_proofs g) p in
set_timelimit (limit.Call_provers.limit_time) a;
set_memlimit (limit.Call_provers.limit_mem) a;
a
......@@ -609,7 +609,7 @@ type report =
| No_former_result of Call_provers.prover_result
let push_report report (g,p,limits,r) =
(g.goal_name,p,limits,r)::report
(goal_name g,p,limits,r)::report
let check_external_proof ~use_steps eS eT todo a =
let callback a ap limits old s =
......@@ -635,9 +635,9 @@ let check_external_proof ~use_steps eS eT todo a =
let rec goal_iter_proof_attempt_with_release ~release f g =
let iter g = goal_iter_proof_attempt_with_release ~release f g in
PHprover.iter (fun _ a -> f a) g.goal_external_proofs;
PHstr.iter (fun _ t -> List.iter iter t.transf_goals) g.goal_transformations;
Mmetas_args.iter (fun _ t -> iter t.metas_goal) g.goal_metas;
PHprover.iter (fun _ a -> f a) (goal_external_proofs g);
PHstr.iter (fun _ t -> List.iter iter t.transf_goals) (goal_transformations g);
Mmetas_args.iter (fun _ t -> iter t.metas_goal) (goal_metas g);
if release then release_task g
let check_all ?(release=false) ~use_steps ?filter eS eT ~callback =
......@@ -733,7 +733,7 @@ let rec play_on_goal_and_children eS eT ~limit todo l g =
| None, Done { Call_provers.pr_answer = Call_provers.Valid } ->
Call_provers.limit_max limit pa.proof_limit, true
| _ -> acc)
g.goal_external_proofs (limit, false) in
(goal_external_proofs g) (limit, false) in
let callback _key status =
if not (running status) then Todo._done todo () in
if auto_proved then begin
......@@ -832,7 +832,7 @@ let edit_proof_v3 ~cntexample eS sched ~default_editor callback a =
in
let file = update_edit_external_proof ~cntexample eS a in
Debug.dprintf debug "[Editing] goal %s with command '%s' on file %s@."
a.proof_parent.goal_name.Ident.id_string editor file;
(goal_name a.proof_parent).Ident.id_string editor file;
schedule_edition sched editor file (fun res -> callback a res)
let edit_proof ~cntexample eS sched ~default_editor a =
......@@ -893,7 +893,7 @@ let proof_removable a =
let rec clean = function
| Goal g when Opt.inhabited g.goal_verified ->
| Goal g when Opt.inhabited (goal_verified g) ->
iter_goal
(fun a -> if proof_removable a then remove_proof_attempt a)
(fun t ->
......
......@@ -40,7 +40,7 @@ let convert_unknown_prover ~keygen env_session =
let pks = Mprover.find_def [] pr.proof_prover unknown_provers in
List.iter (fun pk ->
(* If such a prover already exists we add nothing *)
if not (PHprover.mem pr.proof_parent.goal_external_proofs pk) then
if not (PHprover.mem (goal_external_proofs pr.proof_parent) pk) then
ignore (copy_external_proof ~keygen ~prover:pk pr)
) pks;
) env_session.session
......@@ -64,12 +64,12 @@ let transform_proof_attempt ?notify ~keygen env_session tr_name =
remove_external_proof ?notify pr;
let tr =
try
PHstr.find g.goal_transformations tr_name
PHstr.find (goal_transformations g) tr_name
with Not_found ->
add_registered_transformation ~keygen env_session tr_name g
in
let add_pa sg =
if not (PHprover.mem sg.goal_external_proofs pr.proof_prover) then
if not (PHprover.mem (goal_external_proofs sg) pr.proof_prover) then
ignore (copy_external_proof ~keygen ~goal:sg
~attempt_status:Interrupted pr)
in
......
......@@ -76,7 +76,7 @@ let goal_expl_task ~root task =
let info =
match info with
| Some i -> i
| None -> ""
| None -> gid.Ident.id_string
in
gid, info, task
......
......@@ -214,7 +214,7 @@ let project_dir =
with Not_found -> failwith "file does not exist"
let goal_statistics (goals,n,m) g =
if Opt.inhabited g.S.goal_verified then (goals,n+1,m+1) else (g::goals,n,m+1)
if Opt.inhabited (S.goal_verified g) then (goals,n+1,m+1) else (g::goals,n,m+1)
let theory_statistics (ths,n,m) th =
let goals,n1,m1 =
......@@ -228,7 +228,7 @@ let file_statistics _ f (files,n,m) =
let print_statistics files =
let print_goal g =
printf " +--goal %s not proved@." g.S.goal_name.Ident.id_string
printf " +--goal %s not proved@." (S.goal_name g).Ident.id_string
in
let print_theory (th,goals,n,m) =
if n<m then begin
......
......@@ -132,15 +132,15 @@ let run_one ~action env config filters pk fname =
| Some prover ->
(* If such a prover already exists on the goal *)
let exists =
(PHprover.mem pr.proof_parent.goal_external_proofs prover) in
(PHprover.mem (goal_external_proofs pr.proof_parent) prover) in
let replace = not exists || match !opt_replace with
| Always -> true | Never -> false
| Interactive ->
interactive
(PHprover.find pr.proof_parent.goal_external_proofs prover)
(PHprover.find (goal_external_proofs pr.proof_parent) prover)
| Not_valid ->
let rm =
PHprover.find pr.proof_parent.goal_external_proofs prover
PHprover.find (goal_external_proofs pr.proof_parent) prover
in
not (Opt.inhabited (proof_verified rm))
in
......
......@@ -104,10 +104,10 @@ let print_cell fmt pa =
let rec print_line fmt provers a =
begin match a with
| Session.Goal a ->
fprintf fmt "\"%s\"" a.Session.goal_name.Ident.id_string;
fprintf fmt "\"%s\"" (Session.goal_name a).Ident.id_string;
Whyconf.Sprover.iter (fun p ->
try
let pa = Session.PHprover.find a.Session.goal_external_proofs p in
let pa = Session.PHprover.find (Session.goal_external_proofs a) p in
fprintf fmt ",%a" print_cell pa
with Not_found ->
fprintf fmt ",") provers;
......
......@@ -97,7 +97,7 @@ struct
and goal_depth g =
S.PHstr.fold
(fun _st tr depth -> max depth (1 + transf_depth tr))
g.S.goal_transformations 1
(S.goal_transformations g) 1
let theory_depth t =
List.fold_left
......@@ -161,7 +161,7 @@ let rec num_lines acc tr =
List.fold_left
(fun acc g -> 1 +
PHstr.fold (fun _ tr acc -> 1 + num_lines acc tr)
g.goal_transformations acc)
(goal_transformations g) acc)
acc tr.transf_goals
let rec print_transf fmt depth max_depth provers tr =
......@@ -188,16 +188,16 @@ let rec num_lines acc tr =
if not is_first then fprintf fmt "<tr>";
(* for i=1 to 0 (\* depth-1 *\) do fprintf fmt "<td></td>" done; *)
fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) (Opt.inhabited g.S.goal_verified)
(color_of_status ~dark:false) (Opt.inhabited (S.goal_verified g))
(max_depth - depth + 1);
(* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
fprintf fmt "%s</td>" (S.goal_expl g);
(* for i=depth to max_depth-1 do fprintf fmt "<td></td>" done; *)
print_results fmt provers g.goal_external_proofs;
print_results fmt provers (goal_external_proofs g);
fprintf fmt "</tr>@\n";
PHstr.iter
(fun _ tr -> print_transf fmt depth max_depth provers tr)
g.goal_transformations
(goal_transformations g)
let print_theory fn fmt th =
let depth = theory_depth th in
......@@ -290,13 +290,13 @@ struct
and print_goal fmt g =
fprintf fmt "<li>%s : <ul>%a%a</ul></li>"
g.goal_name.Ident.id_string
(goal_name g).Ident.id_string
(Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
Pp.nothing print_proof_attempt)
g.goal_external_proofs
(goal_external_proofs g)
(Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing
Pp.nothing print_transf)
g.goal_transformations
(goal_transformations g)
let print_theory fmt th =
fprintf fmt "<li>%s : <ul>%a</ul></li>"
......
......@@ -159,13 +159,13 @@ let rec stats_of_goal ~root prefix_name stats goal =
acc
end
| _ -> acc)
goal.goal_external_proofs
(goal_external_proofs goal)
[]
in
List.iter (update_perf_stats stats) proof_list;
PHstr.iter (stats_of_transf prefix_name stats) goal.goal_transformations;
if not (Opt.inhabited goal.goal_verified) then
let goal_name = prefix_name ^ goal.goal_name.Ident.id_string in
PHstr.iter (stats_of_transf prefix_name stats) (goal_transformations goal);
if not (Opt.inhabited (goal_verified goal)) then
let goal_name = prefix_name ^ (goal_name goal).Ident.id_string in
stats.no_proof <- Sstr.add goal_name stats.no_proof
else
begin
......@@ -175,7 +175,7 @@ let rec stats_of_goal ~root prefix_name stats goal =
stats.nb_proved_sub_goals <- stats.nb_proved_sub_goals + 1;
match proof_list with
| [ (prover, _) ] ->
let goal_name = prefix_name ^ goal.goal_name.Ident.id_string in
let goal_name = prefix_name ^ (goal_name goal).Ident.id_string in
stats.only_one_proof <-
Sstr.add
(goal_name ^ " : " ^ (string_of_prover prover))
......@@ -217,7 +217,7 @@ let rec stats2_of_goal ~nb_proofs g : 'a goal_stat =
acc
end
| _ -> acc)
g.goal_external_proofs
(goal_external_proofs g)
[]
in
let l =
......@@ -226,11 +226,11 @@ let rec stats2_of_goal ~nb_proofs g : 'a goal_stat =
match stats2_of_transf ~nb_proofs tr with
| [] -> acc
| r -> (tr,List.rev r)::acc)
g.goal_transformations
(goal_transformations g)
[]
in
if match nb_proofs with
| 0 -> not (Opt.inhabited g.goal_verified)
| 0 -> not (Opt.inhabited (goal_verified g))
| 1 -> List.length proof_list = 1
| _ -> assert false
then Yes(proof_list,l) else No(l)
......@@ -249,7 +249,7 @@ let print_res ~time fmt (p,t) =
let rec print_goal_stats ~time depth (g,l) =
for _i=1 to depth do printf " " done;
printf "+-- goal %s" g.goal_name.Ident.id_string;
printf "+-- goal %s" (goal_name g).Ident.id_string;
match l with
| No l ->
printf "@\n";
......
......@@ -51,7 +51,7 @@ let rec transf_depth tr =
and goal_depth g =
S.PHstr.fold
(fun _st tr depth -> max depth (1 + transf_depth tr))
g.S.goal_transformations 0
(S.goal_transformations g) 0
let theory_depth t =
List.fold_left (fun depth g -> max depth (goal_depth g)) 0 t.S.theory_goals
......@@ -193,7 +193,7 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
fprintf fmt "\\explanation{%s} " (protect (S.goal_expl g))
else
fprintf fmt " " ;
let proofs = g.S.goal_external_proofs in
let proofs = S.goal_external_proofs g in
if (S.PHprover.length proofs) > 0 then
begin
if depth_max <= 1 then
......@@ -214,7 +214,7 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
fprintf fmt "& " done;
print_result_prov proofs prov fmt;
end;
let tr = g.S.goal_transformations in
let tr = S.goal_transformations g in
if S.PHstr.length tr > 0 then
if S.PHprover.length proofs > 0 then
fprintf fmt "\\cline{%d-%d}@." (depth + 2) column;
......@@ -240,7 +240,7 @@ let style_2_row fmt ?(transf=false) depth prov subgoal expl=
fprintf fmt "\\subgoal{%s}{%d} " expl (subgoal + 1)
let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
let proofs = g.S.goal_external_proofs in
let proofs = S.goal_external_proofs g in
if S.PHprover.length proofs > 0 then
begin
style_2_row fmt depth prov subgoal (protect (S.goal_expl g));
......@@ -253,7 +253,7 @@ let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
(List.length prov)
end;
let tr = g.S.goal_transformations in
let tr = S.goal_transformations g in
if S.PHstr.length tr > 0 then
begin
S.PHstr.iter (fun _st tr ->
......@@ -352,7 +352,7 @@ let standalone_goal_latex_stat n _table dir g =
provers [] in
let provers = List.sort Whyconf.Prover.compare provers in
let depth = goal_depth g in
let name = g.S.goal_name.Ident.id_string in
let name = (S.goal_name g).Ident.id_string in
let ch = open_out (Filename.concat dir(name^".tex")) in
let fmt = formatter_of_out_channel ch in
latex_tabular_goal n fmt depth provers g;
......@@ -405,7 +405,7 @@ let element_latex_stat_theory th n table dir e =
| g :: r ->
try
let goals =
List.map (fun g -> (g.S.goal_name.Ident.id_string,g))
List.map (fun g -> (S.goal_name g).Ident.id_string,g)
th.S.theory_goals
in
let g = List.assoc g goals in
......
......@@ -213,7 +213,7 @@ let iter_proof_attempt_by_filter iter filters f session =
let f = three_value f filters.archived (fun a -> a.S.proof_archived) in
(* verified_goal *)
let f = three_value f filters.verified_goal
(fun a -> Opt.inhabited a.S.proof_parent.S.goal_verified) in
(fun a -> Opt.inhabited (S.goal_verified a.S.proof_parent)) in
(* verified *)
let f = three_value f filters.verified
(fun p -> Opt.inhabited (S.proof_verified p)) in
......
......@@ -153,7 +153,7 @@ let print_res fname pa ps old_ps =
print_attempt_status old_ps
let print_proof_goal fmt pa =
pp_print_string fmt pa.proof_parent.goal_name.Ident.id_string
pp_print_string fmt (goal_name pa.proof_parent).Ident.id_string
let same_result r1 r2 =
......@@ -186,7 +186,7 @@ let is_successful env = (* means all goals proved*)
let rec iter = function
| File f -> file_iter iter f
| Theory th -> theory_iter iter th
| Goal g -> if not (Opt.inhabited (g.goal_verified)) then raise Exit
| Goal g -> if not (Opt.inhabited (goal_verified g)) then raise Exit
| Proof_attempt _ | Transf _ | Metas _ -> assert false in
session_iter iter env.session;
true
......
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