Commit cb7c79cf authored by Asma Tafat's avatar Asma Tafat
Browse files

Longtable option

parent fece06cb
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd"> <!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session <why3session
name="programs/fact/why3session.xml"> name="examples/programs/fact/why3session.xml">
<prover <prover
id="alt-ergo" id="alt-ergo"
name="Alt-Ergo" name="Alt-Ergo"
...@@ -9,43 +9,19 @@ ...@@ -9,43 +9,19 @@
<prover <prover
id="coq" id="coq"
name="Coq" name="Coq"
version="8.3pl2"/> version="8.2pl2"/>
<prover <prover
id="cvc3" id="cvc3"
name="CVC3" name="CVC3"
version="2.2"/> version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4 Namring"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover <prover
id="simplify" id="simplify"
name="Simplify" name="Simplify"
version="1.5.4"/> version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover <prover
id="z3" id="z3"
name="Z3" name="Z3 smtv1"
version="2.19"/> version="2.2"/>
<file <file
name="../fact.mlw" name="../fact.mlw"
verified="true" verified="true"
......
...@@ -362,185 +362,240 @@ let protect s = ...@@ -362,185 +362,240 @@ let protect s =
done; done;
Buffer.contents b Buffer.contents b
let rec goal_latex_stat n fmt prov depth depth_max column subgoal g =
let column n depth provers =
if n == 1 then if n == 1 then
begin if depth > 1 then
if depth > 0 then (List.length provers) + depth
if subgoal > 0 then else
fprintf fmt "\\cline{%d-%d} @." (depth + 1) column (List.length provers) + depth + 1
else ()
else
fprintf fmt "\\hline @.";
end
else else
begin (List.length provers) + 1
if depth > 0 then
fprintf fmt "\\cline{%d-%d} @." 2 column
else let rec goal_latex_stat fmt prov depth depth_max subgoal g =
fprintf fmt "\\hline @." let column = column 1 depth prov
end; in
if(n ==1) then if depth > 0 then
begin if subgoal > 0 then
if depth_max > 1 then fprintf fmt "\\cline{%d-%d} @." (depth + 1) column
begin else ()
if subgoal > 0 then else
begin fprintf fmt "\\hline @.";
if(depth < depth_max) then if depth_max > 1 then
for i = 1 to depth do begin
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " if subgoal > 0 then
done begin
else if(depth < depth_max) then
for i = 1 to depth - 1 do for i = 1 to depth do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
done
end
else
if(depth < depth_max) then
if depth > 0 then
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
end done
else else
begin for i = 1 to depth - 1 do
if subgoal > 0 then fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
for i = 1 to depth do done
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done end
else else
if(depth < depth_max) then
if depth > 0 then if depth > 0 then
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
end end
end else
else begin
for i = 1 to depth do fprintf fmt "\\quad" done; if subgoal > 0 then
if (depth <= 1) then for i = 1 to depth do
fprintf fmt "\\explanation{%s} " (protect (M.goal_expl g)) fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done
else else
if n == 2 then if depth > 0 then
fprintf fmt "\\explanation{%d} " (subgoal + 1) fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
end;
if (depth <= 1) then
fprintf fmt "\\explanation{%s} " (protect (M.goal_expl g))
else else
fprintf fmt "\\explanation{%s}" " "; fprintf fmt "\\explanation{%s}" " ";
let proofs = M.external_proofs g in let proofs = M.external_proofs g in
if (Hashtbl.length proofs) > 0 then if (Hashtbl.length proofs) > 0 then
begin begin
if (n == 1) then if depth_max <= 1 then
begin begin
if depth_max <= 1 then if depth > 0 then
begin for i = depth to (depth_max - depth) do
if depth > 0 then fprintf fmt "& \\explanation{%s}" " " done
for i = depth to (depth_max - depth) do else
fprintf fmt "& \\explanation{%s}" " " done for i = depth to (depth_max - depth - 1) do
else fprintf fmt "& \\explanation{%s}" " " done
for i = depth to (depth_max - depth - 1) do end
fprintf fmt "& \\explanation{%s}" " " done else
end if depth > 0 then
for i = depth to (depth_max - depth - 1) do
fprintf fmt "& \\explanation{%s}" " " done
else else
if depth > 0 then for i = depth to (depth_max - depth - 2) do
for i = depth to (depth_max - depth - 1) do fprintf fmt "& \\explanation{%s}" " " done;
fprintf fmt "& \\explanation{%s}" " " done List.iter (fun (p, _pr) ->
else try
for i = depth to (depth_max - depth - 2) do let pr = Hashtbl.find proofs p in
fprintf fmt "& \\explanation{%s}" " " done let s = pr.M.proof_state in
match s with
Session.Done res ->
begin
match res.Call_provers.pr_answer with
Call_provers.Valid ->
fprintf fmt "& \\valid{%.2f} " res.Call_provers.pr_time
| Call_provers.Invalid -> fprintf fmt "& \\invalid "
| Call_provers.Timeout -> fprintf fmt "& \\timeout "
| Call_provers.Unknown _s -> fprintf fmt "& \\unknown "
| _ -> fprintf fmt "& \\failure "
end
| _ -> fprintf fmt "& Undone"
with Not_found -> fprintf fmt "& \\noresult") prov;
fprintf fmt "\\\\ @."
end; end;
List.iter (fun (p, _pr) -> let tr = M.transformations g in
try if Hashtbl.length tr > 0 then
let pr = Hashtbl.find proofs p in begin
let s = pr.M.proof_state in if Hashtbl.length proofs > 0 then
match s with fprintf fmt "\\cline{%d-%d} @." (depth + 2) column;
Session.Done res -> Hashtbl.iter (fun _st tr ->
begin let goals = tr.M.subgoals in
match res.Call_provers.pr_answer with let _ = List.fold_left (fun subgoal g ->
Call_provers.Valid -> goal_latex_stat fmt prov (depth + 1) depth_max (subgoal) g;
fprintf fmt "& \\valid{%.2f} " res.Call_provers.pr_time subgoal + 1) 0 goals in
| Call_provers.Invalid -> fprintf fmt "& \\invalid " () ) tr
| Call_provers.Timeout -> fprintf fmt "& \\timeout " end
| Call_provers.Unknown _s -> fprintf fmt "& \\unknown " else
| _ -> fprintf fmt "& \\failure " if (Hashtbl.length proofs) = 0 then
end fprintf fmt "\\\\ @."
| _ -> fprintf fmt "& Undone"
with Not_found -> fprintf fmt "& \\noresult") prov;
fprintf fmt "\\\\ @." let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
end; let column = column 2 depth prov
let tr = M.transformations g in in
if Hashtbl.length tr > 0 then if depth > 0 then
if n == 2 then fprintf fmt "\\cline{%d-%d} @." 2 column
begin else
if (Hashtbl.length proofs == 0) then fprintf fmt "\\hline @.";
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @." (List.length prov) for i = 1 to depth do fprintf fmt "\\quad" done;
end if (depth <= 1) then
fprintf fmt "\\explanation{%s} " (protect (M.goal_expl g))
else
fprintf fmt "\\explanation{%d} " (subgoal + 1);
let proofs = M.external_proofs g in
if (Hashtbl.length proofs) > 0 then
begin
List.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 ->
begin
match res.Call_provers.pr_answer with
Call_provers.Valid ->
fprintf fmt "& \\valid{%.2f} " res.Call_provers.pr_time
| Call_provers.Invalid -> fprintf fmt "& \\invalid "
| Call_provers.Timeout -> fprintf fmt "& \\timeout "
| Call_provers.Unknown _s -> fprintf fmt "& \\unknown "
| _ -> fprintf fmt "& \\failure "
end
| _ -> fprintf fmt "& Undone"
with Not_found -> fprintf fmt "& \\noresult") prov;
fprintf fmt "\\\\ @."
end;
let tr = M.transformations g in
if Hashtbl.length tr > 0 then
begin
if (Hashtbl.length proofs == 0) then
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @." (List.length prov);
Hashtbl.iter (fun _st tr ->
let goals = tr.M.subgoals 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
end
else
if (Hashtbl.length proofs) == 0 then
fprintf fmt "\\\\ @."
let print_head n depth provers fmt =
if n == 1 then
if (depth > 1) then
fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
depth
else
fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
(depth + 1)
else else
if Hashtbl.length proofs > 0 then fprintf fmt "\\hline Proof obligations ";
fprintf fmt "\\cline{%d-%d} @." (depth + 2) column; List.iter (fun (_, a) -> fprintf fmt "& \\provername{%s} " a) provers;
Hashtbl.iter (fun _st tr -> fprintf fmt "\\\\ @."
let goals = tr.M.subgoals in
let _ = List.fold_left (fun subgoal g ->
goal_latex_stat n fmt prov (depth + 1) depth_max column (subgoal) g;
subgoal + 1) 0 goals in
() ) tr
let theory_latex_stat n dir t = let latex_tabular n fmt depth provers t =
let provers = Hashtbl.create 9 in fprintf fmt "\\begin{tabular}";
List.iter (provers_latex_stats provers) (M.goals t); fprintf fmt "{| l |";
let provers = Hashtbl.fold (fun p pr acc -> (p, prover_name pr) :: acc) for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
provers [] in fprintf fmt "}@.";
let provers = print_head n depth provers fmt;
List.sort (fun (_p1, n1) (_p2, n2) -> String.compare n1 n2) provers in if n == 1 then
let depth = theory_depth t in List.iter (goal_latex_stat fmt provers 0 depth 0) (M.goals t)
let name = M.theory_name t in else
let ch = open_out (Filename.concat dir(name^".tex")) in List.iter (goal_latex2_stat fmt provers 0 depth 0) (M.goals t);
let fmt = formatter_of_out_channel ch in fprintf fmt "\\hline \\end{tabular}@."
fprintf fmt "\\begin{longtable}";
let latex_longtable n fmt depth name provers t=
fprintf fmt "\\begin{longtable}";
fprintf fmt "{| l |"; fprintf fmt "{| l |";
for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done; for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
fprintf fmt "}@."; fprintf fmt "}@.";
let print_head fmt =
if (n == 1) then
if (depth > 1) then
fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
depth
else
fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
(depth + 1)
else
fprintf fmt "\\hline Proof obligations ";
List.iter (fun (_, a) -> fprintf fmt "& \\provername{%s} " a) provers;
fprintf fmt "\\\\ @.";
in
(** First head *) (** First head *)
print_head fmt; print_head n depth provers fmt;
fprintf fmt "\\hline \\endfirsthead @."; fprintf fmt "\\hline \\endfirsthead @.";
(** Other heads : "Continued... " added *) (** Other heads : "Continued... " added *)
fprintf fmt "\\multicolumn{%d}{r}{\\textit{Continued from previous page}} \ fprintf fmt "\\multicolumn{%d}{r}{\\textit{Continued from previous page}} \
\\\\ @." (List.length provers + 1) ; \\\\ @." (List.length provers + 1) ;
fprintf fmt "\\hline @."; fprintf fmt "\\hline @.";
print_head fmt; print_head n depth provers fmt;
fprintf fmt "\\hline \\endhead @."; fprintf fmt "\\hline \\endhead @.";
(** Other foots : "Continued..." added *) (** Other foots : "Continued..." added *)
fprintf fmt "\\hline \\multicolumn{%d}{r}{\\textit{Continued on next page}} \ fprintf fmt "\\hline \\multicolumn{%d}{r}{\\textit{Continued on next page}} \
\\\\ @." (List.length provers); \\\\ @." (List.length provers);
(** Last foot : nothing *) (** Last foot : nothing *)
fprintf fmt "\\endfoot \\endlastfoot @."; fprintf fmt "\\endfoot \\endlastfoot @.";
if n == 1 then
List.iter (goal_latex_stat fmt provers 0 depth 0) (M.goals t)
else
List.iter (goal_latex2_stat fmt provers 0 depth 0) (M.goals t);
fprintf fmt "\\hline \\caption{%s statistics} @." (protect name);
fprintf fmt "\\label{%s} \\end{longtable}@." (protect name)
let column =
if n == 1 then let theory_latex_stat n table dir t =
if depth > 1 let provers = Hashtbl.create 9 in
then List.iter (provers_latex_stats provers) (M.goals t);
(List.length provers) + depth let provers = Hashtbl.fold (fun p pr acc -> (p, prover_name pr) :: acc)
else provers [] in
(List.length provers) + depth + 1 let provers =
List.sort (fun (_p1, n1) (_p2, n2) -> String.compare n1 n2) provers in
let depth = theory_depth t in
let name = M.theory_name t in
let ch = open_out (Filename.concat dir(name^".tex")) in
let fmt = formatter_of_out_channel ch in
if table = "tabular" then
latex_tabular n fmt depth provers t
else else
(List.length provers) + 1 latex_longtable n fmt depth name provers t;
in close_out ch
List.iter (goal_latex_stat n fmt provers 0 depth column 0) (M.goals t);
fprintf fmt "\\hline \\caption{%s statistics} @." (protect name);
fprintf fmt "\\label{%s} \\end{longtable}@." (protect name);
close_out ch
let file_latex_stat n dir f = let file_latex_stat n table dir f =
List.iter (theory_latex_stat n dir) f.M.theories List.iter (theory_latex_stat n table dir) f.M.theories
let print_latex_statistics n dir = let print_latex_statistics n table dir =
let files = M.get_all_files () in let files = M.get_all_files () in
List.iter (file_latex_stat n dir) files List.iter (file_latex_stat n table dir) files
let print_report (g,p,r) = let print_report (g,p,r) =
printf " goal '%s', prover '%s': " g p; printf " goal '%s', prover '%s': " g p;
...@@ -636,24 +691,24 @@ let () = ...@@ -636,24 +691,24 @@ let () =
M.maximum_running_proofs := M.maximum_running_proofs :=
Whyconf.running_provers_max (Whyconf.get_main config); Whyconf.running_provers_max (Whyconf.get_main config);
M.smoke_detector := !opt_smoke; M.smoke_detector := !opt_smoke;
eprintf " done@."; eprintf " done.";
if !opt_longtable && !opt_latex = " " && !opt_latex2 = " " then if !opt_longtable && !opt_latex == "" && !opt_latex2 == "" then
begin begin
eprintf eprintf
"[Error] I can't use option longtable without latex ou latex2"; "[Error] I can't use option longtable without latex ou latex2@.";
exit 1 exit 1
end; end;
if !opt_latex <> "" then if !opt_latex <> "" then
if !opt_longtable then if !opt_longtable then
print_latex_statistics 1 !opt_latex print_latex_statistics 1 "longtable" !opt_latex
else else
print_latex_statistics 1 !opt_latex print_latex_statistics 1 "tabular" !opt_latex
else else
if !opt_latex2 <> "" then if !opt_latex2 <> "" then
if !opt_longtable then if !opt_longtable then
print_latex_statistics 2 !opt_latex2 print_latex_statistics 2 "longtable" !opt_latex2
else else
print_latex_statistics 2 !opt_latex2 print_latex_statistics 2 "tabular "!opt_latex2
else else
begin begin
add_to_check found_obs; add_to_check found_obs;
......
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