Commit 211a72f2 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid

Latex statistics

parent 3b4b7504
......@@ -304,41 +304,66 @@ let print_statistics files =
let rec provers_latex_stats provers depth g =
let proofs = M.external_proofs g in
Hashtbl.iter (fun p _-> Hashtbl.replace provers p ()) proofs;
Hashtbl.iter (fun p a-> Hashtbl.replace provers p a.M.prover) proofs;
let tr = M.transformations g in
Hashtbl.iter (fun _st tr ->
depth := !depth + 1;
let goals = tr.M.subgoals in
List.iter (provers_latex_stats provers depth) goals) tr
let rec goal_latex_stat prov depth depth_max g =
for i = 1 to depth do printf "&" done;
printf "\\verb|%s| " (M.goal_name g);
if depth > 0 then
for i = depth to (depth_max - depth - 1) do printf "&" done
else
for i = depth to (depth_max - depth - 2) do printf "&" done;
let proofs = M.external_proofs g in
Hashtbl.iter (fun p _pr ->
try
let pr = Hashtbl.find proofs p in
let s = pr.M.proof_state in
match s with
Session.Done res ->
if res.Call_provers.pr_answer = Call_provers.Valid
then printf "& %.2f " res.Call_provers.pr_time
else printf "& --- "
| _ -> printf "& "
with Not_found -> printf "&") prov;
printf "\\\\ \\hline @.";
let tr = M.transformations g in
let rec goal_trans_stat rows g =
let tr = M.transformations g in
Hashtbl.iter (fun _st tr -> let goals = tr.M.subgoals in
List.iter (goal_latex_stat prov (depth + 1) depth_max) goals) tr
rows := !rows + (List.length goals);
List.iter (goal_trans_stat rows) goals) tr
let rec goal_latex_stat prov depth depth_max first g =
if not first then
for i = 1 to depth do printf "&" done
else
if depth > 0 then printf "&";
printf "\\verb|%s| " (M.goal_expl g);
let proofs = M.external_proofs g in
if (Hashtbl.length proofs) > 0 then
begin
if depth > 0 then
for i = depth to (depth_max - depth - 1) do printf "&" done
else
for i = depth to (depth_max - depth - 2) do printf "&" done;
Hashtbl.iter (fun p _pr ->
try
let pr = Hashtbl.find proofs p in
let s = pr.M.proof_state in
match s with
Session.Done res ->
if res.Call_provers.pr_answer = Call_provers.Valid
then printf "& %.2f " res.Call_provers.pr_time
else printf "& --- "
| _ -> printf "& "
with Not_found -> printf "&") prov;
printf "\\\\ \\hline @.";
end
else begin
let tr = M.transformations g in
Hashtbl.iter (fun _st tr ->
let goals = tr.M.subgoals in
let _ = List.fold_left (fun first g ->
goal_latex_stat prov (depth + 1) depth_max first g; false) true goals in
() ) tr
end
let prover_name a =
match a with
M.Detected_prover d -> d.Session.prover_name ^ " " ^ d.Session.prover_version
| M.Undetected_prover s -> s
let theory_latex_stat t =
let provers = Hashtbl.create 9 in
let depth = ref 0 in
List.iter (provers_latex_stats provers depth) (M.goals t);
printf "profondeur %d \n " !depth;
printf "\n@.";
printf "\\begin{tabular}";
printf "{| l |";
......@@ -347,10 +372,10 @@ let theory_latex_stat t =
else
for i = 0 to (Hashtbl.length provers) + !depth - 2 do printf "c |" done;
printf "} \n \\hline@.";
printf " \\multicolumn{%d}{|c|}{ WPs } " (!depth );
Hashtbl.iter (fun p _-> printf "& %s " p) provers;
printf " \\multicolumn{%d}{|c|}{ } " (!depth );
Hashtbl.iter (fun _ a-> printf "& %s " (prover_name a)) provers;
printf "\\\\\\hline@.";
List.iter (goal_latex_stat provers 0 !depth) (M.goals t);
List.iter (goal_latex_stat provers 0 !depth true) (M.goals t);
printf "\\end{tabular}@."
let file_latex_stat f =
......
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