documentation for --exec and --extract

CHANGES

@@ -4,8 +4,8 @@
  * [why3replayer] renamed option -obsolete-only to --obsolete-only,
    -smoke-detector to --smoke-detector, -force to --force
  * [library] fixed inconsistency in libraries map.MapPermut and
-   array.ArrayPermut; names and meaning of symbols "permut..." have
-   been modified
+   array.ArrayPermut; names, definitions, and meaning of symbols
+   "permut..." have been modified
 
 version 0.82, December 12, 2013
 ===============================

Makefile.in

@@ -1526,7 +1526,7 @@ doc/bnf: doc/bnf.mll
 	$(OCAMLLEX) $<
 	$(OCAMLOPT) -o $@ doc/bnf.ml
 
-DOC = api glossary ide intro library macros manpages install \
+DOC = api glossary ide intro exec macros manpages install \
       manual starting syntax syntaxref technical version whyml \
       itp pvs coq coq_tactic isabelle
 

doc/api.tex

@@ -289,7 +289,7 @@ constructed.
 Here is the way we build the formula $2+2=4$. The main difficulty is to
 access the internal identifier for addition: it must be retrieved from
 the standard theory \texttt{Int} of the file \texttt{int.why} (see
-Chap~\ref{chap:library}).
+Chap~\ref{sec:library}).
 \begin{ocamlcode}
 let two : Term.term = 
   Term.t_const (Number.ConstInt (Number.int_const_dec "2"))

doc/exec.tex

+
+\chapter{Executing \whyml Programs}
+\label{chap:exec}\index{whyml@\whyml}
+
+This chapter show how \whyml code can be executed, either by being
+interpreted or compiled to some existing programming language.
+
+Let us consider the program in Fig.~\ref{fig:MaxAndSum}
+on page~\pageref{fig:MaxAndSum} that computes the maximum and the sum
+of an array of integers.
+Let us assume it is contained in a file \texttt{maxsum.mlw}.
+
+\section{Interpreting \whyml Code}
+\index{exec@\verb+--exec+}\index{interpretation!of \whyml}
+\index{testing \whyml code}
+
+To test function \texttt{max\_sum}, we can introduce a \whyml test function
+in module \texttt{MaxAndSum}
+\begin{whycode}
+  let test () =
+    let n = 10 in
+    let a = make n 0 in
+    a[0] <- 9; a[1] <- 5; a[2] <- 0; a[3] <- 2;  a[4] <- 7;
+    a[5] <- 3; a[6] <- 2; a[7] <- 1; a[8] <- 10; a[9] <- 6;
+    max_sum a n
+\end{whycode}
+and then we use option \verb+--exec+ to interpret this function,
+as follows:
+\begin{verbatim}
+  > why3  maxsum.mlw --exec MaxAndSum.test
+  Execution of MaxAndSum.test ():
+       type: (int, int)
+     result: Tuple2(45, 10)
+    globals:
+\end{verbatim}
+We get the excepted output, namely the pair \texttt{(45, 10)}.
+
+\section{Compiling \whyml to OCaml}
+\index{OCaml}\index{extraction}
+\index{E@\verb+-E+|see{\texttt{-{}-extract}}}
+\index{extract@\verb+--extract+}
+
+An alternative to interpretation is to compile \whyml to OCaml.
+We do so using option \verb+--extract+, as follows:
+\begin{verbatim}
+  > mkdir dir
+  > why3 --extract ocaml64 maxsum.mlw -o dir
+\end{verbatim}
+Option \verb+--extract+ requires the name of a driver, which indicates
+how theories/modules from the \why standard library are translated to
+OCaml. Here we assume a 64-bit architecture and thus we pass
+\texttt{ocaml64}. On a 32-bit architecture, we would use
+\texttt{ocaml32} instead. Extraction also requires a target directory
+to be specified using option \verb+-o+. Here we pass a freshly created
+directory \texttt{dir}.
+
+Directory \texttt{dir} is now populated with a bunch of OCaml files,
+among which we find a file \texttt{maxsum\_\_MaxAndSum.ml} containing
+the OCaml code for functions \texttt{max\_sum} and \texttt{test}.
+
+To compile it, we create a file \texttt{main.ml}
+containing a call to \texttt{test}, that is
+\begin{whycode}
+  let () = test ()
+\end{whycode}
+and we pass both files \texttt{maxsum\_\_MaxAndSum.ml} and
+\texttt{main.ml} to the OCaml compiler:
+\begin{verbatim}
+  > cd dir
+  > ocamlopt zarith.cmxa why3extract.cmxa maxsum__MaxAndSum.ml main.ml
+\end{verbatim}
+OCaml code extracted from \why must be linked with the library
+\texttt{why3extract.cmxa} that is shipped with \why. It is typically
+stored in subdirectory \texttt{why3} of the OCaml standard library.
+Depending on the way \why was installed, it depends either on library
+\texttt{nums.cmxa} or \texttt{zarith.cmxa} for big integers. Above we
+assumed the latter. it is likely that additional options \texttt{-I}
+must be passed to the OCaml compiler for libraries
+\texttt{zarith.cmxa} and \texttt{why3extract.cmxa} to be found.
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-PDF-mode: t
+%%% TeX-master: "manual"
+%%% End:

doc/intro.tex

@@ -50,8 +50,8 @@ using the API.  It is for the experimented users, who wants to link
 Part 2 provides: 
 \begin{itemize}
 \item In Chapter~\ref{chap:syntaxref}, the input syntax of files.
-\item In Chapter~\ref{chap:library}, the standard library of
-  theories distributed with \why.
+% \item In Chapter~\ref{chap:library}, the standard library of
+%   theories distributed with \why.
 \item In Chapter~\ref{chap:manpages}, the technical manual pages for the
   tools of the platform. All tool options, and all the configuration
   files are described in details there.

doc/manual.tex

@@ -235,7 +235,10 @@ Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
 
 \input{syntaxref.tex}
 
-\input{library.tex}
+\input{exec.tex}
+
+% maintaining library.tex up to date is hopeless
+% \input{library.tex}
 
 \input{itp.tex}
 

doc/syntaxref.tex

@@ -368,6 +368,24 @@ file. If a theory is supposed to be reused from other files, be they
 \why\ or \whyml\ files, it should be defined in a \why\ file.
 
 
+\section{The \why Standard Library}
+\label{sec:library}\index{standard library}\index{library}
+
+The \why standard library provides general-purpose theories and
+modules, to be used in logic and/or programs.
+It can be browsed on-line at \url{http://why3.lri.fr/stdlib/}.
+Each file contains one or several theories and/or modules.
+To \texttt{use} or \texttt{clone} a theory/module \texttt{T} from file
+\texttt{file}, use the syntax \texttt{file.T}, since \texttt{file} is
+available in \why's default load path. For instance, the theory of
+integers and the module of references are imported as follows:
+
+\begin{whycode}
+  use import int.Int
+  use import ref.Ref
+\end{whycode}
+
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-PDF-mode: t