Commit 672eabd4 authored by BECKER Benedikt's avatar BECKER Benedikt

Update manpages.tex for the pretty tool

parent 9eed7878
......@@ -1133,25 +1133,26 @@ same directory as output files. This CSS style can be modified manually,
since regenerating the HTML documentation will not overwrite an existing
\verb|style.css| file.
\section{The \texttt{latex} Command}
\section{The \texttt{pretty} Command}
This tool prints inductive rules defined in Why3 in LaTeX using the
\texttt{mathpartir} package\index{latex@\texttt{latex}}.
This tool pretty prints Why3 declarations. Currenty only the pretty
printing of inductive rules to \LaTeX{} is supported (using the
\texttt{mathpartir} package). \index{latex@\texttt{pretty}}
The typesetting of variables, record fields, and functions is
parameterized by LaTeX commands. Dummy definitions of these commands are
printed in comments and have to be defined by the user. Trailing digits
and quotes are removed from the command names to reduce the number of
commands. The commands have a common, configurable prefix (default: \texttt{IND}).
For the \LaTeX{} output, the typesetting of variables, record fields,
and functions is parameterized by commands. Dummy definitions of these
commands are printed in comments and have to be defined by the user.
Trailing digits and quotes are removed from the command names to reduce
the number of commands. The commands share a common, configurable prefix.
\paragraph{Reconstruction of record updates}
Due to the technical workings of the Why3 parser, record updates in the
source code \texttt{\{x with f=e; ...\}} are normally printed as record
constructions \texttt{\{f=e; g=x.g; ...\}}. However, such record
constructions in the LaTeX export tend to be quite verbose in comparison
constructions in the \LaTeX{} export tend to be quite verbose in comparison
to record updates.
The \texttt{why3 latex} allows for detecting and converting record
The \texttt{why3 pretty} allows for detecting and converting record
constructions back to record updates. It works as follows: Record shapes
(names of the record type and its fields) are specified as command line
arguments \texttt{-{}-record}. Record constructions are then tested,
......@@ -1161,13 +1162,26 @@ corresponding to the order given in the record shape. In this case, the
other field assignments \texttt{f=e} constitute the record update of the
form \texttt{\{x with f=e; ...\}}.
\subsection*{Usage}
\texttt{why3 pretty [options] [--kind=inductive] [--output=latex]\\
\indent [--prefix \textsl{<prefix>}] [--record \textsl{<name>}:\textsl{<field>},\ldots] \ldots{}\\
\indent \textsl{<module>}.\textsl{<Theory>}.\textsl{<ind\_type>} \ldots}
\paragraph{Options}
\begin{description}
\item[\texttt{-{}-prefix~\textsl{<prefix}}] Set the prefix for LaTeX
commands to \textsl{<prefix>}.
\item[\texttt{-{}-record~\textsl{<name>}:\textsl{<field>},\ldots}]
Convert constructions of record \textsl{<name>} to record updates.
\item[\texttt{-{}-kind~\textsl{<kind>}}] Set the syntactic kind to be
pretty printed. Currently, only the pretty printing of inductive types
is supported using \texttt{-{}-kind inductive}.
\item[\texttt{-{}-output~\textsl{<output>}}] Set the output format.
Currently, only the pretty printing to \LaTeX{} is supported using
\texttt{--output latex}.
\item[\texttt{-{}-prefix~\textsl{<prefix>}}] Set the prefix for \LaTeX{}
commands to \texttt{\textsl{<prefix>}}. The default is \texttt{IND}.
\item[\texttt{-{}-record~\textsl{<name>}:\textsl{<field>},\ldots}]
Reconstruct record updates for record type \texttt{\textsl{<name>}}
with field names \texttt{\textsl{<field>},\ldots}
\end{description}
\section{The \texttt{execute} Command}
......
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