doc for extraction (wip)

parent 39d4b1b6
......@@ -50,61 +50,34 @@ We get the expected output, namely the pair \texttt{(45, 10)}.
An alternative to interpretation is to compile \whyml to OCaml.
We do so using the \texttt{extract} command, as follows:
\begin{verbatim}
> mkdir dir
> why3 extract -D ocaml64 maxsum.mlw -o dir
> why3 extract -D ocaml64 maxsum.mlw -o max_sum.ml
\end{verbatim}
The \texttt{extract} command 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}.
\texttt{ocaml64}. We also specify an output file using option
\verb+-o+, namely \texttt{max\_sum.ml}.
After this command, the file \texttt{max\_sum.ml} contains an OCaml
code for function \texttt{max\_sum}.
To compile it, we create a file \texttt{main.ml}
containing a call to \texttt{test}, that is, for example,
containing a call to \texttt{max\_sum}, \emph{e.g.},
\begin{whycode}
let (s,m) = test () in
Format.printf "sum=%s, max=%s@."
(Why3__BigInt.to_string s) (Why3__BigInt.to_string m)
let a = Array.map Z.of_int [| 9; 5; 0; 2; 7; 3; 2; 1; 10; 6 |]
let m, s = Max_sum.max_sum a (Z.of_int 10)
let () = Format.printf "sum=%s, max=%s@." (Z.to_string s) (Z.to_string m)
\end{whycode}
and we pass both files \texttt{maxsum\_\_MaxAndSum.ml} and
\texttt{main.ml} to the OCaml compiler:
It is convenient to use \texttt{ocamlbuild} to compile and link both
files \texttt{max\_sum.ml} and \texttt{main.ml}:
\begin{verbatim}
> cd dir
> ocamlopt zarith.cmxa why3extract.cmxa maxsum__MaxAndSum.ml main.ml
> ocamlbuild -pkg zarith main.native
\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.
For instance, it could be
\begin{verbatim}
> ocamlopt -I `ocamlfind query zarith` zarith.cmxa \
-I `why3 --print-libdir`/why3 why3extract.cmxa \
...
\end{verbatim}
To make the compilation process easier, one can write a
\texttt{Makefile} which can include informations about Why3
configuration as follows.
\begin{whycode}
WHY3SHARE=$(shell why3 --print-datadir)
include $(WHY3SHARE)/Makefile.config
maxsum:
ocamlopt $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa \
-o maxsum maxsum__MaxAndSum.ml main.ml
\end{whycode}
Since Why3's type
\texttt{int} is translated to OCaml arbitrary precision integers using
the \texttt{ZArith} library, we have to pass option \texttt{-pkg
zarith} to \texttt{ocamlbuild}. In order to get extracted code that
uses OCaml's native integers instead, one has to use Why3's types for
63-bit integers from libraries \texttt{mach.int.Int63} and
\texttt{mach.array.Array63}.
%%% Local Variables:
......
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