Commit d92c6303 authored by MARCHE Claude's avatar MARCHE Claude

why3session latex improved again (hopefully)

parent 158fab52
\begin{tabular}{| l |c |c |c |c |c |}
\hline Proof obligations & \provername{Alt-Ergo (0.94)} & \provername{Coq (8.3pl4)} & \provername{Simplify (1.5.4)} \\
\hline
\explanation{G1} & \noresult& \noresult& \valid{0.00} \\
\hline
\explanation{G2} & \unknown{0.00} & \noresult& \unknown{0.00} \\
\cline{2-4}
\quad\transformation{split\_goal} & \multicolumn{3}{|c|}{}\\
\cline{2-4}
\quad\subgoal{G2.1}{1} & \unknown{0.00} & \unknown{0.49} & \unknown{0.00} \\
\cline{2-4}
\quad\subgoal{G2.2}{2} & \valid{0.00} & \noresult& \valid{0.00} \\
\hline
\explanation{G3} & \valid{0.00} & \noresult& \unknown{0.00} \\
\hline \end{tabular}
\begin{tabular}{| l |c |c |c |c |c |}
\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo (0.94)} & \provername{Coq (8.3pl4)} & \provername{Simplify (1.5.4)} \\
\hline
\explanation{G1} & \explanation{ }& \noresult& \noresult& \valid{0.00} \\
\explanation{G1} & & \noresult& \noresult& \valid{0.00} \\
\hline
\explanation{G2} & \explanation{ }& \unknown{0.00} & \noresult& \unknown{0.00} \\
\explanation{G2} & & \unknown{0.00} & \noresult& \unknown{0.00} \\
\cline{2-4}
\explanation{ }& \explanation{ }\explanation{G2.1} & \unknown{0.00} & \unknown{0.49} & \unknown{0.00} \\
& \explanation{G2.1} & \unknown{0.00} & \unknown{0.49} & \unknown{0.00} \\
\cline{2-5}
\explanation{ }& \explanation{ }\explanation{G2.2} & \valid{0.00} & \noresult& \valid{0.00} \\
& \explanation{G2.2} & \valid{0.00} & \noresult& \valid{0.00} \\
\hline
\explanation{G3} & \explanation{ }& \valid{0.00} & \noresult& \unknown{0.00} \\
\explanation{G3} & & \valid{0.00} & \noresult& \unknown{0.00} \\
\hline \end{tabular}
......@@ -777,7 +777,7 @@ output.
\begin{figure}[t]
\begin{center}
\lstinputlisting{./replayer_macros.tex}
\lstinputlisting[basicstyle={\ttfamily\small}]{./replayer_macros.tex}
\end{center}
\caption{Sample macros for the LaTeX command}
\label{fig:custom-latex}
......@@ -792,13 +792,25 @@ output.
\end{toimage}
%HEVEA\imageflush
\end{center}
\caption{LaTeX table produced for the HelloProof example}
\caption{LaTeX table produced for the HelloProof example (style 1)}
\label{fig:latex}
\end{figure}
Figure~\ref{fig:custom-latex} suggests some definitions for these macros,
while Figure~\ref{fig:latex} shows the table obtained from the HelloProof
example of Section~\ref{chap:starting}.
\begin{figure}[t]
\begin{center}
\begin{toimage}
\input{HelloProof-style2.tex}
\end{toimage}
%HEVEA\imageflush
\end{center}
\caption{LaTeX table produced for the HelloProof example (style 2)}
\label{fig:latexstyle2}
\end{figure}
Figure~\ref{fig:custom-latex} suggests some definitions for these
macros, while Figures~\ref{fig:latex} and~\ref{fig:latexstyle2} show
the tables obtained from the HelloProof example of
Section~\ref{chap:starting}, respectively with style 1 and 2.
\subsection{Command \texttt{html}}
......
......@@ -91,7 +91,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, May 2012
Version \whyversion{}, October 2012
%BEGIN LATEX
\end{LARGE}
%END LATEX
......@@ -124,7 +124,7 @@ $^2$ Inria Saclay -- \^Ile-de-France, Toccata, Palaiseau, F-91120
\bigskip
\end{latexonly}
\textcopyright 2010-2012 Univ Paris-Sud, CNRS, INRIA
\textcopyright 2010-2012 Univ Paris-Sud, CNRS, Inria
\urldef{\urlutcat}{\url}{http://frama-c.cea.fr/u3cat}
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}
......
......@@ -4,8 +4,9 @@
\newcommand{\provername}[1]{\cellcolor{yellow!25}
\begin{sideways}\textbf{#1}~~\end{sideways}}
\newcommand{\explanation}[1]{\cellcolor{yellow!13}\textsl{#1}}
\newcommand{\explanation}[1]{\cellcolor{yellow!13}lemma \texttt{#1}}
\newcommand{\transformation}[1]{\cellcolor{yellow!13}transformation \texttt{#1}}
\newcommand{\subgoal}[2]{\cellcolor{yellow!13}subgoal #2}
\newcommand{\valid}[1]{\cellcolor{green!13}#1}
\newcommand{\unknown}[1]{\cellcolor{red!20}#1}
\newcommand{\invalid}[1]{\cellcolor{red!50}#1}
......
......@@ -174,31 +174,29 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
begin
if(depth < depth_max) then
for _i = 1 to depth do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
fprintf fmt " & "
done
else
for _i = 1 to depth - 1 do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
fprintf fmt " & "
done
end
else
if(depth < depth_max) then
if depth > 0 then
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
fprintf fmt " & "
end
else
begin
if subgoal > 0 then
for _i = 1 to depth do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done
for _i = 1 to depth do fprintf fmt " & " done
else
if depth > 0 then
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
if depth > 0 then fprintf fmt " & "
end;
if (depth <= 1) then
fprintf fmt "\\explanation{%s} " (protect (S.goal_expl g))
else
fprintf fmt "\\explanation{%s}" " ";
fprintf fmt " " ;
let proofs = g.S.goal_external_proofs in
if (S.PHprover.length proofs) > 0 then
begin
......@@ -206,18 +204,18 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
begin
if depth > 0 then
for _i = depth to (depth_max - depth) do
fprintf fmt "& \\explanation{%s}" " " done
fprintf fmt "& " done
else
for _i = depth to (depth_max - depth - 1) do
fprintf fmt "& \\explanation{%s}" " " done
fprintf fmt "& " done
end
else
if depth > 0 then
for _i = depth to (depth_max - depth - 1) do
fprintf fmt "& \\explanation{%s}" " " done
fprintf fmt "& " done
else
for _i = depth to (depth_max - depth - 2) do
fprintf fmt "& \\explanation{%s}" " " done;
fprintf fmt "& " done;
print_result_prov proofs prov fmt;
end;
let tr = g.S.goal_transformations in
......@@ -232,31 +230,39 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
() ) tr
let style_2_row fmt depth prov subgoal expl=
let style_2_row fmt ?(transf=false) depth prov subgoal expl=
let column = column 2 depth prov in
if depth > 0 then
if depth > 0 || transf then
fprintf fmt "\\cline{%d-%d} @." 2 column
else
fprintf fmt "\\hline @.";
for _i = 1 to depth do fprintf fmt "\\quad" done;
if (depth <= 1) then
fprintf fmt "\\explanation{%s} " expl
let macro = if transf then "transformation" else "explanation" in
if depth = 0 || transf then
fprintf fmt "\\%s{%s} " macro expl
else
fprintf fmt "\\explanation{%d} " (subgoal + 1)
fprintf fmt "\\subgoal{%s}{%d} " expl (subgoal + 1)
let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
style_2_row fmt depth prov subgoal (protect (S.goal_expl g));
let proofs = g.S.goal_external_proofs in
if (S.PHprover.length proofs) > 0 then
print_result_prov proofs prov fmt;
if S.PHprover.length proofs > 0 then
begin
style_2_row fmt depth prov subgoal (protect (S.goal_expl g));
print_result_prov proofs prov fmt
end
else
if depth = 0 then
begin
style_2_row fmt depth prov subgoal (protect (S.goal_expl g));
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
(List.length prov)
end;
let tr = g.S.goal_transformations in
if S.PHstr.length tr > 0 then
begin
if (S.PHprover.length proofs == 0) then
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
(List.length prov);
S.PHstr.iter (fun _st tr ->
style_2_row fmt depth prov subgoal (protect tr.S.transf_name);
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
......@@ -265,11 +271,10 @@ let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
subgoal + 1) 0 goals in
() ) tr
end
else
if (S.PHprover.length proofs) == 0 then
else
if (S.PHprover.length proofs) == 0 && depth <> 0 then
fprintf fmt "\\\\ @."
let latex_tabular_goal n fmt depth provers g =
print_tabular_head n depth provers fmt;
if n == 1 then
......
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