Commit d6d59f63 authored by MARCHE Claude's avatar MARCHE Claude

update of section API of the doc

parent d1f1c69f
......@@ -50,11 +50,20 @@
* choisir un logo
* complete doc/api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
=== Roadmap for third release 0.70 =======================================
* increment the magic number in config (A)
* Final preparation: put on the web page
** why3-0.70.tar.gz
** manual in PDF
** API doc in HTML (suggestion: http://why3.lri.fr/api/)
Note: check that URL of API doc is correct in doc/api.tex line 9.
* put an up-to-date use_api.ml in the manual (C)
* Check if remark in doc/api.tex line 80 is still valid (A)
* increment the magic number in config (A)
* deplacer le bouton "Cancel" dans le menu "tools",
le renommer en "make obsolete" et le documenter (A)
......@@ -72,6 +81,8 @@
* document new IDE features (C)
* DONE put an up-to-date use_api.ml in the manual (C)
* DONE enlever les caracteres de tab des sources
et les caracteres latin1 (A)
......
......@@ -6,11 +6,12 @@ OCaml code with the \why\ library. We progressively introduce the way
one can use the library to build terms, formulas, theories, proof
tasks, call external provers on tasks, and apply transformations on
tasks. The complete documentation for API calls is given
[TODO in Chapter~ref{chap:apidoc}.]
at URL~\url{http://why3.lri.fr/api/}.
We assume the reader has a fair knowledge of the OCaml
language. Notice that the \why\ library must be installed,
see Section~\ref{sec:installlib}.
language. Notice that the \why\ library must be installed, see
Section~\ref{sec:installlib}. The OCaml code given below is available in
the source distribution as \url{examples/use_api.ml}.
\section{Building Propositional Formulas}
......@@ -79,9 +80,9 @@ As expected, the output is as follows.
\begin{verbatim}
formula 2 is: A /\ B -> A
\end{verbatim}
Notice that the concrete syntax of \why\ forbids predicate identifiers
\todo{Check: Notice that the concrete syntax of \why\ forbids predicate identifiers
to start with a capital letter. This constraint does not exist when
building those directly using library calls.
building those directly using library calls.}
\section{Building Tasks}
......@@ -185,7 +186,12 @@ let env : Env.env =
Env.create_env_of_loadpath (Whyconf.loadpath main)
(* loading the Alt-Ergo driver *)
let alt_ergo_driver : Driver.driver =
Driver.load_driver env alt_ergo.Whyconf.driver
try
Driver.load_driver env alt_ergo.Whyconf.driver
with e ->
eprintf "Failed to load driver for alt-ergo: %a@."
Exn_printer.exn_printer e;
exit 1
\end{verbatim}
We are now ready to call the prover on the tasks. This is done by a
......@@ -312,18 +318,9 @@ let x : Term.term = Term.t_var var_x
let x_times_x : Term.term = Term.t_app_infer mult_symbol [x;x]
let fmla4_aux : Term.term = Term.ps_app ge_symbol [x_times_x;zero]
\end{verbatim}
To quantify on $x$, one can first build an intermediate
value of type \texttt{term\_quant}, representing a closure
under a quantifier:
\begin{verbatim}
let fmla4_quant : Term.term_quant = Term.t_close_quant [var_x] [] fmla4_aux
let fmla4 : Term.term = Term.t_forall fmla4_quant
\end{verbatim}
The second argument of \texttt{t\_close\_quant} is a list of triggers.
A simpler method would be to use an appropriate function:
To quantify on $x$, we use the appropriate smart constructor as follows.
\begin{verbatim}
let fmla4bis : Term.term = Term.t_forall_close [var_x] [] fmla4_aux
let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux
\end{verbatim}
\section{Building Theories}
......
\newcommand{\todo}[1]{{\Huge\bfseries #1}}
\newcommand{\why}{\textsf{Why3}}
\newcommand{\whyml}{\textsf{Why3ML}}
......
......@@ -96,7 +96,7 @@ let alt_ergo_driver : Driver.driver =
Exn_printer.exn_printer e;
exit 1
(* call Alt-Ergo *)
(* calls Alt-Ergo *)
let result1 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
......@@ -166,10 +166,7 @@ let x_times_x : Term.term =
Term.t_app_infer mult_symbol [x;x]
let fmla4_aux : Term.term =
Term.ps_app ge_symbol [x_times_x;zero]
let fmla4_quant : Term.term_quant =
Term.t_close_quant [var_x] [] fmla4_aux
let fmla4 : Term.term =
Term.t_forall fmla4_quant
let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux
let task4 = None
let task4 = Task.use_export task4 int_theory
......@@ -186,4 +183,4 @@ let () = printf "@[On task 4, alt-ergo answers %a@."
(* build a theory with all these goals *)
(* TODO *)
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