Skip to content

GitLab

Commit 53e0e5b2 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

resurected why3sesssion_latex

parent f05392e8
Hide whitespace changes
Inline Side-by-side
Showing with 207 additions and 143 deletions
Makefile.in
View file @ 53e0e5b2
......@@ -822,10 +822,10 @@ install_local:: bin/why3webserver
###############
SESSION_FILES = why3session_lib why3session_info \
why3session_html \
why3session_html why3session_latex \
why3session_main
# TODO: why3session_copy why3session_rm why3session_csv why3session_run
# why3session_latex why3session_output
# why3session_output
SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
......
src/session/session_itp.ml
View file @ 53e0e5b2
......@@ -360,18 +360,35 @@ let rec fold_all_sub_goals_of_proofn s f acc pnid =
in
f acc pn
let goal_iter_proof_attempt s f g =
fold_all_sub_goals_of_proofn
s
(fun _ pn -> Hprover.iter
(fun _ pan ->
let pan = get_proof_attempt_node s pan in
f pan)
pn.proofn_attempts) () g
let fold_all_sub_goals_of_theory s f acc th =
List.fold_left (fold_all_sub_goals_of_proofn s f) acc th.theory_goals
(*
let theory_iter_proofn s f th =
fold_all_sub_goals_of_theory s (fun _ -> f) () th
*)
let theory_iter_proof_attempt s f th =
theory_iter_proofn s
(fun pn -> Hprover.iter (fun _ pan ->
fold_all_sub_goals_of_theory s
(fun _ pn -> Hprover.iter (fun _ pan ->
let pan = get_proof_attempt_node s pan in
f pan)
pn.proofn_attempts) th
pn.proofn_attempts) () th
let file_iter_proof_attempt s f file =
List.iter
(theory_iter_proof_attempt s f)
(file_theories file)
......
src/session/session_itp.mli
View file @ 53e0e5b2
......@@ -70,9 +70,15 @@ type proof_attempt_node = private {
proof_script : string option; (* non empty for external ITP *)
}
val goal_iter_proof_attempt:
session -> (proof_attempt_node -> unit) -> proofNodeID -> unit
val theory_iter_proof_attempt:
session -> (proof_attempt_node -> unit) -> theory -> unit
val file_iter_proof_attempt:
session -> (proof_attempt_node -> unit) -> file -> unit
val session_iter_proof_attempt:
(proofAttemptID -> proof_attempt_node -> unit) -> session -> unit
......
src/why3session/why3session_html.ml
View file @ 53e0e5b2
......@@ -90,19 +90,6 @@ let run_file (context : context) print_session fname =
module Table =
struct
let rec transf_depth s tr =
List.fold_left
(fun depth g -> max depth (goal_depth s g)) 0 (get_sub_tasks s tr)
and goal_depth s g =
List.fold_left
(fun depth tr -> max depth (1 + transf_depth s tr))
1 (get_transformations s g)
let theory_depth s t =
List.fold_left
(fun depth g -> max depth (goal_depth s g)) 0 (theory_goals t)
let provers_stats s provers theory =
theory_iter_proof_attempt s (fun a ->
Hprover.replace provers a.prover a.prover) theory
......@@ -200,10 +187,9 @@ let rec num_lines s acc tr =
let print_theory s fn fmt th =
let depth = theory_depth s th in
if depth > 0 then
let provers = Hprover.create 9 in
provers_stats s provers th;
let provers = get_used_provers_theory s th in
let provers =
Hprover.fold (fun _ pr acc -> pr :: acc) provers []
Whyconf.Sprover.fold (fun pr acc -> pr :: acc) provers []
in
let provers = List.sort Whyconf.Prover.compare provers in
let name =
......
src/why3session/why3session_latex.ml
View file @ 53e0e5b2
......@@ -9,12 +9,12 @@
(* *)
(********************************************************************)
open Format
open Why3
open Session_itp
open Why3session_lib
open Format
module Hprover = Whyconf.Hprover
module S = Session_itp
let opt_style = ref 1
let opt_output_dir = ref ""
......@@ -46,22 +46,9 @@ let spec =
(* Statistics in LaTeX*)
let rec transf_depth tr =
List.fold_left (fun depth g -> max depth (goal_depth g)) 0 tr.S.transf_goals
and goal_depth g =
S.PHstr.fold
(fun _st tr depth -> max depth (1 + transf_depth tr))
(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
let file_depth f =
List.fold_left (fun depth t -> max depth (theory_depth t)) 0
f.S.file_theories
(*
let provers_latex_stats_goal provers goal =
S.goal_iter_proof_attempt (fun a ->
goal_iter_proof_attempt (fun a ->
Hprover.replace provers a.S.proof_prover a.S.proof_prover) goal
let provers_latex_stats provers theory =
......@@ -71,6 +58,7 @@ let provers_latex_stats provers theory =
let provers_latex_stats_file provers file =
S.file_iter_proof_attempt (fun a ->
Hprover.replace provers a.S.proof_prover a.S.proof_prover) file
*)
let protect s =
let b = Buffer.create 7 in
......@@ -117,13 +105,13 @@ let print_tabular_foot fmt =
fprintf fmt "\\hline \\end{tabular}@."
let print_result_prov proofs prov fmt=
let print_result_prov s proofs prov fmt=
List.iter (fun p ->
try
let pr = S.PHprover.find proofs p in
let s = pr.S.proof_state in
let pr = get_proof_attempt_node s (Hprover.find proofs p) in
let s = pr.proof_state in
match s with
| S.Done res ->
| Some res ->
begin
match res.Call_provers.pr_answer with
| Call_provers.Valid ->
......@@ -132,10 +120,10 @@ let print_result_prov proofs prov fmt=
fprintf fmt "& \\invalid{%.2f} " res.Call_provers.pr_time
| Call_provers.Timeout ->
fprintf fmt "& \\timeout{%ds} "
pr.S.proof_limit.Call_provers.limit_time
pr.limit.Call_provers.limit_time
| Call_provers.OutOfMemory ->
fprintf fmt "& \\outofmemory{%dM} "
pr.S.proof_limit.Call_provers.limit_mem
pr.limit.Call_provers.limit_mem
| Call_provers.StepLimitExceeded ->
fprintf fmt "& \\steplimitexceeded "
| Call_provers.Unknown _ ->
......@@ -146,16 +134,12 @@ let print_result_prov proofs prov fmt=
fprintf fmt "& \\highfailure "
end
| S.InternalFailure _ -> fprintf fmt "& Internal Failure"
| S.Interrupted -> fprintf fmt "& Not yet run"
| S.Unedited -> fprintf fmt "& Not yet edited"
| S.Scheduled | S.Running
| S.JustEdited -> assert false
| None -> fprintf fmt "(no result)"
with Not_found -> fprintf fmt "& \\noresult") prov;
fprintf fmt "\\\\ @."
let rec goal_latex_stat fmt prov depth depth_max subgoal g =
let rec goal_latex_stat s fmt prov depth depth_max subgoal g =
let column = column 1 depth prov
in
if depth > 0 then
......@@ -190,11 +174,12 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
if depth > 0 then fprintf fmt " & "
end;
if (depth <= 1) then
fprintf fmt "\\explanation{%s} " (protect (S.goal_user_name g))
fprintf fmt "\\explanation{%s} "
(protect (get_proof_name s g).Ident.id_string)
else
fprintf fmt " " ;
let proofs = S.goal_external_proofs g in
if (S.PHprover.length proofs) > 0 then
let proofs = get_proof_attempt_ids s g in
if (Hprover.length proofs) > 0 then
begin
if depth_max <= 1 then
begin
......@@ -212,16 +197,16 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
else
for _i = depth to (depth_max - depth - 2) do
fprintf fmt "& " done;
print_result_prov proofs prov fmt;
print_result_prov s proofs prov fmt;
end;
let tr = S.goal_transformations g in
if S.PHstr.length tr > 0 then
if S.PHprover.length proofs > 0 then
let tr = get_transformations s g in
if List.length tr > 0 then
if Hprover.length proofs > 0 then
fprintf fmt "\\cline{%d-%d}@." (depth + 2) column;
S.PHstr.iter (fun _st tr ->
let goals = tr.S.transf_goals in
List.iter (fun tr ->
let goals = get_sub_tasks s tr in
let _ = List.fold_left (fun subgoal g ->
goal_latex_stat fmt prov (depth + 1) depth_max (subgoal) g;
goal_latex_stat s fmt prov (depth + 1) depth_max (subgoal) g;
subgoal + 1) 0 goals in
() ) tr
......@@ -239,65 +224,71 @@ let style_2_row fmt ?(transf=false) depth prov subgoal expl=
else
fprintf fmt "\\subgoal{%s}{%d} " expl (subgoal + 1)
let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
let proofs = S.goal_external_proofs g in
if S.PHprover.length proofs > 0 then
let rec goal_latex2_stat s fmt prov depth depth_max subgoal g =
let proofs = get_proof_attempt_ids s g in
if Hprover.length proofs > 0 then
begin
style_2_row fmt depth prov subgoal (protect (S.goal_user_name g));
print_result_prov proofs prov fmt
style_2_row fmt depth prov subgoal
(protect (get_proof_name s g).Ident.id_string);
print_result_prov s proofs prov fmt
end
else
if (*depth = 0*) true then
begin
style_2_row fmt depth prov subgoal (protect (S.goal_user_name g));
style_2_row fmt depth prov subgoal
(protect (get_proof_name s g).Ident.id_string);
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
(List.length prov)
end;
let tr = S.goal_transformations g in
if S.PHstr.length tr > 0 then
let tr = get_transformations s g in
if List.length tr > 0 then
begin
S.PHstr.iter (fun _st tr ->
style_2_row fmt ~transf:true (depth+1) prov subgoal
(protect tr.S.transf_name);
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\@."
(List.length prov);
let goals = tr.S.transf_goals in
let _ = List.fold_left (fun subgoal g ->
goal_latex2_stat fmt prov (depth + 1) depth_max (subgoal) g;
subgoal + 1) 0 goals in
() ) tr
List.iter
(fun tr ->
let name = (get_transf_name s tr) ^
(String.concat "" (get_transf_args s tr)) in
style_2_row fmt ~transf:true (depth+1) prov subgoal
(protect name);
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\@."
(List.length prov);
let goals = get_sub_tasks s tr in
let _ = List.fold_left
(fun subgoal g ->
goal_latex2_stat s fmt prov (depth + 1) depth_max (subgoal) g;
subgoal + 1) 0 goals in
() ) tr
end
else
if (S.PHprover.length proofs) == 0 && depth <> 0 then
fprintf fmt "\\\\@."
if (Hprover.length proofs) == 0 && depth <> 0 then
fprintf fmt "\\\\@."
let latex_tabular_goal n fmt depth provers g =
let latex_tabular_goal n s fmt depth provers g =
print_tabular_head n depth provers fmt;
if n == 1 then
goal_latex_stat fmt provers 0 depth 0 g
goal_latex_stat s fmt provers 0 depth 0 g
else
goal_latex2_stat fmt provers 0 depth 0 g;
goal_latex2_stat s fmt provers 0 depth 0 g;
print_tabular_foot fmt
let latex_tabular_aux n fmt depth provers t =
let latex_tabular_aux n s fmt depth provers t =
if n == 1 then
List.iter (goal_latex_stat fmt provers 0 depth 0) t.S.theory_goals
List.iter (goal_latex_stat s fmt provers 0 depth 0) (theory_goals t)
else
List.iter (goal_latex2_stat fmt provers 0 depth 0) t.S.theory_goals
List.iter (goal_latex2_stat s fmt provers 0 depth 0) (theory_goals t)
let latex_tabular n fmt depth provers t =
let latex_tabular n s fmt depth provers t =
print_tabular_head n depth provers fmt;
latex_tabular_aux n fmt depth provers t;
latex_tabular_aux n s fmt depth provers t;
print_tabular_foot fmt
let latex_tabular_file n fmt depth provers f =
let latex_tabular_file n s fmt depth provers f =
print_tabular_head n depth provers fmt;
List.iter (latex_tabular_aux n fmt depth provers) f.S.file_theories;
List.iter (latex_tabular_aux n s fmt depth provers) (file_theories f);
print_tabular_foot fmt
let latex_longtable n fmt depth name provers t=
let latex_longtable n s fmt depth name provers t=
fprintf fmt "\\begin{longtable}";
fprintf fmt "{| l |";
for _i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
......@@ -317,45 +308,43 @@ let latex_longtable n fmt depth name provers t=
(* Last foot : nothing *)
fprintf fmt "\\endfoot \\endlastfoot @.";
if n == 1 then
List.iter (goal_latex_stat fmt provers 0 depth 0) t.S.theory_goals
List.iter (goal_latex_stat s fmt provers 0 depth 0) (theory_goals t)
else
List.iter (goal_latex2_stat fmt provers 0 depth 0) t.S.theory_goals;
List.iter (goal_latex2_stat s fmt provers 0 depth 0) (theory_goals t);
fprintf fmt "\\hline \\caption{%s statistics} @." (protect name);
fprintf fmt "\\label{%s} \\end{longtable}@." (protect name)
let theory_latex_stat n table dir t =
let provers = Hprover.create 9 in
provers_latex_stats provers t;
let provers = Hprover.fold (fun _ pr acc -> pr :: acc)
let theory_latex_stat n s table dir t =
let provers = get_used_provers_theory s t in
let provers = Whyconf.Sprover.fold (fun pr acc -> pr :: acc)
provers [] in
let provers = List.sort Whyconf.Prover.compare provers in
let depth = theory_depth t in
let name = t.S.theory_name.Ident.id_string in
let depth = theory_depth s t in
let name = (theory_name t).Ident.id_string in
let ch = open_out (Filename.concat dir(name^".tex")) in
let fmt = formatter_of_out_channel ch in
if table = "tabular" then
begin
latex_tabular n fmt depth provers t
latex_tabular n s fmt depth provers t
end
else
latex_longtable n fmt depth name provers t;
latex_longtable n s fmt depth name provers t;
close_out ch
let file_latex_stat n table dir f =
List.iter (theory_latex_stat n table dir) f.S.file_theories
let file_latex_stat n s table dir f =
List.iter (theory_latex_stat n s table dir) (file_theories f)
let standalone_goal_latex_stat n _table dir g =
let provers = Hprover.create 9 in
provers_latex_stats_goal provers g;
let provers = Hprover.fold (fun _ pr acc -> pr :: acc)
let standalone_goal_latex_stat n s _table dir g =
let provers = get_used_provers_goal s g in
let provers = Whyconf.Sprover.fold (fun pr acc -> pr :: acc)
provers [] in
let provers = List.sort Whyconf.Prover.compare provers in
let depth = goal_depth g in
let name = (S.goal_name g).Ident.id_string in
let ch = open_out (Filename.concat dir(name^".tex")) in
let depth = goal_depth s g in
let name = (get_proof_name s 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;
latex_tabular_goal n s fmt depth provers g;
(*
if table = "tabular" then
begin
......@@ -364,19 +353,18 @@ let standalone_goal_latex_stat n _table dir g =
else
latex_longtable_goal n fmt depth name provers g;
*)
close_out ch
close_out ch
let file_latex_stat_all n _table dir f =
let provers = Hprover.create 9 in
provers_latex_stats_file provers f;
let provers = Hprover.fold (fun _ pr acc -> pr :: acc)
let file_latex_stat_all n s _table dir f =
let provers = get_used_provers_file s f in
let provers = Whyconf.Sprover.fold (fun pr acc -> pr :: acc)
provers [] in
let provers = List.sort Whyconf.Prover.compare provers in
let depth = file_depth f in
let name = Filename.basename f.S.file_name in
let depth = file_depth s f in
let name = Filename.basename (file_name f) in
let ch = open_out (Filename.concat dir(name^".tex")) in
let fmt = formatter_of_out_channel ch in
latex_tabular_file n fmt depth provers f;
latex_tabular_file n s fmt depth provers f;
(*
if table = "tabular" then
begin
......@@ -390,82 +378,83 @@ let file_latex_stat_all n _table dir f =
let element_latex_stat_goal g n table dir r =
let element_latex_stat_goal g n s table dir r =
begin
match r with
| [] -> ()
| _ ->
eprintf "Warning: only main goals are supported@.:"
end;
standalone_goal_latex_stat n table dir g
standalone_goal_latex_stat n s table dir g
let element_latex_stat_theory th n table dir e =
let element_latex_stat_theory s th n table dir e =
match e with
| [] -> theory_latex_stat n table dir th
| [] -> theory_latex_stat n s table dir th
| g :: r ->
try
let goals =
List.map (fun g -> (S.goal_name g).Ident.id_string,g)
th.S.theory_goals
List.map (fun g ->
(get_proof_name s g).Ident.id_string,g)
(theory_goals th)
in
let g = List.assoc g goals in
element_latex_stat_goal g n table dir r
element_latex_stat_goal g n s table dir r
with Not_found ->
eprintf "Warning: goal not found in path: %s@." g
let element_latex_stat_file f n table dir e =
let element_latex_stat_file f n s table dir e =
match e with
| [] -> file_latex_stat_all n table dir f
| [] -> file_latex_stat_all n s table dir f
| th :: r ->
try
let ths =
List.map (fun th -> (th.S.theory_name.Ident.id_string,th))
f.S.file_theories
List.map (fun th -> (theory_name th).Ident.id_string,th)
(file_theories f)
in
let th = List.assoc th ths in
element_latex_stat_theory th n table dir r
element_latex_stat_theory s th n table dir r
with Not_found ->
eprintf "Warning: theory not found in path: %s@." th
let element_latex_stat files n table dir e =
let element_latex_stat files n s table dir e =
eprintf "Element %s@." e;
match Strings.split '.' e with
| [] -> ()
| f :: r ->
let found = ref false in
S.PHstr.iter
Stdlib.Hstr.iter
(fun fname file ->
let fname = Filename.basename fname in
let fname = List.hd (Strings.split '.' fname) in
if fname = f then
begin
found := true;
element_latex_stat_file file n table dir r
element_latex_stat_file file n s table dir r
end)
files;
if not !found then
eprintf "Warning: file not found for element %s@." e
let print_latex_statistics n table dir session =
let files = session.S.session_files in
let files = get_files session in
match !opt_elements with
| None ->
S.PHstr.iter (fun _ f -> file_latex_stat n table dir f) files
Stdlib.Hstr.iter (fun _ f -> file_latex_stat n session table dir f) files
| Some l ->
List.iter (element_latex_stat files n table dir) l
List.iter (element_latex_stat files n session table dir) l
let table () = if !opt_longtable then "longtable" else "tabular"
let run_one fname =
let project_dir = S.get_project_dir fname in
let session,_use_shapes = S.read_session project_dir in
let ses,_ = read_session fname in
let project_dir = get_dir ses in
let dir = if !opt_output_dir = "" then project_dir else
!opt_output_dir
in
print_latex_statistics !opt_style (table ()) dir session
print_latex_statistics !opt_style (table ()) dir ses
let run () =
let _,_,should_exit1 = read_env_spec () in
......
src/why3session/why3session_lib.ml
View file @ 53e0e5b2
......@@ -302,9 +302,47 @@ let ask_yn_nonblock ~callback =
end
let get_used_provers_goal session g =
let sprover = ref Whyconf.Sprover.empty in
Session_itp.goal_iter_proof_attempt session
(fun pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
g;
!sprover
let get_used_provers_theory session th =
let sprover = ref Whyconf.Sprover.empty in
Session_itp.theory_iter_proof_attempt session
(fun pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
th;
!sprover
let get_used_provers_file session f =
let sprover = ref Whyconf.Sprover.empty in
Session_itp.file_iter_proof_attempt session
(fun pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
f;
!sprover
let get_used_provers session =
let sprover = ref Whyconf.Sprover.empty in
Session_itp.session_iter_proof_attempt
(fun _ pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
session;
!sprover
let rec transf_depth s tr =
List.fold_left
(fun depth g -> max depth (goal_depth s g)) 0 (Session_itp.get_sub_tasks s tr)
and goal_depth s g =
List.fold_left
(fun depth tr -> max depth (1 + transf_depth s tr))
1 (Session_itp.get_transformations s g)
let theory_depth s t =
List.fold_left
(fun depth g -> max depth (goal_depth s g)) 0 (Session_itp.theory_goals t)
let file_depth s f =
List.fold_left (fun depth t -> max depth (theory_depth s t)) 0
(Session_itp.file_theories f)
src/why3session/why3session_lib.mli
View file @ 53e0e5b2
......@@ -91,6 +91,34 @@ val ask_yn_nonblock : callback:(bool -> unit) -> (unit -> bool)
(** call the callback when an answer have been given,
return true if it must be retried *)
(**)
val get_used_provers : Session_itp.session -> Whyconf.Sprover.t
(** [get_used_provers s] returns the set of provers used somewhere in
session [s] *)