Commit 25350a6b authored by Benedikt Becker's avatar Benedikt Becker

Rename why3pretty to why3pp

parent 75e1a21b
......@@ -1520,49 +1520,49 @@ clean::
endif
###############
# Why3 pretty
# Why3 pp
###############
PRETTY_FILES = why3pretty
PRETTYPRINT_FILES = why3pp
PRETTYMODULES = $(addprefix src/tools/, $(PRETTY_FILES))
PRETTYPRINTMODULES = $(addprefix src/tools/, $(PRETTYPRINT_FILES))
PRETTYDEP = $(addsuffix .dep, $(PRETTYMODULES))
PRETTYCMO = $(addsuffix .cmo, $(PRETTYMODULES))
PRETTYCMX = $(addsuffix .cmx, $(PRETTYMODULES))
PRETTYPRINTDEP = $(addsuffix .dep, $(PRETTYPRINTMODULES))
PRETTYPRINTCMO = $(addsuffix .cmo, $(PRETTYPRINTMODULES))
PRETTYPRINTCMX = $(addsuffix .cmx, $(PRETTYPRINTMODULES))
$(PRETTYDEP): DEPFLAGS += -I src/tools
$(PRETTYCMO) $(PRETTYCMX): INCLUDES += -I src/tools
$(PRETTYPRINTDEP): DEPFLAGS += -I src/tools
$(PRETTYPRINTCMO) $(PRETTYPRINTCMX): INCLUDES += -I src/tools
# build targets
byte: bin/why3pretty.byte
opt: bin/why3pretty.opt
byte: bin/why3pp.byte
opt: bin/why3pp.opt
bin/why3pretty.opt: $(WHY3CMXA) $(PRETTYCMX)
bin/why3pp.opt: $(WHY3CMXA) $(PRETTYPRINTCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3pretty.byte: $(WHY3CMA) $(PRETTYCMO)
bin/why3pp.byte: $(WHY3CMA) $(PRETTYPRINTCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(PRETTYDEP)
-include $(PRETTYPRINTDEP)
endif
depend: $(PRETTYDEP)
depend: $(PRETTYPRINTDEP)
uninstall-bin::
rm -f $(TOOLDIR)/why3pretty$(EXE)
rm -f $(TOOLDIR)/why3pp(EXE)
install-bin::
$(MKDIR_P) $(TOOLDIR)
$(INSTALL) bin/why3pretty.@OCAMLBEST@ $(TOOLDIR)/why3pretty$(EXE)
$(INSTALL) bin/why3pp.@OCAMLBEST@ $(TOOLDIR)/why3pp$(EXE)
install_local:: bin/why3pretty
install_local:: bin/why3pp
#########
# why3doc
......
......@@ -19,7 +19,8 @@ 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{pp}] pretty print \whyml definitions (formatting mlw files
or printing inductive definitions to \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
......@@ -1134,57 +1135,42 @@ 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}
\section{The \texttt{pp} 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; ...\}}.
This tool pretty prints Why3 declarations. Currenty it can be used to
print \whyml inductive definitions to \LaTeX{} (using the
\texttt{mathpartir} package), and to format \whyml source code.
\index{latex@\texttt{pretty}}
\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}
\texttt{why3 pp [-{}-output=latex|mlw] [-{}-kind=inductive] [-{}-prefix \textsl{<prefix>}]\\%
\indent \textsl{<filename>} \textsl{<file>}[.\textsl{<Module>}].\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.
\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{}
\texttt{-{}-output=latex}, and formatting of \whyml source code using
\texttt{-{}-output=mlw}.
\item[\texttt{-{}-kind=\textsl{<kind>}}] Set the syntactic kind to be
pretty printed. Currently, the only supported kind are inductive types
(\texttt{-{}-kind=inductive}) when using the \LaTeX-output
(\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}
\item[\texttt{\textsl{<file>}[.\textsl{<Module>}].\textsl{<ind\_type>}}] One or
more inductive definitions for \texttt{-{}-output=latex} and
\texttt{-{}-kind=inductive}.
\end{description}
For the \LaTeX{} output, the typesetting of variables, record fields,
and functions can be configured 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.
\section{The \texttt{execute} Command}
\label{sec:why3execute}
......
......@@ -15,8 +15,8 @@ module Mlw_printer = struct
(* TODO parenthesis and associativity *)
(* Test with
$ why3 pretty --output=mlw test.mlw > test1.mlw
$ why3 pretty --output=mlw test1.mlw > test2.mlw
$ why3 pp --output=mlw test.mlw > test1.mlw
$ why3 pp --output=mlw test1.mlw > test2.mlw
$ diff test1.mlw test2.mlw *)
open Format
......@@ -607,8 +607,6 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com
open Conf
(** {2 Pretty print simplified AST}*)
let sanitize =
let my_char_to_alpha = function
(* | '_' | '.' -> "" *)
......@@ -997,7 +995,7 @@ let prefix = ref "IND"
let usage =
"Pretty print Why3 declarations (currently only inductive types in LaTeX using mathpartir).\n\
why3 pretty [--output=latex|mlw|ast] [--kind=inductive] [--prefix <prefix>] <filename> [<Module>.]<type> ..."
why3 pp [--output=latex|mlw|ast] [--kind=inductive] [--prefix <prefix>] <filename> [<Module>.]<type> ..."
let options = [
"--output", Arg.String set_output, "<output> Output format";
......
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