Commit 8b67eba7 authored by MARCHE Claude's avatar MARCHE Claude

doc/API tuto: auto extracted code, completed

parent fca13b5b
......@@ -1837,7 +1837,11 @@ doc/call_provers_%.ml: src/driver/call_provers.ml doc/extract_ocaml_code
OCAMLCODE_LOGIC = opening printformula declarepropvars declarepropatoms \
buildtask printtask buildtask2 \
getconf getanyaltergo getaltergo200 \
getdriver callprover calltimelimit
getdriver callprover calltimelimit \
buildfmla buildtermalt buildtaskimport \
quantfmla1 quantfmla2 quantfmla3 quantfmla4 \
buildth1 buildth2 buildth3 buildth4 buildth5 buildth6 buildth7 \
printtheory splittheory printalltasks
OCAMLCODE_CALLPROVERS = proveranswer proverresult resourcelimit
......
......@@ -117,86 +117,27 @@ 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}
\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}
\lstinputlisting{whyconf_provertype.ml}
The map \texttt{provers} provides the set of existing provers.
In the following, we directly
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 = "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}
\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}
\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
......@@ -232,19 +173,6 @@ corresponding to these kinds of answers:
\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}
\lstinputlisting{logic_calltimelimit.ml}
The output of our program is now as follows.
\begin{verbatim}
......@@ -262,65 +190,29 @@ 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{sec:library}).
\begin{ocamlcode}
let two : Term.term =
Term.t_const (Number.ConstInt (Number.int_const_dec "2"))
let four : Term.term =
Term.t_const (Number.ConstInt (Number.int_const_dec "4"))
let int_theory : Theory.theory =
Env.read_theory env ["int"] "Int"
let plus_symbol : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export [Ident.infix "+"]
let two_plus_two : Term.term =
Term.t_app_infer plus_symbol [two;two]
let fmla3 : Term.term = Term.t_equ two_plus_two four
\end{ocamlcode}
\lstinputlisting{logic_buildfmla.ml}
An important point to notice as that when building the application of
$+$ to the arguments, it is checked that the types are correct. Indeed
the constructor \texttt{t\_app\_infer} infers the type of the resulting
term. One could also provide the expected type as follows.
\begin{ocamlcode}
let two_plus_two : Term.term =
Term.fs_app plus_symbol [two;two] Ty.ty_int
\end{ocamlcode}
\lstinputlisting{logic_buildtermalt.ml}
When building a task with this formula, we need to declare that we use
theory \texttt{Int}:
\begin{ocamlcode}
let task3 = None
let task3 = Task.use_export task3 int_theory
let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3")
let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3
\end{ocamlcode}
\lstinputlisting{logic_buildtaskimport.ml}
\section{Building Quantified Formulas}
To illustrate how to build quantified formulas, let us consider
the formula $\forall x:int. x*x \geq 0$. The first step is to
obtain the symbols from \texttt{Int}.
\begin{ocamlcode}
let zero : Term.term =
Term.t_const (Number.ConstInt (Number.int_const_dec "0"))
let mult_symbol : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export [Ident.infix "*"]
let ge_symbol : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export [Ident.infix ">="]
\end{ocamlcode}
\lstinputlisting{logic_quantfmla1.ml}
The next step is to introduce the variable $x$ with the type int.
\begin{ocamlcode}
let var_x : Term.vsymbol =
Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int
\end{ocamlcode}
\lstinputlisting{logic_quantfmla2.ml}
The formula $x*x \geq 0$ is obtained as in the previous example.
\begin{ocamlcode}
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{ocamlcode}
\lstinputlisting{logic_quantfmla3.ml}
To quantify on $x$, we use the appropriate smart constructor as follows.
\begin{ocamlcode}
let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux
\end{ocamlcode}
\lstinputlisting{logic_quantfmla4.ml}
\section{Building Theories}
......@@ -333,76 +225,37 @@ be done by a sequence of calls:
\end{itemize}
Creation of a theory named \verb|My_theory| is done by
\begin{ocamlcode}
let my_theory : Theory.theory_uc =
Theory.create_theory (Ident.id_fresh "My_theory")
\end{ocamlcode}
\lstinputlisting{logic_buildth1.ml}
First let us add formula 1 above as a goal:
\begin{ocamlcode}
let decl_goal1 : Decl.decl =
Decl.create_prop_decl Decl.Pgoal goal_id1 fmla1
let my_theory : Theory.theory_uc =
Theory.add_decl my_theory decl_goal1
\end{ocamlcode}
\lstinputlisting{logic_buildth2.ml}
Note that we reused the goal identifier \verb|goal_id1| that we
already defined to create task 1 above.
Adding formula 2 needs to add the declarations of predicate variables A
and B first:
\begin{ocamlcode}
let my_theory : Theory.theory_uc =
Theory.add_param_decl my_theory prop_var_A
let my_theory : Theory.theory_uc =
Theory.add_param_decl my_theory prop_var_B
let decl_goal2 : Decl.decl =
Decl.create_prop_decl Decl.Pgoal goal_id2 fmla2
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal2
\end{ocamlcode}
\lstinputlisting{logic_buildth3.ml}
Adding formula 3 is a bit more complex since it uses integers, thus it
requires to ``use'' the theory \verb|int.Int|. Using a theory is
indeed not a primitive operation in the API: it must be done by a
combination of an ``export'' and the creation of a namespace. We
provide a helper function for that:
\begin{ocamlcode}
(* [use th1 th2] insert the equivalent of a "use import th2" in
theory th1 under construction *)
let use th1 th2 =
let name = th2.Theory.th_name in
Theory.close_namespace
(Theory.use_export
(Theory.open_namespace th1 name.Ident.id_string) th2) true
\end{ocamlcode}
\lstinputlisting{logic_buildth4.ml}
Addition of formula 3 is then
\begin{ocamlcode}
let my_theory : Theory.theory_uc = use my_theory int_theory
let decl_goal3 : Decl.decl =
Decl.create_prop_decl Decl.Pgoal goal_id3 fmla3
let my_theory : Theory.theory_uc =
Theory.add_decl my_theory decl_goal3
\end{ocamlcode}
\lstinputlisting{logic_buildth5.ml}
Addition of goal 4 is nothing more complex:
\begin{ocamlcode}
let decl_goal4 : Decl.decl =
Decl.create_prop_decl Decl.Pgoal goal_id4 fmla4
let my_theory :
Theory.theory_uc = Theory.add_decl my_theory decl_goal4
\end{ocamlcode}
\lstinputlisting{logic_buildth6.ml}
Finally, we close our theory under construction as follows.
\begin{ocamlcode}
let my_theory : Theory.theory = Theory.close_theory my_theory
\end{ocamlcode}
\lstinputlisting{logic_buildth7.ml}
We can inspect what we did by printing that theory:
\begin{ocamlcode}
let () = printf "@[theory is:@\n%a@]@." Pretty.print_theory my_theory
\end{ocamlcode}
\lstinputlisting{logic_printtheory.ml}
which outputs
\begin{verbatim}
theory is:
my new theory is as follows:
theory My_theory
(* use BuiltIn *)
......@@ -424,23 +277,12 @@ end
From a theory, one can compute at once all the proof tasks it contains
as follows:
\begin{ocamlcode}
let my_tasks : Task.task list =
List.rev (Task.split_theory my_theory None None)
\end{ocamlcode}
\lstinputlisting{logic_splittheory.ml}
Note that the tasks are returned in reverse order, so we reverse the
list above.
We can check our generated tasks by printing them:
\begin{ocamlcode}
let () =
printf "Tasks are:@.";
let _ =
List.fold_left
(fun i t -> printf "Task %d: %a@." i Pretty.print_task t; i+1)
1 my_tasks
in ()
\end{ocamlcode}
\lstinputlisting{logic_printalltasks.ml}
One can run provers on those tasks exactly as we did above.
......
......@@ -159,22 +159,26 @@ An arithmetic goal: 2+2 = 4
*)
(* BEGIN{buildfmla} *)
let two : Term.term = Term.t_nat_const 2
let four : Term.term = Term.t_nat_const 4
let int_theory : Theory.theory = Env.read_theory env ["int"] "Int"
let plus_symbol : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
let two_plus_two : Term.term = Term.fs_app plus_symbol [two;two] Ty.ty_int
let two_plus_two : Term.term = Term.t_app_infer plus_symbol [two;two]
let fmla3 : Term.term = Term.t_equ two_plus_two four
(* END{buildfmla} *)
(* BEGIN{buildtermalt} *)
let two_plus_two : Term.term = Term.fs_app plus_symbol [two;two] Ty.ty_int
(* END{buildtermalt} *)
(* BEGIN{buildtaskimport} *)
let task3 = None
let task3 = Task.use_export task3 int_theory
let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3")
let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3
(* END{buildtaskimport} *)
(*
let () = printf "@[task 3 created:@\n%a@]@." Pretty.print_task task3
......@@ -191,21 +195,28 @@ let () = printf "@[On task 3, alt-ergo answers %a@."
Call_provers.print_prover_result result3
(* quantifiers: let's build "forall x:int. x*x >= 0" *)
(* BEGIN{quantfmla1} *)
let zero : Term.term = Term.t_nat_const 0
let mult_symbol : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
let ge_symbol : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export ["infix >="]
(* END{quantfmla1} *)
(* BEGIN{quantfmla2} *)
let var_x : Term.vsymbol =
Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int
(* END{quantfmla2} *)
(* BEGIN{quantfmla3} *)
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{quantfmla3} *)
(* BEGIN{quantfmla4} *)
let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux
(* END{quantfmla4} *)
let task4 = None
let task4 = Task.use_export task4 int_theory
......@@ -226,53 +237,76 @@ let () = printf "@[On task 4, alt-ergo answers %a@."
(* create a theory *)
let () = printf "@[creating theory 'My_theory'@]@."
(* BEGIN{buildth1} *)
let my_theory : Theory.theory_uc =
Theory.create_theory (Ident.id_fresh "My_theory")
(* END{buildth1} *)
(* add declarations of goals *)
let () = printf "@[adding goal 1@]@."
let decl_goal1 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id1 fmla1
(* BEGIN{buildth2} *)
let decl_goal1 : Decl.decl =
Decl.create_prop_decl Decl.Pgoal goal_id1 fmla1
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal1
(* END{buildth2} *)
let () = printf "@[adding goal 2@]@."
let my_theory : Theory.theory_uc = Theory.add_param_decl my_theory prop_var_A
let my_theory : Theory.theory_uc = Theory.add_param_decl my_theory prop_var_B
(* BEGIN{buildth3} *)
let my_theory : Theory.theory_uc =
Theory.add_param_decl my_theory prop_var_A
let my_theory : Theory.theory_uc =
Theory.add_param_decl my_theory prop_var_B
let decl_goal2 : Decl.decl =
Decl.create_prop_decl Decl.Pgoal goal_id2 fmla2
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal2
(* END{buildth3} *)
(* helper function: [use th1 th2] insert the equivalent of a "use import th2"
in theory th1 under construction *)
(* BEGIN{buildth4} *)
(* helper function: [use th1 th2] insert the equivalent of a
"use import th2" in theory th1 under construction *)
let use th1 th2 =
let name = th2.Theory.th_name in
Theory.close_namespace
(Theory.use_export (Theory.open_namespace th1 name.Ident.id_string) th2)
(Theory.use_export
(Theory.open_namespace th1 name.Ident.id_string) th2)
true
(* END{buildth4} *)
let () = printf "@[adding goal 3@]@."
(* use import int.Int *)
(* BEGIN{buildth5} *)
let my_theory : Theory.theory_uc = use my_theory int_theory
let decl_goal3 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id3 fmla3
let decl_goal3 : Decl.decl =
Decl.create_prop_decl Decl.Pgoal goal_id3 fmla3
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal3
(* END{buildth5} *)
let () = printf "@[adding goal 4@]@."
let decl_goal4 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id4 fmla4
(* BEGIN{buildth6} *)
let decl_goal4 : Decl.decl =
Decl.create_prop_decl Decl.Pgoal goal_id4 fmla4
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal4
(* END{buildth6} *)
(* closing the theory *)
(* BEGIN{buildth7} *)
let my_theory : Theory.theory = Theory.close_theory my_theory
(* END{buildth7} *)
(* printing the result *)
let () = printf "@[theory is:@\n%a@]@." Pretty.print_theory my_theory
(* BEGIN{printtheory} *)
let () = printf "@[my new theory is as follows:@\n@\n%a@]@."
Pretty.print_theory my_theory
(* END{printtheory} *)
(* getting set of task from a theory *)
(* BEGIN{splittheory} *)
let my_tasks : Task.task list =
List.rev (Task.split_theory my_theory None None)
(* END{splittheory} *)
(* BEGIN{printalltasks} *)
let () =
printf "Tasks are:@.";
let _ =
......@@ -280,6 +314,7 @@ let () =
(fun i t -> printf "Task %d: %a@." i Pretty.print_task t; i+1)
1 my_tasks
in ()
(* END{printalltasks} *)
......
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