Commit fca13b5b authored by MARCHE Claude's avatar MARCHE Claude
Browse files

doc/API tuto: make code auto-extracted until section 4.3 included

parent 7249b10c
......@@ -1822,16 +1822,28 @@ doc/bnf$(EXE): doc/bnf.mll
$(OCAMLLEX) $<
$(OCAMLC) -o $@ doc/bnf.ml
doc/extract_ocaml_code: doc/extract_ocaml_code.ml
$(OCAMLC) str.cma -o $@ $<
doc/logic_%.ml: examples/use_api/logic.ml doc/extract_ocaml_code
doc/extract_ocaml_code examples/use_api/logic.ml $* doc
doc/whyconf_%.ml: src/driver/whyconf.ml doc/extract_ocaml_code
doc/extract_ocaml_code src/driver/whyconf.ml $* doc
doc/call_provers_%.ml: src/driver/call_provers.ml doc/extract_ocaml_code
doc/extract_ocaml_code src/driver/call_provers.ml $* doc
OCAMLCODE_LOGIC = opening printformula declarepropvars declarepropatoms \
buildtask printtask buildtask2
buildtask printtask buildtask2 \
getconf getanyaltergo getaltergo200 \
getdriver callprover calltimelimit
OCAMLCODE = $(addprefix doc/logic_, $(addsuffix .ml, $(OCAMLCODE_LOGIC)))
OCAMLCODE_CALLPROVERS = proveranswer proverresult resourcelimit
doc/extract_ocaml_code: doc/extract_ocaml_code.ml
$(OCAMLC) str.cma -o $@ $<
OCAMLCODE = $(addprefix doc/logic_, $(addsuffix .ml, $(OCAMLCODE_LOGIC))) \
$(addprefix doc/call_provers_, $(addsuffix .ml, $(OCAMLCODE_CALLPROVERS))) \
doc/whyconf_provertype.ml
DOC = api glossary ide intro exec macros manpages install \
manual starting syntax syntaxref technical version whyml \
......
......@@ -117,125 +117,135 @@ file \texttt{why3.conf}, as it was built using the \texttt{why3config}
command line tool or the \textsf{Detect Provers} menu of the graphical
IDE. The following API calls allow to access the content of this
configuration file.
\begin{ocamlcode}
(* reads the config file *)
let config : Whyconf.config = Whyconf.read_config None
(* the [main] section of the config file *)
let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get_provers config
\end{ocamlcode}
% \begin{ocamlcode}
% (* reads the config file *)
% let config : Whyconf.config = Whyconf.read_config None
% (* the [main] section of the config file *)
% let main : Whyconf.main = Whyconf.get_main config
% (* all the provers detected, from the config file *)
% let provers : Whyconf.config_prover Whyconf.Mprover.t =
% Whyconf.get_provers config
% \end{ocamlcode}
\lstinputlisting{logic_getconf.ml}
The type \texttt{'a Whyconf.Mprover.t} is a map indexed by provers. A
prover is a record with a name, a version, and an alternative description
(to differentiate between various configurations of a given prover). Its
definition is in the module \texttt{Whyconf}:
\begin{ocamlcode}
type prover =
{ prover_name : string; (* "Alt-Ergo" *)
prover_version : string; (* "2.95" *)
prover_altern : string; (* "special" *)
}
\end{ocamlcode}
% \begin{ocamlcode}
% type prover =
% { prover_name : string; (* "Alt-Ergo" *)
% prover_version : string; (* "2.95" *)
% prover_altern : string; (* "special" *)
% }
% \end{ocamlcode}
\lstinputlisting{whyconf_provertype.ml}
The map \texttt{provers} provides the set of existing provers.
In the following, we directly
attempt to access the prover Alt-Ergo, which is known to be identified
with id \texttt{"alt-ergo"}.
\begin{ocamlcode}
(* the [prover alt-ergo] section of the config file *)
let alt_ergo : Whyconf.config_prover =
try
Whyconf.prover_by_id config "alt-ergo"
with Whyconf.ProverNotFound _ ->
eprintf "Prover alt-ergo not installed or not configured@.";
exit 0
\end{ocamlcode}
attempt to access a prover named ``Alt-Ergo'', any version.
% \begin{ocamlcode}
% (* the [prover alt-ergo] section of the config file *)
% let alt_ergo : Whyconf.config_prover =
% try
% Whyconf.prover_by_id config "alt-ergo"
% with Whyconf.ProverNotFound _ ->
% eprintf "Prover alt-ergo not installed or not configured@.";
% exit 0
% \end{ocamlcode}
\lstinputlisting{logic_getanyaltergo.ml}
We could also get a specific version with :
\begin{ocamlcode}
let alt_ergo : Whyconf.config_prover =
try
let prover = {Whyconf.prover_name = "Alt-Ergo";
prover_version = "0.92.3";
prover_altern = ""} in
Whyconf.Mprover.find prover provers
with Not_found ->
eprintf "Prover alt-ergo not installed or not configured@.";
exit 0
\end{ocamlcode}
% \begin{ocamlcode}
% let alt_ergo : Whyconf.config_prover =
% try
% let prover = {Whyconf.prover_name = "Alt-Ergo";
% prover_version = "2.0.0";
% prover_altern = ""} in
% Whyconf.Mprover.find prover provers
% with Not_found ->
% eprintf "Prover Alt-Ergo 2.0.0 not installed or not configured@.";
% exit 0
% \end{ocamlcode}
\lstinputlisting{logic_getaltergo200.ml}
The next step is to obtain the driver associated to this prover. A
driver typically depends on the standard theories so these should be
loaded first.
\begin{ocamlcode}
(* builds the environment from the [loadpath] *)
let env : Env.env =
Env.create_env (Whyconf.loadpath main)
(* loading the Alt-Ergo driver *)
let alt_ergo_driver : Driver.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{ocamlcode}
% \begin{ocamlcode}
% (* builds the environment from the [loadpath] *)
% let env : Env.env =
% Env.create_env (Whyconf.loadpath main)
% (* loading the Alt-Ergo driver *)
% let alt_ergo_driver : Driver.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{ocamlcode}
\lstinputlisting{logic_getdriver.ml}
We are now ready to call the prover on the tasks. This is done by a
function call that launches the external executable and waits for its
termination. Here is a simple way to proceed:
\begin{ocamlcode}
(* calls Alt-Ergo *)
let result1 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
alt_ergo_driver task1 ()) ()
(* prints Alt-Ergo answer *)
let () = printf "@[On task 1, alt-ergo answers %a@]@."
Call_provers.print_prover_result result1
\end{ocamlcode}
% \begin{ocamlcode}
% (* calls Alt-Ergo *)
% let result1 : Call_provers.prover_result =
% Call_provers.wait_on_call
% (Driver.prove_task ~command:alt_ergo.Whyconf.command
% alt_ergo_driver task1 ()) ()
% (* prints Alt-Ergo answer *)
% let () = printf "@[On task 1, alt-ergo answers %a@]@."
% Call_provers.print_prover_result result1
% \end{ocamlcode}
\lstinputlisting{logic_callprover.ml}
This way to call a prover is in general too naive, since it may never
return if the prover runs without time limit. The function
\texttt{prove\_task} has two optional parameters: \texttt{timelimit}
is the maximum allowed running time in seconds, and \texttt{memlimit}
is the maximum allowed memory in megabytes. The type
\texttt{prover\_result} is a record with three fields:
\texttt{prove\_task} has an optional parameter \texttt{limit}, a record defined
in module \texttt{Call\_provers}:
\lstinputlisting{call_provers_resourcelimit.ml}
where the field \texttt{limit\_time} is the maximum allowed running time in seconds,
and \texttt{limit\_mem} is the maximum allowed memory in megabytes. The type
\texttt{prover\_result} is a record defined in module \texttt{Call\_provers}:
\lstinputlisting{call_provers_proverresult.ml}
with in particular the fields:
\begin{itemize}
\item \texttt{pr\_answer}: the prover answer, explained below;
\item \texttt{pr\_output}: the output of the prover, \ie both
standard output and the standard error of the process
(a redirection in \texttt{why3.conf} is required);
\item \texttt{pr\_time} : the time taken by the prover, in seconds.
\end{itemize}
A \texttt{pr\_answer} is a sum of several kind of answers:
A \texttt{pr\_answer} is the sum type defined in module \texttt{Call\_provers}:
\lstinputlisting{call_provers_proveranswer.ml}
corresponding to these kinds of answers:
\begin{itemize}
\item \texttt{Valid}: the task is valid according to the prover.
\item \texttt{Invalid}: the task is invalid.
\item \texttt{Timeout}: the prover exceeds the time or memory limit.
\item \texttt{Timeout}: the prover exceeds the time limit.
\item \texttt{OutOfMemory}: the prover exceeds the memory limit.
\item \texttt{Unknown} $msg$: the prover can't determine if the task
is valid; the string parameter $msg$ indicates some extra
information.
\item \texttt{Failure} $msg$: the prover reports a failure, \ie it
\item \texttt{Failure} $msg$: the prover reports a failure, \eg it
was unable to read correctly its input task.
\item \texttt{HighFailure}: an error occurred while trying to call the
prover, or the prover answer was not understood (\ie none of the
prover, or the prover answer was not understood (\eg none of the
given regular expressions in the driver file matches the output
of the prover).
\end{itemize}
Here is thus another way of calling the Alt-Ergo prover, on our second
task.
\begin{ocamlcode}
let result2 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
~timelimit:10
alt_ergo_driver task2 ()) ()
let () =
printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
Call_provers.print_prover_answer
result1.Call_provers.pr_answer
result1.Call_provers.pr_time
\end{ocamlcode}
% \begin{ocamlcode}
% let result2 : Call_provers.prover_result =
% Call_provers.wait_on_call
% (Driver.prove_task ~command:alt_ergo.Whyconf.command
% ~timelimit:10
% alt_ergo_driver task2 ()) ()
% let () =
% printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
% Call_provers.print_prover_answer
% result1.Call_provers.pr_answer
% result1.Call_provers.pr_time
% \end{ocamlcode}
\lstinputlisting{logic_calltimelimit.ml}
The output of our program is now as follows.
\begin{verbatim}
On task 1, alt-ergo answers Valid (0.01s)
......
......@@ -77,6 +77,7 @@ let () = printf "@[task 2 created:@\n%a@]@." Pretty.print_task task2
(* To call a prover, we need to access the Why configuration *)
(* BEGIN{getconf} *)
(* reads the config file *)
let config : Whyconf.config = Whyconf.read_config None
(* the [main] section of the config file *)
......@@ -84,7 +85,9 @@ let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get_provers config
(* END{getconf} *)
(* BEGIN{getanyaltergo} *)
(* One prover named Alt-Ergo in the config file *)
let alt_ergo : Whyconf.config_prover =
let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
......@@ -95,7 +98,21 @@ let alt_ergo : Whyconf.config_prover =
exit 0
end else
snd (Whyconf.Mprover.max_binding provers)
(* END{getanyaltergo} *)
(* BEGIN{getaltergo200} *)
(* Specific version 2.0.0 of Alt-Ergo in the config file *)
let alt_ergo_2_0_0 : Whyconf.config_prover =
let fp = Whyconf.parse_filter_prover "Alt-Ergo,2.0.0" in
let provers = Whyconf.filter_provers config fp in
if Whyconf.Mprover.is_empty provers then begin
eprintf "Prover Alt-Ergo 2.0.0 not installed or not configured@.";
exit 0
end else
snd (Whyconf.Mprover.max_binding provers)
(* END{getaltergo200} *)
(* BEGIN{getdriver} *)
(* builds the environment from the [loadpath] *)
let env : Env.env = Env.create_env (Whyconf.loadpath main)
......@@ -107,7 +124,9 @@ let alt_ergo_driver : Driver.driver =
eprintf "Failed to load driver for alt-ergo: %a@."
Exn_printer.exn_printer e;
exit 1
(* END{getdriver} *)
(* BEGIN{callprover} *)
(* calls Alt-Ergo *)
let result1 : Call_provers.prover_result =
Call_provers.wait_on_call
......@@ -116,9 +135,11 @@ let result1 : Call_provers.prover_result =
alt_ergo_driver task1)
(* prints Alt-Ergo answer *)
let () = printf "@[On task 1, alt-ergo answers %a@."
let () = printf "@[On task 1, Alt-Ergo answers %a@."
Call_provers.print_prover_result result1
(* END{callprover} *)
(* BEGIN{calltimelimit} *)
let result2 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
......@@ -128,6 +149,7 @@ let result2 : Call_provers.prover_result =
let () = printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
Call_provers.print_prover_answer result1.Call_provers.pr_answer
result1.Call_provers.pr_time
(* END{calltimelimit} *)
......
......@@ -22,6 +22,7 @@ type reason_unknown =
| Resourceout
| Other
(* BEGIN{proveranswer} anchor for automatic documentation, do not remove *)
type prover_answer =
| Valid
| Invalid
......@@ -31,7 +32,9 @@ type prover_answer =
| Unknown of (string * reason_unknown option)
| Failure of string
| HighFailure
(* END{proveranswer} anchor for automatic documentation, do not remove *)
(* BEGIN{proverresult} anchor for automatic documentation, do not remove *)
type prover_result = {
pr_answer : prover_answer;
pr_status : Unix.process_status;
......@@ -40,12 +43,15 @@ type prover_result = {
pr_steps : int; (* -1 if unknown *)
pr_model : model;
}
(* END{proverresult} anchor for automatic documentation, do not remove *)
(* BEGIN{resourcelimit} anchor for automatic documentation, do not remove *)
type resource_limit = {
limit_time : int;
limit_mem : int;
limit_steps : int;
}
(* END{resourcelimit} anchor for automatic documentation, do not remove *)
let empty_limit = { limit_time = 0 ; limit_mem = 0; limit_steps = 0 }
......
......@@ -52,11 +52,13 @@ let default_conf_file =
(* Prover *)
(* BEGIN{provertype} anchor for automatic documentation, do not remove *)
type prover =
{ prover_name : string;
prover_version : string;
prover_altern : string;
}
(* END{provertype} anchor for automatic documentation, do not remove *)
let print_altern fmt s =
if s <> "" then Format.fprintf fmt " (%s)" s
......
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