...
  View open merge request
Commits (4)
......@@ -1528,6 +1528,51 @@ clean::
endif
###############
# Why3 pretty
###############
PRETTY_FILES = why3pretty
PRETTYMODULES = $(addprefix src/tools/, $(PRETTY_FILES))
PRETTYDEP = $(addsuffix .dep, $(PRETTYMODULES))
PRETTYCMO = $(addsuffix .cmo, $(PRETTYMODULES))
PRETTYCMX = $(addsuffix .cmx, $(PRETTYMODULES))
$(PRETTYDEP): DEPFLAGS += -I src/tools
$(PRETTYCMO) $(PRETTYCMX): INCLUDES += -I src/tools
# build targets
byte: bin/why3pretty.byte
opt: bin/why3pretty.opt
bin/why3pretty.opt: $(WHY3CMXA) $(PRETTYCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3pretty.byte: $(WHY3CMA) $(PRETTYCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(PRETTYDEP)
endif
depend: $(PRETTYDEP)
uninstall-bin::
rm -f $(TOOLDIR)/why3pretty$(EXE)
install-bin::
$(MKDIR_P) $(TOOLDIR)
$(INSTALL) bin/why3pretty.@OCAMLBEST@ $(TOOLDIR)/why3pretty$(EXE)
install_local:: bin/why3pretty
#########
# why3doc
#########
......@@ -2207,6 +2252,10 @@ src/tools/why3extract.cmx: %.cmx: %.ml
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) $<
# src/tools/why3pretty.cmx: %.cmx: %.ml
# $(SHOW) 'Ocamlopt $<'
# $(HIDE)$(OCAMLOPT) -c $(OFLAGS) $<
%.cmx: %.ml
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) $(CMIHACK) $<
......
......@@ -19,6 +19,7 @@ The following commands are available:
input files.
\item[\texttt{extract}] generates an OCaml program corresponding to
\whyml input files.
\item[\texttt{latex}] print an inductive type definition in LaTeX.
\item[\texttt{ide}] provides a graphical interface to display goals
and to run provers and transformations on them.
\item[\texttt{prove}] reads \whyml input files and calls
......@@ -1132,6 +1133,57 @@ 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{pretty} Command}
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}}
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
to record updates.
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,
whether a majority of the assigned expressions have the form
\texttt{x.g} for one variable \texttt{x} and a field \texttt{g}
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{-{}-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}
\label{sec:why3execute}
......
This diff is collapsed.